PolySAT: Word-level Bit-vector Reasoning in Z3

Jakob Rath, Clemens Eisenhofer, Daniela Kaufmann +2

PolySAT is a word-level decision procedure supporting bit-precise SMT reasoning over polynomial arithmetic with large bit-vector operations. The PolySAT calculus extends conflict-d…