Install the STLmc Tool

The STLmc tool supports CPython 3.8 through 3.14. You can install the tool from PyPI using the following command:

python -m pip install stlmc

---

Install and Check Solvers

The Python interfaces for Z3 and Yices are installed with STLmc. After installing the package, check whether all solver prerequisites are available:

stlmc-install-solvers --check

Install all missing solver components where automatic installation is supported:

stlmc-install-solvers

An individual solver can be selected with z3, yices, or dreal:

stlmc-install-solvers dreal
stlmc-install-solvers yices

Automatic Yices installation supports Ubuntu/Debian and macOS with Homebrew. Automatic dReal installation supports macOS and x86-64 Linux. Native package installation may request administrator privileges. If a required solver is unavailable, STLmc reports the corresponding installer command.

Use the following commands to confirm the installation and view the available options:

stlmc -h
stlmc-vis -h

---

Optional PDF Output

• Gnuplot (optional): http://www.gnuplot.info/

  Gnuplot is required only when exporting counterexample graphs in PDF format. It is not required for HTML or text counterexample output. You can install Gnuplot using the following command:

  Ubuntu or Debian

    sudo apt install gnuplot
  

  MacOS

    brew install gnuplot