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 category.

  • 2nd — SMTCOMP 2014
  • 2nd — SMTCOMP 2011
  • 1st — SMTCOMP 2010
  • 1st — SMTCOMP 2006