PolySAT: Word-level Bit-vector Reasoning in Z3
<|reference_start|>PolySAT: Word-level Bit-vector Reasoning in Z3: 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-driven clause learning modulo theories with two key components: (i) a bit-vector plugin to the equality graph, and (ii) a theory solver for bit-vector arithmetic with non-linear polynomials. PolySAT implements dedicated procedures to extract bit-vector intervals from polynomial inequalities. For the purpose of conflict analysis and resolution, PolySAT comes with on-demand lemma generation over non-linear bit-vector arithmetic. PolySAT is integrated into the SMT solver Z3 and has potential applications in model checking and smart contract verification where bit-blasting techniques on multipliers/divisions do not scale.<|reference_end|>
@article{rath2024polysat:,
    title={PolySAT: Word-level Bit-vector Reasoning in Z3},
    author={Jakob Rath and Clemens Eisenhofer and Daniela Kaufmann and Nikolaj
  Bj{o}rner and Laura Kov'acs},
    journal={arXiv preprint arXiv:2406.04696},
    year={2024},
    archivePrefix={arXiv},
    eprint={2406.04696},
    primaryClass={cs.LO}
}