From ebdf031c8fe6a87c2beec877bd9ef4def0dbfc98 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 31 May 2026 15:32:23 -0700
Subject: [PATCH] ensure engine is datalog for dl_table and dl_util tests

---
 src/muz/base/dl_context.cpp |  3 +--
 src/muz/base/dl_context.h   |  4 ++--
 src/test/dl_table.cpp       | 16 ++++++++--------
 src/test/dl_util.cpp        |  1 +
 src/test/doc.cpp            |  4 ++--
 src/test/udoc_relation.cpp  |  3 ++-
 6 files changed, 16 insertions(+), 15 deletions(-)

diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index bf84d7be7..797ce0774 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -777,7 +777,7 @@ namespace datalog {
         datatype_util dt;
         bv_util       bv;
         array_util    ar;
-        DL_ENGINE     m_engine_type;
+        DL_ENGINE     m_engine_type = DATALOG_ENGINE;
 
         bool is_large_bv(expr *e) {
             sort *s = e->get_sort();
@@ -961,7 +961,6 @@ namespace datalog {
             if (get_engine() == DATALOG_ENGINE) {
                 m_rel = dynamic_cast<rel_context_base*>(m_engine.get());
             }
-
         }
     }
 
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 394b217df..1181cf82b 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -192,7 +192,7 @@ namespace datalog {
         model_converter_ref m_mc;
         proof_converter_ref m_pc;
 
-        rel_context_base*               m_rel;
+        rel_context_base*               m_rel = nullptr;
         scoped_ptr<engine_base>         m_engine;
 
         bool               m_closed;
@@ -201,7 +201,7 @@ namespace datalog {
         execution_result   m_last_status;
         expr_ref           m_last_answer;
         expr_ref           m_last_ground_answer;
-        DL_ENGINE          m_engine_type;
+        DL_ENGINE          m_engine_type = LAST_ENGINE;
 
 
 
diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp
index 0f429d223..e435e70e6 100644
--- a/src/test/dl_table.cpp
+++ b/src/test/dl_table.cpp
@@ -23,10 +23,13 @@ static void test_table(mk_table_fn mk_table) {
     sig.push_back(8);
     sig.push_back(4);
     smt_params params;
+    params_ref fp_params;
+    gparams::set("fp.engine", "datalog");
+    // fp_params.set_sym("fp.engine", symbol("datalog"));
     ast_manager ast_m;
     reg_decl_plugins(ast_m);
     datalog::register_engine re;
-    datalog::context ctx(ast_m, re, params);    
+    datalog::context ctx(ast_m, re, params, fp_params);    
     datalog::relation_manager & m = ctx.get_rel_context()->get_rmanager();
 
     m.register_plugin(alloc(datalog::bitvector_table_plugin, m));
@@ -48,13 +51,10 @@ static void test_table(mk_table_fn mk_table) {
     table.add_fact(row2);
     table.display(std::cout);
 
-    datalog::table_base::iterator it = table.begin();
-    datalog::table_base::iterator end = table.end();
-    for (; it != end; ++it) {
-        it->get_fact(row);
-        for (unsigned j = 0; j < row.size(); ++j) {
-            std::cout << row[j] << " ";
-        }
+    for (auto &r : table) {
+        r.get_fact(row);
+        for (auto v : row)
+            std::cout << v << " ";
         std::cout << "\n";
     }
 
diff --git a/src/test/dl_util.cpp b/src/test/dl_util.cpp
index 8c9af0790..57eaac76e 100644
--- a/src/test/dl_util.cpp
+++ b/src/test/dl_util.cpp
@@ -49,6 +49,7 @@ void dl_util_cycle_from_permutation() {
 }
 
 void tst_dl_util() {
+    gparams::set("fp.engine", "datalog");
     dl_util_two_array_sort();
     dl_util_cycle_from_permutation();
 }
diff --git a/src/test/doc.cpp b/src/test/doc.cpp
index d4909a35d..9ea741152 100644
--- a/src/test/doc.cpp
+++ b/src/test/doc.cpp
@@ -436,7 +436,7 @@ public:
         //sub:{xxx \ {1x0, 0x1}}
         //result:{100}
 
-        for (unsigned i = 0; i < 1000; ++i) {
+        for (unsigned i = 0; i < 100; ++i) {
             udoc d1, d2;
             mk_rand_udoc(3, 3, d1);
             mk_rand_udoc(3, 3, d2);
@@ -453,7 +453,7 @@ public:
 
     void test_intersect() {
         expr_ref fml1(m), fml2(m), fml3(m);
-        for (unsigned i = 0; i < 10000; ++i) {
+        for (unsigned i = 0; i < 100; ++i) {
             udoc d1, d2;
             mk_rand_udoc(3, 3, d1);
             mk_rand_udoc(3, 3, d2);
diff --git a/src/test/udoc_relation.cpp b/src/test/udoc_relation.cpp
index c9c6555c5..ffe0d5d71 100644
--- a/src/test/udoc_relation.cpp
+++ b/src/test/udoc_relation.cpp
@@ -44,6 +44,7 @@ class udoc_tester {
     bv_util                   bv;
     expr_ref_vector           m_vars;
     smt_params                m_smt_params;
+    params_ref                m_fp_params;
     datalog::register_engine  m_reg;
     datalog::context          m_ctx;
     datalog::rel_context      rc;
@@ -113,7 +114,7 @@ class udoc_tester {
 
 public:
     udoc_tester(): 
-        m_init(m), bv(m), m_vars(m), m_ctx(m, m_reg, m_smt_params), rc(m_ctx),
+        m_init(m), bv(m), m_vars(m), m_ctx(m, m_reg, m_smt_params, m_fp_params), rc(m_ctx),
         p(dynamic_cast<udoc_plugin&>(*rc.get_rmanager().get_relation_plugin(symbol("doc")))),
         cr(dynamic_cast<datalog::check_relation_plugin&>(*rc.get_rmanager().get_relation_plugin(symbol("check_relation"))))
     {