From f90795c42fc15e812edf61bdab6df1798c5203ef Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 20 Jul 2021 07:58:21 -0700
Subject: [PATCH] #5420

---
 src/sat/smt/q_eval.cpp | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

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;
             }