diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp index accc4f526..4d5a37821 100644 --- a/src/sat/smt/q_eval.cpp +++ b/src/sat/smt/q_eval.cpp @@ -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; }