mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-16 07:05:35 +00:00
Code Activity

Fix soundness bug in sat.smt incremental mode (#7990)

Browse source 
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.
This commit is contained in:
tryh4rd-26 2026-05-14 01:33:24 +05:30
parent 2f7ff62173
commit 8027b11427
1 changed files with 3 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

5
src/solver/solver_preprocess.cpp
View file

@ -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
//
}