Boosting MCSat Modulo Nonlinear Integer Arithmetic via Local Search

Enrico Lipparini, Thomas Hader, Ahmed Irfan +1

The Model Constructing Satisfiability (MCSat) approach to the SMT problem extends the ideas of CDCL from the SAT level to the theory level. Like SAT, its search is driven by increm…