mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
fix #5225
This commit is contained in:
parent
9031b5b949
commit
7b3a587505
|
@ -385,10 +385,10 @@ namespace smt {
|
|||
expr* e = kv.m_key;
|
||||
expr* val = kv.m_value;
|
||||
literal lit = mk_diseq(e, val);
|
||||
mark_as_relevant(lit);
|
||||
if (get_assignment(lit) != l_undef) {
|
||||
continue;
|
||||
}
|
||||
mark_as_relevant(lit);
|
||||
++num_vars;
|
||||
push_scope();
|
||||
assign(lit, b_justification::mk_axiom(), true);
|
||||
|
|
|
@ -333,7 +333,8 @@ namespace smt {
|
|||
if (e != nullptr) {
|
||||
enode * curr = e;
|
||||
do {
|
||||
set_relevant(curr->get_expr());
|
||||
if (!is_relevant_core(curr->get_expr()))
|
||||
set_relevant(curr->get_expr());
|
||||
curr = curr->get_next();
|
||||
}
|
||||
while (curr != e);
|
||||
|
|
Loading…
Reference in a new issue