STP



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.

Features

  • Easy to embed or run standalone
  • Bindings for C, C++, and Python
  • Supports multiple query input formats
  • Open source and MIT licensed

Awards

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