diff --git a/src/api/api_datalog.cpp b/src/api/api_datalog.cpp
index 394df7a17..7674e8676 100644
--- a/src/api/api_datalog.cpp
+++ b/src/api/api_datalog.cpp
@@ -26,6 +26,9 @@ Revision History:
 #include"datalog_parser.h"
 #include"cancel_eh.h"
 #include"scoped_timer.h"
+#include"dl_cmds.h"
+#include"cmd_context.h"
+#include"smt2parser.h"
 
 namespace api {
     
@@ -124,55 +127,6 @@ namespace api {
         return str.str();
     } 
 
-    void fixedpoint_context::simplify_rules(
-        unsigned num_rules, expr* const* rules, 
-        unsigned num_outputs,  func_decl* const* outputs, expr_ref_vector& result) {
-        ast_manager& m = m_context.get_manager();
-        
-        datalog::context ctx(m, m_context.get_fparams());
-        for (unsigned i = 0; i < num_rules; ++i) {
-            expr* rule = rules[i], *body, *head;
-            while (true) {
-                if (is_quantifier(rule)) {
-                    rule = to_quantifier(rule)->get_expr();
-                }
-                else if (m.is_implies(rule, body, head)) {
-                    rule = head;
-                }
-                else {
-                    break;
-                }
-            }
-            if (is_app(rule)) {
-                func_decl* r = to_app(rule)->get_decl();
-                if (!ctx.is_predicate(r)) {
-                    ctx.register_predicate(r);
-                    if (num_outputs == 0) {
-                        ctx.set_output_predicate(r);
-                    }
-                }
-            }
-        }
-        for (unsigned i = 0; i < num_outputs; ++i) {
-            ctx.set_output_predicate(outputs[i]);
-        }
-        for (unsigned i = 0; i < num_rules; ++i) {
-            expr* rule = rules[i];
-            ctx.add_rule(rule, symbol::null);
-        }
-        model_converter_ref mc; // not exposed.
-        proof_converter_ref pc; // not exposed.
-        ctx.apply_default_transformation(mc, pc);
-        datalog::rule_set const& new_rules = ctx.get_rules();
-        datalog::rule_set::iterator it = new_rules.begin(), end = new_rules.end();
-        for (; it != end; ++it) {
-            datalog::rule* r = *it;
-            expr_ref fml(m);
-            r->to_formula(fml);
-            result.push_back(fml);
-        }
-    }
-
 };
 
 extern "C" {
@@ -384,6 +338,62 @@ extern "C" {
         Z3_CATCH_RETURN("");
     }
 
+    Z3_ast_vector Z3_fixedpoint_from_stream(
+        Z3_context    c,
+        Z3_fixedpoint d,
+        std::istream& s) {
+        ast_manager& m = mk_c(c)->m();
+        dl_collected_cmds coll(m);
+        cmd_context ctx(&mk_c(c)->fparams(), false, &m);
+        install_dl_collect_cmds(coll, ctx);
+        ctx.set_ignore_check(true);
+        if (!parse_smt2_commands(ctx, s)) {
+            SET_ERROR_CODE(Z3_PARSER_ERROR);
+            return 0;
+        }
+
+        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
+        mk_c(c)->save_object(v);
+        for (unsigned i = 0; i < coll.m_queries.size(); ++i) {
+            v->m_ast_vector.push_back(coll.m_queries[i].get());
+        }
+        for (unsigned i = 0; i < coll.m_rels.size(); ++i) {
+            to_fixedpoint_ref(d)->ctx().register_predicate(coll.m_rels[i].get());
+        }
+        for (unsigned i = 0; i < coll.m_rules.size(); ++i) {
+            to_fixedpoint_ref(d)->add_rule(coll.m_rules[i].get(), coll.m_names[i]);
+        }
+        return of_ast_vector(v);
+    }
+
+    Z3_ast_vector Z3_API Z3_fixedpoint_from_string(
+        Z3_context    c,
+        Z3_fixedpoint d,
+        Z3_string     s) {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_from_string(c, d, s);
+        std::string str(s);
+        std::istringstream is(str);
+        RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is));
+        Z3_CATCH_RETURN(0);        
+    }
+
+    Z3_ast_vector Z3_API Z3_fixedpoint_from_file(
+        Z3_context    c,
+        Z3_fixedpoint d,
+        Z3_string     s) {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_from_file(c, d, s);
+        std::ifstream is(s);
+        if (!is) {
+            SET_ERROR_CODE(Z3_PARSER_ERROR);
+            RETURN_Z3(0);
+        }
+        RETURN_Z3(Z3_fixedpoint_from_stream(c, d, is));
+        Z3_CATCH_RETURN(0);        
+    }
+
+
     Z3_stats Z3_API Z3_fixedpoint_get_statistics(Z3_context c,Z3_fixedpoint d) {
         Z3_TRY;
         LOG_Z3_fixedpoint_get_statistics(c, d);
@@ -419,6 +429,27 @@ extern "C" {
         Z3_CATCH;
     }
 
+
+    Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
+        Z3_context c,
+        Z3_fixedpoint d)
+    {
+        Z3_TRY;
+        LOG_Z3_fixedpoint_get_rules(c, d);
+        ast_manager& m = mk_c(c)->m();
+        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, m);
+        mk_c(c)->save_object(v);
+        datalog::rule_set const& rules = to_fixedpoint_ref(d)->ctx().get_rules();
+        datalog::rule_set::iterator it = rules.begin(), end = rules.end();
+        for (; it != end; ++it) {
+            expr_ref fml(m);
+            (*it)->to_formula(fml);
+            v->m_ast_vector.push_back(fml);
+        }
+        RETURN_Z3(of_ast_vector(v));
+        Z3_CATCH_RETURN(0);
+    }
+    
     void Z3_API Z3_fixedpoint_set_reduce_assign_callback(
         Z3_context c, Z3_fixedpoint d, Z3_fixedpoint_reduce_assign_callback_fptr f) {
         Z3_TRY;
@@ -435,31 +466,6 @@ extern "C" {
         Z3_CATCH;
     }
 
-    Z3_ast_vector Z3_API Z3_fixedpoint_simplify_rules(
-        Z3_context c,
-        Z3_fixedpoint d,
-        unsigned num_rules,
-        Z3_ast _rules[],
-        unsigned num_outputs,
-        Z3_func_decl _outputs[]) {
-        Z3_TRY;
-        LOG_Z3_fixedpoint_simplify_rules(c, d, num_rules, _rules, num_outputs, _outputs);
-        RESET_ERROR_CODE();        
-        expr** rules = (expr**)_rules;
-        func_decl** outputs = (func_decl**)_outputs;
-        ast_manager& m = mk_c(c)->m();        
-        expr_ref_vector result(m);
-        to_fixedpoint_ref(d)->simplify_rules(num_rules, rules, num_outputs, outputs, result);        
-        Z3_ast_vector_ref* v = alloc(Z3_ast_vector_ref, mk_c(c)->m());
-        mk_c(c)->save_object(v);
-        for (unsigned i = 0; i < result.size(); ++i) {
-            v->m_ast_vector.push_back(result[i].get());
-        }
-        RETURN_Z3(of_ast_vector(v));
-        Z3_CATCH_RETURN(0)
-    }
-
-
     void Z3_API Z3_fixedpoint_init(Z3_context c,Z3_fixedpoint d, void* state) {
         Z3_TRY;
         // not logged
diff --git a/src/api/api_datalog.h b/src/api/api_datalog.h
index 1d6bb995a..97bedfc9b 100644
--- a/src/api/api_datalog.h
+++ b/src/api/api_datalog.h
@@ -62,9 +62,6 @@ namespace api {
         void collect_param_descrs(param_descrs & p) { m_context.collect_params(p); }
         void updt_params(params_ref const& p) { m_context.updt_params(p); }
 
-        void simplify_rules(
-            unsigned num_rules, expr* const* rules, 
-            unsigned num_outputs,  func_decl* const* outputs, expr_ref_vector& result);
     };
 };
 
diff --git a/src/api/dotnet/Fixedpoint.cs b/src/api/dotnet/Fixedpoint.cs
index 3e04e6169..c8a677196 100644
--- a/src/api/dotnet/Fixedpoint.cs
+++ b/src/api/dotnet/Fixedpoint.cs
@@ -261,6 +261,23 @@ namespace Microsoft.Z3
                              AST.ArrayLength(queries), AST.ArrayToNative(queries));
         }
 
+        /// <summary>
+        /// Retrieve set of rules added to fixedpoint context.
+        /// </summary>                
+        public BoolExpr[] Rules {
+            get
+            {
+                Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
+
+                ASTVector v = new ASTVector(Context, Native.Z3_fixedpoint_get_rules(Context.nCtx, NativeObject));
+                uint n = v.Size;
+                BoolExpr[] res = new BoolExpr[n];
+                for (uint i = 0; i < n; i++)
+                    res[i] = new BoolExpr(Context, v[i].NativeObject);
+                return res;
+            }
+        }
+
 
         #region Internal
         internal Fixedpoint(Context ctx, IntPtr obj)
diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index f3de4258a..2c4a51826 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -6102,7 +6102,6 @@ class Fixedpoint(Z3PPObject):
         """Add property to predicate for the level'th unfolding. -1 is treated as infinity (infinity)"""
         Z3_fixedpoint_add_cover(self.ctx.ref(), self.fixedpoint, level, predicate.ast, property.ast)
 
-
     def register_relation(self, *relations):
 	"""Register relation as recursive"""
 	relations = _get_args(relations)
@@ -6119,16 +6118,35 @@ class Fixedpoint(Z3PPObject):
 	    args[i] = representations[i]
 	Z3_fixedpoint_set_predicate_representation(self.ctx.ref(), self.fixedpoint, f.ast, sz, args)
 
+    def parse_string(self, s):
+	"""Parse rules and queries from a string"""
+	return AstVector(Z3_fixedpoint_from_string(self.ctx.ref(), self.fixedpoint, s), self.ctx)
+	
+    def parse_file(self, f):
+	"""Parse rules and queries from a file"""
+	return AstVector(Z3_fixedpoint_from_file(self.ctx.ref(), self.fixedpoint, f), self.ctx)
+
+    def get_rules(self):
+	"""retrieve rules that have been added to fixedpoint context"""
+	return AstVector(Z3_fixedpoint_get_rules(self.ctx.ref(), self.fixedpoint), self.ctx)
+    
     def __repr__(self):
         """Return a formatted string with all added rules and constraints."""
 	return self.sexpr()
 
     def sexpr(self):
