mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
This commit is contained in:
parent
49bd3ad159
commit
f90795c42f
|
@ -179,8 +179,9 @@ namespace q {
|
|||
SASSERT(!is_ground(t) || ctx.get_egraph().find(t));
|
||||
if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) {
|
||||
m_mark.mark(t);
|
||||
m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);
|
||||
SASSERT(m_eval[t->get_id()]);
|
||||
m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);
|
||||
if (!m_eval[t->get_id()])
|
||||
return nullptr;
|
||||
todo.pop_back();
|
||||
continue;
|
||||
}
|
||||
|
|
Loading…
Reference in a new issue