mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

#4740

Browse source 
Fix https://github.com/Z3Prover/z3/issues/4740#issuecomment-712092917
This commit is contained in:
Nikolaj Bjorner 2020-11-12 16:55:07 -08:00
parent 7f869e513b
commit cb4e5197fa
1 changed files with 5 additions and 4 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/smt/theory_bv.cpp
View file

@ -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<expr*(void)> 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<bit_atom*>(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;