From 9efe6f6afa5bef2975040b6e014ae9da149549e7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 29 Nov 2023 14:54:54 -0800
Subject: [PATCH] fix regression in fix for #7006

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/model/model_evaluator.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp
index 5a5bd79b60b..9cef0472fa4 100644
--- a/src/model/model_evaluator.cpp
+++ b/src/model/model_evaluator.cpp
@@ -447,7 +447,7 @@ struct evaluator_cfg : public default_rewriter_cfg {
         }
         else if (m_dt.is_accessor(f)) {
             expr* arg = args[0];
-            if (is_ground(arg) && !fi) {
+            if (m.is_value(arg) && !fi) {
                 fi = alloc(func_interp, m, f->get_arity());
                 expr* val = m_model.get_some_value(f->get_range());
                 fi->set_else(val);