From 76ac9917c8da5d172fba03121af8016090198958 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 9 Apr 2020 13:12:37 -0700
Subject: [PATCH] fix #3890

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_context.h        |  1 -
 src/muz/base/rule_properties.cpp | 13 +++++++------
 src/muz/base/rule_properties.h   |  5 +++--
 src/muz/fp/horn_tactic.cpp       |  1 -
 4 files changed, 10 insertions(+), 10 deletions(-)

diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 5a19bfd43..8edf66945 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -608,7 +608,6 @@ namespace datalog {
         */
         void reset_tables();
 
-
         void flush_add_rules();
 
         void ensure_engine(expr* e = nullptr);
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index f8f6a6f53..14f641c44 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -28,7 +28,7 @@ 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_a(m), m_bv(m), m_ar(m), 
-    m_generate_proof(false), m_collected(false) {}
+    m_generate_proof(false), m_collected(false), m_is_monotone(true) {}
 
 rule_properties::~rule_properties() {}
 
@@ -36,11 +36,16 @@ void rule_properties::collect(rule_set const& rules) {
     reset();
     m_collected = true;
     expr_sparse_mark visited;
+    visit_rules(visited, rules);
+}
+
+void rule_properties::visit_rules(expr_sparse_mark& visited, rule_set const& rules) {
     for (rule* r : rules) {
         m_rule = r;
         unsigned ut_size = r->get_uninterpreted_tail_size();
         unsigned t_size  = r->get_tail_size();  
         if (r->has_negation()) {
+            m_is_monotone = false;
             m_negative_rules.push_back(r);            
         }
         for (unsigned i = ut_size; i < t_size; ++i) {
@@ -52,11 +57,7 @@ void rule_properties::collect(rule_set const& rules) {
         
         for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {            
             sort* d = r->get_decl()->get_domain(i);
-            sort_size sz = d->get_num_elements();
-            if (m_ar.is_array(d) || (!sz.is_finite() && !m_dl.is_rule_sort(d))) {
-                TRACE("dl", tout << "sort " << mk_pp(d, m) << " is not finite " << sz << "\n";);
-                m_inf_sort.push_back(m_rule);
-            }
+            check_sort(d);
         }
     }     
 }
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
index fbc2466fb..6946a7854 100644
--- a/src/muz/base/rule_properties.h
+++ b/src/muz/base/rule_properties.h
@@ -47,10 +47,11 @@ namespace datalog {
         ptr_vector<rule>           m_negative_rules;
         ptr_vector<rule>           m_inf_sort;
         bool                       m_collected;
+        bool                       m_is_monotone;
 
         void insert(ptr_vector<rule>& rules, rule* r);
         void check_sort(sort* s);
-
+        void visit_rules(expr_sparse_mark& visited, rule_set const& rules);
     public:
         rule_properties(ast_manager & m, rule_manager& rm, context& ctx, i_expr_pred& is_predicate);
         ~rule_properties();    
@@ -62,7 +63,7 @@ namespace datalog {
         void check_for_negated_predicates();
         void check_nested_free();
         void check_infinite_sorts();
-        bool is_monotone() { SASSERT(m_collected); return m_negative_rules.empty(); }
+        bool is_monotone() { return m_is_monotone; }
         void operator()(var* n);
         void operator()(quantifier* n);
         void operator()(app* n);
diff --git a/src/muz/fp/horn_tactic.cpp b/src/muz/fp/horn_tactic.cpp
index b15171e88..dca3d5228 100644
--- a/src/muz/fp/horn_tactic.cpp
+++ b/src/muz/fp/horn_tactic.cpp
@@ -84,7 +84,6 @@ class horn_tactic : public tactic {
             if (!is_positive) {
                 f = m.mk_not(f);
             }
-
         }
 
         bool is_predicate(expr* a) {