From 8027b1142767c3d92723feb71e1677b50aeca7d3 Mon Sep 17 00:00:00 2001 From: tryh4rd-26 Date: Thu, 14 May 2026 01:33:24 +0530 Subject: [PATCH] Fix soundness bug in sat.smt incremental mode (#7990) Disable elim_unconstrained simplifier when sat.smt is enabled. This prevents the preprocessor from removing variables that are required by theory solvers or for correct model reconstruction in incremental sessions. This resolves the incorrect SAT verdict and 'invalid model' errors reported on the dglm.txt benchmark. --- src/solver/solver_preprocess.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/solver/solver_preprocess.cpp b/src/solver/solver_preprocess.cpp index e91c63d79..9d8593aa3 100644 --- a/src/solver/solver_preprocess.cpp +++ b/src/solver/solver_preprocess.cpp @@ -42,6 +42,7 @@ Notes: #include "ast/simplifiers/bound_simplifier.h" #include "ast/simplifiers/cnf_nnf.h" #include "params/smt_params.h" +#include "params/sat_params.hpp" #include "solver/solver_preprocess.h" #include "qe/lite/qe_lite_tactic.h" @@ -59,10 +60,11 @@ void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, de return r; }; smt_params smtp(p); + sat_params satp(p); s.add_simplifier(alloc(rewriter_simplifier, m, p, st)); if (smtp.m_propagate_values) s.add_simplifier(alloc(propagate_values, m, p, st)); if (smtp.m_solve_eqs) s.add_simplifier(alloc(euf::solve_eqs, m, st)); - if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st)); + if (smtp.m_elim_unconstrained && !satp.smt()) s.add_simplifier(alloc(elim_unconstrained, m, st)); if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st)); if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st)); if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifier(m, p, st)); @@ -88,4 +90,3 @@ void init_preprocess(ast_manager& m, params_ref const& p, then_simplifier& s, de // } -