diff --git a/src/muz/base/dl_engine_base.h b/src/muz/base/dl_engine_base.h
index e0d8680b2..f353fbf2e 100644
--- a/src/muz/base/dl_engine_base.h
+++ b/src/muz/base/dl_engine_base.h
@@ -44,7 +44,26 @@ namespace datalog {
 
         virtual expr_ref get_answer() = 0;
         virtual lbool query(expr* q) = 0;
-        virtual lbool query(unsigned num_rels, func_decl*const* rels) { return l_undef; }
+        virtual lbool query(unsigned num_rels, func_decl*const* rels) { 
+            if (num_rels != 1) return l_undef;
+            expr_ref q(m);
+            expr_ref_vector args(m);
+            sort_ref_vector sorts(m);
+            svector<symbol> names;
+            func_decl* r = rels[0];
+            for (unsigned i = 0; i < r->get_arity(); ++i) {
+                args.push_back(m.mk_var(i, r->get_domain(i)));
+                sorts.push_back(r->get_domain(i));
+                names.push_back(symbol(i));
+            }
+            sorts.reverse();
+            names.reverse();
+            q = m.mk_app(r, args.size(), args.c_ptr());
+            if (!args.empty()) {
+                q = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), q);
+            }
+            return query(q);
+        }
 
         virtual void reset_statistics() {}
         virtual void display_profile(std::ostream& out) const {}
diff --git a/src/muz/fp/dl_cmds.cpp b/src/muz/fp/dl_cmds.cpp
index f8e97d95d..2a6ff04d4 100644
--- a/src/muz/fp/dl_cmds.cpp
+++ b/src/muz/fp/dl_cmds.cpp
@@ -268,10 +268,10 @@ public:
             print_certificate(ctx);
             break;
         case l_undef: 
-            if(dlctx.get_status() == datalog::BOUNDED){
-              ctx.regular_stream() << "bounded\n";
-              print_certificate(ctx);
-              break;
+            if (dlctx.get_status() == datalog::BOUNDED){
+                ctx.regular_stream() << "bounded\n";
+                print_certificate(ctx);
+                break;
             }
             ctx.regular_stream() << "unknown\n";
             switch(dlctx.get_status()) {