From d2ec661ec63446bea4e6c9801b3b3b2522e51ff4 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 6 Apr 2020 16:42:01 -0700
Subject: [PATCH] fix #3020

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_context.cpp      | 6 +++++-
 src/muz/base/rule_properties.cpp | 8 +++-----
 src/muz/base/rule_properties.h   | 2 ++
 3 files changed, 10 insertions(+), 6 deletions(-)

diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 68b3f1e4d..97c780de6 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -766,6 +766,7 @@ namespace datalog {
         arith_util    a;        
         datatype_util dt;
         bv_util       bv;
+        array_util    ar;
         DL_ENGINE     m_engine_type;
 
         bool is_large_bv(sort* s) {
@@ -773,7 +774,7 @@ namespace datalog {
         }
 
     public:
-        engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), m_engine_type(DATALOG_ENGINE) {}
+        engine_type_proc(ast_manager& m): m(m), a(m), dt(m), bv(m), ar(m), m_engine_type(DATALOG_ENGINE) {}
 
         DL_ENGINE get_engine() const { return m_engine_type; }
 
@@ -793,6 +794,9 @@ namespace datalog {
             else if (!m.get_sort(e)->get_num_elements().is_finite()) {
                 m_engine_type = SPACER_ENGINE;
             }
+            else if (ar.is_array(e)) {
+                m_engine_type = SPACER_ENGINE;
+            }
         }
     };
 
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index b53996aed..d43a156eb 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -26,16 +26,14 @@ 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_generate_proof(false) {}
+    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) {}
 
 rule_properties::~rule_properties() {}
 
 void rule_properties::collect(rule_set const& rules) {
     reset();
-    rule_set::iterator it = rules.begin(), end = rules.end();
     expr_sparse_mark visited;
-    for (; it != end; ++it) {
-        rule* r = *it;
+    for (rule* r : rules) {
         m_rule = r;
         unsigned ut_size = r->get_uninterpreted_tail_size();
         unsigned t_size  = r->get_tail_size();  
@@ -51,7 +49,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 (!sz.is_finite() && !m_dl.is_rule_sort(d)) {
+            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);
             }
diff --git a/src/muz/base/rule_properties.h b/src/muz/base/rule_properties.h
index 197633aff..8df718516 100644
--- a/src/muz/base/rule_properties.h
+++ b/src/muz/base/rule_properties.h
@@ -24,6 +24,7 @@ Notes:
 #include "ast/ast.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/bv_decl_plugin.h"
+#include "ast/array_decl_plugin.h"
 #include "muz/base/dl_rule.h"
 
 namespace datalog {
@@ -35,6 +36,7 @@ namespace datalog {
         datatype_util m_dt;
         dl_decl_util  m_dl;
         bv_util       m_bv;
+        array_util    m_ar;
         bool          m_generate_proof;
         rule*         m_rule;
         obj_map<quantifier, rule*> m_quantifiers;