diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 9e5e7b23e..dca2f3dc9 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -773,19 +773,19 @@ namespace datalog {
         DL_ENGINE get_engine() const { return m_engine_type; }
 
         void operator()(expr* e) {
-                if (a.is_int_real(e)) {
-                   m_engine_type = SPACER_ENGINE;
-                }
-                else if (is_var(e) && m.is_bool(e)) {
-                    m_engine_type = SPACER_ENGINE;
-                }
-                else if (dt.is_datatype(m.get_sort(e))) {
-                     m_engine_type = SPACER_ENGINE;
+            if (a.is_int_real(e)) {
+                m_engine_type = SPACER_ENGINE;
+            }
+            else if (is_var(e) && m.is_bool(e)) {
+                m_engine_type = SPACER_ENGINE;
+            }
+            else if (dt.is_datatype(m.get_sort(e))) {
+                m_engine_type = SPACER_ENGINE;
             }
         }
     };
 
-    void context::configure_engine() {
+    void context::configure_engine(expr* q) {
         if (m_engine_type != LAST_ENGINE) {
             return;
         }
@@ -817,6 +817,10 @@ namespace datalog {
             expr_fast_mark1 mark;
             engine_type_proc proc(m);
             m_engine_type = DATALOG_ENGINE;
+            std::cout << "configure engine " << m_rule_set.get_num_rules() << " " << m_rule_fmls.size() << " " << q << "\n";
+            if (q) {
+                quick_for_each_expr(proc, mark, q);
+            }
             for (unsigned i = 0; m_engine_type == DATALOG_ENGINE && i < m_rule_set.get_num_rules(); ++i) {
                 rule * r = m_rule_set.get_rule(i);
                 quick_for_each_expr(proc, mark, r->get_head());
@@ -837,12 +841,13 @@ namespace datalog {
     }
 
     lbool context::query(expr* query) {
+        std::cout << "query: " << mk_pp(query, m) << "\n";
         expr_ref _query(query, m);
         m_mc = mk_skip_model_converter();
         m_last_status = OK;
         m_last_answer = nullptr;
         m_last_ground_answer = nullptr;
-        switch (get_engine()) {
+        switch (get_engine(query)) {
         case DATALOG_ENGINE:
         case SPACER_ENGINE:
         case BMC_ENGINE:
@@ -855,7 +860,7 @@ namespace datalog {
         default:
             UNREACHABLE();
         }
-        ensure_engine();
+        ensure_engine(query);
         lbool r = m_engine->query(query);
         if (r != l_undef && get_params().print_certificate()) {
             display_certificate(std::cout) << "\n";
@@ -893,9 +898,9 @@ namespace datalog {
         return m_engine->get_proof();
     }
 
-    void context::ensure_engine() {
+    void context::ensure_engine(expr* e) {
         if (!m_engine.get()) {
-            m_engine = m_register_engine.mk_engine(get_engine());
+            m_engine = m_register_engine.mk_engine(get_engine(e));
             m_engine->updt_params();
 
             // break abstraction.
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 20f40fb22..2ae0e53ef 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -227,13 +227,13 @@ namespace datalog {
         bool saturation_was_run() const { return m_saturation_was_run; }
         void notify_saturation_was_run() { m_saturation_was_run = true; }
 
-        void configure_engine();
+        void configure_engine(expr* e);
 
         ast_manager & get_manager() const { return m; }
         rule_manager & get_rule_manager() { return m_rule_manager; }
         smt_params & get_fparams() const { return m_fparams; }
         fp_params const&  get_params() const { return *m_params; }
-        DL_ENGINE get_engine() { configure_engine(); return m_engine_type; }
+        DL_ENGINE get_engine(expr* e = nullptr) { configure_engine(e); return m_engine_type; }
         register_engine_base& get_register_engine() { return m_register_engine; }
         th_rewriter& get_rewriter() { return m_rewriter; }
         var_subst & get_var_subst() { return m_var_subst; }
@@ -609,7 +609,7 @@ namespace datalog {
 
         void flush_add_rules();
 
-        void ensure_engine();
+        void ensure_engine(expr* e = nullptr);
 
         // auxiliary functions for SMT2 pretty-printer.
         void declare_vars(expr_ref_vector& rules, mk_fresh_name& mk_fresh, std::ostream& out);