mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 16:45:31 +00:00
Code Activity

Remove outdated note

Browse source
This commit is contained in:
Jakob Rath 2023-11-06 11:12:23 +01:00
parent 5eb5313ac6
commit 9e90b353e9
1 changed files with 0 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -1623,21 +1623,6 @@ namespace polysat {
}
while (e != first);
// TODO: violated in 5133-min.smt2:
//
// viable lemma:
// 35: -31 <= -1*v17 + -1*v11*v0 + -1*v5*v2 + 32 [ b:l_true p:l_false bprop@0 idx:28 pwatched ]
// -22: v17 + v11*v0 + v6 + v5*v2 != 0 [ b:l_false p:l_undef assert@0 idx:8 pwatched dep:16 ]
// 36: v17 + v11*v0 + v5*v2 + 1 == 0 [ b:l_false p:l_false eval@39 idx:75 ]
// -7: -31 > v6 + 32 [ b:l_false p:l_undef assert@0 idx:17 pwatched dep:33 ]
// ASSERTION VIOLATION
// File: /Users/jakob/projects/z3/src/math/polysat/viable.cpp
// Line: 2036
// all_of(lemma, [this](sat::literal lit) { return s.m_bvars.value(lit) != l_true; })
//
// Reason: there is an eval/bool conflict that we didn't discover before,
// because not-yet-assigned variables are watched but the constraint already evaluates due to cancellation of some terms.
//
// verbose_stream() << "viable lemma:\n";
// for (auto lit : lemma)
// verbose_stream() << " " << lit_pp(s, lit) << "\n";