-        """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.
-        
+        """Return a formatted string (in Lisp-like format) with all added constraints. We say the string is in s-expression format.        
         """
-        return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())    
+        return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, 0, (Ast * 0)())
 
+    def to_string(self, queries):
+	"""Return a formatted string (in Lisp-like format) with all added constraints.
+           We say the string is in s-expression format.
+	   Include also queries.
+        """
+	args, len = _to_ast_array(queries)
+        return Z3_fixedpoint_to_string(self.ctx.ref(), self.fixedpoint, len, args)
+    
     def statistics(self):
         """Return statistics for the last `query()`.
 	"""
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 8d00fb044..4a28807f1 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -5688,19 +5688,13 @@ END_MLAPI_EXCLUDE
         __in_ecount(num_relations) Z3_symbol const relation_kinds[]);
                 
     /**
-        \brief Simplify rules into a set of new rules that are returned.
-        The simplification routines apply inlining, quantifier elimination, and other
-        algebraic simplifications.
+       \brief Retrieve set of rules from fixedpoint context.
 
-        def_API('Z3_fixedpoint_simplify_rules', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(UINT), _in_array(2,AST), _in(UINT), _in_array(4,FUNC_DECL)))
-    */
-    Z3_ast_vector Z3_API Z3_fixedpoint_simplify_rules(
+       def_API('Z3_fixedpoint_get_rules', AST_VECTOR, (_in(CONTEXT),_in(FIXEDPOINT)))
+     */
+    Z3_ast_vector Z3_API Z3_fixedpoint_get_rules(
         __in Z3_context c,
-        __in Z3_fixedpoint f,
-        __in unsigned num_rules,
-        __in_ecount(num_rules) Z3_ast rules[],
-        __in unsigned num_outputs,
-        __in_ecount(num_outputs) Z3_func_decl outputs[]);
+        __in Z3_fixedpoint f);
 
     /**
        \brief Set parameters on fixedpoint context.       
@@ -5738,6 +5732,38 @@ END_MLAPI_EXCLUDE
         __in unsigned num_queries,
         __in_ecount(num_queries) Z3_ast queries[]);
 
+    /**
+       \brief Parse an SMT-LIB2 string with fixedpoint rules. 
+       Add the rules to the current fixedpoint context. 
+       Return the set of queries in the file.
+
+       \param c - context.
+       \param f - fixedpoint context.
+       \param s - string containing SMT2 specification.       
+
+       def_API('Z3_fixedpoint_from_string', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
+    */
+    Z3_ast_vector Z3_API Z3_fixedpoint_from_string(
+        __in Z3_context c, 
+        __in Z3_fixedpoint f,
+        __in Z3_string s);
+
+    /**
+       \brief Parse an SMT-LIB2 file with fixedpoint rules. 
+       Add the rules to the current fixedpoint context. 
+       Return the set of queries in the file.
+
+       \param c - context.
+       \param f - fixedpoint context.
+       \param s - string containing SMT2 specification.       
+
+       def_API('Z3_fixedpoint_from_file', AST_VECTOR, (_in(CONTEXT), _in(FIXEDPOINT), _in(STRING)))
+    */
+    Z3_ast_vector Z3_API Z3_fixedpoint_from_file(
+        __in Z3_context c, 
+        __in Z3_fixedpoint f,
+        __in Z3_string s);
+
     /**
        \brief Create a backtracking point.
        
diff --git a/src/ast/ast_smt_pp.cpp b/src/ast/ast_smt_pp.cpp
index aa3a9c76d..944eb1e26 100644
--- a/src/ast/ast_smt_pp.cpp
+++ b/src/ast/ast_smt_pp.cpp
@@ -317,8 +317,8 @@ class smt_printer {
     }
 
     void visit_sort(sort* s, bool bool2int = false) {
-        symbol sym; 
-        if (bool2int && is_bool(s)) {
+        symbol sym;  
+        if (bool2int && is_bool(s) && !m_is_smt2) {
             sym = symbol("Int");
         } else if (s->is_sort_of(m_bv_fid, BV_SORT)) {
             sym = symbol("BitVec");
diff --git a/src/ast/proof_checker/proof_checker.cpp b/src/ast/proof_checker/proof_checker.cpp
index 6a9df1ef4..8a064a315 100644
--- a/src/ast/proof_checker/proof_checker.cpp
+++ b/src/ast/proof_checker/proof_checker.cpp
@@ -6,8 +6,9 @@
 #include "arith_decl_plugin.h"
 #include "front_end_params.h"
 #include "th_rewriter.h"
+#include "var_subst.h"
 
-#define IS_EQUIV(_e_) (m_manager.is_eq(_e_) || m_manager.is_iff(_e_))
+#define IS_EQUIV(_e_) (m.is_eq(_e_) || m.is_iff(_e_))
 
 #define SAME_OP(_d1_, _d2_) ((_d1_ == _d2_) || (IS_EQUIV(_d1_) && IS_EQUIV(_d2_)))
 
@@ -79,7 +80,7 @@ void proof_checker::hyp_decl_plugin::get_sort_names(svector<builtin_name> & sort
     }
 }
 
-proof_checker::proof_checker(ast_manager& m) : m_manager(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m), 
+proof_checker::proof_checker(ast_manager& m) : m(m), m_todo(m), m_marked(), m_pinned(m), m_nil(m), 
                                                m_dump_lemmas(false), m_logic("AUFLIA"), m_proof_lemma_id(0) {
     symbol fam_name("proof_hypothesis");
     if (!m.has_plugin(fam_name)) {
@@ -87,11 +88,11 @@ proof_checker::proof_checker(ast_manager& m) : m_manager(m), m_todo(m), m_marked
     }
     m_hyp_fid = m.get_family_id(fam_name);
     // m_spc_fid = m.get_family_id("spc");
-    m_nil = m_manager.mk_const(m_hyp_fid, OP_NIL);
+    m_nil = m.mk_const(m_hyp_fid, OP_NIL);
 }
 
 bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
-    proof_ref curr(m_manager);
+    proof_ref curr(m);
     m_todo.push_back(p);
     
     bool result = true;
@@ -100,7 +101,7 @@ bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
         m_todo.pop_back();
         result = check1(curr.get(), side_conditions);
         if (!result) {
-            IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m_manager, curr.get()););            
+            IF_VERBOSE(0, ast_ll_pp(verbose_stream() << "Proof check failed\n", m, curr.get()););            
             UNREACHABLE();
         }        
     }
@@ -114,7 +115,7 @@ bool proof_checker::check(proof* p, expr_ref_vector& side_conditions) {
 }
 
 bool proof_checker::check1(proof* p, expr_ref_vector& side_conditions) {
-    if (p->get_family_id() == m_manager.get_basic_family_id()) {
+    if (p->get_family_id() == m.get_basic_family_id()) {
         return check1_basic(p, side_conditions);
     }
 #if 0
@@ -129,11 +130,11 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
 #if 0
     decl_kind k = p->get_decl_kind();
     bool is_univ = false;
-    expr_ref fact(m_manager), fml(m_manager);
-    expr_ref body(m_manager), fml1(m_manager), fml2(m_manager);
-    sort_ref_vector sorts(m_manager);
-    proof_ref p1(m_manager), p2(m_manager);
-    proof_ref_vector proofs(m_manager);
+    expr_ref fact(m), fml(m);
+    expr_ref body(m), fml1(m), fml2(m);
+    sort_ref_vector sorts(m);
+    proof_ref p1(m), p2(m);
+    proof_ref_vector proofs(m);
 
     if (match_proof(p, proofs)) {
         for (unsigned i = 0; i < proofs.size(); ++i) {
@@ -159,15 +160,15 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
     case PR_FACTORING:
     case PR_SPC_DER: {
         if (match_fact(p, fact)) {
-            expr_ref_vector rewrite_eq(m_manager);
+            expr_ref_vector rewrite_eq(m);
             rewrite_eq.push_back(fact.get());
             for (unsigned i = 0; i < proofs.size(); ++i) {
                 if (match_fact(proofs[i].get(), fml)) {
-                    rewrite_eq.push_back(m_manager.mk_not(fml.get()));
+                    rewrite_eq.push_back(m.mk_not(fml.get()));
                 }
             }
-            expr_ref rewrite_cond(m_manager);
-            rewrite_cond = m_manager.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
+            expr_ref rewrite_cond(m);
+            rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
             side_conditions.push_back(rewrite_cond.get());
             return true;
         }
@@ -184,18 +185,18 @@ bool proof_checker::check1_spc(proof* p, expr_ref_vector& side_conditions) {
 
 bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
     decl_kind k = p->get_decl_kind();
-    expr_ref fml0(m_manager), fml1(m_manager), fml2(m_manager), fml(m_manager);
-    expr_ref t1(m_manager), t2(m_manager);
-    expr_ref s1(m_manager), s2(m_manager);
-    expr_ref u1(m_manager), u2(m_manager);
-    expr_ref fact(m_manager), body1(m_manager), body2(m_manager);
-    expr_ref l1(m_manager), l2(m_manager), r1(m_manager), r2(m_manager);
-    func_decl_ref d1(m_manager), d2(m_manager), d3(m_manager);
-    proof_ref p0(m_manager), p1(m_manager), p2(m_manager);
-    proof_ref_vector proofs(m_manager);
-    func_decl_ref f1(m_manager), f2(m_manager);
-    expr_ref_vector terms1(m_manager), terms2(m_manager), terms(m_manager);
-    sort_ref_vector decls1(m_manager), decls2(m_manager);
+    expr_ref fml0(m), fml1(m), fml2(m), fml(m);
+    expr_ref t1(m), t2(m);
+    expr_ref s1(m), s2(m);
+    expr_ref u1(m), u2(m);
+    expr_ref fact(m), body1(m), body2(m);
+    expr_ref l1(m), l2(m), r1(m), r2(m);
+    func_decl_ref d1(m), d2(m), d3(m);
+    proof_ref p0(m), p1(m), p2(m);
+    proof_ref_vector proofs(m);
+    func_decl_ref f1(m), f2(m);
+    expr_ref_vector terms1(m), terms2(m), terms(m);
+    sort_ref_vector decls1(m), decls2(m);
     
     if (match_proof(p, proofs)) {
         for (unsigned i = 0; i < proofs.size(); ++i) {
@@ -296,7 +297,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         return false;
     }        
     case PR_MONOTONICITY: {
-        TRACE("proof_checker", tout << mk_bounded_pp(p, m_manager, 3) << "\n";);
+        TRACE("proof_checker", tout << mk_bounded_pp(p, m, 3) << "\n";);
         if (match_fact(p, fact) &&
             match_binary(fact.get(), d1, t1, t2) &&
             match_app(t1.get(), f1, terms1) &&
@@ -334,7 +335,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             match_fact(p1.get(), fml) &&
             (match_iff(fact.get(), t1, t2) || match_oeq(fact.get(), t1, t2)) &&
             (match_iff(fml.get(), s1, s2) || match_oeq(fml.get(), s1, s2)) &&
-            m_manager.is_oeq(fact.get()) == m_manager.is_oeq(fml.get()) &&
+            m.is_oeq(fact.get()) == m.is_oeq(fml.get()) &&
             is_quantifier(t1.get()) &&
             is_quantifier(t2.get()) &&
             to_quantifier(t1.get())->get_expr() == s1.get() &&
@@ -366,7 +367,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         return false;
     }
     case PR_AND_ELIM: {
-        expr_ref_vector terms(m_manager);
+        expr_ref_vector terms(m);
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
             match_fact(p1.get(), fml) &&
@@ -381,7 +382,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         return false;
     }
     case PR_NOT_OR_ELIM: {
-        expr_ref_vector terms(m_manager);
+        expr_ref_vector terms(m);
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
             match_fact(p1.get(), fml) &&
@@ -403,25 +404,25 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             side_conditions.push_back(fact.get());
             return true;
         }
-        IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m_manager);); 
+        IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m);); 
         return false;
     }
     case PR_REWRITE_STAR: {
         if (match_fact(p, fact) &&
             match_equiv(fact.get(), t1, t2)) {
-            expr_ref_vector rewrite_eq(m_manager);
+            expr_ref_vector rewrite_eq(m);
             rewrite_eq.push_back(fact.get());
             for (unsigned i = 0; i < proofs.size(); ++i) {
                 if (match_fact(proofs[i].get(), fml)) {
-                    rewrite_eq.push_back(m_manager.mk_not(fml.get()));
+                    rewrite_eq.push_back(m.mk_not(fml.get()));
                 }
             }
-            expr_ref rewrite_cond(m_manager);
-            rewrite_cond = m_manager.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
+            expr_ref rewrite_cond(m);
+            rewrite_cond = m.mk_or(rewrite_eq.size(), rewrite_eq.c_ptr());
             side_conditions.push_back(rewrite_cond.get());
             return true;
         }
-        IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m_manager);); 
+        IF_VERBOSE(0, verbose_stream() << "Expected proof of equality:\n" << mk_bounded_pp(p, m);); 
         return false;        
     }
     case PR_PULL_QUANT: {
@@ -432,7 +433,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             // TBD: check the enchilada.
             return true;
         }
-        IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m_manager);); 
+        IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence with a quantifier:\n" << mk_bounded_pp(p, m);); 
         return false;
     }
     case PR_PULL_QUANT_STAR: {
@@ -442,7 +443,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             // TBD: check the enchilada.
             return true;
         }
-        IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m_manager);); 
+        IF_VERBOSE(0, verbose_stream() << "Expected proof of equivalence:\n" << mk_bounded_pp(p, m);); 
         return false;
     }
     case PR_PUSH_QUANT: {
@@ -509,9 +510,9 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         if (match_proof(p, p1) &&
             match_fact(p, fact) &&
             match_fact(p1.get(), fml) &&
-            m_manager.is_false(fml.get())) {
-            expr_ref_vector hypotheses(m_manager);
-            expr_ref_vector ors(m_manager);
+            m.is_false(fml.get())) {
+            expr_ref_vector hypotheses(m);
+            expr_ref_vector ors(m);
             get_hypotheses(p1.get(), hypotheses);
             if (hypotheses.size() == 1 && match_negated(hypotheses.get(0), fact)) {
                 // Suppose fact is (or a b c) and hypothesis is (not (or a b c))
@@ -531,18 +532,18 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
                           tout << "i: " << i << "\n";
                           tout << "ORs:\n";
                           for (unsigned i = 0; i < ors.size(); i++) {
-                              tout << mk_pp(ors.get(i), m_manager) << "\n";
+                              tout << mk_pp(ors.get(i), m) << "\n";
                           }
                           tout << "HYPOTHESIS:\n";
                           for (unsigned i = 0; i < hypotheses.size(); i++) {
-                              tout << mk_pp(hypotheses.get(i), m_manager) << "\n";
+                              tout << mk_pp(hypotheses.get(i), m) << "\n";
                           });
                     UNREACHABLE();
                     return false;
                 }                    
                 TRACE("proof_checker", tout << "Matched:\n";
-                      ast_ll_pp(tout, m_manager, hypotheses[i].get());
-                      ast_ll_pp(tout, m_manager, ors[j-1].get()););
+                      ast_ll_pp(tout, m, hypotheses[i].get());
+                      ast_ll_pp(tout, m, ors[j-1].get()););
             }
             return true;
         }
@@ -555,7 +556,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             match_fact(proofs[0].get(), fml1) &&
             match_fact(proofs[1].get(), fml2) &&
             match_negated(fml1.get(), fml2.get()) &&
-            m_manager.is_false(fact.get())) {
+            m.is_false(fact.get())) {
             return true;
         }
         if (match_fact(p, fact) &&
@@ -580,15 +581,15 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
                     TRACE("pr_unit_bug", 
                           tout << "Parents:\n";
                           for (unsigned i = 0; i < proofs.size(); i++) {
-                              expr_ref p(m_manager);
+                              expr_ref p(m);
                               match_fact(proofs.get(i), p);
-                              tout << mk_pp(p, m_manager) << "\n";
+                              tout << mk_pp(p, m) << "\n";
                           }
                           tout << "Fact:\n";
-                          tout << mk_pp(fact, m_manager) << "\n";
+                          tout << mk_pp(fact, m) << "\n";
                           tout << "Clause:\n";
-                          tout << mk_pp(fml, m_manager) << "\n";
-                          tout << "Could not find premise " << mk_pp(fml2, m_manager) << "\n";
+                          tout << mk_pp(fml, m) << "\n";
+                          tout << "Could not find premise " << mk_pp(fml2, m) << "\n";
                           );
 
                     UNREACHABLE();
@@ -597,7 +598,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             }
             switch(terms1.size()) {
             case 0: 
-                return m_manager.is_false(fact.get());
+                return m.is_false(fact.get());
             case 1: 
                 return fact.get() == terms1[0].get();
             default: {
@@ -609,15 +610,15 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
                             found = term1 == terms2[j].get();
                         }
                         if (!found) {
-                            IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m_manager) << "\n";);
+                            IF_VERBOSE(0, verbose_stream() << "Premise not found:" << mk_pp(term1, m) << "\n";);
                             return false;
                         }
                     }
                     return true;
                 }
                 IF_VERBOSE(0, verbose_stream() << "Conclusion is not a disjunction:\n";
-                           verbose_stream() << mk_pp(fml.get(), m_manager) << "\n";
-                           verbose_stream() << mk_pp(fact.get(), m_manager) << "\n";);
+                           verbose_stream() << mk_pp(fml.get(), m) << "\n";
+                           verbose_stream() << mk_pp(fact.get(), m) << "\n";);
 
                 return false;
             }
@@ -634,7 +635,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             match_fact(p1.get(), fml1) &&
             match_iff(fact.get(), l1, r1) &&
             fml1.get() == l1.get() &&
-            r1.get() == m_manager.mk_true()) {
+            r1.get() == m.mk_true()) {
             return true;
         }
         UNREACHABLE();
@@ -648,7 +649,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
             match_iff(fact.get(), l1, r1) &&
             match_not(fml1.get(), t1) &&
             t1.get() == l1.get() &&
-            r1.get() == m_manager.mk_false()) {
+            r1.get() == m.mk_false()) {
             return true;
         }
         UNREACHABLE();
@@ -674,7 +675,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // axiom(?fml)
         if (match_fact(p, fact) &&
             match_proof(p) &&
-            m_manager.is_bool(fact.get())) {
+            m.is_bool(fact.get())) {
             return true;
         }
         UNREACHABLE();
@@ -689,7 +690,7 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // 
         if (match_fact(p, fact) &&
             match_proof(p) &&
-            m_manager.is_bool(fact.get())) {
+            m.is_bool(fact.get())) {
             return true;
         }
         UNREACHABLE();
@@ -790,16 +791,138 @@ bool proof_checker::check1_basic(proof* p, expr_ref_vector& side_conditions) {
         // TODO
         return true;
     }
+    case PR_HYPER_RESOLVE: {
+        proof_ref_vector premises(m);
+        expr_ref_vector fmls(m);
+        expr_ref conclusion(m), premise(m), premise0(m), premise1(m);
+        svector<std::pair<unsigned, unsigned> > positions;
+        vector<expr_ref_vector> substs;
+        VERIFY(m.is_hyper_resolve(p, premises, conclusion, positions, substs));
+        var_subst vs(m, false);
+        for (unsigned i = 0; i < premises.size(); ++i) {
+            expr_ref_vector const& sub = substs[i];
+            premise = m.get_fact(premises[i].get());
+            if (!sub.empty()) {
+                if (is_forall(premise)) {
+                    // SASSERT(to_quantifier(premise)->get_num_decls() == sub.size());
+                    premise = to_quantifier(premise)->get_expr();
+                }
+                vs(premise, sub.size(), sub.c_ptr(), premise);
+            }
+            fmls.push_back(premise.get());
+            TRACE("proof_checker",                   
+                  tout << mk_pp(premise.get(), m) << "\n";
+                  for (unsigned j = 0; j < sub.size(); ++j) {
+                      tout << mk_pp(sub[j], m) << " ";
+                  }
+                  tout << "\n";);
+        }
+        premise0 = fmls[0].get();
+        for (unsigned i = 1; i < fmls.size(); ++i) {
+            expr_ref lit1(m), lit2(m);
+            expr* lit3 = 0;
+            std::pair<unsigned, unsigned> pos = positions[i-1];
+            premise1 = fmls[i].get();
+            set_false(premise0, pos.first, lit1);
+            set_false(premise1, pos.second, lit2);
+            if (m.is_not(lit1, lit3) && lit3 == lit2) {
+                // ok
+            }
+            else if (m.is_not(lit2, lit3) && lit3 == lit1) {
+                // ok
+            }
+            else {
+                IF_VERBOSE(0, verbose_stream() << "Could not establish complementarity for:\n" << 
+                           mk_pp(lit1, m) << "\n" << mk_pp(lit2, m) << "\n";);
+            }
+            fmls[i] = premise1;
+        }
+        fmls[0] = premise0;
+        premise0 = m.mk_or(fmls.size(), fmls.c_ptr());
+        if (is_forall(conclusion)) {
+            quantifier* q = to_quantifier(conclusion);
+            premise0 = m.mk_iff(premise0, q->get_expr());
+            premise0 = m.mk_forall(q->get_num_decls(), q->get_decl_sorts(), q->get_decl_names(), premise0);
+        }
+        else {
+            premise0 = m.mk_iff(premise0, conclusion);
+        }
+        side_conditions.push_back(premise0);        
+        return true;
+    }
     default:
         UNREACHABLE();
         return false;
     }
 }
 
+/**
+   \brief Premises of the rules are of the form
+      (or l0 l1 l2 .. ln)
+   or
+      (=> (and ln+1 ln+2 .. ln+m) l0)
+   or in the most general (ground) form:
+      (=> (and ln+1 ln+2 .. ln+m) (or l0 l1 .. ln-1))
+   In other words we use the following (Prolog style) convention for Horn 
+   implications:
+   The head of a Horn implication is position 0,
+   the first conjunct in the body of an implication is position 1
+   the second conjunct in the body of an implication is position 2
+
+   Set the position provided in the argument to 'false'.
+*/
+void proof_checker::set_false(expr_ref& e, unsigned position, expr_ref& lit) {
+    app* a = to_app(e);
+    expr* head, *body;
+    expr_ref_vector args(m);
+    if (m.is_or(e)) {        
+        SASSERT(position < a->get_num_args());
+        args.append(a->get_num_args(), a->get_args());
+        lit = args[position].get();
+        args[position] = m.mk_false();
+        e = m.mk_or(args.size(), args.c_ptr());
+    }
+    else if (m.is_implies(e, body, head)) {
+        expr* const* heads = &head;
+        unsigned num_heads = 1;
+        if (m.is_or(head)) {
+            num_heads = to_app(head)->get_num_args();
+            heads = to_app(head)->get_args();            
+        }
+        expr*const* bodies = &body;
+        unsigned num_bodies = 1;
+        if (m.is_and(body)) {
+            num_bodies = to_app(body)->get_num_args();
+            bodies = to_app(body)->get_args();            
+        }
+        if (position < num_heads) {
+            args.append(num_heads, heads);
+            lit = args[position].get();
+            args[position] = m.mk_false();
+            e = m.mk_implies(body, m.mk_or(args.size(), args.c_ptr()));
+        }
+        else {
+            position -= num_heads;
+            args.append(num_bodies, bodies);
+            lit = m.mk_not(args[position].get());
+            args[position] = m.mk_true();
+            e = m.mk_implies(m.mk_and(args.size(), args.c_ptr()), head);            
+        }
+    }
+    else if (position == 0) {
+        lit = e;
+        e = m.mk_false();
+    }
+    else {
+        IF_VERBOSE(0, verbose_stream() << position << "\n" << mk_pp(e, m) << "\n";);
+        UNREACHABLE();
+    }
+}
+
 bool proof_checker::match_fact(proof* p, expr_ref& fact) {
-    if (m_manager.is_proof(p) &&
-        m_manager.has_fact(p)) {
-        fact = m_manager.get_fact(p);
+    if (m.is_proof(p) &&
+        m.has_fact(p)) {
+        fact = m.get_fact(p);
         return true;
     }
     return false;
@@ -814,33 +937,33 @@ void proof_checker::add_premise(proof* p) {
 
 bool proof_checker::match_proof(proof* p) {
     return 
-        m_manager.is_proof(p) &&
-        m_manager.get_num_parents(p) == 0;
+        m.is_proof(p) &&
+        m.get_num_parents(p) == 0;
 }
 
 bool proof_checker::match_proof(proof* p, proof_ref& p0) {
-    if (m_manager.is_proof(p) &&
-        m_manager.get_num_parents(p) == 1) {
-        p0 = m_manager.get_parent(p, 0);
+    if (m.is_proof(p) &&
+        m.get_num_parents(p) == 1) {
+        p0 = m.get_parent(p, 0);
         return true;
     }
     return false;
 }
  
 bool proof_checker::match_proof(proof* p, proof_ref& p0, proof_ref& p1) {
-    if (m_manager.is_proof(p) &&
-        m_manager.get_num_parents(p) == 2) {
-        p0 = m_manager.get_parent(p, 0);
-        p1 = m_manager.get_parent(p, 1);
+    if (m.is_proof(p) &&
+        m.get_num_parents(p) == 2) {
+        p0 = m.get_parent(p, 0);
+        p1 = m.get_parent(p, 1);
         return true;
     }
     return false;
 }
 
 bool proof_checker::match_proof(proof* p, proof_ref_vector& parents) {
-    if (m_manager.is_proof(p)) {
-        for (unsigned i = 0; i < m_manager.get_num_parents(p); ++i) {
-            parents.push_back(m_manager.get_parent(p, i));
+    if (m.is_proof(p)) {
+        for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+            parents.push_back(m.get_parent(p, i));
         }
         return true;
     }
@@ -886,7 +1009,7 @@ bool proof_checker::match_quantifier(expr* e, bool& is_univ, sort_ref_vector& so
 
 bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
     if (e->get_kind() == AST_APP &&
-        to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
+        to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
         to_app(e)->get_num_args() == 2) {
         t1 = to_app(e)->get_arg(0);
@@ -898,7 +1021,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t1, expr_ref& t2) {
 
 bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
     if (e->get_kind() == AST_APP &&
-        to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
+        to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k) {
         for (unsigned i = 0; i < to_app(e)->get_num_args(); ++i) {
             terms.push_back(to_app(e)->get_arg(i));
@@ -911,7 +1034,7 @@ bool proof_checker::match_op(expr* e, decl_kind k, expr_ref_vector& terms) {
 
 bool proof_checker::match_op(expr* e, decl_kind k, expr_ref& t) {
     if (e->get_kind() == AST_APP &&
-        to_app(e)->get_family_id() == m_manager.get_basic_family_id() &&
+        to_app(e)->get_family_id() == m.get_basic_family_id() &&
         to_app(e)->get_decl_kind() == k &&
         to_app(e)->get_num_args() == 1) {
         t = to_app(e)->get_arg(0);
@@ -953,7 +1076,7 @@ bool proof_checker::match_oeq(expr* e, expr_ref& t1, expr_ref& t2) {
 }
 
 bool proof_checker::match_negated(expr* a, expr* b) {
-    expr_ref t(m_manager);
+    expr_ref t(m);
     return 
         (match_not(a, t) && t.get() == b) ||
         (match_not(b, t) && t.get() == a);
@@ -961,7 +1084,7 @@ bool proof_checker::match_negated(expr* a, expr* b) {
 
 void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
     ptr_buffer<expr> buffer;
-    if (m_manager.is_or(e)) {
+    if (m.is_or(e)) {
         app* a = to_app(e);
         ors.append(a->get_num_args(), a->get_args());
     }
@@ -974,12 +1097,12 @@ void proof_checker::get_ors(expr* e, expr_ref_vector& ors) {
 void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
     ptr_vector<proof> stack;
     expr* h = 0;
-    expr_ref hyp(m_manager);
+    expr_ref hyp(m);
 
     stack.push_back(p);
     while (!stack.empty()) {
         p = stack.back();
-        SASSERT(m_manager.is_proof(p));
+        SASSERT(m.is_proof(p));
         if (m_hypotheses.contains(p)) {
             stack.pop_back();            
             continue;
@@ -992,15 +1115,15 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
             continue;
         }
         // in this system all hypotheses get bound by lemmas.
-        if (m_manager.is_lemma(p)) {
+        if (m.is_lemma(p)) {
             m_hypotheses.insert(p, mk_nil());
             stack.pop_back();
             continue;
         }
         bool all_found = true;
         ptr_vector<expr> hyps;
-        for (unsigned i = 0; i < m_manager.get_num_parents(p); ++i) {
-            proof* p_i = m_manager.get_parent(p, i);
+        for (unsigned i = 0; i < m.get_num_parents(p); ++i) {
+            proof* p_i = m.get_parent(p, i);
             if (m_hypotheses.find(p_i, h)) {
                 hyps.push_back(h);
             }
@@ -1028,7 +1151,7 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
     ptr_buffer<expr> todo;
     expr_mark mark;
     todo.push_back(h);
-    expr_ref a(m_manager), b(m_manager);
+    expr_ref a(m), b(m);
     
     while (!todo.empty()) {
         h = todo.back();
@@ -1051,10 +1174,10 @@ void proof_checker::get_hypotheses(proof* p, expr_ref_vector& ante) {
     }
     TRACE("proof_checker",
           {
-              ast_ll_pp(tout << "Getting hypotheses from: ", m_manager, p);
+              ast_ll_pp(tout << "Getting hypotheses from: ", m, p);
               tout << "Found hypotheses:\n";
               for (unsigned i = 0; i < ante.size(); ++i) {
-                  ast_ll_pp(tout, m_manager, ante[i].get()); 
+                  ast_ll_pp(tout, m, ante[i].get()); 
               }
           });
 
@@ -1090,11 +1213,11 @@ bool proof_checker::match_atom(expr* e, expr_ref& a) const {
 }
 
 expr* proof_checker::mk_atom(expr* e) {
-    return m_manager.mk_app(m_hyp_fid, OP_ATOM, e);
+    return m.mk_app(m_hyp_fid, OP_ATOM, e);
 }
 
 expr* proof_checker::mk_cons(expr* a, expr* b) {
-    return m_manager.mk_app(m_hyp_fid, OP_CONS, a, b);
+    return m.mk_app(m_hyp_fid, OP_CONS, a, b);
 }
 
 expr* proof_checker::mk_nil() {
@@ -1103,7 +1226,7 @@ expr* proof_checker::mk_nil() {
 
 bool proof_checker::is_hypothesis(proof* p) const {
     return 
-        m_manager.is_proof(p) &&
+        m.is_proof(p) &&
         p->get_decl_kind() == PR_HYPOTHESIS;
 }
 
@@ -1130,14 +1253,14 @@ expr* proof_checker::mk_hyp(unsigned num_hyps, expr * const * hyps) {
 void proof_checker::dump_proof(proof * pr) {
     if (!m_dump_lemmas)
         return;
-    SASSERT(m_manager.has_fact(pr));
-    expr * consequent = m_manager.get_fact(pr);
-    unsigned num      = m_manager.get_num_parents(pr);
+    SASSERT(m.has_fact(pr));
+    expr * consequent = m.get_fact(pr);
+    unsigned num      = m.get_num_parents(pr);
     ptr_buffer<expr> antecedents;
     for (unsigned i = 0; i < num; i++) {
-        proof * a = m_manager.get_parent(pr, i);
-        SASSERT(m_manager.has_fact(a));
-        antecedents.push_back(m_manager.get_fact(a));
+        proof * a = m.get_parent(pr, i);
+        SASSERT(m.has_fact(a));
+        antecedents.push_back(m.get_fact(a));
     }
     dump_proof(antecedents.size(), antecedents.c_ptr(), consequent);
 }
@@ -1150,21 +1273,20 @@ void proof_checker::dump_proof(unsigned num_antecedents, expr * const * antecede
     sprintf(buffer, "proof_lemma_%d.smt", m_proof_lemma_id);
 #endif
     std::ofstream out(buffer);
-    ast_smt_pp pp(m_manager);
+    ast_smt_pp pp(m);
     pp.set_benchmark_name("lemma");
     pp.set_status("unsat");
     pp.set_logic(m_logic.c_str());
     for (unsigned i = 0; i < num_antecedents; i++)
         pp.add_assumption(antecedents[i]);
-    expr_ref n(m_manager);
-    n = m_manager.mk_not(consequent);
+    expr_ref n(m);
+    n = m.mk_not(consequent);
     pp.display(out, n);
     out.close();
     m_proof_lemma_id++;
 }
 
 bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const& coeff, expr_ref& sum, bool& is_strict) {
-    ast_manager& m = m_manager;
     arith_util a(m);
     app* lit = lit0;
     
@@ -1173,7 +1295,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
         is_pos = !is_pos;
     }
     if (!a.is_le(lit) && !a.is_lt(lit) && !a.is_ge(lit) && !a.is_gt(lit) && !m.is_eq(lit)) {
-        std::cout << mk_pp(lit, m) << "\n";
+        IF_VERBOSE(0, verbose_stream() << mk_pp(lit, m) << "\n";);
         return false;
     }
     SASSERT(lit->get_num_args() == 2);
@@ -1237,7 +1359,7 @@ bool proof_checker::check_arith_literal(bool is_pos, app* lit0, rational const&
         rw(sum);
     }
 
-    std::cout << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";
+    IF_VERBOSE(0, verbose_stream() << coeff << "\n" << mk_pp(lit0, m) << "\n" << mk_pp(sum, m) << "\n";);
 #endif
 
     return true;
@@ -1247,7 +1369,6 @@ bool proof_checker::check_arith_proof(proof* p) {
     func_decl* d = p->get_decl();
     SASSERT(PR_TH_LEMMA == p->get_decl_kind());
     SASSERT(d->get_parameter(0).get_symbol() == "arith");
-    ast_manager& m = m_manager;
     unsigned num_params = d->get_num_parameters();
     arith_util autil(m);
 
@@ -1257,7 +1378,7 @@ bool proof_checker::check_arith_proof(proof* p) {
         return true;
     }
     expr_ref fact(m);
-    proof_ref_vector proofs(m_manager);
+    proof_ref_vector proofs(m);
     
     if (!match_fact(p, fact)) {
         UNREACHABLE();
@@ -1331,7 +1452,7 @@ bool proof_checker::check_arith_proof(proof* p) {
     rw(sum);
 
     if (!m.is_false(sum)) {
-        std::cout << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";
+        IF_VERBOSE(0, verbose_stream() << "Arithmetic proof check failed: " << mk_pp(sum, m) << "\n";);
         m_dump_lemmas = true;
         dump_proof(p);
         return false;
diff --git a/src/ast/proof_checker/proof_checker.h b/src/ast/proof_checker/proof_checker.h
index 6704f154a..9c5f8a749 100644
--- a/src/ast/proof_checker/proof_checker.h
+++ b/src/ast/proof_checker/proof_checker.h
@@ -23,7 +23,7 @@ Revision History:
 #include "map.h"
 
 class proof_checker {
-    ast_manager&     m_manager;
+    ast_manager&     m;
     proof_ref_vector m_todo;
     expr_mark        m_marked;
     expr_ref_vector  m_pinned;
@@ -111,6 +111,8 @@ private:
     expr* mk_hyp(unsigned num_hyps, expr * const * hyps);
     void dump_proof(proof * pr);
     void dump_proof(unsigned num_antecedents, expr * const * antecedents, expr * consequent);
+
+    void set_false(expr_ref& e, unsigned idx, expr_ref& lit);
 };
 
 #endif
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 1be6fe395..225f0be87 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -459,7 +459,8 @@ bool cmd_context::logic_has_arith_core(symbol const & s) const {
         s == "UFNIA" ||
         s == "LIA" ||        
         s == "LRA" || 
-        s == "QF_FPA" ;
+        s == "QF_FPA" ||
+        s == "HORN";
 }
 
 bool cmd_context::logic_has_arith() const {
@@ -479,6 +480,12 @@ bool cmd_context::logic_has_bv_core(symbol const & s) const {
         s == "QF_BVRE";
 }
 
+bool cmd_context::logic_has_horn(symbol const& s) const {
+    return
+        s == "HORN";
+
+}
+
 bool cmd_context::logic_has_bv() const {
     return !has_logic() || logic_has_bv_core(m_logic);
 }
@@ -589,6 +596,7 @@ bool cmd_context::supported_logic(symbol const & s) const {
     return s == "QF_UF" || s == "UF" || 
         logic_has_arith_core(s) || logic_has_bv_core(s) || 
         logic_has_array_core(s) || logic_has_seq_core(s) ||
+        logic_has_horn(s) ||
         s == "QF_FPA";
 }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 34a3375d7..5f83e0224 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -233,6 +233,7 @@ protected:
     bool logic_has_bv_core(symbol const & s) const;
     bool logic_has_array_core(symbol const & s) const;
     bool logic_has_seq_core(symbol const & s) const;
+    bool logic_has_horn(symbol const& s) const;
     bool logic_has_arith() const;
     bool logic_has_bv() const;
     bool logic_has_seq() const;
diff --git a/src/muz_qe/dl_bmc_engine.cpp b/src/muz_qe/dl_bmc_engine.cpp
index 91c2d72ee..02791bc6f 100644
--- a/src/muz_qe/dl_bmc_engine.cpp
+++ b/src/muz_qe/dl_bmc_engine.cpp
@@ -1096,6 +1096,10 @@ namespace datalog {
         m_solver.collect_statistics(st);
     }
 
+    void bmc::reset_statistics() {
+        m_solver.reset_statistics();
+    }
+
     void bmc::collect_params(param_descrs& p) {
     }
 
diff --git a/src/muz_qe/dl_bmc_engine.h b/src/muz_qe/dl_bmc_engine.h
index b8bb2e1e0..5de54f843 100644
--- a/src/muz_qe/dl_bmc_engine.h
+++ b/src/muz_qe/dl_bmc_engine.h
@@ -127,6 +127,8 @@ namespace datalog {
 
         void collect_statistics(statistics& st) const;
 
+        void reset_statistics(); 
+
         expr_ref get_answer();
 
         static void collect_params(param_descrs& p);
diff --git a/src/muz_qe/dl_cmds.cpp b/src/muz_qe/dl_cmds.cpp
index 92f5cfc89..a4bc4de6d 100644
--- a/src/muz_qe/dl_cmds.cpp
+++ b/src/muz_qe/dl_cmds.cpp
@@ -28,20 +28,25 @@ Notes:
 #include"cancel_eh.h"
 #include"scoped_ctrl_c.h"
 #include"scoped_timer.h"
+#include"trail.h"
 #include<iomanip>
 
 
 class dl_context {
     cmd_context &                 m_cmd;
+    dl_collected_cmds*            m_collected_cmds;
     unsigned                      m_ref_count;
     datalog::dl_decl_plugin*      m_decl_plugin;
-    scoped_ptr<datalog::context>  m_context;    
+    scoped_ptr<datalog::context>  m_context; 
+    trail_stack<dl_context>       m_trail;
 
 public:
-    dl_context(cmd_context & ctx):
+    dl_context(cmd_context & ctx, dl_collected_cmds* collected_cmds):
         m_cmd(ctx),
+        m_collected_cmds(collected_cmds),
         m_ref_count(0),
-        m_decl_plugin(0) {}
+        m_decl_plugin(0),
+        m_trail(*this) {}
     
     void inc_ref() {
         ++m_ref_count;
@@ -74,14 +79,53 @@ public:
     void reset() {
         m_context = 0;
     }
+
+    void register_predicate(func_decl* pred, unsigned num_kinds, symbol const* kinds) {
+        if (m_collected_cmds) {
+            m_collected_cmds->m_rels.push_back(pred);
+            m_trail.push(push_back_vector<dl_context, func_decl_ref_vector>(m_collected_cmds->m_rels));
+        }
+        dlctx().register_predicate(pred, false);
+        dlctx().set_predicate_representation(pred, num_kinds, kinds);        
+    }
     
     void add_rule(expr * rule, symbol const& name) {
         init();
-        std::string error_msg;
-        m_context->add_rule(rule, name);
+        if (m_collected_cmds) {
+            expr_ref rl = m_context->bind_variables(rule, true);
+            m_collected_cmds->m_rules.push_back(rl);
+            m_collected_cmds->m_names.push_back(name);
+            m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_rules));
+            m_trail.push(push_back_vector<dl_context, svector<symbol> >(m_collected_cmds->m_names));
+        }
+        else {
+            m_context->add_rule(rule, name);
+        }
     }    
+
+    bool collect_query(expr* q) {
+        if (m_collected_cmds) {
+            expr_ref qr = m_context->bind_variables(q, false);
+            m_collected_cmds->m_queries.push_back(qr);
+            m_trail.push(push_back_vector<dl_context, expr_ref_vector>(m_collected_cmds->m_queries));
+            return true;
+        }        
+        else {
+            return false;
+        }
+    }
+
+    void push() {
+        m_trail.push_scope();
+        dlctx().push();
+    }
+
+    void pop() {
+        m_trail.pop_scope(1);
+        dlctx().pop();
+    }
     
-    datalog::context & get_dl_context() {
+    datalog::context & dlctx() {
         init();
         return *m_context;
     }
@@ -160,7 +204,10 @@ public:
         if (m_target == 0) {
             throw cmd_exception("invalid query command, argument expected");
         }
-        datalog::context& dlctx = m_dl_ctx->get_dl_context();
+        if (m_dl_ctx->collect_query(m_target)) {
+            return;
+        }
+        datalog::context& dlctx = m_dl_ctx->dlctx();
         set_background(ctx);        
         dlctx.updt_params(m_params);
         unsigned timeout   = m_params.get_uint(":timeout", UINT_MAX);
@@ -217,7 +264,7 @@ public:
     }
 
     virtual void init_pdescrs(cmd_context & ctx, param_descrs & p) {
-        m_dl_ctx->get_dl_context().collect_params(p);
+        m_dl_ctx->dlctx().collect_params(p);
         insert_timeout(p);
         p.insert(":print-answer", CPK_BOOL, "(default: false) print answer instance(s) to query.");
         p.insert(":print-certificate", CPK_BOOL, "(default: false) print certificate for reachability or non-reachability.");
@@ -227,7 +274,7 @@ public:
 
 private:
     void set_background(cmd_context& ctx) {
-        datalog::context& dlctx = m_dl_ctx->get_dl_context();
+        datalog::context& dlctx = m_dl_ctx->dlctx();
         ptr_vector<expr>::const_iterator it  = ctx.begin_assertions();
         ptr_vector<expr>::const_iterator end = ctx.end_assertions();
         for (; it != end; ++it) {
@@ -237,7 +284,7 @@ private:
 
     void print_answer(cmd_context& ctx) {
         if (m_params.get_bool(":print-answer", false)) {
-            datalog::context& dlctx = m_dl_ctx->get_dl_context();
+            datalog::context& dlctx = m_dl_ctx->dlctx();
             ast_manager& m = ctx.m();
             expr_ref query_result(dlctx.get_answer_as_formula(), m);
             sbuffer<symbol> var_names;
@@ -253,7 +300,7 @@ private:
     void print_statistics(cmd_context& ctx) {
         if (m_params.get_bool(":print-statistics", false)) {
             statistics st;
-            datalog::context& dlctx = m_dl_ctx->get_dl_context();
+            datalog::context& dlctx = m_dl_ctx->dlctx();
             unsigned long long max_mem = memory::get_max_used_memory();
             unsigned long long mem = memory::get_allocation_size();
             dlctx.collect_statistics(st);
@@ -266,7 +313,7 @@ private:
 
     void print_certificate(cmd_context& ctx) {
         if (m_params.get_bool(":print-certificate", false)) {
-            datalog::context& dlctx = m_dl_ctx->get_dl_context();
+            datalog::context& dlctx = m_dl_ctx->dlctx();
             if (!dlctx.display_certificate(ctx.regular_stream())) {
                 throw cmd_exception("certificates are not supported for selected DL_ENGINE");
             }
@@ -286,6 +333,7 @@ class dl_declare_rel_cmd : public cmd {
     void ensure_domain(cmd_context& ctx) {
         if (!m_domain) m_domain = alloc(sort_ref_vector, ctx.m());
     }
+
 public:
     dl_declare_rel_cmd(dl_context * dl_ctx):
         cmd("declare-rel"),
@@ -334,11 +382,7 @@ public:
         func_decl_ref pred(
             m.mk_func_decl(m_rel_name, m_domain->size(), m_domain->c_ptr(), m.mk_bool_sort()), m);
         ctx.insert(pred);
-        datalog::context& dctx = m_dl_ctx->get_dl_context();
-        dctx.register_predicate(pred, false);
-        if(!m_kinds.empty()) {
-            dctx.set_predicate_representation(pred, m_kinds.size(), m_kinds.c_ptr());
-        }
+        m_dl_ctx->register_predicate(pred, m_kinds.size(), m_kinds.c_ptr());
         m_domain = 0;
     }
 
@@ -385,7 +429,7 @@ public:
         ast_manager& m = ctx.m();
         func_decl_ref var(m.mk_func_decl(m_var_name, 0, static_cast<sort*const*>(0), m_var_sort), m);
         ctx.insert(var);
-        m_dl_ctx->get_dl_context().register_variable(var);
+        m_dl_ctx->dlctx().register_variable(var);
     }
 
 };
@@ -402,7 +446,7 @@ public:
     virtual char const * get_descr(cmd_context & ctx) const { return "push context on the fixedpoint engine"; }
         
     virtual void execute(cmd_context& ctx) {
-        m_ctx->get_dl_context().push();
+        m_ctx->push();
     }
 };
 
@@ -418,19 +462,24 @@ public:
     virtual char const * get_descr(cmd_context & ctx) const { return "pop context on the fixedpoint engine"; }
         
     virtual void execute(cmd_context& ctx) {
-        m_ctx->get_dl_context().pop();
+        m_ctx->pop();
     }
 };
 
-
-
-void install_dl_cmds(cmd_context & ctx) {
-    dl_context * dl_ctx = alloc(dl_context, ctx);
+static void install_dl_cmds_aux(cmd_context& ctx, dl_collected_cmds* collected_cmds) {
+    dl_context * dl_ctx = alloc(dl_context, ctx, collected_cmds);
     ctx.insert(alloc(dl_rule_cmd, dl_ctx));
     ctx.insert(alloc(dl_query_cmd, dl_ctx));
     ctx.insert(alloc(dl_declare_rel_cmd, dl_ctx));
     ctx.insert(alloc(dl_declare_var_cmd, dl_ctx));
     PRIVATE_PARAMS(ctx.insert(alloc(dl_push_cmd, dl_ctx));); // not exposed to keep command-extensions simple.
-    PRIVATE_PARAMS(ctx.insert(alloc(dl_pop_cmd, dl_ctx)););
+    PRIVATE_PARAMS(ctx.insert(alloc(dl_pop_cmd, dl_ctx)););    
 }
 
+void install_dl_cmds(cmd_context & ctx) {
+    install_dl_cmds_aux(ctx, 0);
+}
+
+void install_dl_collect_cmds(dl_collected_cmds& collected_cmds, cmd_context & ctx) {
+    install_dl_cmds_aux(ctx, &collected_cmds);
+}
diff --git a/src/muz_qe/dl_cmds.h b/src/muz_qe/dl_cmds.h
index 72eb2dee2..d71b319c4 100644
--- a/src/muz_qe/dl_cmds.h
+++ b/src/muz_qe/dl_cmds.h
@@ -10,7 +10,7 @@ Abstract:
 
 Author:
 
-    Leonardo (leonardo) 2011-03-28
+    Nikolaj Bjorner (nbjorner) 2012-11-17
 
 Notes:
 
@@ -18,30 +18,20 @@ Notes:
 #ifndef _DL_CMDS_H_
 #define _DL_CMDS_H_
 
-class cmd;
+#include "ast.h"
+
 class cmd_context;
 
+struct dl_collected_cmds {
+    expr_ref_vector m_rules;
+    svector<symbol> m_names;
+    expr_ref_vector m_queries;
+    func_decl_ref_vector m_rels;
+    dl_collected_cmds(ast_manager& m) : m_rules(m), m_queries(m), m_rels(m) {}    
+};
+
 void install_dl_cmds(cmd_context & ctx);
+void install_dl_collect_cmds(dl_collected_cmds& collected_cmds, cmd_context& ctx);
 
-namespace datalog {
-
-    class context;
-
-    /**
-    Create a command for declaring relations which is connected to 
-    a particular datalog context.
-
-    Caller must ensure the returned object is deallocated (e.g. by passing it to a cmd_context).
-    */
-    cmd * mk_declare_rel_cmd(context& dctx);
-
-    /**
-       Declare a constant as a universal/existential variable.
-       It is implicitly existentially or universally quantified
-       by the rules.
-    */
-    cmd * mk_declare_var_cmd(context& dctx);
-
-}
 
 #endif
diff --git a/src/muz_qe/dl_context.cpp b/src/muz_qe/dl_context.cpp
index dd94796a0..59ab65bbd 100644
--- a/src/muz_qe/dl_context.cpp
+++ b/src/muz_qe/dl_context.cpp
@@ -49,11 +49,14 @@ Revision History:
 #include"dl_skip_table.h"
 #endif
 #include"for_each_expr.h"
+#include"ast_smt_pp.h"
 #include"ast_smt2_pp.h"
 #include"expr_functors.h"
 #include"dl_mk_partial_equiv.h"
 #include"dl_mk_bit_blast.h"
 #include"datatype_decl_plugin.h"
+#include"expr_abstract.h"
+
 
 namespace datalog {
 
@@ -331,8 +334,39 @@ namespace datalog {
         m_vars.push_back(m.mk_const(var));
     }
 
+    expr_ref context::bind_variables(expr* fml, bool is_forall) {
+        expr_ref result(m);
+        app_ref_vector const& vars = m_vars;
+        if (vars.empty()) {
+            result = fml;
+        }
+        else {
+            ptr_vector<sort> sorts;
+            expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
+            get_free_vars(result, sorts);
+            if (sorts.empty()) {
+                result = fml;
+            }
+            else {
+                svector<symbol> names;
+                for (unsigned i = 0; i < sorts.size(); ++i) {
+                    if (!sorts[i]) {
+                        sorts[i] = m.mk_bool_sort();
+                    }
+                    names.push_back(symbol(i));
+                }
+                quantifier_ref q(m);
+                q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result); 
+                elim_unused_vars(m, q, result);
+            }
+        }
+        return result;
+    }
+
     void context::register_predicate(func_decl * decl, bool named) {
-        SASSERT(!m_preds.contains(decl));
+        if (m_preds.contains(decl)) {
+            return;
+        }
         m_pinned.push_back(decl);
         m_preds.insert(decl);
         if (named) {
@@ -429,57 +463,35 @@ namespace datalog {
     }
 
     void context::set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
-            symbol * const relation_names) {
+            symbol const * relation_names) {
         relation_manager & rmgr = get_rmanager();
 
         family_id target_kind = null_family_id;
-        if (relation_name_cnt==1) {
+        switch (relation_name_cnt) {
+        case 0: 
+            return;
+        case 1:
             target_kind = get_ordinary_relation_plugin(relation_names[0]).get_kind();
-        } else {
-            relation_plugin * tr_plugin = 0; //table plugin, if there is such
-            ptr_vector<relation_plugin> rel_plugins; //plugins that are not table plugins
-            svector<family_id> rel_kinds; //kinds of plugins that are not table plugins
-            for (unsigned i=0; i<relation_name_cnt; i++) {
+            break;
+        default: {
+            svector<family_id> rel_kinds; // kinds of plugins that are not table plugins
+            family_id rel_kind;           // the aggregate kind of non-table plugins
+            for (unsigned i = 0; i < relation_name_cnt; i++) {
                 relation_plugin & p = get_ordinary_relation_plugin(relation_names[i]);
-                //commented out, because support combining relations with tables using fpr is not yet implemented
-                /*if (p.from_table()) {
-                    if (tr_plugin) {
-                        //it does not give any extra benefit to have an intersection of two tables.
-                        //Maybe when we can specify which columns belong to which plugin,
-                        //it might be of use.
-                        throw default_exception("two table plugins cannot be specified as relation type");
-                    }
-                    tr_plugin = &p;
-                }
-                else {*/
-                    rel_plugins.push_back(&p);
-                    rel_kinds.push_back(p.get_kind());
-                /*}*/
+                rel_kinds.push_back(p.get_kind());                
             }
-            SASSERT(!rel_kinds.empty());
-            // relation_plugin * rel_plugin; //the aggregate kind of non-table plugins
-            family_id rel_kind; //the aggregate kind of non-table plugins
-            if (rel_kinds.size()==1) {
+            if (rel_kinds.size() == 1) {
                 rel_kind = rel_kinds[0];
-                // rel_plugin = rel_plugins[0];
             }
             else {
                 relation_signature rel_sig;
                 //rmgr.from_predicate(pred, rel_sig);
                 product_relation_plugin & prod_plugin = product_relation_plugin::get_plugin(rmgr);
                 rel_kind = prod_plugin.get_relation_kind(rel_sig, rel_kinds);
-                // rel_plugin = &prod_plugin;
-            }
-            if (tr_plugin==0) {
-                target_kind = rel_kind;
-            }
-            else {
-                NOT_IMPLEMENTED_YET();
-#if 0
-                finite_product_relation_plugin & fprp = finite_product_relation_plugin::get_plugin(rmgr, *rel_plugin);
-                finite_product_relation_plugin::rel_spec spec;
-#endif           
             }
+            target_kind = rel_kind;
+            break;
+        }       
         }
 
         SASSERT(target_kind != null_family_id);
@@ -958,7 +970,8 @@ namespace datalog {
         p.insert(":output-profile", CPK_BOOL, "determines whether profile informations should be output when outputting Datalog rules or instructions");
         p.insert(":output-tuples", CPK_BOOL, "determines whether tuples for output predicates should be output");
         p.insert(":profile-timeout-milliseconds", CPK_UINT, "instructions and rules that took less than the threshold will not be printed when printed the instruction/rule list");
-                       
+                      
+        p.insert(":print-with-fixedpoint-extensions", CPK_BOOL, "(default true) use SMT-LIB2 fixedpoint extensions, instead of pure SMT2, when printing rules");
         PRIVATE_PARAMS(
             p.insert(":dbg-fpr-nonempty-relation-signature", CPK_BOOL, 
                               "if true, finite_product_relation will attempt to avoid creating inner relation with empty signature "
@@ -1198,7 +1211,6 @@ namespace datalog {
         case DATALOG_ENGINE:
             return dl_query(query);
         case PDR_ENGINE:
-            return pdr_query(query);
         case QPDR_ENGINE:
             return pdr_query(query);
         case BMC_ENGINE:
@@ -1219,6 +1231,28 @@ namespace datalog {
         m_last_answer = get_manager().mk_true();
     }
 
+    model_ref context::get_model() {
+        switch(get_engine()) {
+        case PDR_ENGINE:
+        case QPDR_ENGINE:
+            ensure_pdr();
+            return m_pdr->get_model();
+        default:
+            return model_ref(alloc(model, m));
+        }        
+    }
+
+    proof_ref context::get_proof() {
+        switch(get_engine()) {
+        case PDR_ENGINE:
+        case QPDR_ENGINE:
+            ensure_pdr();
+            return m_pdr->get_proof();
+        default:
+            return proof_ref(m.mk_asserted(m.mk_true()), m);
+        }                
+    }
+
     void context::ensure_pdr() {
         if (!m_pdr.get()) {
             m_pdr = alloc(pdr::dl_interface, *this);
@@ -1479,13 +1513,12 @@ namespace datalog {
         case DATALOG_ENGINE:            
             return false;
         case PDR_ENGINE: 
-            m_pdr->display_certificate(out);
-            return true;
-        case QPDR_ENGINE:
+            ensure_pdr();
             m_pdr->display_certificate(out);
             return true;
         case BMC_ENGINE:
         case QBMC_ENGINE:
+            ensure_bmc();
             m_bmc->display_certificate(out);
             return true;
         default: 
@@ -1493,20 +1526,31 @@ namespace datalog {
         }        
     }
 
+    void context::reset_statistics() {
+        if (m_pdr) {
+            m_pdr->reset_statistics();
+        }
+        if (m_bmc) {
+            m_bmc->reset_statistics();
+        }
+    }
 
-    void context::collect_statistics(statistics& st) {
-        switch(get_engine()) {
+    void context::collect_statistics(statistics& st) const {
+
+        switch(m_engine) {
         case DATALOG_ENGINE: 
             break;
         case PDR_ENGINE: 
-            m_pdr->collect_statistics(st);
-            break;
         case QPDR_ENGINE:
-            m_pdr->collect_statistics(st);
+            if (m_pdr) {
+                m_pdr->collect_statistics(st);
+            }
             break;
         case BMC_ENGINE:
         case QBMC_ENGINE:
-            m_bmc->collect_statistics(st);
+            if (m_bmc) {
+                m_bmc->collect_statistics(st);
+            }
             break;
         default: 
             break;
@@ -1564,6 +1608,7 @@ namespace datalog {
         expr* const* axioms = m_background.c_ptr();
         expr_ref fml(m);
         expr_ref_vector rules(m);
+        bool use_fixedpoint_extensions = m_params.get_bool(":print-with-fixedpoint-extensions", true);
         {
             rule_set::iterator it = m_rule_set.begin(), end = m_rule_set.end();
             for (; it != end; ++it) {
@@ -1586,13 +1631,17 @@ namespace datalog {
             if (f->get_family_id() != null_family_id) {
                 // 
             }
-            else if (is_predicate(f)) {
+            else if (is_predicate(f) && use_fixedpoint_extensions) {
                 rels.insert(f);
             }
             else {
                 funcs.insert(f);
             }
         }
+
+        if (!use_fixedpoint_extensions) {
+            out << "(set-logic HORN)\n";
+        }
         
         it = funcs.begin(), end = funcs.end();
         
@@ -1619,23 +1668,44 @@ namespace datalog {
             out << "))\n";
         }
 
-        declare_vars(rules, fresh_names, out);
-
+        if (use_fixedpoint_extensions) {
+            declare_vars(rules, fresh_names, out);
+        }
 
         for (unsigned i = 0; i < num_axioms; ++i) {
+            SASSERT(use_fixedpoint_extensions);
             out << "(assert ";
             ast_smt2_pp(out, axioms[i], env, params);
             out << ")\n";
         }
-        for (unsigned i = 0; i < rules.size(); ++i) {
-            out << "(rule ";
-            ast_smt2_pp(out, rules[i].get(), env, params);
+        for (unsigned i = 0; i < rules.size(); ++i) {            
+            out << (use_fixedpoint_extensions?"(rule ":"(assert ");
+            if (use_fixedpoint_extensions) {
+                ast_smt2_pp(out, rules[i].get(), env, params);
+            }
+            else {
+                out << mk_smt_pp(rules[i].get(), m);
+            }
             out << ")\n";
         }
-        for (unsigned i = 0; i < num_queries; ++i) {
-            out << "(query ";
-            ast_smt2_pp(out, queries[i], env, params);
-            out << ")\n";
+        if (use_fixedpoint_extensions) {
+            for (unsigned i = 0; i < num_queries; ++i) {
+                out << "(query ";
+                ast_smt2_pp(out, queries[i], env, params);
+                out << ")\n";
+            }
+        }
+        else {
+            for (unsigned i = 0; i < num_queries; ++i) {
+                if (num_queries > 1) out << "(push)\n";
+                out << "(assert ";
+                expr_ref q(m);
+                q = m.mk_not(queries[i]);
+                ast_smt2_pp(out, q, env, params);
+                out << ")\n";
+                out << "(check-sat)\n";
+                if (num_queries > 1) out << "(pop)\n";
+            }
         }
     }
 
diff --git a/src/muz_qe/dl_context.h b/src/muz_qe/dl_context.h
index 462e83ede..a6f8fc5e2 100644
--- a/src/muz_qe/dl_context.h
+++ b/src/muz_qe/dl_context.h
@@ -184,7 +184,7 @@ namespace datalog {
 
         void register_variable(func_decl* var);
 
-        app_ref_vector const& get_variables() const { return m_vars; }
+        expr_ref bind_variables(expr* fml, bool is_forall);
 
         /**
            Register datalog relation.
@@ -242,7 +242,7 @@ namespace datalog {
         symbol get_argument_name(const func_decl * pred, unsigned arg_index);
 
         void set_predicate_representation(func_decl * pred, unsigned relation_name_cnt, 
-            symbol * const relation_names);
+            symbol const *  relation_names);
 
         void set_output_predicate(func_decl * pred);
         bool is_output_predicate(func_decl * pred) { return m_output_preds.contains(pred); }
@@ -383,6 +383,21 @@ namespace datalog {
 
         lbool query(expr* q);
 
+        /**
+           \brief retrieve model from inductive invariant that shows query is unsat.
+           
+           \pre engine == 'pdr' - this option is only supported for PDR mode.
+         */
+        model_ref get_model();
+
+        /**
+           \brief retrieve proof from derivation of the query.
+           
+           \pre engine == 'pdr' - this option is only supported for PDR mode.
+         */
+        proof_ref get_proof();
+
+
         /**
            Query multiple output relations.
         */
@@ -411,7 +426,9 @@ namespace datalog {
         expr* get_answer_as_formula();
 
 
-        void collect_statistics(statistics& st);
+        void collect_statistics(statistics& st) const;
+
+        void reset_statistics();
 
         /**
            \brief Display a certificate for reachability and/or unreachability.
diff --git a/src/muz_qe/dl_mk_rule_inliner.cpp b/src/muz_qe/dl_mk_rule_inliner.cpp
index b7e31a75d..f92a56a4f 100644
--- a/src/muz_qe/dl_mk_rule_inliner.cpp
+++ b/src/muz_qe/dl_mk_rule_inliner.cpp
@@ -116,16 +116,20 @@ namespace datalog {
         apply(src, false, UINT_MAX,   tail, tail_neg);
         mk_rule_inliner::remove_duplicate_tails(tail, tail_neg);
         SASSERT(tail.size()==tail_neg.size());
-        res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr());
+        res = m_rm.mk(new_head, tail.size(), tail.c_ptr(), tail_neg.c_ptr(), tgt.name(), m_normalize);
         res->set_accounting_parent_object(m_context, const_cast<rule*>(&tgt));
-        res->norm_vars(m_rm);
-        m_rm.fix_unbound_vars(res, true);        
-        if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) {
-            res = simpl_rule;
-            return true;
+        if (m_normalize) {
+            m_rm.fix_unbound_vars(res, true);        
+            if (m_interp_simplifier.transform_rule(res.get(), simpl_rule)) {
+                res = simpl_rule;
+                return true;
+            }
+            else {
+                return false;
+            }
         }
         else {
-            return false;
+            return true;
         }
     }
 
diff --git a/src/muz_qe/dl_mk_rule_inliner.h b/src/muz_qe/dl_mk_rule_inliner.h
index 1be7ef059..6d5448cd6 100644
--- a/src/muz_qe/dl_mk_rule_inliner.h
+++ b/src/muz_qe/dl_mk_rule_inliner.h
@@ -38,11 +38,12 @@ namespace datalog {
         substitution   m_subst;
         unifier        m_unif;
         bool           m_ready;
+        bool           m_normalize;
         unsigned       m_deltas[2];
     public:
         rule_unifier(context& ctx)
             : m(ctx.get_manager()), m_rm(ctx.get_rule_manager()), m_context(ctx), 
-              m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false) {}
+            m_interp_simplifier(ctx), m_subst(m), m_unif(m), m_ready(false), m_normalize(true) {}
             
         /** Reset subtitution and unify tail tgt_idx of the target rule and the head of the src rule */
         bool unify_rules(rule const& tgt, unsigned tgt_idx, rule const& src);
@@ -60,6 +61,13 @@ namespace datalog {
         */
         expr_ref_vector get_rule_subst(rule const& r, bool is_tgt);
 
+        /**
+           Control if bound variables are normalized after unification.
+           The default is 'true': bound variables are re-mapped to an 
+           initial segment of de-Bruijn indices.
+         */
+        void set_normalize(bool n) { m_normalize = n; }
+
     private:
         void apply(app * a, bool is_tgt, app_ref& res);
 
diff --git a/src/muz_qe/dl_rule.cpp b/src/muz_qe/dl_rule.cpp
index b5e6b9305..9b0af2554 100644
--- a/src/muz_qe/dl_rule.cpp
+++ b/src/muz_qe/dl_rule.cpp
@@ -33,7 +33,6 @@ Revision History:
 #include"for_each_expr.h"
 #include"used_vars.h"
 #include"var_subst.h"
-#include"expr_abstract.h"
 #include"rewriter_def.h"
 #include"th_rewriter.h"
 #include"ast_smt2_pp.h"
@@ -291,30 +290,7 @@ namespace datalog {
     }
 
     void rule_manager::bind_variables(expr* fml, bool is_forall, expr_ref& result) {
-        app_ref_vector const& vars = m_ctx.get_variables();
-        if (vars.empty()) {
-            result = fml;
-        }
-        else {
-            ptr_vector<sort> sorts;
-            expr_abstract(m, 0, vars.size(), reinterpret_cast<expr*const*>(vars.c_ptr()), fml, result);
-            get_free_vars(result, sorts);
-            if (sorts.empty()) {
-                result = fml;
-            }
-            else {
-                svector<symbol> names;
-                for (unsigned i = 0; i < sorts.size(); ++i) {
-                    if (!sorts[i]) {
-                        sorts[i] = m.mk_bool_sort();
-                    }
-                    names.push_back(symbol(i));
-                }
-                quantifier_ref q(m);
-                q = m.mk_quantifier(is_forall, sorts.size(), sorts.c_ptr(), names.c_ptr(), result); 
-                elim_unused_vars(m, q, result);
-            }
-        }
+        result = m_ctx.bind_variables(fml, is_forall);
     }
 
     void rule_manager::flatten_body(app_ref_vector& body) {
@@ -526,7 +502,7 @@ namespace datalog {
         }
     }
 
-    rule * rule_manager::mk(app * head, unsigned n, app * const * tail, bool const * is_negated, symbol const& name) {
+    rule * rule_manager::mk(app * head, unsigned n, app * const * tail, bool const * is_negated, symbol const& name, bool normalize) {
         DEBUG_CODE(check_valid_rule(head, n, tail););
         unsigned sz     = rule::get_obj_size(n);
         void * mem      = m.get_allocator().allocate(sz);
@@ -588,7 +564,9 @@ namespace datalog {
             r->m_positive_cnt = r->m_uninterp_cnt;
         }
 
-        r->norm_vars(*this);
+        if (normalize) {
+            r->norm_vars(*this);
+        }
         return r;
     }
 
@@ -823,7 +801,7 @@ namespace datalog {
             new_tail.push_back(to_app(tmp));
             tail_neg.push_back(r->is_neg_tail(i));
         }
-        r = mk(new_head.get(), new_tail.size(), new_tail.c_ptr(), tail_neg.c_ptr(), r->name());
+        r = mk(new_head.get(), new_tail.size(), new_tail.c_ptr(), tail_neg.c_ptr(), r->name(), false);
 
         // keep old variable indices around so we can compose with substitutions. 
         // r->norm_vars(*this);
@@ -1068,24 +1046,25 @@ namespace datalog {
         us(fml);
         sorts.reverse();
         
-        for (unsigned i = 0; i < sorts.size(); ) {
+        for (unsigned i = 0; i < sorts.size(); ++i) {
             if (!sorts[i]) {
                 sorts[i] = m.mk_bool_sort();
             }
-            for (unsigned j = 0; i < sorts.size(); ++j) {
-                for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
-                    func_decl_ref f(m);
-                    std::stringstream _name;
-                    _name << c;
-                    if (j > 0) _name << j;
-                    symbol name(_name.str().c_str());
-                    if (!us.contains(name)) {
-                        names.push_back(name);
-                        ++i;
-                    }
+        }
+
+        for (unsigned j = 0, i = 0; i < sorts.size(); ++j) {
+            for (char c = 'A'; i < sorts.size() && c <= 'Z'; ++c) {
+                func_decl_ref f(m);
+                std::stringstream _name;
+                _name << c;
+                if (j > 0) _name << j;
+                symbol name(_name.str().c_str());
+                if (!us.contains(name)) {
+                    names.push_back(name);
+                    ++i;
                 }
             }
-        }
+        }        
         fml = m.mk_forall(sorts.size(), sorts.c_ptr(), names.c_ptr(), fml); 
     }
 
diff --git a/src/muz_qe/dl_rule.h b/src/muz_qe/dl_rule.h
index 0882a52f3..79a46052c 100644
--- a/src/muz_qe/dl_rule.h
+++ b/src/muz_qe/dl_rule.h
@@ -116,7 +116,7 @@ namespace datalog {
            \remark A tail may contain negation. tail[i] is assumed to be negated if is_neg != 0 && is_neg[i] == true
         */
         rule * mk(app * head, unsigned n, app * const * tail, bool const * is_neg = 0, 
-                         symbol const& name = symbol::null);
+                  symbol const& name = symbol::null, bool normalize = true);
 
         /**
            \brief Create a rule with the same tail as \c source and with a specified head.
@@ -252,7 +252,7 @@ namespace datalog {
 
         std::ostream& display_smt2(ast_manager& m, std::ostream & out) const;
 
-        symbol const& name() { return m_name; }
+        symbol const& name() const { return m_name; }
 
         unsigned hash() const;
 
diff --git a/src/muz_qe/pdr_context.cpp b/src/muz_qe/pdr_context.cpp
index 13c2c0f6d..21ad6b1ee 100644
--- a/src/muz_qe/pdr_context.cpp
+++ b/src/muz_qe/pdr_context.cpp
@@ -20,9 +20,6 @@ Revision History:
 
 Notes:
 
-   TODO:
-   - fix the slicing with covers.
-   - 
    
 --*/
 
@@ -100,6 +97,13 @@ namespace pdr {
             np += m_levels[i].size();
         } 
         st.update("PDR num properties", np); 
+        std::cout << m_stats.m_num_propagations << " " << np << "\n";
+    }
+
+    void pred_transformer::reset_statistics() {
+        m_solver.reset_statistics();
+        m_reachable.reset_statistics();
+        m_stats.reset();
     }
     
     void pred_transformer::init_sig() {
@@ -971,6 +975,7 @@ namespace pdr {
         proof_ref_vector trail(m);
         datalog::rule_ref_vector rules_trail(rm);
         proof* pr = 0;
+        unifier.set_normalize(false);
         todo.push_back(m_root);
         while (!todo.empty()) {
             model_node* n = todo.back();
@@ -1022,6 +1027,7 @@ namespace pdr {
                 binding_is_id = is_var(v) && to_var(v)->get_idx() == i;
             }
             if (rls.size() > 1 || !binding_is_id) {
+                expr_ref tmp(m);
                 vector<expr_ref_vector> substs;
                 svector<std::pair<unsigned,unsigned> > positions;
                 substs.push_back(binding); // TODO base substitution.
@@ -1029,9 +1035,10 @@ namespace pdr {
                     datalog::rule& src = *rls[i];
                     bool unified = unifier.unify_rules(*reduced_rule, 0, src);
                     if (!unified) {
-                        std::cout << "Could not unify rules: ";
-                        reduced_rule->display(dctx, std::cout);
-                        src.display(dctx, std::cout);
+                        IF_VERBOSE(0,
+                                   verbose_stream() << "Could not unify rules: ";
+                                   reduced_rule->display(dctx, verbose_stream());
+                                   src.display(dctx, verbose_stream()););
                     }
                     expr_ref_vector sub1 = unifier.get_rule_subst(*reduced_rule, true);
                     TRACE("pdr",
@@ -1040,8 +1047,15 @@ namespace pdr {
                           }
                           tout << "\n";
                           );
+
                     for (unsigned j = 0; j < substs.size(); ++j) {
-                        // TODO. apply sub1 to subst.
+                        for (unsigned k = 0; k < substs[j].size(); ++k) {
+                            var_subst(m, false)(substs[j][k].get(), sub1.size(), sub1.c_ptr(), tmp);
+                            substs[j][k] = tmp;
+                        }
+                        while (substs[j].size() < sub1.size()) {
+                            substs[j].push_back(sub1[substs[j].size()].get());
+                        }
                     }
 
                     positions.push_back(std::make_pair(i,0));
@@ -1049,9 +1063,11 @@ namespace pdr {
                     VERIFY(unifier.apply(*reduced_rule.get(), 0, src, r3));
                     reduced_rule = r3;
                 }
+
                 expr_ref fml_concl(m);
                 reduced_rule->to_formula(fml_concl);                    
                 p1 = m.mk_hyper_resolve(pfs.size(), pfs.c_ptr(), fml_concl, positions, substs);
+
             }
             cache.insert(n->state(), p1);
             rules.insert(n->state(), reduced_rule);
@@ -1334,24 +1350,68 @@ namespace pdr {
             if (!ok) {
                 IF_VERBOSE(0, verbose_stream() << "proof validation failed\n";);
             }
+            for (unsigned i = 0; i < side_conditions.size(); ++i) {
+                expr* cond = side_conditions[i].get();
+                expr_ref tmp(m);
+                tmp = m.mk_not(cond);
+                IF_VERBOSE(2, verbose_stream() << "checking side-condition:\n" << mk_pp(cond, m) << "\n";);
+                smt::kernel solver(m, get_fparams());
+                solver.assert_expr(tmp);
+                lbool res = solver.check();
+                if (res != l_false) {
+                    IF_VERBOSE(0, verbose_stream() << "rule validation failed\n";
+                               verbose_stream() << mk_pp(cond, m) << "\n";
+                               );
+                }                                
+            }
             break;
         }            
         case l_false: {
-            expr_ref_vector refs(m);
+            expr_ref_vector refs(m), fmls(m);
+            expr_ref tmp(m);
             model_ref model;
             vector<relation_info> rs;
+            model_converter_ref mc;
             get_level_property(m_inductive_lvl, refs, rs);    
-            inductive_property ex(m, const_cast<model_converter_ref&>(m_mc), rs);
+            inductive_property ex(m, mc, rs);
             ex.to_model(model);
             decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
-            var_subst vs(m, false);
+            var_subst vs(m, false);   
             for (; it != end; ++it) {
                 ptr_vector<datalog::rule> const& rules = it->m_value->rules();
                 for (unsigned i = 0; i < rules.size(); ++i) {
-                    // datalog::rule* rule = rules[i];
-                    // vs(rule->get_head(), 
-                    // apply interpretation of predicates to rule.
-                    // create formula and check for unsat.
+                    datalog::rule& r = *rules[i];
+                    model->eval(r.get_head(), tmp);
+                    fmls.push_back(m.mk_not(tmp));
+                    unsigned utsz = r.get_uninterpreted_tail_size();
+                    unsigned tsz  = r.get_tail_size();
+                    for (unsigned j = 0; j < utsz; ++j) {
+                        model->eval(r.get_tail(j), tmp);
+                        fmls.push_back(tmp);
+                    }
+                    for (unsigned j = utsz; j < tsz; ++j) {
+                        fmls.push_back(r.get_tail(j));
+                    }
+                    tmp = m.mk_and(fmls.size(), fmls.c_ptr()); 
+                    ptr_vector<sort> sorts;
+                    svector<symbol> names;
+                    get_free_vars(tmp, sorts);
+                    for (unsigned i = 0; i < sorts.size(); ++i) {
+                        if (!sorts[i]) {
+                            sorts[i] = m.mk_bool_sort();
+                        }
+                        names.push_back(symbol(i));
+                    }
+                    sorts.reverse();
+                    tmp = m.mk_exists(sorts.size(), sorts.c_ptr(), names.c_ptr(), tmp);
+                    smt::kernel solver(m, get_fparams());
+                    solver.assert_expr(tmp);
+                    lbool res = solver.check();
+                    if (res != l_false) {
+                        IF_VERBOSE(0, verbose_stream() << "rule validation failed\n";
+                                   verbose_stream() << mk_pp(tmp, m) << "\n";
+                                   );
+                    }
                 }
             }
             break;
@@ -1476,13 +1536,15 @@ namespace pdr {
         }
     }
 
-    void context::get_model(model_ref& md) {
+    model_ref context::get_model() {
         SASSERT(m_last_result == l_false);        
         expr_ref_vector refs(m);
         vector<relation_info> rs;
+        model_ref md;
         get_level_property(m_inductive_lvl, refs, rs);            
         inductive_property ex(m, m_mc, rs);
         ex.to_model(md);
+        return md;
     }
     
     proof_ref context::get_proof() const {
@@ -1870,6 +1932,20 @@ namespace pdr {
         }
     }
 
+    void context::reset_statistics() {
+        decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
+        for (it = m_rels.begin(); it != end; ++it) {
+            it->m_value->reset_statistics();
+        }
+        m_stats.reset();
+        m_pm.reset_statistics();
+
+        for (unsigned i = 0; i < m_core_generalizers.size(); ++i) {
+            m_core_generalizers[i]->reset_statistics();
+        }
+
+    }
+
 
     std::ostream& context::display(std::ostream& out) const {
         decl2rel::iterator it = m_rels.begin(), end = m_rels.end();
diff --git a/src/muz_qe/pdr_context.h b/src/muz_qe/pdr_context.h
index 0f9af5649..14be82dae 100644
--- a/src/muz_qe/pdr_context.h
+++ b/src/muz_qe/pdr_context.h
@@ -132,6 +132,7 @@ namespace pdr {
         std::ostream& display(std::ostream& strm) const;
 
         void collect_statistics(statistics& st) const;
+        void reset_statistics();
 
         bool is_reachable(expr* state);
         void remove_predecessors(expr_ref_vector& literals);
@@ -275,6 +276,7 @@ namespace pdr {
             }
         }
         virtual void collect_statistics(statistics& st) const {}
+        virtual void reset_statistics() {}
     };
 
     class context {
@@ -366,6 +368,7 @@ namespace pdr {
 
 
         void collect_statistics(statistics& st) const;
+        void reset_statistics();
 
         std::ostream& display(std::ostream& strm) const;        
 
@@ -401,7 +404,7 @@ namespace pdr {
 
         void add_cover(int level, func_decl* pred, expr* property);
 
-        void get_model(model_ref& md);
+        model_ref get_model();
 
         proof_ref get_proof() const;
 
diff --git a/src/muz_qe/pdr_dl_interface.cpp b/src/muz_qe/pdr_dl_interface.cpp
index 098fd0c56..19c604162 100644
--- a/src/muz_qe/pdr_dl_interface.cpp
+++ b/src/muz_qe/pdr_dl_interface.cpp
@@ -197,6 +197,10 @@ void dl_interface::collect_statistics(statistics& st) const {
     m_context->collect_statistics(st);
 }
 
+void dl_interface::reset_statistics() {
+    m_context->reset_statistics();
+}
+
 void dl_interface::display_certificate(std::ostream& out) const {
     m_context->display_certificate(out);
 }
@@ -218,6 +222,14 @@ void dl_interface::updt_params() {
     m_context = alloc(pdr::context, m_ctx.get_fparams(), m_ctx.get_params(), m_ctx.get_manager());
 }
 
+model_ref dl_interface::get_model() {
+    return m_context->get_model();
+}
+
+proof_ref dl_interface::get_proof() {
+    return m_context->get_proof();
+}
+
 void dl_interface::collect_params(param_descrs& p) {
     p.insert(":bfs-model-search", CPK_BOOL, "PDR: (default true) use BFS strategy for expanding model search");
     p.insert(":use-farkas", CPK_BOOL, "PDR: (default true) use lemma generator based on Farkas (for linear real arithmetic)");
diff --git a/src/muz_qe/pdr_dl_interface.h b/src/muz_qe/pdr_dl_interface.h
index 096583a70..61f56282e 100644
--- a/src/muz_qe/pdr_dl_interface.h
+++ b/src/muz_qe/pdr_dl_interface.h
@@ -57,6 +57,8 @@ namespace pdr {
 
         void collect_statistics(statistics& st) const;
 
+        void reset_statistics();
+
         expr_ref get_answer();
 
         unsigned get_num_levels(func_decl* pred);
@@ -66,8 +68,12 @@ namespace pdr {
         void add_cover(int level, func_decl* pred, expr* property);
 
         static void collect_params(param_descrs& p);
-
+               
         void updt_params();
+
+        model_ref get_model();
+
+        proof_ref get_proof();
         
     };
 }
diff --git a/src/muz_qe/pdr_manager.h b/src/muz_qe/pdr_manager.h
index 398f2716f..85f2116e9 100644
--- a/src/muz_qe/pdr_manager.h
+++ b/src/muz_qe/pdr_manager.h
@@ -313,6 +313,8 @@ namespace pdr {
         pdr::smt_context* mk_fresh() {  return m_contexts.mk_fresh();   }
         
         void collect_statistics(statistics& st) const { m_contexts.collect_statistics(st); }
+
+        void reset_statistics() { m_contexts.reset_statistics(); }
     };
 }
 
diff --git a/src/muz_qe/pdr_prop_solver.cpp b/src/muz_qe/pdr_prop_solver.cpp
index 865bfe32b..574be63b1 100644
--- a/src/muz_qe/pdr_prop_solver.cpp
+++ b/src/muz_qe/pdr_prop_solver.cpp
@@ -364,8 +364,7 @@ namespace pdr {
         m_core->append(lemmas);
     }
 
-    lbool prop_solver::check_assumptions(const expr_ref_vector & atoms)
-    {
+    lbool prop_solver::check_assumptions(const expr_ref_vector & atoms) {
         return check_assumptions_and_formula(atoms, m.mk_true());
     }
 
@@ -393,5 +392,10 @@ namespace pdr {
     void prop_solver::collect_statistics(statistics& st) const {
     }
 
+    void prop_solver::reset_statistics() {
+    }
+
+    
+
 
 }
diff --git a/src/muz_qe/pdr_prop_solver.h b/src/muz_qe/pdr_prop_solver.h
index da0a1b31e..15122a21a 100644
--- a/src/muz_qe/pdr_prop_solver.h
+++ b/src/muz_qe/pdr_prop_solver.h
@@ -122,6 +122,8 @@ namespace pdr {
             expr * form);
         
         void collect_statistics(statistics& st) const;
+
+        void reset_statistics();
         
     };
 }
diff --git a/src/muz_qe/pdr_reachable_cache.cpp b/src/muz_qe/pdr_reachable_cache.cpp
index baa18839c..ed9926f85 100644
--- a/src/muz_qe/pdr_reachable_cache.cpp
+++ b/src/muz_qe/pdr_reachable_cache.cpp
@@ -27,9 +27,6 @@ namespace pdr {
           m_ctx(0),
           m_ref_holder(m), 
           m_disj_connector(m),
-          m_cache_hits(0),
-          m_cache_miss(0),
-          m_cache_inserts(0),
           m_cache_mode((datalog::PDR_CACHE_MODE)params.get_uint(":cache-mode",0)) {
         if (m_cache_mode == datalog::CONSTRAINT_CACHE) {
             m_ctx = pm.mk_fresh();
@@ -63,13 +60,13 @@ namespace pdr {
             break;
             
         case datalog::HASH_CACHE: 
-            m_cache_inserts++;
+            m_stats.m_inserts++;
             m_cache.insert(cube);
             m_ref_holder.push_back(cube);
             break;
             
         case datalog::CONSTRAINT_CACHE: 
-            m_cache_inserts++;
+            m_stats.m_inserts++;
             TRACE("pdr", tout << mk_pp(cube, m) << "\n";);
             add_disjuncted_formula(cube);
             break;
@@ -112,14 +109,18 @@ namespace pdr {
             UNREACHABLE();
             break;
         }
-        if (found) m_cache_hits++; m_cache_miss++;
+        if (found) m_stats.m_hits++; m_stats.m_miss++;
         return found;
     }
 
     void reachable_cache::collect_statistics(statistics& st) const {
-        st.update("cache inserts", m_cache_inserts);
-        st.update("cache miss", m_cache_miss);
-        st.update("cache hits", m_cache_hits);
+        st.update("cache inserts", m_stats.m_inserts);
+        st.update("cache miss", m_stats.m_miss);
+        st.update("cache hits", m_stats.m_hits);
+    }
+
+    void reachable_cache::reset_statistics() {
+        m_stats.reset();
     }
 
 
diff --git a/src/muz_qe/pdr_reachable_cache.h b/src/muz_qe/pdr_reachable_cache.h
index d40e0e703..d8096f15c 100644
--- a/src/muz_qe/pdr_reachable_cache.h
+++ b/src/muz_qe/pdr_reachable_cache.h
@@ -28,15 +28,21 @@ Revision History:
 
 namespace pdr {
     class reachable_cache {
+        struct stats {
+            unsigned             m_hits;
+            unsigned             m_miss;
+            unsigned             m_inserts;
+            stats() { reset(); }
+            void reset() { memset(this, 0, sizeof(*this)); }
+        };
+
         ast_manager &        m;
         manager &            m_pm;
         scoped_ptr<smt_context>    m_ctx;
         ast_ref_vector       m_ref_holder;
         app_ref              m_disj_connector;
         obj_hashtable<expr>  m_cache;
-        unsigned             m_cache_hits;
-        unsigned             m_cache_miss;
-        unsigned             m_cache_inserts;
+        stats                m_stats;
         datalog::PDR_CACHE_MODE m_cache_mode;
         
         void add_disjuncted_formula(expr * f);
@@ -53,6 +59,8 @@ namespace pdr {
         bool is_reachable(expr * cube);
         
         void collect_statistics(statistics& st) const;
+
+        void reset_statistics();
     };
 }
 
diff --git a/src/muz_qe/pdr_smt_context_manager.cpp b/src/muz_qe/pdr_smt_context_manager.cpp
index 36b8e2325..d79192769 100644
--- a/src/muz_qe/pdr_smt_context_manager.cpp
+++ b/src/muz_qe/pdr_smt_context_manager.cpp
@@ -136,6 +136,12 @@ namespace pdr {
         }
     }
 
+    void smt_context_manager::reset_statistics() {
+        for (unsigned i = 0; i < m_contexts.size(); ++i) {
+            m_contexts[i]->reset_statistics();
+        }
+    }
+
 
 };
 
diff --git a/src/muz_qe/pdr_smt_context_manager.h b/src/muz_qe/pdr_smt_context_manager.h
index d6aef9776..31fb8ccb3 100644
--- a/src/muz_qe/pdr_smt_context_manager.h
+++ b/src/muz_qe/pdr_smt_context_manager.h
@@ -100,6 +100,7 @@ namespace pdr {
         ~smt_context_manager();
         smt_context* mk_fresh();                
         void collect_statistics(statistics& st) const;
+        void reset_statistics();
         bool is_aux_predicate(func_decl* p) const { return m_predicate_set.contains(p); }
     };
 
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 50d972a0d..eb0534eea 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -33,6 +33,7 @@ Notes:
 #include"default_tactic.h"
 #include"ufbv_tactic.h"
 #include"qffpa_tactic.h"
+#include"pdr_tactic.h"
 #include"smt_solver.h"
 
 MK_SIMPLE_TACTIC_FACTORY(qfuf_fct, mk_qfuf_tactic(m, p));
@@ -54,6 +55,7 @@ MK_SIMPLE_TACTIC_FACTORY(qfnia_fct, mk_qfnia_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(qfnra_fct, mk_qfnra_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(qffpa_fct, mk_qffpa_tactic(m, p));
 MK_SIMPLE_TACTIC_FACTORY(ufbv_fct, mk_ufbv_tactic(m, p));
+MK_SIMPLE_TACTIC_FACTORY(horn_fct, mk_pdr_tactic(m, p));
 
 static void init(strategic_solver * s) {
     s->set_default_tactic(alloc(default_fct));
@@ -77,6 +79,7 @@ static void init(strategic_solver * s) {
     s->set_tactic_for(symbol("UFBV"),      alloc(ufbv_fct));
     s->set_tactic_for(symbol("BV"),        alloc(ufbv_fct));        
     s->set_tactic_for(symbol("QF_FPA"),    alloc(qffpa_fct));
+    s->set_tactic_for(symbol("HORN"),      alloc(horn_fct));
 }
 
 solver * mk_smt_strategic_solver(bool force_tactic) {