diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 35fc9d2f1..98a148df5 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -763,7 +763,7 @@ namespace datalog {
 
     class context::engine_type_proc {
         ast_manager&  m;
-        arith_util    a;
+        arith_util    a;        
         datatype_util dt;
         bv_util       bv;
         DL_ENGINE     m_engine_type;
@@ -790,10 +790,14 @@ namespace datalog {
             else if (is_large_bv(m.get_sort(e))) {
                 m_engine_type = SPACER_ENGINE;
             }
+            else if (!m.get_sort(e)->get_num_elements().is_finite()) {
+                m_engine_type = SPACER_ENGINE;
+            }
         }
     };
 
     void context::configure_engine(expr* q) {
+        TRACE("dl", tout << mk_pp(q, m) << " " << m_engine_type << "\n";);
         if (m_engine_type != LAST_ENGINE) {
             return;
         }
diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp
index e4b20d250..b0a5ca9ee 100644
--- a/src/muz/rel/dl_compiler.cpp
+++ b/src/muz/rel/dl_compiler.cpp
@@ -728,7 +728,7 @@ namespace datalog {
             expr_ref renamed = m_context.get_var_subst()(filter_cond, binding.size(), binding.c_ptr());
             app_ref app_renamed(to_app(renamed), m);
             if (remove_columns.empty()) {
-                if (!dealloc)
+                if (!dealloc && filtered_res != UINT_MAX)
                     make_clone(filtered_res, filtered_res, acc);
                 acc.push_back(instruction::mk_filter_interpreted(filtered_res, app_renamed));
             } else {
diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp
index bc41a3265..5478f9177 100644
--- a/src/muz/rel/rel_context.cpp
+++ b/src/muz/rel/rel_context.cpp
@@ -156,7 +156,7 @@ namespace datalog {
             TRACE("dl", m_context.display(tout););
             //IF_VERBOSE(3, m_context.display_smt2(0,0,verbose_stream()););
 
-            if (!m_context.print_aig().is_null()) {
+            if (m_context.print_aig().is_non_empty_string()) {
                 const char *filename = m_context.print_aig().bare_str();
                 aig_exporter aig(m_context.get_rules(), get_context(), &m_table_facts);
                 std::ofstream strm(filename, std::ios_base::binary);