From 876bd80bea17e8936cd7b6822122f2d88ba6d0be Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 4 Feb 2020 14:07:24 -0800
Subject: [PATCH] fix model generation for underspecified operators in
 theory_lra

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/theory_lra.cpp | 12 ++++++++++++
 src/smt/theory_lra.h   |  1 +
 2 files changed, 13 insertions(+)

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);