diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index 13008d059..81826daec 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -238,6 +238,7 @@ namespace datalog {
         m_pinned(m),
         m_vars(m),
         m_rule_set(*this),
+        m_rule_fmls(m),
         m_background(m),
         m_closed(false),
         m_saturation_was_run(false),
@@ -521,10 +522,19 @@ namespace datalog {
     }
 
     void context::add_rule(expr* rl, symbol const& name) {
+        m_rule_fmls.push_back(rl);
+        m_rule_names.push_back(name);
+    }
+
+    void context::flush_add_rules() {
         datalog::rule_manager& rm = get_rule_manager();
         datalog::rule_ref_vector rules(rm);
-        rm.mk_rule(rl, rules, name);
+        for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
+            rm.mk_rule(m_rule_fmls[i].get(), rules, m_rule_names[i]);
+        }
         add_rules(rules);
+        m_rule_fmls.reset();
+        m_rule_names.reset();
     }
 
     //
@@ -1223,6 +1233,7 @@ namespace datalog {
     }
 
     void context::new_query() {
+        flush_add_rules();
         if (m_last_result_relation) {
             m_last_result_relation->deallocate();
             m_last_result_relation = 0;
@@ -1618,6 +1629,10 @@ namespace datalog {
                 names.push_back((*it)->name());
             }
         }
+        for (unsigned i = 0; i < m_rule_fmls.size(); ++i) {
+            rules.push_back(m_rule_fmls[i].get());
+            names.push_back(m_rule_names[i]);
+        }
 
         smt2_pp_environment_dbg env(m);
         pp_params params;
@@ -1674,8 +1689,11 @@ namespace datalog {
             declare_vars(rules, fresh_names, out);
         }
 
+        if (num_axioms > 0 && !use_fixedpoint_extensions) {
+            throw default_exception("Background axioms cannot be used with SMT-LIB2 HORN format");
+        }
+
         for (unsigned i = 0; i < num_axioms; ++i) {
-            SASSERT(use_fixedpoint_extensions);
             out << "(assert ";
             ast_smt2_pp(out, axioms[i], env, params);
             out << ")\n";
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index a6f8fc5e2..ef9e8004b 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -96,6 +96,8 @@ namespace datalog {
         pred2syms          m_argument_var_names;
         decl_set           m_output_preds;
         rule_set           m_rule_set;
+        expr_ref_vector    m_rule_fmls;
+        svector<symbol>    m_rule_names;
         expr_ref_vector    m_background;
 
         scoped_ptr<pdr::dl_interface>   m_pdr;
@@ -454,6 +456,8 @@ namespace datalog {
 
     private:
 
+        void flush_add_rules();
+
         void ensure_pdr();
 
         void ensure_bmc();