STP: an SMT solver for bitvectors, arrays and floating point

A solver for the theories that program analysis actually produces

STP is described as a constraint solver, or SMT solver, for the quantifier-free theories of bitvectors, arrays, floating-point and linear real arithmetic.

The word quantifier-free is the boundary of the tool, and it is the same boundary that SMT-LIB draws: you state a formula without existentials or universals over quantified variables, and the solver looks for a satisfying assignment or proves there is none. The theories listed are the ones that appear when you take a C program and ask questions about it.

Bitvectors cover the machine word semantics of integer types, where overflow wraps and shifts are defined, and the difference from mathematical integers is where most of the interesting bugs live. Floating-point covers IEEE 754 rounding, which is a notoriously hard theory for a solver because the rounding rules are piecewise. Arrays cover memory as a set of index-value pairs. Linear real arithmetic covers the geometry that shows up in constraint solvers and scheduling problems.

The README says these constraint types are generated by program analysis tools, theorem provers, automated bug finders, cryptographic attack tools, intelligent fuzzers and model checkers, and by many other applications. That list is the real user base, and it tells you the two things that matter about STP. It is a component in someone else's pipeline, usually as a decision procedure for a bit-level property. And it is asked questions of the form can this input reach that state, where the answer decides whether a test case is a bug.

The project is written in C++ and the topic tags are cnf, cryptography, sat-solver, smt, symbolic-execution and verification, which is the same set of application areas named in the README. The homepage is stp.github.io/stp, the last push was on 2026-10-19, and the listed releases are STP 2.4.1 from 2026-08-01 and STP 2.4.0 from 2026-07-30, with a 2.3.4_cadical tag from 2024-06-13 before them.

The default SAT backend now carries an interface upstream does not have

The most consequential paragraph in the README is the one about CryptoMiniSat, and it is about a change in what the default backend can do.

CryptoMiniSat is the backend STP solves with by default, and `--auto-download` covers it like every other dependency: STP clones and builds a fork at a pinned commit that carries the IPASIR-UP propagator interface the linear-arithmetic theory drives.

So the default backend is not upstream CryptoMiniSat. It is a fork, pinned, with an extra interface added. The consequence is stated plainly: a CryptoMiniSat without the interface still builds STP, but the theory then runs full-lazy on it, configure warns about it, and `--cadical` restores propagation for a run. An installed one is found and preferred.

Full-lazy is the term to understand here. In lazy SMT solving, a theory only explains its constraints to the SAT solver when the SAT solver needs to, rather than eagerly. That is more memory-efficient and less likely to fail, and it is slower on the formulas where propagation would have simplified the problem quickly. So the choice of backend and the choice of propagation mode are the same tuning decision, and the README is telling you that a stock CryptoMiniSat build silently changes the performance profile of the linear-arithmetic theory.

The build system also distinguishes what belongs to STP and what belongs to the backend. `libgmp-dev`, `pkg-config` and `zlib1g-dev` are CryptoMiniSat's packages, not STP's, so the dependency list in the quick install is not simply STP's own requirements.

And STP builds CryptoMiniSat with `-DNOCADICAL=ON`, so it bundles no CaDiCaL of its own and links the revision it pins, which is what keeps `--cadical-factor` available. That option removes only backbone extraction, which STP never asks for. The reasoning is that if each project vendored its own CaDiCaL, the two copies would drift and the option would break.

CaDiCaL is compiled in alongside CryptoMiniSat and is what a build without CryptoMiniSat solves with, and `--cryptominisat`, `--cadical` or `--minisat` selects a compiled-in backend for one run.

Tuning the CaDiCaL backend without reading the source

The CaDiCaL options are documented in detail, which is unusual and welcome, because they are the knobs that determine whether a formula solves in seconds or hours.

With `--cadical`, `--cadical-elim=0|1` controls variable elimination, and `--cadical-elimmineff=N` and `--cadical-elimmaxeff=N` set its minimum and maximum effort. The examples given are:

stp input.smt2 --cadical --cadical-elim=0
stp input.smt2 --cadical --cadical-elimmineff=10000 --cadical-elimmaxeff=100000

Unspecified options retain the backend settings and STP's automatic policies. Explicit values override the corresponding `CADICAL_*` environment variables and search-bias settings, survive backend rebuilds, and an explicit `--cadical-elim=1` keeps elimination enabled when incremental inprocessing is retired. Invalid values and requests with another backend are rejected before solving, and you can add `-s` to see the effective settings.

Two caveats are stated. Effort limits follow CaDiCaL's cost model, and it can raise the allowance for large formulas, so the maximum is not a hard resolution-count limit. And these are tuning controls with measured tradeoffs, and none of them is set by default. The phrase measured tradeoffs is doing work: the numbers in the examples are not magic values but a starting point, and the effective settings are printable, which means you can see what your run actually did.

