mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 09:35:32 +00:00
Code Activity

Assertion was too strong (via test_ineq1)

Browse source
This commit is contained in:
Jakob Rath 2022-12-07 16:13:24 +01:00
parent 05a1f4d096
commit 71acba20e2
1 changed files with 5 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/polysat/conflict.cpp
View file

@ -322,7 +322,11 @@ namespace polysat {
lemma->set_redundant(true);
for (sat::literal lit : *lemma) {
LOG(lit_pp(s, lit));
SASSERT(s.m_bvars.value(lit) != l_true);
// NOTE: it can happen that the literal's bvalue is l_true at this point.
// E.g., lit has been assigned to true on the search stack but not yet propagated.
// A propagation before lit will cause a conflict, and by chance the viable conflict will contain lit.
// (in that case, the evaluation of lit in the current assignment must be false, and it would have caused a conflict by itself when propagated.)
SASSERT(s.m_bvars.value(lit) != l_true || !s.lit2cnstr(lit).is_currently_true(s));
}
m_lemmas.push_back(std::move(lemma));
// TODO: pass to inference_logger (with name)