From dda4d66325d9cfa219ce79e1eb959bcf131597af Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 12 Dec 2020 12:33:48 -0800 Subject: [PATCH] fix #4888 Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 13 ++++++++----- 1 file changed, 8 insertions(+), 5 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index abfa8bcd6..df519c158 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -1321,17 +1321,20 @@ namespace smt { SASSERT(!inconsistent()); literal l = m_atom_propagation_queue[i]; bool_var v = l.var(); - bool_var_data & d = get_bdata(v); lbool val = get_assignment(v); - TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() << ", is_enode(): " << d.is_enode() - << " tag: " << (d.is_eq()?"eq":"") << (d.is_theory_atom()?"th":"") << (d.is_quantifier()?"q":"") << " " << l << "\n";); + TRACE("propagate_atoms", tout << "propagating atom, #" << bool_var2expr(v)->get_id() + << ", is_enode(): " << get_bdata(v).is_enode() << " tag: " + << (get_bdata(v).is_eq()?"eq":"") + << (get_bdata(v).is_theory_atom()?"th":"") + << (get_bdata(v).is_quantifier()?"q":"") << " " << l << "\n";); SASSERT(val != l_undef); - if (d.is_enode()) + if (get_bdata(v).is_enode()) propagate_bool_var_enode(v); if (inconsistent()) return false; + bool_var_data & d = get_bdata(v); if (d.is_eq()) { - app * n = to_app(m_bool_var2expr[v]); + app * n = to_app(m_bool_var2expr[v]); SASSERT(m.is_eq(n)); expr * lhs = n->get_arg(0); expr * rhs = n->get_arg(1);