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

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