From 9e90b353e953dade2b3e72d85888d464219030aa Mon Sep 17 00:00:00 2001 From: Jakob Rath Date: Mon, 6 Nov 2023 11:12:23 +0100 Subject: [PATCH] Remove outdated note --- src/math/polysat/viable.cpp | 15 --------------- 1 file changed, 15 deletions(-) diff --git a/src/math/polysat/viable.cpp b/src/math/polysat/viable.cpp index d9ac96ad2..5b4309fa5 100644 --- a/src/math/polysat/viable.cpp +++ b/src/math/polysat/viable.cpp @@ -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";