  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.
