From a3ba4e136634b0c94806e6508b5f2002d020344a Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 1 Sep 2021 11:34:44 -0700
Subject: [PATCH] #5528

---
 src/sat/smt/q_eval.cpp | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp
index 73232fb7c..600dcd2c5 100644
--- a/src/sat/smt/q_eval.cpp
+++ b/src/sat/smt/q_eval.cpp
@@ -181,23 +181,25 @@ namespace q {
         while (!todo.empty()) {
             expr* t = todo.back();
             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);                
-                if (!m_eval[t->get_id()])
-                    return nullptr;
-                todo.pop_back();
-                continue;
-            }
             if (m_mark.is_marked(t)) {
                 todo.pop_back();
                 continue;
             }
-            if (is_var(t)) {
+            if (is_ground(t) || (has_quantifiers(t) && !has_free_vars(t))) {
+                m_eval.setx(t->get_id(), ctx.get_egraph().find(t), nullptr);                
+                if (!m_eval[t->get_id()])
+                    return nullptr;
                 m_mark.mark(t);
+                todo.pop_back();
+                continue;
+            }
+            if (is_var(t)) {
                 if (to_var(t)->get_idx() >= n)
                     return nullptr;
                 m_eval.setx(t->get_id(), binding[n - 1 - to_var(t)->get_idx()], nullptr);
+                if (!m_eval[t->get_id()])
+                    return nullptr;
+                m_mark.mark(t);
                 todo.pop_back();
                 continue;
             }