The Simple Theorem Prover
STP is a constraint solver for the theory of quantifier-free bitvectors that can solve many kinds of problems generated by program analysis tools, theorem provers, automated bug finders, cryptographic algorithms, intelligent fuzzers and model checkers.
- Easy to embed or run standalone
- Bindings for C, C++, and Python
- Supports multiple query input formats
- Open source and MIT licensed
STP's speed and accuracy compare favorably with other solvers in the bitvector (QF_BV) category.
- 1st Single Query — SMTCOMP 2023
- 1st Single Query UNSAT & Single Query 24sec Performance — SMTCOMP 2022
- 1st Cloud & Incremental — SMTCOMP 2021
- 2nd — SMTCOMP 2014
- 2nd — SMTCOMP 2011
- 1st — SMTCOMP 2010
- 1st — SMTCOMP 2006