fix #7017

Z3Prover · Nov 28, 2023 · 8179f8b · 8179f8b
1 parent f36f21f
commit 8179f8b
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 3 deletions.
diff --git 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
@@ -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
@@ -1513,7 +1513,7 @@ class theory_lra::imp {
         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 @@ class theory_lra::imp {
             }
         }
         return r;
-
     }
 
     model_value_proc * mk_value(enode * n, model_generator & mg) {
@@ -3402,6 +3401,10 @@ class theory_lra::imp {
             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))