From 7e330c15e763ce1eb956f3cba9d6a1972adf4232 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 5 May 2021 16:57:06 -0700
Subject: [PATCH] #5223

---
 src/sat/smt/arith_solver.cpp | 9 +++++++++
 src/sat/smt/arith_solver.h   | 1 +
 2 files changed, 10 insertions(+)

diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index bb8e1d054..a005b10c7 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -580,6 +580,7 @@ namespace arith {
                        verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n";
                        verbose_stream() << *b << "\n";);
             IF_VERBOSE(0, ctx.display(verbose_stream()));
+            IF_VERBOSE(0, verbose_stream() << mdl << "\n");
             UNREACHABLE();
         }
     }
@@ -1438,4 +1439,12 @@ namespace arith {
         ctx.get_antecedents(l, jst, r, probing);
     }
 
+    bool solver::include_func_interp(func_decl* f) const {
+        return 
+            a.is_div0(f) ||
+            a.is_idiv0(f) ||
+            a.is_power0(f) ||
+            a.is_rem0(f) ||
+            a.is_mod0(f);        
+    }
 }
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 91955c716..17887535d 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -444,6 +444,7 @@ namespace arith {
         void apply_sort_cnstr(euf::enode* n, sort* s) override {}
         bool is_shared(theory_var v) const override;
         lbool get_phase(bool_var v) override;
+        bool include_func_interp(func_decl* f) const override;
 
         // bounds and equality propagation callbacks
         lp::lar_solver& lp() { return *m_solver; }