There is a third backend, incremental Kissat, and it is optional rather than compiled in. You configure STP with `--kissat --auto-download` to build the pinned fork, then select it with `stp --kissat input.smt2`, or point at a prebuilt checkout with `--kissat-dir=/path/to/kissat`. The Kissat integration guide covers the build options and the incremental API.

The distinguishing feature of Kissat here is incrementality, and that matters because incremental solving is how you avoid re-solving from scratch in a loop. If your application asks many related questions about the same program, an incremental backend changes the shape of the workload rather than just the constant factor.

Building it, and the pinned dependency policy behind --auto-download

The quick install is a single block, and the second half of it is the interesting part.

sudo apt-get install git build-essential cmake bison flex python3 \
                     libgmp-dev pkg-config zlib1g-dev
git clone https://github.com/stp/stp
cd stp
./configure.sh --auto-download
cmake --build build -j$(nproc)
sudo cmake --install build

There are no submodules. `--auto-download` fetches every dependency at a pinned revision and builds it with this build's own compiler and flags. Without it, configuration stops and says what to install or where to point it, and nothing here reaches the network unless it is asked to.

That last clause is a security property worth pausing on. A build that fetches from the network by default is a build that can change under you, and a build that refuses to fetch unless asked is one that cannot. The pinning means the dependency set is reproducible, and the Dockerfile comment explains the mechanism in detail: `--auto-download` supplies CryptoMiniSat, MiniSat, CaDiCaL, LibBF, ABC, SymFPU, CLI11 and the rest, each at the revision its `cmake/Find*.cmake` pins and with the flags it builds it with, the combination CI exercises, with one pin per dependency to move.

The Dockerfile also documents a specific build problem that the pin policy has to accommodate. MiniSat 2.2.1 declares `cmake_minimum_required(VERSION 2.6)`, which the CMake on the base image refuses, and `cmake/deps-helper.cmake` passes the `-DCMAKE_POLICY_VERSION_MINIMUM` that gets it through. Building it by hand outside that does not work. That is a small, concrete example of why a helper script exists at all.

Two other install paths are offered. Homebrew, which is one line, `brew install stp`, and Docker, which needs nothing installed but Docker itself and reads the problem on standard input:

git clone https://github.com/stp/stp
cd stp
docker build -t stp .
echo "(set-logic QF_BV)
(assert (= (bvsdiv (_ bv3 2) (_ bv2 2)) (_ bv0 2)))
(check-sat)
(exit)" | docker run --rm -i stp

The Dockerfile produces a statically compiled instance with MiniSat and CryptoMiniSat that evaluates SMTLIB2 inputs provided on standard input, and the final image is a static binary on scratch, which carries no distribution with it and so runs anywhere.

The Python interface is the shortest path to a first answer

For someone trying STP for the first time, the Python binding is the most direct route, and the README gives a worked example that demonstrates the point of the tool in four lines.

from stp import *

x, y = BitVecs('x y', 32)
s = Solver()
s.add(ULT(x + y, 20), UGT(x, 10), UGT(y, 10))
print(s.check())  # sat
print(s.model())  # e.g. [x = 4294967288, y = 11]

Reading that example carefully teaches most of what you need to know about bitvector solving. `BitVecs('x y', 32)` creates two 32-bit bitvector variables. The constraints use unsigned comparison operators, `ULT` and `UGT`, because the values are meant to be non-negative. And the model that comes back, x = 4294967288 with y = 11, is the tell: 4294967288 is 2^32 minus 8, so x plus y has wrapped around the 32-bit boundary while still satisfying x + y < 20 in unsigned arithmetic. That is exactly the class of bug a bitvector solver exists to find, and it is not something you would spot by reading the code.

The command line is the other entry point, and the recommended input format is SMT-LIB2, run as `stp myproblem.smt2`. STP also reads from standard input, as in the Docker example above. The command line documentation covers the input formats, output and exit status, choosing a SAT solver, limits, statistics, and writing CNF, which is the last item worth noting because CNF output is how a solver gets plugged into another SAT tool.

The manual documents the accepted subset of SMT-LIB2, the C, C++ and Python APIs, incremental solving and array extensionality, and how STP works. The sources are in the `docs/` directory, and the repository layout follows the same split, with `lib/`, `include/`, `cmake/`, `bindings/`, `scripts/`, `tools/`, `utils/`, `tests/`, `papers/` and a `windows/` directory for the Windows build. The `tools/` directory holds the programs under it other than `stp` itself, and the `papers/` directory is where the published literature behind the solver lives.

Editorial conclusion

Adopt STP when you need to reason about bitwise programs, floating-point rounding or array properties, for example in a fuzzer's oracle, a cryptographic search or a model checker, and use the SMT-LIB2 input format since that is the recommended one. Do not adopt it as a general purpose theorem prover, because the supported theories are quantifier-free, and check first which SAT backend your build has, since the default CryptoMiniSat build now carries an extra interface that a plain upstream build lacks, and that changes propagation and therefore speed.

Frequently asked questions

Official sources

1. Issues
2. Project website
3. README
4. Releases
5. stp/stp on GitHub