mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-19 02:42:02 +00:00
Code Activity

fix test_l4

Browse source
This commit is contained in:
Jakob Rath 2021-09-14 14:39:41 +02:00
parent f9b1b4e65d
commit 8103627e47
2 changed files with 5 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/math/polysat/conflict_core.cpp
View file

@ -82,6 +82,7 @@ namespace polysat {
for (auto v : c->vars()) for (auto v : c->vars())
if (s().is_assigned(v)) if (s().is_assigned(v))
m_vars.insert(v); m_vars.insert(v);
SASSERT(!empty());
} }
/** /**
@ -102,6 +103,7 @@ namespace polysat {
if (s().is_assigned(v)) if (s().is_assigned(v))
m_vars.insert(v); m_vars.insert(v);
} }
SASSERT(!empty());
} }
void conflict_core::insert(signed_constraint c) { void conflict_core::insert(signed_constraint c) {
@ -110,7 +112,6 @@ namespace polysat {
// (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology) // (e.g., constant ones such as "4 > 1"... only true ones should appear, otherwise the lemma would be a tautology)
if (c.is_always_true()) if (c.is_always_true())
return; return;
SASSERT(!c.is_always_false());
if (c->is_marked()) if (c->is_marked())
return; return;
set_mark(c); set_mark(c);

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

@ -178,7 +178,9 @@ namespace polysat {
SASSERT(!is_conflict()); SASSERT(!is_conflict());
SASSERT(c->unit_clause()); SASSERT(c->unit_clause());
if (c.bvalue(*this) == l_false) if (c.bvalue(*this) == l_false)
m_conflict.set(c); // we already added ~c => conflict at base level m_conflict.set(~c); // we already added ~c => conflict
else if (c.is_always_false())
m_conflict.set(c);
else else
propagate_bool(c.blit(), c->unit_clause()); propagate_bool(c.blit(), c->unit_clause());
} }