From 889a7ad3f2d5a6f6e590ccbefe9401e3a8ce6475 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 7 Apr 2020 11:23:37 -0700
Subject: [PATCH] fix #3819

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/rule_properties.cpp | 12 ++++++++++--
 src/muz/base/rule_properties.h   |  4 ++++
 2 files changed, 14 insertions(+), 2 deletions(-)

diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index d90d4a59b..3696ae1de 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -26,7 +26,7 @@ Notes:
 
 using namespace datalog;
 rule_properties::rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& p): 
-    m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_bv(m), m_ar(m), m_generate_proof(false) {}
+    m(m), rm(rm), m_ctx(ctx), m_is_predicate(p), m_dt(m), m_dl(m), m_a(m), m_bv(m), m_ar(m), m_generate_proof(false) {}
 
 rule_properties::~rule_properties() {}
 
@@ -173,12 +173,14 @@ void rule_properties::insert(ptr_vector<rule>& rules, rule* r) {
 }
 
 void rule_properties::operator()(var* n) { 
+    check_sort(m.get_sort(n));
 }
 
 void rule_properties::operator()(quantifier* n) {
     m_quantifiers.insert(n, m_rule);
 }
 void rule_properties::operator()(app* n) {
+    func_decl_ref f_out(m);
     if (m_is_predicate(n)) {
         insert(m_interp_pred, m_rule);
     }    
@@ -204,7 +206,13 @@ void rule_properties::operator()(app* n) {
             }
         }
     }
-    sort* s = m.get_sort(n);
+    else if (m_a.is_considered_uninterpreted(n->get_decl(), n->get_num_args(), n->get_args(), f_out)) {
+        m_uninterp_funs.insert(n->get_decl(), m_rule);
+    }
+    check_sort(m.get_sort(n));
+}
+
+void rule_properties::check_sort(sort* s) {
     sort_size sz = s->get_num_elements();
     if (m_ar.is_array(s) || (!sz.is_finite() && !m_dl.is_rule_sort(s))) {
         m_inf_sort.push_back(m_rule);
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
index 8df718516..364af65b9 100644
--- a/src/muz/base/rule_properties.h
+++ b/src/muz/base/rule_properties.h
@@ -25,6 +25,7 @@ Notes:
 #include "ast/datatype_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
 #include "ast/array_decl_plugin.h"
+#include "ast/arith_decl_plugin.h"
 #include "muz/base/dl_rule.h"
 
 namespace datalog {
@@ -35,6 +36,7 @@ namespace datalog {
         i_expr_pred&  m_is_predicate;
         datatype_util m_dt;
         dl_decl_util  m_dl;
+        arith_util    m_a;
         bv_util       m_bv;
         array_util    m_ar;
         bool          m_generate_proof;
@@ -46,6 +48,8 @@ namespace datalog {
         ptr_vector<rule>           m_inf_sort;
 
         void insert(ptr_vector<rule>& rules, rule* r);
+        void check_sort(sort* s);
+
     public:
         rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& is_predicate);
         ~rule_properties();