2 papers
cs.LO2025
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…
cs.LO2024
MCSat-based Finite Field Reasoning in the Yices2 SMT Solver
Thomas Hader, Daniela Kaufmann, Ahmed Irfan +2
This system description introduces an enhancement to the Yices2 SMT solver, enabling it to reason over non-linear polynomial systems over finite fields. Our reasoning approach fits…