From 49b94a00902a8a591be1c62a70aa8e2fe34c44b8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 19 Jul 2021 11:38:04 -0700
Subject: [PATCH] #5417 extend definition of ground to be variable free

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

diff --git a/src/sat/smt/q_eval.cpp b/src/sat/smt/q_eval.cpp
index 9dcf5755f..accc4f526 100644
--- a/src/sat/smt/q_eval.cpp
+++ b/src/sat/smt/q_eval.cpp
@@ -15,6 +15,7 @@ Author:
 
 --*/
 
+#include "ast/has_free_vars.h"
 #include "sat/smt/q_eval.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/q_solver.h"
@@ -176,7 +177,7 @@ namespace q {
         while (!todo.empty()) {
             expr* t = todo.back();
             SASSERT(!is_ground(t) || ctx.get_egraph().find(t));
-            if (is_ground(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()]);