From 8179f8b5d7424c697d18afa5515f33e120f6bc32 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 28 Nov 2023 14:32:56 -0800
Subject: [PATCH] fix #7017

---
 src/sat/smt/arith_solver.cpp | 7 ++++++-
 src/sat/smt/arith_solver.h   | 1 +
 src/smt/theory_lra.cpp       | 7 +++++--
 3 files changed, 12 insertions(+), 3 deletions(-)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index fe7b0aa46..537291280 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -899,6 +899,11 @@ namespace arith {
             lp().random_update(vars.size(), vars.data());
     }
 
+    bool solver::include_func_interp(enode* n) const {
+        func_decl* d = n->get_decl();
+        return d && include_func_interp(d);
+    }
+
     bool solver::assume_eqs() {
         if (delayed_assume_eqs())
             return true;
@@ -913,7 +918,7 @@ namespace arith {
             theory_var v = (i + start) % sz;
             if (is_bool(v))
                 continue;
-            if (!ctx.is_shared(var2enode(v)))
+            if (!ctx.is_shared(var2enode(v)) && !include_func_interp(var2enode(v)))
                 continue;
             ensure_column(v);
             if (!is_registered_var(v))
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index ddaaa6164..84be3caa7 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -401,6 +401,7 @@ namespace arith {
         bool delayed_assume_eqs();
         bool is_eq(theory_var v1, theory_var v2);
         bool use_nra_model();
+        bool include_func_interp(enode* n) const;
 
         lbool make_feasible();
         bool  check_delayed_eqs();
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index a23472e5b..bbe29da74 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1513,7 +1513,7 @@ public:
         for (theory_var i = 0; i < sz; ++i) {
             theory_var v = (i + start) % sz;
             enode* n1 = get_enode(v);
-            if (!th.is_relevant_and_shared(n1))                     
+            if (!th.is_relevant_and_shared(n1) && !include_func_interp(n1))                     
                 continue;
             ensure_column(v);
             if (!is_registered_var(v))
@@ -3346,7 +3346,6 @@ public:
             }
         }
         return r;
-
     }
 
     model_value_proc * mk_value(enode * n, model_generator & mg) {
@@ -3402,6 +3401,10 @@ public:
             a.is_mod0(f);        
     }
 
+    bool include_func_interp(enode* n) {
+        return include_func_interp(n->get_decl());
+    }
+
     bool get_lower(enode* n, rational& val, bool& is_strict) {
         theory_var v = n->get_th_var(get_id());
         if (!is_registered_var(v))