diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index ad6b5ad69..2d2b50f3d 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -125,7 +125,7 @@ namespace api {
                 return "unknown";
             }
         }
-        std::string to_string(unsigned num_queries, expr*const* queries) {
+        std::string to_string(unsigned num_queries, expr* const* queries) {
             std::stringstream str;
             m_context.display_smt2(num_queries, queries, str);
             return str.str();
@@ -466,13 +466,16 @@ extern "C" {
         ast_manager& m = mk_c(c)->m();
         Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
         mk_c(c)->save_object(v);
-        expr_ref_vector rules(m);
+        expr_ref_vector rules(m), queries(m);
         svector<symbol> names;
         
-        to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, names);
+        to_fixedpoint_ref(d)->ctx().get_rules_as_formulas(rules, queries, names);
         for (unsigned i = 0; i < rules.size(); ++i) {
             v->m_ast_vector.push_back(rules[i].get());
         }
+        for (unsigned i = 0; i < queries.size(); ++i) {
+            v->m_ast_vector.push_back(m.mk_not(queries[i].get()));
+        }
         RETURN_Z3(of_ast_vector(v));
         Z3_CATCH_RETURN(0);
     }
diff --git a/src/muz/base/dl_context.cpp b/src/muz/base/dl_context.cpp
index 774db6c6a..f3088fa04 100644
--- a/src/muz/base/dl_context.cpp
+++ b/src/muz/base/dl_context.cpp
@@ -1117,7 +1117,7 @@ namespace datalog {
         }
     }
 
