mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

fix #4888

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-12-12 12:33:48 -08:00
parent 8cb30d0505
commit dda4d66325
1 changed files with 8 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

13
src/smt/smt_context.cpp
View file

@ -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);