mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
fix bca condition for tautology check
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
ac0202630e
commit
0919fd4075
|
@ -1070,7 +1070,7 @@ namespace sat {
|
|||
for (; !it.at_end(); it.next()) {
|
||||
bool tautology = false;
|
||||
clause & c = it.curr();
|
||||
if (c.is_blocked()) continue;
|
||||
if (c.is_blocked() && !adding) continue;
|
||||
for (literal lit : c) {
|
||||
if (s.is_marked(~lit) && lit != ~l) {
|
||||
tautology = true;
|
||||
|
@ -1322,8 +1322,12 @@ namespace sat {
|
|||
}
|
||||
if (!found) {
|
||||
IF_VERBOSE(100, verbose_stream() << "bca " << l << " " << l2 << "\n";);
|
||||
s.get_wlist(~l).push_back(watched(l2, true));
|
||||
s.get_wlist(~l2).push_back(watched(l, true));
|
||||
watched w1(l2, false);
|
||||
w1.set_blocked();
|
||||
watched w2(l, false);
|
||||
w2.set_blocked();
|
||||
s.get_wlist(~l).push_back(w1);
|
||||
s.get_wlist(~l2).push_back(w2);
|
||||
++s.m_num_bca;
|
||||
}
|
||||
}
|
||||
|
|
|
@ -1553,8 +1553,10 @@ namespace sat {
|
|||
|
||||
// #ifndef _EXTERNAL_RELEASE
|
||||
IF_VERBOSE(10, verbose_stream() << "\"checking model\"\n";);
|
||||
if (!check_model(m_model))
|
||||
if (!check_model(m_model)) {
|
||||
UNREACHABLE();
|
||||
throw solver_exception("check model failed");
|
||||
}
|
||||
|
||||
if (m_clone) {
|
||||
IF_VERBOSE(SAT_VB_LVL, verbose_stream() << "\"checking model (on original set of clauses)\"\n";);
|
||||
|
@ -1576,6 +1578,9 @@ namespace sat {
|
|||
tout << "model: " << m << "\n";
|
||||
m_mc.display(tout);
|
||||
);
|
||||
for (literal l : c) {
|
||||
if (was_eliminated(l.var())) IF_VERBOSE(0, verbose_stream() << "eliminated: " << l << "\n";);
|
||||
}
|
||||
ok = false;
|
||||
}
|
||||
}
|
||||
|
@ -1588,7 +1593,7 @@ namespace sat {
|
|||
continue;
|
||||
literal l2 = w.get_literal();
|
||||
if (value_at(l2, m) != l_true) {
|
||||
IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " " << l2 << " " << "\n";);
|
||||
IF_VERBOSE(0, verbose_stream() << "failed binary: " << l << " " << l2 << "\n";);
|
||||
TRACE("sat", m_mc.display(tout << "failed binary: " << l << " " << l2 << "\n"););
|
||||
ok = false;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue