diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index d86f5cb01..ac1aa01c4 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -3484,6 +3484,15 @@ public:
         }
     }    
 
+    bool include_func_interp(func_decl* f) {
+        return 
+            a.is_div0(f) ||
+            a.is_idiv0(f) ||
+            a.is_power0(f) ||
+            a.is_rem0(f) ||
+            a.is_mod0(f);        
+    }
+
     bool get_lower(enode* n, rational& val, bool& is_strict) {
         theory_var v = n->get_th_var(get_id());
         if (!can_get_bound(v)) {
@@ -3980,6 +3989,9 @@ bool theory_lra::get_value(enode* n, rational& r) {
 bool theory_lra::get_value(enode* n, expr_ref& r) {
     return m_imp->get_value(n, r);
 }
+bool theory_lra::include_func_interp(func_decl* f) {
+    return m_imp->include_func_interp(f);
+}
 bool theory_lra::get_lower(enode* n, expr_ref& r) {
     return m_imp->get_lower(n, r);
 }
diff --git a/src/smt/theory_lra.h b/src/smt/theory_lra.h
index f3f7c8e55..9611e9ce6 100644
--- a/src/smt/theory_lra.h
+++ b/src/smt/theory_lra.h
@@ -82,6 +82,7 @@ namespace smt {
         model_value_proc * mk_value(enode * n, model_generator & mg) override;
 
         bool get_value(enode* n, expr_ref& r) override;
+        bool include_func_interp(func_decl* f) override;
         bool get_value(enode* n, rational& r);
         bool get_lower(enode* n, expr_ref& r);
         bool get_upper(enode* n, expr_ref& r);