From cb4e5197faa4b0af421edc7cc7b547bde820067f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 12 Nov 2020 16:55:07 -0800 Subject: [PATCH] #4740 Fix https://github.com/Z3Prover/z3/issues/4740#issuecomment-712092917 --- src/smt/theory_bv.cpp | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) diff --git a/src/smt/theory_bv.cpp b/src/smt/theory_bv.cpp index 6b7db2d8f..a613e61fd 100644 --- a/src/smt/theory_bv.cpp +++ b/src/smt/theory_bv.cpp @@ -229,8 +229,8 @@ namespace smt { m_stats.m_num_diseq_static++; app * e1 = get_expr(v1); app * e2 = get_expr(v2); - literal l = ~(mk_eq(e1, e2, true)); - expr * eq = ctx.bool_var2expr(l.var()); + expr_ref eq(m.mk_eq(e1, e2), m); + literal l = ~mk_literal(eq); std::function logfn = [&]() { return m.mk_implies(m.mk_eq(mk_bit2bool(e1, idx), m.mk_not(mk_bit2bool(e2, idx))), m.mk_not(eq)); }; @@ -1191,7 +1191,7 @@ namespace smt { void theory_bv::assign_eh(bool_var v, bool is_true) { atom * a = get_bv2a(v); - TRACE("bv", tout << "assert: p" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << "\n";); + TRACE("bv", tout << "assert: p" << v << " #" << ctx.bool_var2expr(v)->get_id() << " is_true: " << is_true << " " << ctx.inconsistent() << "\n";); if (a->is_bit()) { m_prop_queue.reset(); bit_atom * b = static_cast(a); @@ -1238,10 +1238,11 @@ namespace smt { while (v2 != v) { literal_vector & bits2 = m_bits[v2]; literal bit2 = bits2[idx]; - SASSERT(bit != ~bit2); lbool val2 = ctx.get_assignment(bit2); TRACE("bv_bit_prop", tout << "propagating #" << get_enode(v2)->get_owner_id() << "[" << idx << "] = " << val2 << "\n";); TRACE("bv", tout << bit << " -> " << bit2 << " " << val << " -> " << val2 << " " << ctx.get_scope_level() << "\n";); + + SASSERT(bit != ~bit2); if (val != val2) { literal consequent = bit2;