AAProver is a bit-precise theorem prover for typical operations present in programming languages. It takes a single bit vector expression and reduces it to a CNF by replacing all operations with circuits and then applying Tseitin tautologies. Finally, the CNF is solved using MiniSAT. If a solution is found the satisfying assignment may be queried.
Though this library was not a main objective for the original thesis, it is shortly described there as well (more extensive than here).

The code is available for download.


For the following (simple) example assume that x and y are both 4 bit wide signed integers (*):
(y == x + 1) && (y < x)

AAProver is then able to prove that there is a single solution, with the satisfying assignment being (x == 7) && (y == -8).
This is just a very basic example, please look at AACalysto to see what is possible with this library.

(*) AAProver supports arbitrary bit-width (even mixed in the same expression), 4 bits were chosen to keep the example simple.