2 papers
cs.LO2026
A Modern View on MCSat
Thomas Hader, Theo Jauschneg, Daniela Kaufmann +1
The Model Constructing Satisfiability (MCSat) approach has shown strong performance in solving complex SMT problems, in particular in algebraic SMT theories such as non-linear inte…
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…