-    void context::get_rules_as_formulas(expr_ref_vector& rules, svector<symbol>& names) {
+    void context::get_rules_as_formulas(expr_ref_vector& rules, expr_ref_vector& queries, svector<symbol>& names) {
         expr_ref fml(m);
         datalog::rule_manager& rm = get_rule_manager();
         
@@ -1136,9 +1136,30 @@ namespace datalog {
         }
         rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
         for (; it != end; ++it) {
-            (*it)->to_formula(fml);
-            rules.push_back(fml);
-            names.push_back((*it)->name());
+            rule* r = *it;
+            r->to_formula(fml);
+            func_decl* h = r->get_decl();
+            if (m_rule_set.is_output_predicate(h)) {
+                expr* body = fml;
+                expr* e2;
+                if (is_quantifier(body)) {
+                    quantifier* q = to_quantifier(body);
+                    expr* e = q->get_expr();
+                    VERIFY(m.is_implies(e, body, e2));
+                    fml = m.mk_quantifier(false, q->get_num_decls(),
+                                          q->get_decl_sorts(), q->get_decl_names(),
+                                          body);
+                }
+                else {
+                    VERIFY(m.is_implies(body, body, e2));
+                    fml = body;
+                }
+                queries.push_back(fml);
+            }
+            else {
+                rules.push_back(fml);
+                names.push_back(r->name());
+            }
         }
         for (unsigned i = m_rule_fmls_head; i < m_rule_fmls.size(); ++i) {
             rules.push_back(m_rule_fmls[i].get());
@@ -1146,10 +1167,7 @@ namespace datalog {
         }
     }
  
-    void context::display_smt2(
-        unsigned num_queries, 
-        expr* const* queries, 
-        std::ostream& out) {
+    void context::display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out) {
         ast_manager& m = get_manager();
         free_func_visitor visitor(m);
         expr_mark visited;
@@ -1157,7 +1175,7 @@ namespace datalog {
         unsigned num_axioms = m_background.size();
         expr* const* axioms = m_background.c_ptr();
         expr_ref fml(m);
-        expr_ref_vector rules(m);
+        expr_ref_vector rules(m), queries(m);
         svector<symbol> names;
         bool use_fixedpoint_extensions = m_params->print_fixedpoint_extensions();
         bool print_low_level = m_params->print_low_level_smt2();
@@ -1165,13 +1183,14 @@ namespace datalog {
 
 #define PP(_e_) if (print_low_level) out << mk_smt_pp(_e_, m); else ast_smt2_pp(out, _e_, env);
 
-        get_rules_as_formulas(rules, names);
+        get_rules_as_formulas(rules, queries, names);
+        queries.append(num_queries, qs);
 
         smt2_pp_environment_dbg env(m);
         mk_fresh_name fresh_names;
         collect_free_funcs(num_axioms,  axioms,  visited, visitor, fresh_names);
         collect_free_funcs(rules.size(), rules.c_ptr(),   visited, visitor, fresh_names);
-        collect_free_funcs(num_queries, queries, visited, visitor, fresh_names);
+        collect_free_funcs(queries.size(), queries.c_ptr(), visited, visitor, fresh_names);
         func_decl_set funcs;
         func_decl_set::iterator it  = visitor.funcs().begin();
         func_decl_set::iterator end = visitor.funcs().end();
@@ -1257,22 +1276,22 @@ namespace datalog {
             out << ")\n";
         }
         if (use_fixedpoint_extensions) {
-            for (unsigned i = 0; i < num_queries; ++i) {
+            for (unsigned i = 0; i < queries.size(); ++i) {
                 out << "(query ";
-                PP(queries[i]);                
+                PP(queries[i].get());                
                 out << ")\n";
             }
         }
         else {
-            for (unsigned i = 0; i < num_queries; ++i) {
-                if (num_queries > 1) out << "(push)\n";
+            for (unsigned i = 0; i < queries.size(); ++i) {
+                if (queries.size() > 1) out << "(push)\n";
                 out << "(assert ";
                 expr_ref q(m);
-                q = m.mk_not(queries[i]);
+                q = m.mk_not(queries[i].get());
                 PP(q);
                 out << ")\n";
                 out << "(check-sat)\n";
-                if (num_queries > 1) out << "(pop)\n";
+                if (queries.size() > 1) out << "(pop)\n";
             }
         }
     }
diff --git a/src/muz/base/dl_context.h b/src/muz/base/dl_context.h
index 1952cc42f..b7bcbb5fe 100644
--- a/src/muz/base/dl_context.h
+++ b/src/muz/base/dl_context.h
@@ -362,7 +362,7 @@ namespace datalog {
 
         rule_set & get_rules() { flush_add_rules(); return m_rule_set; }
 
-        void get_rules_as_formulas(expr_ref_vector& fmls, svector<symbol>& names);
+        void get_rules_as_formulas(expr_ref_vector& fmls, expr_ref_vector& qs, svector<symbol>& names);
         void get_raw_rule_formulas(expr_ref_vector& fmls, svector<symbol>& names);
 
         void add_fact(app * head);
@@ -463,7 +463,7 @@ namespace datalog {
 
         void display(std::ostream & out) const;
 
-        void display_smt2(unsigned num_queries, expr* const* queries, std::ostream& out);
+        void display_smt2(unsigned num_queries, expr* const* qs, std::ostream& out);
 
         void display_profile(std::ostream& out) const;
 
diff --git a/src/muz/ddnf/ddnf.cpp b/src/muz/ddnf/ddnf.cpp
index dc45a9879..9a47976b2 100644
--- a/src/muz/ddnf/ddnf.cpp
+++ b/src/muz/ddnf/ddnf.cpp
@@ -25,7 +25,6 @@ Revision History:
 #include "dl_context.h"
 #include "scoped_proof.h"
 #include "bv_decl_plugin.h"
-//#include "dl_decl_plugin.h"
 
 namespace datalog {
 
@@ -485,7 +484,6 @@ namespace datalog {
         ast_manager&           m;
         rule_manager&          rm;
         bv_util                bv;
-        // dl_decl_util           dl;
         volatile bool          m_cancel;
         ptr_vector<expr>       m_todo;
         ast_mark               m_visited1, m_visited2;
@@ -502,7 +500,6 @@ namespace datalog {
             m(ctx.get_manager()),
             rm(ctx.get_rule_manager()),
             bv(m),
-            // dl(m),
             m_cancel(false),
             m_trail(m),
             m_inner_ctx(m, m_ctx.get_register_engine(), m_ctx.get_fparams())
@@ -688,25 +685,7 @@ namespace datalog {
 
         void dump_rules(rule_set& rules) {
             init_ctx(rules);
-            func_decl* q = rules.get_output_predicate();
-            rule_vector const& qs = rules.get_predicate_rules(q);
-            SASSERT(qs.size() == 1);
-            app* qa = qs[0]->get_head();
-            expr_ref query(m);
-            ptr_vector<sort> sorts;
-            vector<symbol> names;
-            get_free_vars(qa, sorts);
-            // TBD: get the real names from the original query.
-            for (unsigned i = 0; i < sorts.size(); ++i) {
-                if (!sorts[i]) sorts[i] = m.mk_bool_sort();
-                std::ostringstream strm;
-                strm << "q" << i;
-                names.push_back(symbol(strm.str().c_str()));                
-            }
-            sorts.reverse();
-            query = m.mk_quantifier(false, sorts.size(), sorts.c_ptr(), names.c_ptr(), qa);
-            expr* qe = query;
-            m_inner_ctx.display_smt2(1, &qe, std::cout);
+            m_inner_ctx.display_smt2(0, 0, std::cout);
         }
 
         lbool execute_rules(rule_set& rules) {
@@ -806,12 +785,6 @@ namespace datalog {
                     ++nb;                    
                 }
                 return bv.mk_sort(nb);
-#if 0
-                std::ostringstream strm;
-                strm << "S" << num_elems;
-                symbol name(strm.str().c_str());
-                return dl.mk_sort(name, num_elems);
-#endif
             }
             UNREACHABLE();
             return 0;