mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-23 19:47:52 +00:00
Code Activity

Fix to bench15 bug was unsound

Browse source
This commit is contained in:
Jakob Rath 2023-02-01 11:17:29 +01:00
parent f0625b604a
commit 975fb25221
1 changed files with 13 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/math/polysat/solver.cpp
View file

@ -1174,7 +1174,18 @@ namespace polysat {
LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause); LOG((clause.is_redundant() ? "Lemma: ": "Aux: ") << clause);
for (sat::literal lit : clause) { for (sat::literal lit : clause) {
LOG(" " << lit_pp(*this, lit)); LOG(" " << lit_pp(*this, lit));
// SASSERT(m_bvars.value(lit) != l_true); if (!m_bvars.is_assigned(lit)) {
switch (lit2cnstr(lit).eval(*this)) {
case l_true:
assign_eval(lit);
break;
case l_false:
assign_eval(~lit);
break;
default:
break;
}
}
// it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint // it could be that such a literal has been created previously but we don't detect it when e.g. narrowing a mul_ovfl_constraint
if (m_bvars.value(lit) == l_true) { if (m_bvars.value(lit) == l_true) {
// in this case the clause is useless // in this case the clause is useless
@ -1225,7 +1236,7 @@ namespace polysat {
clause_ref solver::mk_clause(unsigned n, signed_constraint const* cs, bool is_redundant) { clause_ref solver::mk_clause(unsigned n, signed_constraint const* cs, bool is_redundant) {
clause_builder cb(*this); clause_builder cb(*this);
for (unsigned i = 0; i < n; ++i) for (unsigned i = 0; i < n; ++i)
cb.insert_try_eval(cs[i]); cb.insert(cs[i]);
cb.set_redundant(is_redundant); cb.set_redundant(is_redundant);
return cb.build(); return cb.build();
} }