diff --git a/contrib/cmake/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
index 74fddd2bb..abf09ff0c 100644
--- a/contrib/cmake/src/ast/rewriter/CMakeLists.txt
+++ b/contrib/cmake/src/ast/rewriter/CMakeLists.txt
@@ -8,6 +8,7 @@ z3_add_component(rewriter
     bv_rewriter.cpp
     datatype_rewriter.cpp
     der.cpp
+    distribute_forall.cpp
     dl_rewriter.cpp
     enum2bv_rewriter.cpp
     expr_replacer.cpp
diff --git a/contrib/cmake/src/ast/simplifier/CMakeLists.txt b/contrib/cmake/src/ast/simplifier/CMakeLists.txt
index 7597374a6..9575c5c89 100644
--- a/contrib/cmake/src/ast/simplifier/CMakeLists.txt
+++ b/contrib/cmake/src/ast/simplifier/CMakeLists.txt
@@ -10,7 +10,6 @@ z3_add_component(simplifier
     bv_simplifier_params.cpp
     bv_simplifier_plugin.cpp
     datatype_simplifier_plugin.cpp
-    distribute_forall.cpp
     elim_bounds.cpp
     fpa_simplifier_plugin.cpp
     inj_axiom.cpp
diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp
index 67c0f2f08..d867900e8 100644
--- a/src/api/api_model.cpp
+++ b/src/api/api_model.cpp
@@ -349,10 +349,10 @@ extern "C" {
     //
     // ----------------------------
 
+#if 0
     void Z3_API Z3_del_model(Z3_context c, Z3_model  m) {
         Z3_model_dec_ref(c, m);
     }
-
     unsigned Z3_API Z3_get_model_num_constants(Z3_context c, Z3_model m) {
         return Z3_model_get_num_consts(c, m);
     }
@@ -368,6 +368,7 @@ extern "C" {
     Z3_func_decl Z3_API Z3_get_model_func_decl(Z3_context c, Z3_model m, unsigned i) {
         return Z3_model_get_func_decl(c, m, i);
     }
+#endif
     
 
     unsigned get_model_func_num_entries_core(Z3_context c, Z3_model m, unsigned i) {
diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp
index 6dc41efb2..c6eae7488 100644
--- a/src/api/api_solver.cpp
+++ b/src/api/api_solver.cpp
@@ -477,4 +477,60 @@ extern "C" {
         Z3_CATCH_RETURN(Z3_L_UNDEF);        
     }
 
+    Z3_ast Z3_API Z3_solver_lookahead(Z3_context c,
+                                      Z3_solver s,
+                                      Z3_ast_vector candidates)  {
+        Z3_TRY;
+        LOG_Z3_solver_lookahead(c, s, candidates);
+        ast_manager& m = mk_c(c)->m();
+        expr_ref_vector _candidates(m);
+        ast_ref_vector const& __candidates = to_ast_vector_ref(candidates);
+        for (auto & e : __candidates) {
+            if (!is_expr(e)) {
+                SET_ERROR_CODE(Z3_INVALID_USAGE);
+                return 0;
+            }
+            _candidates.push_back(to_expr(e));
+        }
+
+        expr_ref result(m);
+        unsigned timeout     = to_solver(s)->m_params.get_uint("timeout", mk_c(c)->get_timeout());
+        unsigned rlimit      = to_solver(s)->m_params.get_uint("rlimit", mk_c(c)->get_rlimit());
+        bool     use_ctrl_c  = to_solver(s)->m_params.get_bool("ctrl_c", false);
+        cancel_eh<reslimit> eh(mk_c(c)->m().limit());
+        api::context::set_interruptable si(*(mk_c(c)), eh);
+        {
+            scoped_ctrl_c ctrlc(eh, false, use_ctrl_c);
+            scoped_timer timer(timeout, &eh);
+            scoped_rlimit _rlimit(mk_c(c)->m().limit(), rlimit);
+            try {
+                result = to_solver_ref(s)->lookahead(_candidates);
+            }
+            catch (z3_exception & ex) {
+                mk_c(c)->handle_exception(ex);
+                return 0;
+            }
+        }
+        mk_c(c)->save_ast_trail(result);
+        RETURN_Z3(of_ast(result));
+        Z3_CATCH_RETURN(0);
+    }
+    
+    Z3_ast_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s)  {
+        Z3_TRY;
+        LOG_Z3_solver_get_lemmas(c, s);
+        RESET_ERROR_CODE();
+        ast_manager& m = mk_c(c)->m();
+        init_solver(c, s);
+        Z3_ast_vector_ref * v = alloc(Z3_ast_vector_ref, *mk_c(c), mk_c(c)->m());
+        mk_c(c)->save_object(v);
+        expr_ref_vector lemmas(m);
+        to_solver_ref(s)->get_lemmas(lemmas);
+        for (expr* e : lemmas) {
+            v->m_ast_vector.push_back(e);
+        }
+        RETURN_Z3(of_ast_vector(v));                
+        Z3_CATCH_RETURN(0);
+    }
+
 };
diff --git a/src/api/dotnet/Solver.cs b/src/api/dotnet/Solver.cs
index dff2677df..6dd19cddf 100644
--- a/src/api/dotnet/Solver.cs
+++ b/src/api/dotnet/Solver.cs
@@ -252,6 +252,29 @@ namespace Microsoft.Z3
             return lboolToStatus(r);
         }
 
+	/// <summary>
+	/// Select a lookahead literal from the set of supplied candidates.
+	/// </summary>
+	public BoolExpr Lookahead(IEnumerable<BoolExpr> candidates) 
+	{
+             ASTVector cands = new ASTVector(Context);
+             foreach (var c in candidates) cands.Push(c);
+	     return (BoolExpr)Expr.Create(Context, Native.Z3_solver_lookahead(Context.nCtx, NativeObject, cands.NativeObject));
+        }
+
+	/// <summary>
+	/// Retrieve set of lemmas that have been inferred by solver.
+	/// </summary>
+	public BoolExpr[] Lemmas
+        {
+	    get 
+	    {
+	        var r = Native.Z3_solver_get_lemmas(Context.nCtx, NativeObject);
+	        var v = new ASTVector(Context, r);
+                return v.ToBoolExprArray();
+            }
+        }
+
         /// <summary>
         /// The model of the last <c>Check</c>.
         /// </summary>
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 84a80ddf7..7e93e58ae 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -6216,6 +6216,21 @@ class Solver(Z3PPObject):
         consequences = [ consequences[i] for i in range(sz) ]
         return CheckSatResult(r), consequences
     
+    def lemmas(self):
+        """Extract auxiliary lemmas produced by solver"""
+        return AstVector(Z3_solver_get_lemmas(self.ctx.ref(), self.solver), self.ctx)
+        
+    def lookahead(self, candidates = None):
+        """Get lookahead literal"""
+        if candidates is None:
+            candidates = AstVector(None, self.ctx)
+        elif not isinstance(candidates, AstVector):
+            _cs = AstVector(None, self.ctx)
+            for c in candidates:
+                _asms.push(c)
+            candidates = _cs
+        return _to_expr_ref(Z3_solver_lookahead(self.ctx.ref(), self.solver, candidates), self.ctx)        
+
     def proof(self):
         """Return a proof for the last `check()`. Proof construction must be enabled."""
         return _to_expr_ref(Z3_solver_get_proof(self.ctx.ref(), self.solver), self.ctx)
diff --git a/src/api/z3_api.h b/src/api/z3_api.h
index 45065f856..e3bd942bd 100644
--- a/src/api/z3_api.h
+++ b/src/api/z3_api.h
@@ -6023,6 +6023,29 @@ extern "C" {
                                                Z3_ast_vector assumptions,
                                                Z3_ast_vector variables,
                                                Z3_ast_vector consequences);
+
+    /**
+       \brief select a literal from the list of candidate propositional variables to split on.
+       If the candidate list is empty, then the solver chooses a formula based on its internal state.
+       
+       def_API('Z3_solver_lookahead', AST, (_in(CONTEXT), _in(SOLVER), _in(AST_VECTOR)))
+    */
+
+    Z3_ast Z3_API Z3_solver_lookahead(Z3_context c, Z3_solver s, Z3_ast_vector candidates);
+
+
+    /**
+       \brief retrieve lemmas from solver state. Lemmas are auxiliary unit literals, 
+       binary clauses and other learned clauses that are below a minimal glue level.
+       Lemmas that have been retrieved in a previous call may be suppressed from subsequent
+       calls.
+
+       def_API('Z3_solver_get_lemmas', AST_VECTOR, (_in(CONTEXT), _in(SOLVER)))
+    */
+
+    Z3_ast_vector Z3_API Z3_solver_get_lemmas(Z3_context c, Z3_solver s);
+
+       
     /**
        \brief Retrieve the model for the last #Z3_solver_check or #Z3_solver_check_assumptions
 
@@ -6031,6 +6054,7 @@ extern "C" {
 
        def_API('Z3_solver_get_model', MODEL, (_in(CONTEXT), _in(SOLVER)))
     */
+
     Z3_model Z3_API Z3_solver_get_model(Z3_context c, Z3_solver s);
 
     /**
diff --git a/src/ast/simplifier/distribute_forall.cpp b/src/ast/rewriter/distribute_forall.cpp
similarity index 92%
rename from src/ast/simplifier/distribute_forall.cpp
rename to src/ast/rewriter/distribute_forall.cpp
index 78e5d5ded..c64c0f089 100644
--- a/src/ast/simplifier/distribute_forall.cpp
+++ b/src/ast/rewriter/distribute_forall.cpp
@@ -20,12 +20,12 @@ Revision History:
 --*/
 #include"var_subst.h"
 #include"ast_ll_pp.h"
-
+#include"ast_util.h"
 #include"distribute_forall.h"
+#include"bool_rewriter.h"
 
-distribute_forall::distribute_forall(ast_manager & m, basic_simplifier_plugin & p) :
+distribute_forall::distribute_forall(ast_manager & m) :
     m_manager(m),
-    m_bsimp(p),
     m_cache(m) {
 }
 
@@ -109,6 +109,8 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
 
     expr * e = get_cached(q->get_expr());
     if (m_manager.is_not(e) && m_manager.is_or(to_app(e)->get_arg(0))) {
+        bool_rewriter br(m_manager);
+
         // found target for simplification
         // (forall X (not (or F1 ... Fn)))
         // -->
@@ -121,8 +123,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
         for (unsigned i = 0; i < num_args; i++) {
             expr * arg = or_e->get_arg(i);
             expr_ref not_arg(m_manager);
-            // m_bsimp.mk_not applies basic simplifications. For example, if arg is of the form (not a), then it will return a.
-            m_bsimp.mk_not(arg, not_arg);
+            br.mk_not(arg, not_arg);
             quantifier_ref tmp_q(m_manager);
             tmp_q = m_manager.update_quantifier(q, not_arg);
             expr_ref new_q(m_manager);
@@ -132,7 +133,7 @@ void distribute_forall::reduce1_quantifier(quantifier * q) {
         expr_ref result(m_manager);
         // m_bsimp.mk_and actually constructs a (not (or ...)) formula,
         // it will also apply basic simplifications.
-        m_bsimp.mk_and(new_args.size(), new_args.c_ptr(), result);
+        br.mk_and(new_args.size(), new_args.c_ptr(), result);
         cache_result(q, result);
     }
     else {
diff --git a/src/ast/simplifier/distribute_forall.h b/src/ast/rewriter/distribute_forall.h
similarity index 90%
rename from src/ast/simplifier/distribute_forall.h
rename to src/ast/rewriter/distribute_forall.h
index 4c2eefb56..b2c239239 100644
--- a/src/ast/simplifier/distribute_forall.h
+++ b/src/ast/rewriter/distribute_forall.h
@@ -22,7 +22,6 @@ Revision History:
 #define DISTRIBUTE_FORALL_H_
 
 #include"ast.h"
-#include"basic_simplifier_plugin.h"
 #include"act_cache.h"
 
 /**
@@ -47,7 +46,6 @@ Revision History:
 class distribute_forall {
     typedef act_cache expr_map;
     ast_manager &             m_manager;
-    basic_simplifier_plugin & m_bsimp; // useful for constructing formulas and/or/not in simplified form.
     ptr_vector<expr>          m_todo;
     expr_map                  m_cache;
     ptr_vector<expr>          m_new_args;
@@ -57,7 +55,7 @@ class distribute_forall {
 
 
 public:
-    distribute_forall(ast_manager & m, basic_simplifier_plugin & p);
+    distribute_forall(ast_manager & m);
 
     /**
        \brief Apply the distribute_forall transformation (when possible) to all universal quantifiers in \c f.
diff --git a/src/ast/rewriter/pb2bv_rewriter.cpp b/src/ast/rewriter/pb2bv_rewriter.cpp
index aedd62081..bcc050048 100644
--- a/src/ast/rewriter/pb2bv_rewriter.cpp
+++ b/src/ast/rewriter/pb2bv_rewriter.cpp
@@ -822,8 +822,7 @@ struct pb2bv_rewriter::imp {
             p.get_bool("keep_cardinality_constraints", false) ||
             p.get_bool("sat.cardinality.solver", false) ||
             p.get_bool("cardinality.solver", false) || 
-            gparams::get_module("sat").get_bool("cardinality.solver", false) ||
-            keep_pb();
+            gparams::get_module("sat").get_bool("cardinality.solver", false);
     }
 
     bool keep_pb() const {
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index f590725a7..36afeb87d 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -326,6 +326,7 @@ cmd_context::cmd_context(bool main_ctx, ast_manager * m, symbol const & l):
     m_numeral_as_real(false),
     m_ignore_check(false),
     m_exit_on_error(false),
+    m_processing_pareto(false),
     m_manager(m),
     m_own_manager(m == 0),
     m_manager_initialized(false),
@@ -1130,6 +1131,7 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
 }
 
 void cmd_context::reset(bool finalize) {
+    m_processing_pareto = false;
     m_logic = symbol::null;
     m_check_sat_result = 0;
     m_numeral_as_real = false;
@@ -1174,6 +1176,7 @@ void cmd_context::reset(bool finalize) {
 }
 
 void cmd_context::assert_expr(expr * t) {
+    m_processing_pareto = false;
     if (!m_check_logic(t))
         throw cmd_exception(m_check_logic.get_last_error());
     m_check_sat_result = 0;
@@ -1186,6 +1189,7 @@ void cmd_context::assert_expr(expr * t) {
 }
 
 void cmd_context::assert_expr(symbol const & name, expr * t) {
+    m_processing_pareto = false;
     if (!m_check_logic(t))
         throw cmd_exception(m_check_logic.get_last_error());
     if (!produce_unsat_cores() || name == symbol::null) {
@@ -1286,6 +1290,7 @@ static void restore(ast_manager & m, ptr_vector<expr> & c, unsigned old_sz) {
 }
 
 void cmd_context::restore_assertions(unsigned old_sz) {
+    m_processing_pareto = false;
     if (!has_manager()) {
         // restore_assertions invokes m(), so if cmd_context does not have a manager, it will try to create one.
         SASSERT(old_sz == m_assertions.size());
@@ -1303,6 +1308,7 @@ void cmd_context::restore_assertions(unsigned old_sz) {
 
 void cmd_context::pop(unsigned n) {
     m_check_sat_result = 0;
+    m_processing_pareto = false;
     if (n == 0)
         return;
     unsigned lvl     = m_scopes.size();
@@ -1333,7 +1339,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
     unsigned rlimit  = m_params.m_rlimit;
     scoped_watch sw(*this);
     lbool r;
-    bool was_pareto = false, was_opt = false;
+    bool was_opt = false;
 
     if (m_opt && !m_opt->empty()) {
         was_opt = true;
@@ -1342,21 +1348,15 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         scoped_ctrl_c ctrlc(eh);
         scoped_timer timer(timeout, &eh);
         scoped_rlimit _rlimit(m().limit(), rlimit);
-        ptr_vector<expr> cnstr(m_assertions);
-        cnstr.append(num_assumptions, assumptions);
-        get_opt()->set_hard_constraints(cnstr);
+        if (!m_processing_pareto) {
+            ptr_vector<expr> cnstr(m_assertions);
+            cnstr.append(num_assumptions, assumptions);
+            get_opt()->set_hard_constraints(cnstr);
+        }
         try {
             r = get_opt()->optimize();
-            while (r == l_true && get_opt()->is_pareto()) {
-                was_pareto = true;
-                get_opt()->display_assignment(regular_stream());
-                regular_stream() << "\n";
-                if (get_opt()->print_model()) {
-                    model_ref mdl;
-                    get_opt()->get_model(mdl);
-                    display_model(mdl);
-                }
-                r = get_opt()->optimize();
+            if (r == l_true && get_opt()->is_pareto()) {
+                m_processing_pareto = true;
             }
         }
         catch (z3_error & ex) {
@@ -1366,8 +1366,8 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
             get_opt()->display_assignment(regular_stream());
             throw cmd_exception(ex.msg());
         }
-        if (was_pareto && r == l_false) {
-            r = l_true;
+        if (m_processing_pareto && r != l_true) {
+            m_processing_pareto = false;
         }
         get_opt()->set_status(r);
     }
@@ -1400,7 +1400,7 @@ void cmd_context::check_sat(unsigned num_assumptions, expr * const * assumptions
         validate_model();
     }
     validate_check_sat_result(r);
-    if (was_opt && r != l_false && !was_pareto) {
+    if (was_opt && r != l_false && !m_processing_pareto) {
         get_opt()->display_assignment(regular_stream());
     }
 
diff --git a/src/cmd_context/cmd_context.h b/src/cmd_context/cmd_context.h
index 8885bc5d6..c72e2ac0e 100644
--- a/src/cmd_context/cmd_context.h
+++ b/src/cmd_context/cmd_context.h
@@ -123,7 +123,6 @@ public:
     virtual void display_assignment(std::ostream& out) = 0;
     virtual bool is_pareto() = 0;
     virtual void set_logic(symbol const& s) = 0;
-    virtual bool print_model() const = 0;
     virtual void get_box_model(model_ref& mdl, unsigned index) = 0;
     virtual void updt_params(params_ref const& p) = 0;
 };
@@ -161,6 +160,7 @@ protected:
     status                       m_status;
     bool                         m_numeral_as_real;
     bool                         m_ignore_check; // used by the API to disable check-sat() commands when parsing SMT 2.0 files.
+    bool                         m_processing_pareto; // used when re-entering check-sat for pareto front.
     bool                         m_exit_on_error;
     
     static std::ostringstream    g_error_stream;
diff --git a/src/muz/base/rule_properties.cpp b/src/muz/base/rule_properties.cpp
index 619f88e3b..518e848c4 100644
--- a/src/muz/base/rule_properties.cpp
+++ b/src/muz/base/rule_properties.cpp
@@ -50,7 +50,8 @@ void rule_properties::collect(rule_set const& rules) {
         }
         for (unsigned i = 0; m_inf_sort.empty() && i < r->get_decl()->get_arity(); ++i) {
             sort* d = r->get_decl()->get_domain(i);
-            if (!m.is_bool(d) && !m_dl.is_finite_sort(d) && !m_bv.is_bv_sort(d)) {
+            sort_size sz = d->get_num_elements();
+            if (!sz.is_finite()) {
                 m_inf_sort.push_back(m_rule);
             }
         }
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 834f4fa81..94313b13b 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -318,11 +318,6 @@ namespace opt {
         return r;
     }
 
-    bool context::print_model() const {
-        opt_params optp(m_params);
-        return optp.print_model();
-    }
-
     void context::get_base_model(model_ref& mdl) {
         mdl = m_model;
     }
diff --git a/src/opt/opt_context.h b/src/opt/opt_context.h
index 53bfc19c5..66f0ef015 100644
--- a/src/opt/opt_context.h
+++ b/src/opt/opt_context.h
@@ -183,7 +183,6 @@ namespace opt {
         virtual bool empty() { return m_scoped_state.m_objectives.empty(); }
         virtual void set_hard_constraints(ptr_vector<expr> & hard);
         virtual lbool optimize();
-        virtual bool print_model() const;
         virtual void set_model(model_ref& _m) { m_model = _m; }
         virtual void get_model(model_ref& _m);
         virtual void get_box_model(model_ref& _m, unsigned index);
diff --git a/src/opt/opt_params.pyg b/src/opt/opt_params.pyg
index 51f58396c..13bf51313 100644
--- a/src/opt/opt_params.pyg
+++ b/src/opt/opt_params.pyg
@@ -7,7 +7,6 @@ def_module_params('opt',
                           ('dump_benchmarks', BOOL, False, 'dump benchmarks for profiling'),
                           ('timeout', UINT, UINT_MAX, 'timeout (in milliseconds) (UINT_MAX and 0 mean no timeout)'),
                           ('rlimit', UINT, 0, 'resource limit (0 means no limit)'),
-                          ('print_model', BOOL, False, 'display model for satisfiable constraints'),
                           ('enable_sls', BOOL, False, 'enable SLS tuning during weighted maxsast'),
                           ('enable_sat', BOOL, True, 'enable the new SAT core for propositional constraints'),
                           ('elim_01', BOOL, True, 'eliminate 01 variables'),
diff --git a/src/sat/card_extension.h b/src/sat/card_extension.h
index 41219fae5..fbe1141b1 100644
--- a/src/sat/card_extension.h
+++ b/src/sat/card_extension.h
@@ -42,7 +42,8 @@ namespace sat {
             stats() { reset(); }
             void reset() { memset(this, 0, sizeof(*this)); }
         };
-        
+
+    public:        
         class card {
             unsigned       m_index;
             literal        m_lit;
@@ -105,6 +106,7 @@ namespace sat {
             void swap(unsigned i, unsigned j) { std::swap(m_lits[i], m_lits[j]); }
             void negate() { m_lits[0].neg(); }
         };
+    protected:
 
         struct ineq {
             literal_vector  m_lits;
@@ -304,6 +306,13 @@ namespace sat {
         void    add_at_least(bool_var v, literal_vector const& lits, unsigned k);
         void    add_pb_ge(bool_var v, svector<wliteral> const& wlits, unsigned k);
         void    add_xor(bool_var v, literal_vector const& lits);
+        unsigned num_pb() const { return m_pbs.size(); }
+        pb const&      get_pb(unsigned i) const { return *m_pbs[i]; }
+        unsigned num_card() const { return m_cards.size(); }
+        card const&    get_card(unsigned i) const { return *m_cards[i]; }
+        unsigned num_xor() const { return m_xors.size(); }
+        xor const&     get_xor(unsigned i) const { return *m_xors[i]; }
+
         virtual void propagate(literal l, ext_constraint_idx idx, bool & keep);
         virtual bool resolve_conflict();
         virtual void get_antecedents(literal l, ext_justification_idx idx, literal_vector & r);
diff --git a/src/sat/sat_config.cpp b/src/sat/sat_config.cpp
index 9d81ce886..3d803d164 100644
--- a/src/sat/sat_config.cpp
+++ b/src/sat/sat_config.cpp
@@ -126,6 +126,27 @@ namespace sat {
         m_drat_file       = p.drat_file();
         m_drat            = (m_drat_check || m_drat_file != symbol("")) && p.threads() == 1;
         m_dyn_sub_res     = p.dyn_sub_res();
+
+        // Parameters used in Liang, Ganesh, Poupart, Czarnecki AAAI 2016.
+        m_branching_heuristic = BH_VSIDS;
+        if (p.branching_heuristic() == symbol("vsids")) {
+            m_branching_heuristic = BH_VSIDS;
+        }
+        else if (p.branching_heuristic() == symbol("chb")) {
+            m_branching_heuristic = BH_CHB;
+        }
+        else if (p.branching_heuristic() == symbol("lrb")) {
+            m_branching_heuristic = BH_LRB;
+        }
+        else {
+            throw sat_param_exception("invalid branching heuristic: accepted heuristics are 'vsids', 'lrb' or 'chb'");
+        }
+        m_anti_exploration = m_branching_heuristic != BH_VSIDS;
+        m_step_size_init = 0.40;
+        m_step_size_dec  = 0.000001;
+        m_step_size_min  = 0.06;
+        m_reward_multiplier = 0.9;
+        m_reward_offset = 1000000.0;
     }
 
     void config::collect_param_descrs(param_descrs & r) {
diff --git a/src/sat/sat_config.h b/src/sat/sat_config.h
index a34384e87..d8b0bc7d2 100644
--- a/src/sat/sat_config.h
+++ b/src/sat/sat_config.h
@@ -44,6 +44,12 @@ namespace sat {
         GC_PSM_GLUE
     };
 
+    enum branching_heuristic {
+        BH_VSIDS,
+        BH_CHB,
+        BH_LRB
+    };
+
     struct config {
         unsigned long long m_max_memory;
         phase_selection    m_phase;
@@ -95,6 +101,14 @@ namespace sat {
         symbol             m_glue_psm;        
         symbol             m_psm_glue;        
         
+        // branching heuristic settings.
+        branching_heuristic m_branching_heuristic;
+        bool               m_anti_exploration;
+        double             m_step_size_init;
+        double             m_step_size_dec;
+        double             m_step_size_min;
+        double             m_reward_multiplier;
+        double             m_reward_offset;
         config(params_ref const & p);
         void updt_params(params_ref const & p);
         static void collect_param_descrs(param_descrs & d);
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index aae99c28f..a875bad6c 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -46,7 +46,7 @@ namespace sat {
         virtual std::ostream& display(std::ostream& out) const = 0;
         virtual std::ostream& display_justification(std::ostream& out, ext_justification_idx idx) const = 0;
         virtual void collect_statistics(statistics& st) const = 0;
-        virtual extension* copy(solver* s) = 0;
+        virtual extension* copy(solver* s) = 0;       
         virtual void find_mutexes(literal_vector& lits, vector<literal_vector> & mutexes) = 0;
     };
 
diff --git a/src/sat/sat_lookahead.h b/src/sat/sat_lookahead.h
index d56d864dd..6708e61f5 100644
--- a/src/sat/sat_lookahead.h
+++ b/src/sat/sat_lookahead.h
@@ -384,6 +384,7 @@ namespace sat {
             candidate(bool_var v, float r): m_var(v), m_rating(r) {}
         };
         svector<candidate> m_candidates;
+        uint_set           m_select_lookahead_vars;
 
         float get_rating(bool_var v) const { return m_rating[v]; }
         float get_rating(literal l) const { return get_rating(l.var()); }
@@ -468,7 +469,11 @@ namespace sat {
             for (bool_var const* it = m_freevars.begin(), * end = m_freevars.end(); it != end; ++it) {
                 SASSERT(is_undef(*it));
                 bool_var x = *it;
-                if (newbies || active_prefix(x)) {
+                if (!m_select_lookahead_vars.empty() && m_select_lookahead_vars.contains(x)) {
+                    m_candidates.push_back(candidate(x, m_rating[x]));
+                    sum += m_rating[x];                
+                }
+                else if (newbies || active_prefix(x)) {
                     m_candidates.push_back(candidate(x, m_rating[x]));
                     sum += m_rating[x];                
                 }           
@@ -1857,6 +1862,31 @@ namespace sat {
             return search();
         }
 
+        literal select_lookahead(bool_var_vector const& vars) {
+            m_search_mode = lookahead_mode::searching;
+            scoped_level _sl(*this, c_fixed_truth);
+            init();                
+            if (inconsistent()) return null_literal;
+            inc_istamp();            
+            for (auto v : vars) {
+                m_select_lookahead_vars.insert(v);
+            }
+            literal l = choose();
+            m_select_lookahead_vars.reset();
+            if (inconsistent()) return null_literal;
+
+            // assign unit literals that were found during search for lookahead.
+            unsigned num_assigned = 0;
+            for (literal lit : m_trail) {
+                if (!m_s.was_eliminated(lit.var()) && m_s.value(lit) != l_true) {
+                    m_s.assign(lit, justification());
+                    ++num_assigned;
+                }
+            }
+            IF_VERBOSE(1, verbose_stream() << "(sat-lookahead :units " << num_assigned << ")\n";);
+            return l;
+        }
+
         /**
            \brief simplify set of clauses by extracting units from a lookahead at base level.
          */
diff --git a/src/sat/sat_params.pyg b/src/sat/sat_params.pyg
index 2c09ecdc1..c60ceee07 100644
--- a/src/sat/sat_params.pyg
+++ b/src/sat/sat_params.pyg
@@ -9,6 +9,7 @@ def_module_params('sat',
                           ('restart.initial', UINT, 100, 'initial restart (number of conflicts)'),
                           ('restart.max', UINT, UINT_MAX, 'maximal number of restarts.'),
                           ('restart.factor', DOUBLE, 1.5, 'restart increment factor for geometric strategy'),
+                          ('branching.heuristic', SYMBOL, 'vsids', 'branching heuristic vsids, lrb or chb'),
                           ('random_freq', DOUBLE, 0.01, 'frequency of random case splits'),
                           ('random_seed', UINT, 0, 'random seed'),
                           ('burst_search', UINT, 100, 'number of conflicts before first global simplification'),
@@ -21,8 +22,7 @@ def_module_params('sat',
                           ('minimize_lemmas', BOOL, True, 'minimize learned clauses'),
                           ('dyn_sub_res', BOOL, True, 'dynamic subsumption resolution for minimizing learned clauses'),
                           ('core.minimize', BOOL, False, 'minimize computed core'),
-                          ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),
-                          ('threads', UINT, 1, 'number of parallel threads to use'),
+                          ('core.minimize_partial', BOOL, False, 'apply partial (cheap) core minimization'),                                                  ('threads', UINT, 1, 'number of parallel threads to use'),
                           ('dimacs.core', BOOL, False, 'extract core from DIMACS benchmarks'),
                           ('drat.file', SYMBOL, '', 'file to dump DRAT proofs'),
                           ('drat.check', BOOL, False, 'build up internal proof and check'),
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 0e1e771d6..a3383ed55 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -175,6 +175,11 @@ namespace sat {
         m_phase.push_back(PHASE_NOT_AVAILABLE);
         m_prev_phase.push_back(PHASE_NOT_AVAILABLE);
         m_assigned_since_gc.push_back(false);
+        m_last_conflict.push_back(0);
+        m_last_propagation.push_back(0);
+        m_participated.push_back(0);
+        m_canceled.push_back(0);
+        m_reasoned.push_back(0);
         m_case_split_queue.mk_var_eh(v);
         m_simplifier.insert_elim_todo(v);
         SASSERT(!was_eliminated(v));
@@ -581,6 +586,29 @@ namespace sat {
         if (m_ext && m_external[v])
             m_ext->asserted(l);
 
+        switch (m_config.m_branching_heuristic) {
+        case BH_VSIDS: 
+            break;
+        case BH_CHB:
+            m_last_propagation[v] = m_stats.m_conflict;
+            break;
+        case BH_LRB: 
+            m_participated[v] = 0;
+            m_reasoned[v] = 0;
+            break;
+        }
+        if (m_config.m_anti_exploration) {
+            uint64 age = m_stats.m_conflict - m_canceled[v];
+            if (age > 0) {
+                double decay = pow(0.95, age);
+                m_activity[v] = static_cast<unsigned>(m_activity[v] * decay);
+                // NB. MapleSAT does not update canceled.
+                m_canceled[v] = m_stats.m_conflict;
+                m_case_split_queue.activity_changed_eh(v, false);
+            }
+        }
+
+
         SASSERT(!l.sign() || m_phase[v] == NEG_PHASE);
         SASSERT(l.sign()  || m_phase[v] == POS_PHASE);
 
@@ -772,12 +800,26 @@ namespace sat {
     }
 
     bool solver::propagate(bool update) {
+        unsigned qhead = m_qhead;
         bool r = propagate_core(update);
+        if (m_config.m_branching_heuristic == BH_CHB) {
+            update_chb_activity(r, qhead);
+        }
         CASSERT("sat_propagate", check_invariant());
         CASSERT("sat_missed_prop", check_missed_propagation());
         return r;
     }
 
+    literal solver::select_lookahead(bool_var_vector const& vars) {
+        lookahead lh(*this);
+        literal result = lh.select_lookahead(vars);
+        if (result == null_literal) {
+            set_conflict(justification());
+        }
+        // extract unit literals from lh
+        return result;
+    }
+
     // -----------------------
     //
     // Search
@@ -1065,6 +1107,18 @@ namespace sat {
         }
 
         while (!m_case_split_queue.empty()) {
+            if (m_config.m_anti_exploration) {
+                next = m_case_split_queue.min_var();
+                auto age = m_stats.m_conflict - m_canceled[next];
+                while (age > 0) {
+                    double decay = pow(0.95, age);
+                    m_activity[next] = static_cast<unsigned>(m_activity[next] * pow(0.95, age));
+                    m_case_split_queue.activity_changed_eh(next, false);
+                    m_canceled[next] = m_stats.m_conflict;
+                    next = m_case_split_queue.min_var();
+                    age = m_stats.m_conflict - m_canceled[next];                    
+                }
+            }
             next = m_case_split_queue.next_var();
             if (value(next) == l_undef && !was_eliminated(next))
                 return next;
@@ -1829,6 +1883,9 @@ namespace sat {
         m_conflicts_since_restart++;
         m_conflicts_since_gc++;
         m_stats.m_conflict++;
+        if (m_step_size > m_config.m_step_size_min) {
+            m_step_size -= m_config.m_step_size_dec;
+        }
 
         m_conflict_lvl = get_max_lvl(m_not_l, m_conflict);
         TRACE("sat", tout << "conflict detected at level " << m_conflict_lvl << " for ";
@@ -2176,7 +2233,16 @@ namespace sat {
         SASSERT(var < num_vars());
         if (!is_marked(var) && var_lvl > 0) {
             mark(var);
-            inc_activity(var);
+            switch (m_config.m_branching_heuristic) {
+            case BH_VSIDS:
+                inc_activity(var);
+                break;
+            case BH_CHB:
+                m_last_conflict[var] = m_stats.m_conflict;
+                break;
+            default:
+                break;
+            }
             if (var_lvl == m_conflict_lvl)
                 num_marks++;
             else
@@ -2432,6 +2498,9 @@ namespace sat {
        \brief Reset the mark of the variables in the current lemma.
     */
     void solver::reset_lemma_var_marks() {
+        if (m_config.m_branching_heuristic == BH_LRB) {
+            update_lrb_reasoned();
+        }        
         literal_vector::iterator it  = m_lemma.begin();
         literal_vector::iterator end = m_lemma.end();
         SASSERT(!is_marked((*it).var()));
@@ -2442,6 +2511,58 @@ namespace sat {
         }
     }
 
+    void solver::update_lrb_reasoned() {
+        unsigned sz = m_lemma.size();
+        SASSERT(!is_marked(m_lemma[0].var()));
+        mark(m_lemma[0].var());
+        for (unsigned i = m_lemma.size(); i > 0; ) {
+            --i;
+            justification js = m_justification[m_lemma[i].var()];
+            switch (js.get_kind()) {
+            case justification::NONE:
+                break;                    
+            case justification::BINARY:
+                update_lrb_reasoned(js.get_literal());
+                break;
+            case justification::TERNARY:
+                update_lrb_reasoned(js.get_literal1());
+                update_lrb_reasoned(js.get_literal2());
+                break;
+            case justification::CLAUSE: {
+                clause & c = *(m_cls_allocator.get_clause(js.get_clause_offset()));
+                for (unsigned i = 0; i < c.size(); ++i) {
+                    update_lrb_reasoned(c[i]);
+                }
+                break;
+            }
+            case justification::EXT_JUSTIFICATION: {
+                fill_ext_antecedents(m_lemma[i], js);
+                literal_vector::iterator it  = m_ext_antecedents.begin();
+                literal_vector::iterator end = m_ext_antecedents.end();
+                for (; it != end; ++it) {
+                    update_lrb_reasoned(*it);
+                }
+                break;
+            }
+            }
+        }
+        reset_mark(m_lemma[0].var());
+        for (unsigned i = m_lemma.size(); i > sz; ) {
+            --i;
+            reset_mark(m_lemma[i].var());
+        }
+        m_lemma.shrink(sz);
+    }
+
+    void solver::update_lrb_reasoned(literal lit) {
+        bool_var v = lit.var();
+        if (!is_marked(v)) {
+            mark(v);
+            m_reasoned[v]++;
+            m_lemma.push_back(lit);
+        }
+    }
+
     /**
        \brief Apply dynamic subsumption resolution to new lemma.
        Only binary and ternary clauses are used.
@@ -2618,6 +2739,18 @@ namespace sat {
             bool_var v = l.var();
             SASSERT(value(v) == l_undef);
             m_case_split_queue.unassign_var_eh(v);
+            if (m_config.m_branching_heuristic == BH_LRB) {
+                uint64 interval = m_stats.m_conflict - m_last_propagation[v];
+                if (interval > 0) {
+                    auto activity = m_activity[v];
+                    auto reward = (m_config.m_reward_offset * (m_participated[v] + m_reasoned[v])) / interval;
+                    m_activity[v] = static_cast<unsigned>(m_step_size * reward + ((1 - m_step_size) * activity));
+                    m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity);
+                }
+            }
+            if (m_config.m_anti_exploration) {
+                m_canceled[v] = m_stats.m_conflict;
+            }
         }
         m_trail.shrink(old_sz);
         m_qhead = old_sz;
@@ -2800,6 +2933,8 @@ namespace sat {
         m_probing.updt_params(p);
         m_scc.updt_params(p);
         m_rand.set_seed(m_config.m_random_seed);
+
+        m_step_size = m_config.m_step_size_init;
     }
 
     void solver::collect_param_descrs(param_descrs & d) {
@@ -2837,6 +2972,7 @@ namespace sat {
     // -----------------------
 
     void solver::rescale_activity() {
+        SASSERT(m_config.m_branching_heuristic == BH_VSIDS);
         svector<unsigned>::iterator it  = m_activity.begin();
         svector<unsigned>::iterator end = m_activity.end();
         for (; it != end; ++it) {
@@ -2845,6 +2981,18 @@ namespace sat {
         m_activity_inc >>= 14;
     }
 
+    void solver::update_chb_activity(bool is_sat, unsigned qhead) {
+        SASSERT(m_config.m_branching_heuristic == BH_CHB);
+        double multiplier = m_config.m_reward_offset * (is_sat ? m_config.m_reward_multiplier : 1.0);
+        for (unsigned i = qhead; i < m_trail.size(); ++i) {
+            auto v = m_trail[i].var();
+            auto reward = multiplier / (m_stats.m_conflict - m_last_conflict[v] + 1);
+            auto activity = m_activity[v];
+            m_activity[v] = static_cast<unsigned>(m_step_size * reward + ((1.0 - m_step_size) * activity));
+            m_case_split_queue.activity_changed_eh(v, m_activity[v] > activity);
+        }
+    }
+
     // -----------------------
     //
     // Iterators
diff --git a/src/sat/sat_solver.h b/src/sat/sat_solver.h
index 0429fe624..54ea360e4 100644
--- a/src/sat/sat_solver.h
+++ b/src/sat/sat_solver.h
@@ -110,8 +110,17 @@ namespace sat {
         svector<char>           m_eliminated;
         svector<char>           m_external;
         svector<unsigned>       m_level; 
+        // branch variable selection:
         svector<unsigned>       m_activity;
         unsigned                m_activity_inc;
+        svector<uint64>         m_last_conflict;
+        svector<uint64>         m_last_propagation;
+        svector<uint64>         m_participated;
+        svector<uint64>         m_canceled;
+        svector<uint64>         m_reasoned;
+        int                     m_action;
+        double                  m_step_size;
+        // phase
         svector<char>           m_phase; 
         svector<char>           m_prev_phase;
         svector<char>           m_assigned_since_gc;
@@ -300,7 +309,7 @@ namespace sat {
         }
         void set_par(parallel* p, unsigned id);
         bool canceled() { return !m_rlimit.inc(); }
-        config const& get_config() { return m_config; }
+        config const& get_config() const { return m_config; }
         extension* get_extension() const { return m_ext.get(); }
         void       set_extension(extension* e);
         typedef std::pair<literal, literal> bin_clause;
@@ -343,6 +352,8 @@ namespace sat {
         model_converter const & get_model_converter() const { return m_mc; }
         void set_model(model const& mdl);
 
+        literal select_lookahead(bool_var_vector const& vars);
+
     protected:
         unsigned m_conflicts;
         unsigned m_restarts;
@@ -555,6 +566,12 @@ namespace sat {
     private:
         void rescale_activity();
 
+        void update_chb_activity(bool is_sat, unsigned qhead);
+
+        void update_lrb_reasoned();
+
+        void update_lrb_reasoned(literal lit);
+
         // -----------------------
         //
         // Iterators
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 0d12c0a94..225fd8d63 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -66,7 +66,11 @@ class inc_sat_solver : public solver {
     expr_dependency_ref m_dep_core;
     svector<double>     m_weights;
     std::string         m_unknown;
-
+    // access formulas after they have been pre-processed and handled by the sat solver.
+    // this allows to access the internal state of the SAT solver and carry on partial results.
+    bool                m_internalized;           // are formulas internalized?
+    bool                m_internalized_converted; // have internalized formulas been converted back
+    expr_ref_vector     m_internalized_fmls;      // formulas in internalized format
 
     typedef obj_map<expr, sat::literal> dep2asm_t;
 public:
@@ -81,7 +85,10 @@ public:
         m_map(m),
         m_num_scopes(0),
         m_dep_core(m),
-        m_unknown("no reason given") {
+        m_unknown("no reason given"),
+        m_internalized(false), 
+        m_internalized_converted(false), 
+        m_internalized_fmls(m) {
         updt_params(p);
         init_preprocess();
     }
@@ -141,6 +148,8 @@ public:
         if (r != l_true) return r;
         r = internalize_assumptions(sz, assumptions, dep2asm);
         if (r != l_true) return r;
+        m_internalized = true;
+        m_internalized_converted = false;
 
         r = m_solver.check(m_asms.size(), m_asms.c_ptr());
         
@@ -170,8 +179,11 @@ public:
         m_fmls_head_lim.push_back(m_fmls_head);
         if (m_bb_rewriter) m_bb_rewriter->push();
         m_map.push();
+        m_internalized = true;
+        m_internalized_converted = false;
     }
     virtual void pop(unsigned n) {
+        m_internalized = false;
         if (n > m_num_scopes) {   // allow inc_sat_solver to
             n = m_num_scopes;     // take over for another solver.
         }
@@ -204,6 +216,7 @@ public:
     }
     virtual ast_manager& get_manager() const { return m; }
     virtual void assert_expr(expr * t) {
+        m_internalized = false;
         TRACE("goal2sat", tout << mk_pp(t, m) << "\n";);
         m_fmls.push_back(t);
     }
@@ -242,6 +255,28 @@ public:
         return 0;
     }
 
+    virtual expr_ref lookahead(expr_ref_vector const& candidates) { 
+        sat::bool_var_vector vars;
+        u_map<expr*> var2candidate;
+        for (auto c : candidates) {
+            // TBD: check membership
+            sat::bool_var v = m_map.to_bool_var(c);
+            SASSERT(v != sat::null_bool_var);
+            vars.push_back(v);
+            var2candidate.insert(v, c);
+        }
+        sat::literal l = m_solver.select_lookahead(vars);
+        if (l == sat::null_literal) {
+            return expr_ref(m.mk_true(), m);
+        }
+        expr* e;
+        if (!var2candidate.find(l.var(), e)) {
+            // TBD: if candidate set is empty, then do something else.
+            e = m.mk_true();
+        }
+        return expr_ref(l.sign() ? m.mk_not(e) : e, m);
+    }
+
     virtual lbool get_consequences_core(expr_ref_vector const& assumptions, expr_ref_vector const& vars, expr_ref_vector& conseq) {
         init_preprocess();
         TRACE("sat", tout << assumptions << "\n" << vars << "\n";);
@@ -320,9 +355,18 @@ public:
     virtual void get_labels(svector<symbol> & r) {
     }
     virtual unsigned get_num_assertions() const {
-        return m_fmls.size();
+        const_cast<inc_sat_solver*>(this)->convert_internalized();
+        if (m_internalized && m_internalized_converted) {            
+            return m_internalized_fmls.size();
+        }
+        else {
+            return m_fmls.size();
+        }
     }
     virtual expr * get_assertion(unsigned idx) const {
+        if (m_internalized && m_internalized_converted) {
+            return m_internalized_fmls[idx];
+        }
         return m_fmls[idx];
     }
     virtual unsigned get_num_assumptions() const {
@@ -332,6 +376,32 @@ public:
         return m_asmsf[idx];
     }
 
+    void convert_internalized() {
+        if (!m_internalized) return;
+        sat2goal s2g;
+        model_converter_ref mc;
+        goal g(m, false, false, false);
+        s2g(m_solver, m_map, m_params, g, mc);
+        extract_model();
+        if (!m_model) {
+            m_model = alloc(model, m);
+        }
+        model_ref mdl = m_model;
+        if (m_mc) (*m_mc)(mdl);
+        for (unsigned i = 0; i < mdl->get_num_constants(); ++i) {
+            func_decl* c = mdl->get_constant(i);
+            expr_ref eq(m.mk_eq(m.mk_const(c), mdl->get_const_interp(c)), m);
+            g.assert_expr(eq);
+        }
+        m_internalized_fmls.reset();
+        g.get_formulas(m_internalized_fmls);
+        // g.display(std::cout);
+        m_internalized_converted = true;
+ //       if (mc) mc->display(std::cout << "mc");
+ //       if (m_mc) m_mc->display(std::cout << "m_mc\n");
+ //       if (m_mc0) m_mc0->display(std::cout << "m_mc0\n");
+    }
+
     void init_preprocess() {
         if (m_preprocess) {
             m_preprocess->reset();
@@ -374,7 +444,7 @@ private:
         init_preprocess();
         SASSERT(g->models_enabled());
         SASSERT(!g->proofs_enabled());
-        TRACE("goal2sat", g->display(tout););
+        TRACE("sat", g->display(tout););
         try {
             (*m_preprocess)(g, m_subgoals, m_mc, m_pc, m_dep_core);
         }
@@ -391,7 +461,7 @@ private:
         }
         g = m_subgoals[0];
         expr_ref_vector atoms(m);
-        TRACE("goal2sat", g->display_with_dependencies(tout););
+        TRACE("sat", g->display_with_dependencies(tout););
         m_goal2sat(*g, m_params, m_solver, m_map, dep2asm, true);
         m_goal2sat.get_interpreted_atoms(atoms);
         if (!atoms.empty()) {
diff --git a/src/sat/sat_var_queue.h b/src/sat/sat_var_queue.h
index f008fbb88..97e7b64f0 100644
--- a/src/sat/sat_var_queue.h
+++ b/src/sat/sat_var_queue.h
@@ -39,6 +39,15 @@ namespace sat {
                 m_queue.decreased(v);
         }
 
+        void activity_changed_eh(bool_var v, bool up) {
+            if (m_queue.contains(v)) {
+                if (up) 
+                    m_queue.decreased(v);
+                else 
+                    m_queue.increased(v);
+            }
+        }
+
         void mk_var_eh(bool_var v) {
             m_queue.reserve(v+1);
             m_queue.insert(v);
@@ -61,6 +70,8 @@ namespace sat {
         bool empty() const { return m_queue.empty(); }
 
         bool_var next_var() { SASSERT(!empty()); return m_queue.erase_min(); }
+
+        bool_var min_var() { SASSERT(!empty()); return m_queue.min_value(); }
     };
 };
 
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 9d07ec3e6..6604bab89 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -137,7 +137,7 @@ struct goal2sat::imp {
                 sat::bool_var v = m_solver.mk_var(ext);
                 m_map.insert(t, v);
                 l = sat::literal(v, sign);
-                TRACE("goal2sat", tout << "new_var: " << v << "\n" << mk_ismt2_pp(t, m) << "\n";);
+                TRACE("sat", tout << "new_var: " << v << ": " << mk_ismt2_pp(t, m) << "\n";);
                 if (ext && !is_uninterp_const(t)) {
                     m_interpreted_atoms.push_back(t);
                 }
@@ -993,6 +993,7 @@ struct sat2goal::imp {
     expr_ref_vector         m_lit2expr;
     unsigned long long      m_max_memory;
     bool                    m_learned;
+    unsigned                m_glue;
     
     imp(ast_manager & _m, params_ref const & p):m(_m), m_lit2expr(m) {
         updt_params(p);
@@ -1000,6 +1001,7 @@ struct sat2goal::imp {
 
     void updt_params(params_ref const & p) {
         m_learned        = p.get_bool("learned", false);
+        m_glue           = p.get_uint("glue", UINT_MAX);
         m_max_memory     = megabytes_to_bytes(p.get_uint("max_memory", UINT_MAX));
     }
 
@@ -1042,20 +1044,71 @@ struct sat2goal::imp {
         return m_lit2expr.get(l.index());
     }
 
-    void assert_clauses(sat::clause * const * begin, sat::clause * const * end, goal & r) {
+    void assert_pb(goal& r, sat::card_extension::pb const& p) {
+        pb_util pb(m);
+        ptr_buffer<expr> lits;
+        vector<rational> coeffs;
+        for (unsigned i = 0; i < p.size(); ++i) {
+            lits.push_back(lit2expr(p[i].second));
+            coeffs.push_back(rational(p[i].first));
+        }
+        rational k(p.k());
+        expr_ref fml(pb.mk_ge(p.size(), coeffs.c_ptr(), lits.c_ptr(), k), m);
+        
+        if (p.lit() != sat::null_literal) {
+            fml = m.mk_eq(lit2expr(p.lit()), fml);            
+        }
+        r.assert_expr(fml);
+    }
+
+    void assert_card(goal& r, sat::card_extension::card const& c) {
+        pb_util pb(m);
+        ptr_buffer<expr> lits;
+        for (unsigned i = 0; i < c.size(); ++i) {
+            lits.push_back(lit2expr(c[i]));
+        }
+        expr_ref fml(pb.mk_at_most_k(c.size(), lits.c_ptr(), c.k()), m);
+        
+        if (c.lit() != sat::null_literal) {
+            fml = m.mk_eq(lit2expr(c.lit()), fml);            
+        }
+        r.assert_expr(fml);
+    }
+
+    void assert_xor(goal & r, sat::card_extension::xor const& x) {
+        ptr_buffer<expr> lits;
+        for (unsigned i = 0; i < x.size(); ++i) {
+            lits.push_back(lit2expr(x[i]));
+        }
+        expr_ref fml(m.mk_xor(x.size(), lits.c_ptr()), m);
+        
+        if (x.lit() != sat::null_literal) {
+            fml = m.mk_eq(lit2expr(x.lit()), fml);            
+        }
+        r.assert_expr(fml);
+    }
+
+    void assert_clauses(sat::solver const & s, sat::clause * const * begin, sat::clause * const * end, goal & r, bool asserted) {
         ptr_buffer<expr> lits;
         for (sat::clause * const * it = begin; it != end; it++) {
             checkpoint();
             lits.reset();
             sat::clause const & c = *(*it);
             unsigned sz = c.size();
-            for (unsigned i = 0; i < sz; i++) {
-                lits.push_back(lit2expr(c[i]));
+            if (asserted || m_learned || c.glue() <= s.get_config().m_gc_small_lbd) {
+                for (unsigned i = 0; i < sz; i++) {
+                    lits.push_back(lit2expr(c[i]));
+                }
+                r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
             }
-            r.assert_expr(m.mk_or(lits.size(), lits.c_ptr()));
         }
     }
 
+    sat::card_extension* get_card_extension(sat::solver const& s) {
+        sat::extension* ext = s.get_extension();
+        return dynamic_cast<sat::card_extension*>(ext);
+    }
+
     void operator()(sat::solver const & s, atom2bool_var const & map, goal & r, model_converter_ref & mc) {
         if (s.inconsistent()) {
             r.assert_expr(m.mk_false());
@@ -1087,9 +1140,22 @@ struct sat2goal::imp {
             r.assert_expr(m.mk_or(lit2expr(it->first), lit2expr(it->second)));
         }
         // collect clauses
-        assert_clauses(s.begin_clauses(), s.end_clauses(), r);
-        if (m_learned)
-            assert_clauses(s.begin_learned(), s.end_learned(), r);
+        assert_clauses(s, s.begin_clauses(), s.end_clauses(), r, true);
+        assert_clauses(s, s.begin_learned(), s.end_learned(), r, false);
+
+        // TBD: collect assertions from plugin
+        sat::card_extension* ext = get_card_extension(s);
+        if (ext) {
+            for (unsigned i = 0; i < ext->num_pb(); ++i) {
+                assert_pb(r, ext->get_pb(i));
+            }
+            for (unsigned i = 0; i < ext->num_card(); ++i) {
+                assert_card(r, ext->get_card(i));
+            }
+            for (unsigned i = 0; i < ext->num_xor(); ++i) {
+                assert_xor(r, ext->get_xor(i));
+            }
+        }
     }
 
 };
@@ -1100,6 +1166,7 @@ sat2goal::sat2goal():m_imp(0) {
 void sat2goal::collect_param_descrs(param_descrs & r) {
     insert_max_memory(r);
     r.insert("learned", CPK_BOOL, "(default: false) collect also learned clauses.");
+    r.insert("glue", CPK_UINT, "(default: max-int) collect learned clauses with glue level below parameter.");
 }
 
 struct sat2goal::scoped_set_imp {
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index 6598c3a05..b329a4cd8 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -43,7 +43,7 @@ Revision History:
 #include"quasi_macros.h"
 
 asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
-    m_manager(m),
+    m(m),
     m_params(p),
     m_pre_simplifier(m),
     m_simplifier(m),
@@ -63,7 +63,7 @@ asserted_formulas::asserted_formulas(ast_manager & m, smt_params & p):
     setup_simplifier_plugins(m_simplifier, m_bsimp, arith_simp, m_bvsimp);
     SASSERT(m_bsimp != 0);
     SASSERT(arith_simp != 0);
-    m_macro_finder = alloc(macro_finder, m_manager, m_macro_manager);
+    m_macro_finder = alloc(macro_finder, m, m_macro_manager);
 
     basic_simplifier_plugin * basic_simp = 0;
     bv_simplifier_plugin * bv_simp = 0;
@@ -90,16 +90,16 @@ void asserted_formulas::setup() {
 }
 
 void asserted_formulas::setup_simplifier_plugins(simplifier & s, basic_simplifier_plugin * & bsimp, arith_simplifier_plugin * & asimp, bv_simplifier_plugin * & bvsimp) {
-    bsimp = alloc(basic_simplifier_plugin, m_manager);
+    bsimp = alloc(basic_simplifier_plugin, m);
     s.register_plugin(bsimp);
-    asimp = alloc(arith_simplifier_plugin, m_manager, *bsimp, m_params);
+    asimp = alloc(arith_simplifier_plugin, m, *bsimp, m_params);
     s.register_plugin(asimp);
-    s.register_plugin(alloc(array_simplifier_plugin, m_manager, *bsimp, s, m_params));
-    bvsimp = alloc(bv_simplifier_plugin, m_manager, *bsimp, m_params);
+    s.register_plugin(alloc(array_simplifier_plugin, m, *bsimp, s, m_params));
+    bvsimp = alloc(bv_simplifier_plugin, m, *bsimp, m_params);
     s.register_plugin(bvsimp);
-    s.register_plugin(alloc(datatype_simplifier_plugin, m_manager, *bsimp));    
-    s.register_plugin(alloc(fpa_simplifier_plugin, m_manager, *bsimp));
-    s.register_plugin(alloc(seq_simplifier_plugin, m_manager, *bsimp));
+    s.register_plugin(alloc(datatype_simplifier_plugin, m, *bsimp));    
+    s.register_plugin(alloc(fpa_simplifier_plugin, m, *bsimp));
+    s.register_plugin(alloc(seq_simplifier_plugin, m, *bsimp));
 }
 
 void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, proof * const * prs) {
@@ -108,7 +108,7 @@ void asserted_formulas::init(unsigned num_formulas, expr * const * formulas, pro
     SASSERT(!m_inconsistent);
     SASSERT(m_scopes.empty());
     m_asserted_formulas.append(num_formulas, formulas);
-    if (m_manager.proofs_enabled())
+    if (m.proofs_enabled())
         m_asserted_formula_prs.append(num_formulas, prs);
 }
 
@@ -125,9 +125,9 @@ void asserted_formulas::push_assertion(expr * e, proof * pr, expr_ref_vector & r
         SASSERT(!result.empty());
         return;
     }
-    if (m_manager.is_false(e))
+    if (m.is_false(e))
         m_inconsistent = true;
-    ::push_assertion(m_manager, e, pr, result, result_prs);
+    ::push_assertion(m, e, pr, result, result_prs);
 }
 
 void asserted_formulas::set_eliminate_and(bool flag) {
@@ -145,13 +145,13 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
         push_assertion(e, _in_pr, m_asserted_formulas, m_asserted_formula_prs);
         return;
     }
-    proof_ref  in_pr(_in_pr, m_manager);
-    expr_ref   r1(m_manager);
-    proof_ref  pr1(m_manager);
-    expr_ref   r2(m_manager);
-    proof_ref  pr2(m_manager);
-    TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m_manager) << "\n";);
-    TRACE("assert_expr_bug", tout << mk_pp(e, m_manager) << "\n";);
+    proof_ref  in_pr(_in_pr, m);
+    expr_ref   r1(m);
+    proof_ref  pr1(m);
+    expr_ref   r2(m);
+    proof_ref  pr2(m);
+    TRACE("assert_expr_before_simp", tout << mk_ll_pp(e, m) << "\n";);
+    TRACE("assert_expr_bug", tout << mk_pp(e, m) << "\n";);
     if (m_params.m_pre_simplifier) {
         m_pre_simplifier(e, r1, pr1);
     }
@@ -161,14 +161,14 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
     }
     set_eliminate_and(false); // do not eliminate and before nnf.
     m_simplifier(r1, r2, pr2);
-    TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m_manager) << "\n";);
-    if (m_manager.proofs_enabled()) {
+    TRACE("assert_expr_bug", tout << "after...\n" << mk_pp(r1, m) << "\n";);
+    if (m.proofs_enabled()) {
         if (e == r2)
             pr2 = in_pr;
         else
-            pr2 = m_manager.mk_modus_ponens(in_pr, m_manager.mk_transitivity(pr1, pr2));
+            pr2 = m.mk_modus_ponens(in_pr, m.mk_transitivity(pr1, pr2));
     }
-    TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m_manager) << "\n";);
+    TRACE("assert_expr_after_simp", tout << mk_ll_pp(r1, m) << "\n";);
     push_assertion(r2, pr2, m_asserted_formulas, m_asserted_formula_prs);
     TRACE("asserted_formulas_bug", tout << "after assert_expr\n"; display(tout););
 }
@@ -176,7 +176,7 @@ void asserted_formulas::assert_expr(expr * e, proof * _in_pr) {
 void asserted_formulas::assert_expr(expr * e) {
     if (inconsistent()) 
         return;
-    assert_expr(e, m_manager.mk_asserted(e));
+    assert_expr(e, m.mk_asserted(e));
 }
 
 void asserted_formulas::get_assertions(ptr_vector<expr> & result) {
@@ -184,13 +184,13 @@ void asserted_formulas::get_assertions(ptr_vector<expr> & result) {
 }
 
 void asserted_formulas::push_scope() {
-    SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m_manager.canceled());
+    SASSERT(inconsistent() || m_asserted_qhead == m_asserted_formulas.size() || m.canceled());
     TRACE("asserted_formulas_scopes", tout << "push:\n"; display(tout););
     m_scopes.push_back(scope());
     m_macro_manager.push_scope();
     scope & s = m_scopes.back();
     s.m_asserted_formulas_lim    = m_asserted_formulas.size();
-    SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m_manager.canceled());
+    SASSERT(inconsistent() || s.m_asserted_formulas_lim == m_asserted_qhead || m.canceled());
     s.m_inconsistent_old         = m_inconsistent;
     m_defined_names.push();
     m_bv_sharing.push_scope();
@@ -206,7 +206,7 @@ void asserted_formulas::pop_scope(unsigned num_scopes) {
     m_inconsistent      = s.m_inconsistent_old;
     m_defined_names.pop(num_scopes);
     m_asserted_formulas.shrink(s.m_asserted_formulas_lim);
-    if (m_manager.proofs_enabled())
+    if (m.proofs_enabled())
         m_asserted_formula_prs.shrink(s.m_asserted_formulas_lim);
     m_asserted_qhead    = s.m_asserted_formulas_lim;
     m_scopes.shrink(new_lvl);
@@ -228,7 +228,7 @@ void asserted_formulas::reset() {
 #ifdef Z3DEBUG
 bool asserted_formulas::check_well_sorted() const {
     for (unsigned i = 0; i < m_asserted_formulas.size(); i++) { 
-        if (!is_well_sorted(m_manager, m_asserted_formulas.get(i))) return false; 
+        if (!is_well_sorted(m, m_asserted_formulas.get(i))) return false; 
     }
     return true;
 }
@@ -322,7 +322,7 @@ void asserted_formulas::display(std::ostream & out) const {
     for (unsigned i = 0; i < m_asserted_formulas.size(); i++) {
         if (i == m_asserted_qhead)
             out << "[HEAD] ==>\n";
-        out << mk_pp(m_asserted_formulas.get(i), m_manager) << "\n";
+        out << mk_pp(m_asserted_formulas.get(i), m) << "\n";
     }
     out << "inconsistent: " << inconsistent() << "\n";
 }
@@ -331,7 +331,7 @@ void asserted_formulas::display_ll(std::ostream & out, ast_mark & pp_visited) co
     if (!m_asserted_formulas.empty()) {
         unsigned sz = m_asserted_formulas.size();
         for (unsigned i = 0; i < sz; i++) 
-            ast_def_ll_pp(out, m_manager, m_asserted_formulas.get(i), pp_visited, true, false);
+            ast_def_ll_pp(out, m, m_asserted_formulas.get(i), pp_visited, true, false);
         out << "asserted formulas:\n";
         for (unsigned i = 0; i < sz; i++) 
             out << "#" << m_asserted_formulas[i]->get_id() << " ";
@@ -346,23 +346,23 @@ void asserted_formulas::reduce_asserted_formulas() {
     if (inconsistent()) {
         return;
     }
-    expr_ref_vector  new_exprs(m_manager);
-    proof_ref_vector new_prs(m_manager);
+    expr_ref_vector  new_exprs(m);
+    proof_ref_vector new_prs(m);
     unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
     for (; i < sz && !inconsistent(); i++) {
         expr * n    = m_asserted_formulas.get(i);
         SASSERT(n != 0);
         proof * pr  = m_asserted_formula_prs.get(i, 0);
-        expr_ref new_n(m_manager);
-        proof_ref new_pr(m_manager);
+        expr_ref new_n(m);
+        proof_ref new_pr(m);
         m_simplifier(n, new_n, new_pr);
-        TRACE("reduce_asserted_formulas", tout << mk_pp(n, m_manager) << " -> " << mk_pp(new_n, m_manager) << "\n";);
+        TRACE("reduce_asserted_formulas", tout << mk_pp(n, m) << " -> " << mk_pp(new_n, m) << "\n";);
         if (n == new_n.get()) {
             push_assertion(n, pr, new_exprs, new_prs);
         }
         else {
-            new_pr = m_manager.mk_modus_ponens(pr, new_pr);
+            new_pr = m.mk_modus_ponens(pr, new_pr);
             push_assertion(new_n, new_pr, new_exprs, new_prs);
         }
         if (canceled()) {
@@ -376,15 +376,15 @@ void asserted_formulas::swap_asserted_formulas(expr_ref_vector & new_exprs, proo
     SASSERT(!inconsistent() || !new_exprs.empty());
     m_asserted_formulas.shrink(m_asserted_qhead);
     m_asserted_formulas.append(new_exprs);
-    if (m_manager.proofs_enabled()) {
+    if (m.proofs_enabled()) {
         m_asserted_formula_prs.shrink(m_asserted_qhead);
         m_asserted_formula_prs.append(new_prs);
     }
 }
 
 void asserted_formulas::find_macros_core() {
-    expr_ref_vector  new_exprs(m_manager);
-    proof_ref_vector new_prs(m_manager);
+    expr_ref_vector  new_exprs(m);
+    proof_ref_vector new_prs(m);
     unsigned sz = m_asserted_formulas.size();
     m_macro_finder->operator()(sz - m_asserted_qhead, m_asserted_formulas.c_ptr() + m_asserted_qhead, 
                                m_asserted_formula_prs.c_ptr() + m_asserted_qhead, new_exprs, new_prs);
@@ -407,9 +407,9 @@ void asserted_formulas::expand_macros() {
 void asserted_formulas::apply_quasi_macros() {
     IF_VERBOSE(10, verbose_stream() << "(smt.find-quasi-macros)\n";);
     TRACE("before_quasi_macros", display(tout););
-    expr_ref_vector  new_exprs(m_manager);
-    proof_ref_vector new_prs(m_manager);      
-    quasi_macros proc(m_manager, m_macro_manager, m_simplifier);    
+    expr_ref_vector  new_exprs(m);
+    proof_ref_vector new_prs(m);      
+    quasi_macros proc(m, m_macro_manager, m_simplifier);    
     while (proc(m_asserted_formulas.size() - m_asserted_qhead, 
                 m_asserted_formulas.c_ptr() + m_asserted_qhead, 
                 m_asserted_formula_prs.c_ptr() + m_asserted_qhead,
@@ -423,28 +423,29 @@ void asserted_formulas::apply_quasi_macros() {
 }
 
 void asserted_formulas::nnf_cnf() {
+
     IF_VERBOSE(10, verbose_stream() << "(smt.nnf)\n";);
-    nnf              apply_nnf(m_manager, m_defined_names);
-    expr_ref_vector  new_exprs(m_manager);
-    proof_ref_vector new_prs(m_manager);
-    expr_ref_vector  push_todo(m_manager);
-    proof_ref_vector push_todo_prs(m_manager);
+    nnf              apply_nnf(m, m_defined_names);
+    expr_ref_vector  new_exprs(m);
+    proof_ref_vector new_prs(m);
+    expr_ref_vector  push_todo(m);
+    proof_ref_vector push_todo_prs(m);
     
     unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
     TRACE("nnf_bug", tout << "i: " << i << " sz: " << sz << "\n";);
     for (; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);
-        TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m_manager) << "\n";);
+        TRACE("nnf_bug", tout << "processing:\n" << mk_pp(n, m) << "\n";);
         proof * pr  = m_asserted_formula_prs.get(i, 0);
-        expr_ref   r1(m_manager);
-        proof_ref  pr1(m_manager);
-        CASSERT("well_sorted",is_well_sorted(m_manager, n));
+        expr_ref   r1(m);
+        proof_ref  pr1(m);
+        CASSERT("well_sorted",is_well_sorted(m, n));
         push_todo.reset();
         push_todo_prs.reset();
         apply_nnf(n, push_todo, push_todo_prs, r1, pr1);
-        CASSERT("well_sorted",is_well_sorted(m_manager, r1));
-        pr = m_manager.mk_modus_ponens(pr, pr1);
+        CASSERT("well_sorted",is_well_sorted(m, r1));
+        pr = m.mk_modus_ponens(pr, pr1);
         push_todo.push_back(r1);
         push_todo_prs.push_back(pr);
 
@@ -456,13 +457,13 @@ void asserted_formulas::nnf_cnf() {
             expr * n   = push_todo.get(k);
             proof * pr = 0;
             m_simplifier(n, r1, pr1);
-            CASSERT("well_sorted",is_well_sorted(m_manager, r1));
+            CASSERT("well_sorted",is_well_sorted(m, r1));
             if (canceled()) {
                 return;
             }        
             
-            if (m_manager.proofs_enabled())
-                pr = m_manager.mk_modus_ponens(push_todo_prs.get(k), pr1);
+            if (m.proofs_enabled())
+                pr = m.mk_modus_ponens(push_todo_prs.get(k), pr1);
             else
                 pr = 0;
             push_assertion(r1, pr, new_exprs, new_prs);
@@ -476,23 +477,23 @@ void asserted_formulas::NAME() {
     IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";);     \
     TRACE(LABEL, tout << "before:\n"; display(tout););                                                                  \
     FUNCTOR_DEF;                                                                                                        \
-    expr_ref_vector  new_exprs(m_manager);                                                                              \
-    proof_ref_vector new_prs(m_manager);                                                                                \
+    expr_ref_vector  new_exprs(m);                                                                              \
+    proof_ref_vector new_prs(m);                                                                                \
     unsigned i  = m_asserted_qhead;                                                                                     \
     unsigned sz = m_asserted_formulas.size();                                                                           \
     for (; i < sz; i++) {                                                                                               \
         expr * n    = m_asserted_formulas.get(i);                                                                       \
         proof * pr  = m_asserted_formula_prs.get(i, 0);                                                                 \
-        expr_ref new_n(m_manager);                                                                                      \
+        expr_ref new_n(m);                                                                                      \
         functor(n, new_n);                                                                                              \
-        TRACE("simplifier_simple_step", tout << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";);       \
+        TRACE("simplifier_simple_step", tout << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";);       \
         if (n == new_n.get()) {                                                                                         \
             push_assertion(n, pr, new_exprs, new_prs);                                                                  \
         }                                                                                                               \
-        else if (m_manager.proofs_enabled()) {                                                                          \
-            proof_ref new_pr(m_manager);                                                                                \
-            new_pr = m_manager.mk_rewrite_star(n, new_n, 0, 0);            \
-            new_pr = m_manager.mk_modus_ponens(pr, new_pr);                                                             \
+        else if (m.proofs_enabled()) {                                                                          \
+            proof_ref new_pr(m);                                                                                \
+            new_pr = m.mk_rewrite_star(n, new_n, 0, 0);            \
+            new_pr = m.mk_modus_ponens(pr, new_pr);                                                             \
             push_assertion(new_n, new_pr, new_exprs, new_prs);                                                          \
         }                                                                                                               \
         else {                                                                                                          \
@@ -505,7 +506,7 @@ void asserted_formulas::NAME() {
     TRACE(LABEL, display(tout););                                                                                       \
 }
 
-MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m_manager, *m_bsimp), "distribute_forall", "distribute-forall");
+MK_SIMPLE_SIMPLIFIER(apply_distribute_forall, distribute_forall functor(m), "distribute_forall", "distribute-forall");
 
 void asserted_formulas::reduce_and_solve() {
     IF_VERBOSE(10, verbose_stream() << "(smt.reducing)\n";);
@@ -516,22 +517,22 @@ void asserted_formulas::reduce_and_solve() {
 void asserted_formulas::infer_patterns() {
     IF_VERBOSE(10, verbose_stream() << "(smt.pattern-inference)\n";);
     TRACE("before_pattern_inference", display(tout););
-    pattern_inference infer(m_manager, m_params);
-    expr_ref_vector  new_exprs(m_manager);
-    proof_ref_vector new_prs(m_manager);
+    pattern_inference infer(m, m_params);
+    expr_ref_vector  new_exprs(m);
+    proof_ref_vector new_prs(m);
     unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
     for (; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);
         proof * pr  = m_asserted_formula_prs.get(i, 0);
-        expr_ref  new_n(m_manager);
-        proof_ref new_pr(m_manager);
+        expr_ref  new_n(m);
+        proof_ref new_pr(m);
         infer(n, new_n, new_pr);
         if (n == new_n.get()) {
             push_assertion(n, pr, new_exprs, new_prs);
         }
-        else if (m_manager.proofs_enabled()) {
-            new_pr = m_manager.mk_modus_ponens(pr, new_pr);
+        else if (m.proofs_enabled()) {
+            new_pr = m.mk_modus_ponens(pr, new_pr);
             push_assertion(new_n, new_pr, new_exprs, new_prs);
         }
         else {
@@ -554,16 +555,16 @@ void asserted_formulas::commit(unsigned new_qhead) {
 void asserted_formulas::eliminate_term_ite() {
     IF_VERBOSE(10, verbose_stream() << "(smt.eliminating-ite-term)\n";);
     TRACE("before_elim_term_ite", display(tout););
-    elim_term_ite   elim(m_manager, m_defined_names);
-    expr_ref_vector  new_exprs(m_manager);
-    proof_ref_vector new_prs(m_manager);
+    elim_term_ite   elim(m, m_defined_names);
+    expr_ref_vector  new_exprs(m);
+    proof_ref_vector new_prs(m);
     unsigned i  = m_asserted_qhead;
     unsigned sz = m_asserted_formulas.size();
     for (; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);
         proof * pr  = m_asserted_formula_prs.get(i, 0);
-        expr_ref  new_n(m_manager);
-        proof_ref new_pr(m_manager);
+        expr_ref  new_n(m);
+        proof_ref new_pr(m);
         elim(n, new_exprs, new_prs, new_n, new_pr);
         SASSERT(new_n.get() != 0);
         DEBUG_CODE({
@@ -574,8 +575,8 @@ void asserted_formulas::eliminate_term_ite() {
         if (n == new_n.get()) {
             push_assertion(n, pr, new_exprs, new_prs);
         }
-        else if (m_manager.proofs_enabled()) {
-            new_pr = m_manager.mk_modus_ponens(pr, new_pr);
+        else if (m.proofs_enabled()) {
+            new_pr = m.mk_modus_ponens(pr, new_pr);
             push_assertion(new_n, new_pr, new_exprs, new_prs);
         }
         else {
@@ -602,31 +603,31 @@ void asserted_formulas::propagate_values() {
     // - new_exprs2 is the set R
     //
     // The loop also updates the m_cache. It adds the entries x -> n to it.
-    expr_ref_vector  new_exprs1(m_manager);
-    proof_ref_vector new_prs1(m_manager);
-    expr_ref_vector  new_exprs2(m_manager);
-    proof_ref_vector new_prs2(m_manager);
+    expr_ref_vector  new_exprs1(m);
+    proof_ref_vector new_prs1(m);
+    expr_ref_vector  new_exprs2(m);
+    proof_ref_vector new_prs2(m);
     unsigned sz = m_asserted_formulas.size();
     for (unsigned i = 0; i < sz; i++) {
-        expr_ref   n(m_asserted_formulas.get(i), m_manager);
-        proof_ref pr(m_asserted_formula_prs.get(i, 0), m_manager);
-        TRACE("simplifier", tout << mk_pp(n, m_manager) << "\n";);
+        expr_ref   n(m_asserted_formulas.get(i), m);
+        proof_ref pr(m_asserted_formula_prs.get(i, 0), m);
+        TRACE("simplifier", tout << mk_pp(n, m) << "\n";);
         expr* lhs, *rhs;
-        if (m_manager.is_eq(n, lhs, rhs) &&
-            (m_manager.is_value(lhs) || m_manager.is_value(rhs))) {
-            if (m_manager.is_value(lhs)) {
+        if (m.is_eq(n, lhs, rhs) &&
+            (m.is_value(lhs) || m.is_value(rhs))) {
+            if (m.is_value(lhs)) {
                 std::swap(lhs, rhs);
-                n  = m_manager.mk_eq(lhs, rhs);
-                pr = m_manager.mk_symmetry(pr);
+                n  = m.mk_eq(lhs, rhs);
+                pr = m.mk_symmetry(pr);
             }
-            if (!m_manager.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
+            if (!m.is_value(lhs) && !m_simplifier.is_cached(lhs)) {
                 if (i >= m_asserted_qhead) {
                     new_exprs1.push_back(n);
-                    if (m_manager.proofs_enabled())
+                    if (m.proofs_enabled())
                         new_prs1.push_back(pr);
                 }
-                TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m_manager) << "\n->\n" << mk_pp(rhs, m_manager) << "\n";
-                      if (pr) tout << "proof: " << mk_pp(pr, m_manager) << "\n";);
+                TRACE("propagate_values", tout << "found:\n" << mk_pp(lhs, m) << "\n->\n" << mk_pp(rhs, m) << "\n";
+                      if (pr) tout << "proof: " << mk_pp(pr, m) << "\n";);
                 m_simplifier.cache_result(lhs, rhs, pr);
                 found = true;
                 continue;
@@ -634,7 +635,7 @@ void asserted_formulas::propagate_values() {
         }
         if (i >= m_asserted_qhead) {
             new_exprs2.push_back(n);
-            if (m_manager.proofs_enabled())
+            if (m.proofs_enabled())
                 new_prs2.push_back(pr);
         }
     }
@@ -646,14 +647,14 @@ void asserted_formulas::propagate_values() {
         for (unsigned i = 0; i < sz; i++) {
             expr * n    = new_exprs2.get(i);
             proof * pr  = new_prs2.get(i, 0);
-            expr_ref new_n(m_manager);
-            proof_ref new_pr(m_manager);
+            expr_ref new_n(m);
+            proof_ref new_pr(m);
             m_simplifier(n, new_n, new_pr);
             if (n == new_n.get()) {
                 push_assertion(n, pr, new_exprs1, new_prs1);
             }
             else {
-                new_pr = m_manager.mk_modus_ponens(pr, new_pr);
+                new_pr = m.mk_modus_ponens(pr, new_pr);
                 push_assertion(new_n, new_pr, new_exprs1, new_prs1);
             }
         }
@@ -677,25 +678,25 @@ void asserted_formulas::propagate_booleans() {
         cont        = false;
         unsigned i  = m_asserted_qhead;
         unsigned sz = m_asserted_formulas.size();
-#define PROCESS() {                                                                                                             \
-            expr * n    = m_asserted_formulas.get(i);                                                                           \
-            proof * pr  = m_asserted_formula_prs.get(i, 0);                                                                     \
-            expr_ref new_n(m_manager);                                                                                          \
-            proof_ref new_pr(m_manager);                                                                                        \
-            m_simplifier(n, new_n, new_pr);                                                                                     \
-            m_asserted_formulas.set(i, new_n);                                                                                  \
-            if (m_manager.proofs_enabled()) {                                                                                   \
-                new_pr = m_manager.mk_modus_ponens(pr, new_pr);                                                                 \
-                m_asserted_formula_prs.set(i, new_pr);                                                                          \
-            }                                                                                                                   \
-            if (n != new_n) {                                                                                                   \
-                cont = true;                                                                                                    \
-                modified = true;                                                                                                \
-            }                                                                                                                   \
-            if (m_manager.is_not(new_n))                                                                                        \
-                m_simplifier.cache_result(to_app(new_n)->get_arg(0), m_manager.mk_false(), m_manager.mk_iff_false(new_pr));     \
-            else                                                                                                                \
-                m_simplifier.cache_result(new_n, m_manager.mk_true(), m_manager.mk_iff_true(new_pr));                           \
+#define PROCESS() {                                                     \
+            expr * n    = m_asserted_formulas.get(i);                   \
+            proof * pr  = m_asserted_formula_prs.get(i, 0);             \
+            expr_ref new_n(m);                                          \
+            proof_ref new_pr(m);                                        \
+            m_simplifier(n, new_n, new_pr);                             \
+            m_asserted_formulas.set(i, new_n);                          \
+            if (m.proofs_enabled()) {                                   \
+                new_pr = m.mk_modus_ponens(pr, new_pr);                 \
+                m_asserted_formula_prs.set(i, new_pr);                  \
+            }                                                           \
+            if (n != new_n) {                                           \
+                cont = true;                                            \
+                modified = true;                                        \
+            }                                                           \
+            if (m.is_not(new_n))                                        \
+                m_simplifier.cache_result(to_app(new_n)->get_arg(0), m.mk_false(), m.mk_iff_false(new_pr)); \
+            else                                                        \
+                m_simplifier.cache_result(new_n, m.mk_true(), m.mk_iff_true(new_pr)); \
         }
         for (; i < sz; i++) {
             PROCESS();
@@ -715,57 +716,58 @@ void asserted_formulas::propagate_booleans() {
 }
 
 #define MK_SIMPLIFIER(NAME, FUNCTOR, TAG, MSG, REDUCE)                  \
-bool asserted_formulas::NAME() {                                        \
-    IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";);     \
-    TRACE(TAG, ast_mark visited; display_ll(tout, visited););           \
-    FUNCTOR;                                                            \
-    bool changed = false;                                               \
-    expr_ref_vector  new_exprs(m_manager);                              \
-    proof_ref_vector new_prs(m_manager);                                \
-    unsigned i  = m_asserted_qhead;                                     \
-    unsigned sz = m_asserted_formulas.size();                           \
-    for (; i < sz; i++) {                                               \
-        expr * n    = m_asserted_formulas.get(i);                       \
-        proof * pr  = m_asserted_formula_prs.get(i, 0);                 \
-        expr_ref  new_n(m_manager);                                     \
-        proof_ref new_pr(m_manager);                                    \
-        functor(n, new_n, new_pr);                                      \
-        if (n == new_n.get()) {                                         \
-            push_assertion(n, pr, new_exprs, new_prs);                  \
-        }                                                               \
-        else if (m_manager.proofs_enabled()) {                          \
-            changed = true;                                             \
-            if (!new_pr) new_pr = m_manager.mk_rewrite(n, new_n);       \
-            new_pr = m_manager.mk_modus_ponens(pr, new_pr);             \
-            push_assertion(new_n, new_pr, new_exprs, new_prs);          \
-        }                                                               \
-        else {                                                          \
-            changed = true;                                             \
-            push_assertion(new_n, 0, new_exprs, new_prs);               \
-        }                                                               \
-    }                                                                   \
-    swap_asserted_formulas(new_exprs, new_prs);                         \
-    TRACE(TAG, ast_mark visited; display_ll(tout, visited););           \
-    if (changed && REDUCE) {                                            \
-        reduce_and_solve();                                             \
+    bool asserted_formulas::NAME() {                                    \
+        IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";);  \
         TRACE(TAG, ast_mark visited; display_ll(tout, visited););       \
-    }                                                                   \
-    return changed;                                                     \
-}
+        FUNCTOR;                                                        \
+        bool changed = false;                                           \
+        expr_ref_vector  new_exprs(m);                                  \
+        proof_ref_vector new_prs(m);                                    \
+        unsigned i  = m_asserted_qhead;                                 \
+        unsigned sz = m_asserted_formulas.size();                       \
+        for (; i < sz; i++) {                                           \
+            expr * n    = m_asserted_formulas.get(i);                   \
+            proof * pr  = m_asserted_formula_prs.get(i, 0);             \
+            expr_ref  new_n(m);                                         \
+            proof_ref new_pr(m);                                        \
+            functor(n, new_n, new_pr);                                  \
+            if (n == new_n.get()) {                                     \
+                push_assertion(n, pr, new_exprs, new_prs);              \
+            }                                                           \
+            else if (m.proofs_enabled()) {                              \
+                changed = true;                                         \
+                if (!new_pr) new_pr = m.mk_rewrite(n, new_n);           \
+                new_pr = m.mk_modus_ponens(pr, new_pr);                 \
+                push_assertion(new_n, new_pr, new_exprs, new_prs);      \
+            }                                                           \
+            else {                                                      \
+                changed = true;                                         \
+                push_assertion(new_n, 0, new_exprs, new_prs);           \
+            }                                                           \
+        }                                                               \
+        swap_asserted_formulas(new_exprs, new_prs);                     \
+        TRACE(TAG, ast_mark visited; display_ll(tout, visited););       \
+        if (changed && REDUCE) {                                        \
+            reduce_and_solve();                                         \
+            TRACE(TAG, ast_mark visited; display_ll(tout, visited););   \
+        }                                                               \
+        return changed;                                                 \
+    }
 
-MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m_manager, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
 
-MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m_manager), "pull_nested_quantifiers", "pull-nested-quantifiers", false);
+MK_SIMPLIFIER(pull_cheap_ite_trees, pull_cheap_ite_tree_star functor(m, m_simplifier), "pull_cheap_ite_trees", "pull-cheap-ite-trees", false);
+
+MK_SIMPLIFIER(pull_nested_quantifiers, pull_nested_quant functor(m), "pull_nested_quantifiers", "pull-nested-quantifiers", false);
 
 proof * asserted_formulas::get_inconsistency_proof() const {
     if (!inconsistent())
         return 0;
-    if (!m_manager.proofs_enabled())
+    if (!m.proofs_enabled())
         return 0;
     unsigned sz = m_asserted_formulas.size();
     for (unsigned i = 0; i < sz; i++) {
         expr * f = m_asserted_formulas.get(i);
-        if (m_manager.is_false(f))
+        if (m.is_false(f))
             return m_asserted_formula_prs.get(i);
     }
     UNREACHABLE();
@@ -780,14 +782,14 @@ void asserted_formulas::refine_inj_axiom() {
     for (; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);
         proof * pr  = m_asserted_formula_prs.get(i, 0);
-        expr_ref new_n(m_manager);
-        if (is_quantifier(n) && simplify_inj_axiom(m_manager, to_quantifier(n), new_n)) {
-            TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m_manager) << "\n" << mk_pp(new_n, m_manager) << "\n";);
+        expr_ref new_n(m);
+        if (is_quantifier(n) && simplify_inj_axiom(m, to_quantifier(n), new_n)) {
+            TRACE("inj_axiom", tout << "simplifying...\n" << mk_pp(n, m) << "\n" << mk_pp(new_n, m) << "\n";);
             m_asserted_formulas.set(i, new_n);
-            if (m_manager.proofs_enabled()) {
-                proof_ref new_pr(m_manager);     
-                new_pr = m_manager.mk_rewrite(n, new_n);
-                new_pr = m_manager.mk_modus_ponens(pr, new_pr);
+            if (m.proofs_enabled()) {
+                proof_ref new_pr(m);     
+                new_pr = m.mk_rewrite(n, new_n);
+                new_pr = m.mk_modus_ponens(pr, new_pr);
                 m_asserted_formula_prs.set(i, new_pr);
             }
         }
@@ -797,36 +799,36 @@ void asserted_formulas::refine_inj_axiom() {
 
 MK_SIMPLIFIER(apply_bit2int, bit2int& functor = m_bit2int, "bit2int", "propagate-bit-vector-over-integers", true);
 
-MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m_manager), "elim_bounds", "cheap-fourier-motzkin", true);
+MK_SIMPLIFIER(cheap_quant_fourier_motzkin, elim_bounds_star functor(m), "elim_bounds", "cheap-fourier-motzkin", true);
 
 
 
-MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m_manager), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
+MK_SIMPLIFIER(elim_bvs_from_quantifiers, bv_elim_star functor(m), "bv_elim", "eliminate-bit-vectors-from-quantifiers", true);
 
-#define LIFT_ITE(NAME, FUNCTOR, MSG)                                                                                            \
-void asserted_formulas::NAME() {                                                                                                \
-    IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";);            \
-    TRACE("lift_ite", display(tout););                                                                                          \
-    FUNCTOR;                                                                                                                    \
-    unsigned i  = m_asserted_qhead;                                                                                             \
-    unsigned sz = m_asserted_formulas.size();                                                                                   \
-    for (; i < sz; i++) {                                                                                                       \
-        expr * n    = m_asserted_formulas.get(i);                                                                               \
-        proof * pr  = m_asserted_formula_prs.get(i, 0);                                                                         \
-        expr_ref  new_n(m_manager);                                                                                             \
-        proof_ref new_pr(m_manager);                                                                                            \
-        functor(n, new_n, new_pr);                                                                                              \
-        TRACE("lift_ite_step", tout << mk_pp(n, m_manager) << "\n";);                                                           \
-        IF_VERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n)  << ", after: " << get_num_exprs(new_n) << "\n";);  \
-        m_asserted_formulas.set(i, new_n);                                                                                      \
-        if (m_manager.proofs_enabled()) {                                                                                       \
-            new_pr = m_manager.mk_modus_ponens(pr, new_pr);                                                                     \
-            m_asserted_formula_prs.set(i, new_pr);                                                                              \
-        }                                                                                                                       \
-    }                                                                                                                           \
-    TRACE("lift_ite", display(tout););                                                                                          \
-    reduce_and_solve();                                                                                                         \
-}
+#define LIFT_ITE(NAME, FUNCTOR, MSG)                                    \
+    void asserted_formulas::NAME() {                                    \
+        IF_VERBOSE(10, verbose_stream() << "(smt." << MSG << ")\n";);  \
+        TRACE("lift_ite", display(tout););                              \
+        FUNCTOR;                                                        \
+        unsigned i  = m_asserted_qhead;                                 \
+        unsigned sz = m_asserted_formulas.size();                       \
+        for (; i < sz; i++) {                                           \
+            expr * n    = m_asserted_formulas.get(i);                   \
+            proof * pr  = m_asserted_formula_prs.get(i, 0);             \
+            expr_ref  new_n(m);                                         \
+            proof_ref new_pr(m);                                        \
+            functor(n, new_n, new_pr);                                  \
+            TRACE("lift_ite_step", tout << mk_pp(n, m) << "\n";);       \
+            IF_VERBOSE(10000, verbose_stream() << "lift before: " << get_num_exprs(n)  << ", after: " << get_num_exprs(new_n) << "\n";); \
+            m_asserted_formulas.set(i, new_n);                          \
+            if (m.proofs_enabled()) {                                   \
+                new_pr = m.mk_modus_ponens(pr, new_pr);                 \
+                m_asserted_formula_prs.set(i, new_pr);                  \
+            }                                                           \
+        }                                                               \
+        TRACE("lift_ite", display(tout););                              \
+        reduce_and_solve();                                             \
+    }
 
 LIFT_ITE(lift_ite, push_app_ite functor(m_simplifier, m_params.m_lift_ite == LI_CONSERVATIVE), "lifting ite");
 LIFT_ITE(ng_lift_ite, ng_push_app_ite functor(m_simplifier, m_params.m_ng_lift_ite == LI_CONSERVATIVE), "lifting ng ite");
@@ -848,12 +850,12 @@ void asserted_formulas::max_bv_sharing() {
     for (; i < sz; i++) {
         expr * n    = m_asserted_formulas.get(i);
         proof * pr  = m_asserted_formula_prs.get(i, 0);
-        expr_ref new_n(m_manager);
-        proof_ref new_pr(m_manager);
+        expr_ref new_n(m);
+        proof_ref new_pr(m);
         m_bv_sharing(n, new_n, new_pr);
         m_asserted_formulas.set(i, new_n);
-        if (m_manager.proofs_enabled()) {
-            new_pr = m_manager.mk_modus_ponens(pr, new_pr);
+        if (m.proofs_enabled()) {
+            new_pr = m.mk_modus_ponens(pr, new_pr);
             m_asserted_formula_prs.set(i, new_pr);
         }
     }
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index 9e9ecf33a..6ad36cc70 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -35,7 +35,7 @@ class arith_simplifier_plugin;
 class bv_simplifier_plugin;
 
 class asserted_formulas {
-    ast_manager &                m_manager;
+    ast_manager &                m;
     smt_params &                 m_params;
     simplifier                   m_pre_simplifier;
     simplifier                   m_simplifier;
@@ -94,7 +94,7 @@ class asserted_formulas {
     unsigned get_total_size() const;
     bool has_bv() const;
     void max_bv_sharing();
-    bool canceled() { return m_manager.canceled(); }
+    bool canceled() { return m.canceled(); }
 
 public:
     asserted_formulas(ast_manager & m, smt_params & p);
@@ -115,7 +115,7 @@ public:
     void commit(); 
     void commit(unsigned new_qhead); 
     expr * get_formula(unsigned idx) const { return m_asserted_formulas.get(idx); }
-    proof * get_formula_proof(unsigned idx) const { return m_manager.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
+    proof * get_formula_proof(unsigned idx) const { return m.proofs_enabled() ? m_asserted_formula_prs.get(idx) : 0; }
     expr * const * get_formulas() const { return m_asserted_formulas.c_ptr(); }
     proof * const * get_formula_proofs() const { return m_asserted_formula_prs.c_ptr(); }
     void init(unsigned num_formulas, expr * const * formulas, proof * const * prs);
diff --git a/src/smt/params/smt_params_helper.pyg b/src/smt/params/smt_params_helper.pyg
index 6c2ff4962..a501f474a 100644
--- a/src/smt/params/smt_params_helper.pyg
+++ b/src/smt/params/smt_params_helper.pyg
@@ -44,6 +44,7 @@ def_module_params(module_name='smt',
                           ('arith.euclidean_solver', BOOL, False, 'eucliean solver for linear integer arithmetic'),
                           ('arith.propagate_eqs', BOOL, True, 'propagate (cheap) equalities'),
                           ('arith.propagation_mode', UINT, 2, '0 - no propagation, 1 - propagate existing literals, 2 - refine bounds'),
+                          ('arith.reflect', BOOL, True, 'reflect arithmetical operators to the congruence closure'),
                           ('arith.branch_cut_ratio', UINT, 2, 'branch/cut ratio for linear integer arithmetic'),
                           ('arith.int_eq_branch', BOOL, False, 'branching using derived integer equations'),
                           ('arith.ignore_int', BOOL, False, 'treat integer variables as real'),
diff --git a/src/smt/params/theory_arith_params.cpp b/src/smt/params/theory_arith_params.cpp
index 1e3f29142..944911f9b 100644
--- a/src/smt/params/theory_arith_params.cpp
+++ b/src/smt/params/theory_arith_params.cpp
@@ -35,6 +35,7 @@ void theory_arith_params::updt_params(params_ref const & _p) {
     m_arith_ignore_int = p.arith_ignore_int();
     m_arith_bound_prop = static_cast<bound_prop_mode>(p.arith_propagation_mode());
     m_arith_dump_lemmas = p.arith_dump_lemmas();
+    m_arith_reflect = p.arith_reflect();
 }
 
 
@@ -85,4 +86,4 @@ void theory_arith_params::display(std::ostream & out) const {
     DISPLAY_PARAM(m_nl_arith_branching);
     DISPLAY_PARAM(m_nl_arith_rounds);
     DISPLAY_PARAM(m_arith_euclidean_solver);
-}
\ No newline at end of file
+}
diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 62846e709..63f0a88bd 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -7304,7 +7304,7 @@ namespace smt {
                     TRACE("str", tout << "variable " << mk_ismt2_pp(ap, get_manager()) << " is #" << v << std::endl;);
                 }
             }
-        } else if (ex_sort == bool_sort) {
+        } else if (ex_sort == bool_sort && !is_quantifier(ex)) {
             TRACE("str", tout << "setting up axioms for " << mk_ismt2_pp(ex, get_manager()) <<
                   ": expr is of sort Bool" << std::endl;);
             // set up axioms for boolean terms
@@ -7351,7 +7351,7 @@ namespace smt {
 
         // if expr is an application, recursively inspect all arguments
         if (is_app(ex)) {
-            app * term = (app*)ex;
+            app * term = to_app(ex);
             unsigned num_args = term->get_num_args();
             for (unsigned i = 0; i < num_args; i++) {
                 set_up_axioms(term->get_arg(i));
diff --git a/src/solver/solver.cpp b/src/solver/solver.cpp
index 9163cfeda..59b950972 100644
--- a/src/solver/solver.cpp
+++ b/src/solver/solver.cpp
@@ -162,3 +162,9 @@ bool solver::is_literal(ast_manager& m, expr* e) {
     return is_uninterp_const(e) || (m.is_not(e, e) && is_uninterp_const(e));
 }
 
+expr_ref solver::lookahead(expr_ref_vector const& candidates) {
+    ast_manager& m = candidates.get_manager();
+    return expr_ref(m.mk_true(), m);
+}
+
+
diff --git a/src/solver/solver.h b/src/solver/solver.h
index 6b9d38f29..51bff08ad 100644
--- a/src/solver/solver.h
+++ b/src/solver/solver.h
@@ -172,6 +172,17 @@ public:
      */
     virtual lbool preferred_sat(expr_ref_vector const& asms, vector<expr_ref_vector>& cores);
 
+    /**
+       \brief extract a lookahead candidates for branching.
+    */
+
+    virtual expr_ref lookahead(expr_ref_vector const& candidates);
+
+    /**
+       \brief extract learned lemmas.
+    */
+    virtual void get_lemmas(expr_ref_vector& lemmas) {}
+
     /**
        \brief Display the content of this solver.
     */
diff --git a/src/solver/solver2tactic.cpp b/src/solver/solver2tactic.cpp
index 1a02c97e6..4283da50a 100644
--- a/src/solver/solver2tactic.cpp
+++ b/src/solver/solver2tactic.cpp
@@ -150,7 +150,21 @@ public:
             if (m.canceled()) {
                 throw tactic_exception(Z3_CANCELED_MSG);
             }
-            throw tactic_exception(local_solver->reason_unknown().c_str());
+            if (in->models_enabled()) {
+                model_ref mdl;
+                local_solver->get_model(mdl);
+                if (mdl) {
+                    mc = model2model_converter(mdl.get());
+                    mc = concat(fmc.get(), mc.get());
+                }
+            }
+            in->reset();
+            unsigned sz = local_solver->get_num_assertions();
+            for (unsigned i = 0; i < sz; ++i) {
+                in->assert_expr(local_solver->get_assertion(i));
+            }
+            result.push_back(in.get());
+            break;
         }
         local_solver->collect_statistics(m_st);
     }
diff --git a/src/tactic/bv/bit_blaster_model_converter.cpp b/src/tactic/bv/bit_blaster_model_converter.cpp
index a18862ee8..c9ba2f09c 100644
--- a/src/tactic/bv/bit_blaster_model_converter.cpp
+++ b/src/tactic/bv/bit_blaster_model_converter.cpp
@@ -117,8 +117,10 @@ struct bit_blaster_model_converter : public model_converter {
                     SASSERT(is_uninterp_const(bit));
                     func_decl * bit_decl = to_app(bit)->get_decl();
                     expr * bit_val = old_model->get_const_interp(bit_decl);
-                    // remark: if old_model does not assign bit_val, then assume it is false.
-                    if (bit_val != 0 && m().is_true(bit_val))
+                    if (bit_val == 0) {
+                        goto bail;
+                    }
+                    if (m().is_true(bit_val))
                         val++;
                 }
             }
@@ -133,15 +135,50 @@ struct bit_blaster_model_converter : public model_converter {
                     func_decl * bit_decl = to_app(bit)->get_decl();
                     expr * bit_val = old_model->get_const_interp(bit_decl);
                     // remark: if old_model does not assign bit_val, then assume it is false.
-                    if (bit_val != 0 && !util.is_zero(bit_val))
+                    if (bit_val == 0) {
+                        goto bail;
+                    }
+                    if (!util.is_zero(bit_val))
                         val++;
                 }
             }
             new_val = util.mk_numeral(val, bv_sz);
             new_model->register_decl(m_vars.get(i), new_val);
+            continue;
+        bail:
+            new_model->register_decl(m_vars.get(i), mk_bv(bs, *old_model));                                    
         }
     }
 
+    app_ref mk_bv(expr* bs, model& old_model) {
+        bv_util util(m());
+        unsigned bv_sz = to_app(bs)->get_num_args();
+        expr_ref_vector args(m());
+        app_ref result(m());
+        for (unsigned j = 0; j < bv_sz; ++j) {
+            expr * bit = to_app(bs)->get_arg(j);
+            SASSERT(is_uninterp_const(bit));
+            func_decl * bit_decl = to_app(bit)->get_decl();
+            expr * bit_val = old_model.get_const_interp(bit_decl);
+            if (bit_val != 0) {
+                args.push_back(bit_val);
+            }
+            else {
+                args.push_back(bit);
+            }
+        }
+
+        if (TO_BOOL) {
+            SASSERT(is_app_of(bs, m().get_family_id("bv"), OP_MKBV));
+            result = util.mk_bv(bv_sz, args.c_ptr());
+        }
+        else {
+            SASSERT(is_app_of(bs, m().get_family_id("bv"), OP_CONCAT));
+            result = util.mk_concat(bv_sz, args.c_ptr());
+        }
+        return result;
+    }
+
     virtual void operator()(model_ref & md, unsigned goal_idx) {
         SASSERT(goal_idx == 0);
         model * new_model = alloc(model, m());
diff --git a/src/tactic/goal.cpp b/src/tactic/goal.cpp
index b14d2676c..af58d8331 100644
--- a/src/tactic/goal.cpp
+++ b/src/tactic/goal.cpp
@@ -262,6 +262,13 @@ void goal::get_formulas(ptr_vector<expr> & result) {
     }
 }
 
+void goal::get_formulas(expr_ref_vector & result) {
+    unsigned sz = size();
+    for (unsigned i = 0; i < sz; i++) {
+        result.push_back(form(i));
+    }
+}
+
 void goal::update(unsigned i, expr * f, proof * pr, expr_dependency * d) {
     // KLM: don't know why this assertion is no longer true
     // SASSERT(proofs_enabled() == (pr != 0 && !m().is_undef_proof(pr)));
diff --git a/src/tactic/goal.h b/src/tactic/goal.h
index ea02dfa17..5ccbd4529 100644
--- a/src/tactic/goal.h
+++ b/src/tactic/goal.h
@@ -120,6 +120,7 @@ public:
     void update(unsigned i, expr * f, proof * pr = 0, expr_dependency * dep = 0);
 
     void get_formulas(ptr_vector<expr> & result);
+    void get_formulas(expr_ref_vector & result);
     
     void elim_true();
     void elim_redundancies();
diff --git a/src/tactic/portfolio/bounded_int2bv_solver.cpp b/src/tactic/portfolio/bounded_int2bv_solver.cpp
index 83693abba..cee8688e5 100644
--- a/src/tactic/portfolio/bounded_int2bv_solver.cpp
+++ b/src/tactic/portfolio/bounded_int2bv_solver.cpp
@@ -149,6 +149,7 @@ public:
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
+    virtual expr_ref lookahead(expr_ref_vector& candidates) { flush_assertions(); return m_solver->lookahead(candidates); }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         flush_assertions();
diff --git a/src/tactic/portfolio/default_tactic.cpp b/src/tactic/portfolio/default_tactic.cpp
index 4f5eb5ed0..2052894d2 100644
--- a/src/tactic/portfolio/default_tactic.cpp
+++ b/src/tactic/portfolio/default_tactic.cpp
@@ -30,7 +30,6 @@ Notes:
 #include"qffp_tactic.h"
 #include"qfaufbv_tactic.h"
 #include"qfauflia_tactic.h"
-#include"qfufnra_tactic.h"
 
 tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
     tactic * st = using_params(and_then(mk_simplify_tactic(m),
@@ -44,7 +43,6 @@ tactic * mk_default_tactic(ast_manager & m, params_ref const & p) {
                                         cond(mk_is_nra_probe(),   mk_nra_tactic(m),
                                         cond(mk_is_lira_probe(),  mk_lira_tactic(m, p),
                                         cond(mk_is_qffp_probe(), mk_qffp_tactic(m, p),
-                                        //cond(mk_is_qfufnra_probe(), mk_qfufnra_tactic(m, p),
                                              mk_smt_tactic()))))))))))),
                                p);
     return st;
diff --git a/src/tactic/portfolio/enum2bv_solver.cpp b/src/tactic/portfolio/enum2bv_solver.cpp
index 35601f374..ef7ee6cd8 100644
--- a/src/tactic/portfolio/enum2bv_solver.cpp
+++ b/src/tactic/portfolio/enum2bv_solver.cpp
@@ -97,6 +97,7 @@ public:
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }
+    virtual expr_ref lookahead(expr_ref_vector& candidates) { return m_solver->lookahead(candidates); }
     
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         datatype_util dt(m);
diff --git a/src/tactic/portfolio/fd_solver.cpp b/src/tactic/portfolio/fd_solver.cpp
index a534337bc..12842daac 100644
--- a/src/tactic/portfolio/fd_solver.cpp
+++ b/src/tactic/portfolio/fd_solver.cpp
@@ -18,11 +18,13 @@ Notes:
 --*/
 
 #include "fd_solver.h"
+#include "fd_tactic.h"
 #include "tactic.h"
 #include "inc_sat_solver.h"
 #include "enum2bv_solver.h"
 #include "pb2bv_solver.h"
 #include "bounded_int2bv_solver.h"
+#include "solver/solver2tactic.h"
 
 solver * mk_fd_solver(ast_manager & m, params_ref const & p) {
     solver* s = mk_inc_sat_solver(m, p);
@@ -31,3 +33,7 @@ solver * mk_fd_solver(ast_manager & m, params_ref const & p) {
     s = mk_bounded_int2bv_solver(m, p, s);
     return s;
 }
+
+tactic * mk_fd_tactic(ast_manager & m, params_ref const& p) {
+    return mk_solver2tactic(mk_fd_solver(m, p));
+}
diff --git a/src/tactic/portfolio/fd_solver.h b/src/tactic/portfolio/fd_solver.h
index 51abb087f..41605c460 100644
--- a/src/tactic/portfolio/fd_solver.h
+++ b/src/tactic/portfolio/fd_solver.h
@@ -26,4 +26,5 @@ class solver;
 
 solver * mk_fd_solver(ast_manager & m, params_ref const & p);
 
+
 #endif
diff --git a/src/tactic/portfolio/pb2bv_solver.cpp b/src/tactic/portfolio/pb2bv_solver.cpp
index c8aa82e97..673db03c0 100644
--- a/src/tactic/portfolio/pb2bv_solver.cpp
+++ b/src/tactic/portfolio/pb2bv_solver.cpp
@@ -93,6 +93,7 @@ public:
     virtual void set_reason_unknown(char const* msg) { m_solver->set_reason_unknown(msg); }
     virtual void get_labels(svector<symbol> & r) { m_solver->get_labels(r); }
     virtual ast_manager& get_manager() const { return m;  }
+    virtual expr_ref lookahead(expr_ref_vector& candidates) { flush_assertions(); return m_solver->lookahead(candidates); }
     virtual lbool find_mutexes(expr_ref_vector const& vars, vector<expr_ref_vector>& mutexes) { return m_solver->find_mutexes(vars, mutexes); }    
     virtual lbool get_consequences_core(expr_ref_vector const& asms, expr_ref_vector const& vars, expr_ref_vector& consequences) {
         flush_assertions(); 
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index a4a579ddd..15d2e02c2 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -34,11 +34,11 @@ Notes:
 #include"default_tactic.h"
 #include"ufbv_tactic.h"
 #include"qffp_tactic.h"
-#include"qfufnra_tactic.h"
 #include"horn_tactic.h"
 #include"smt_solver.h"
 #include"inc_sat_solver.h"
 #include"fd_solver.h"
+#include"fd_tactic.h"
 #include"bv_rewriter.h"
 #include"solver2tactic.h"
 
@@ -91,9 +91,7 @@ tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const
     else if (logic=="HORN")
         return mk_horn_tactic(m, p);
     else if (logic == "QF_FD")
-        return mk_solver2tactic(mk_fd_solver(m, p));
-    //else if (logic=="QF_UFNRA")
-    //    return mk_qfufnra_tactic(m, p);
+        return mk_fd_tactic(m, p);
     else 
         return mk_default_tactic(m, p);
 }
diff --git a/src/test/lp.cpp b/src/test/lp.cpp
index 235dab960..9e05112f5 100644
--- a/src/test/lp.cpp
+++ b/src/test/lp.cpp
@@ -1159,12 +1159,14 @@ void solve_mps_double(std::string file_name, bool look_for_min, unsigned max_ite
     
     lp_solver<double, double> * solver =  reader.create_solver(dual);
     setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver);
-    int begin = get_millisecond_count();
+    stopwatch sw;
+    sw.start();
     if (dual) {
         std::cout << "solving for dual" << std::endl;
     }
     solver->find_maximal_solution();
-    int span = get_millisecond_span(begin);
+    sw.stop();
+    double span = sw.get_seconds(); 
     std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl;
     if (solver->get_status() == lp_status::OPTIMAL) {
         if (reader.column_names().size() < 20) {
@@ -1213,7 +1215,8 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i
     if (reader.is_ok()) {
         auto * solver =  reader.create_solver(dual);
         setup_solver(max_iterations, time_limit, look_for_min, args_parser, solver);
-        int begin = get_millisecond_count();
+        stopwatch sw;
+        sw.start();
         solver->find_maximal_solution();
         std::cout << "Status: " << lp_status_to_string(solver->get_status()) << std::endl;
 
@@ -1227,7 +1230,7 @@ void solve_mps_rational(std::string file_name, bool look_for_min, unsigned max_i
             }
             std::cout << "cost = " << cost.get_double() << std::endl;
         }
-        std::cout << "processed in " << get_millisecond_span(begin) / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl;
+        std::cout << "processed in " << sw.get_current_seconds() / 1000.0 << " seconds, running for " << solver->m_total_iterations << " iterations" << std::endl;
         delete solver;
     } else {
         std::cout << "cannot process " << file_name << std::endl;
@@ -2426,9 +2429,10 @@ void run_lar_solver(argument_parser & args_parser, lar_solver * solver, mps_read
         std::cout << "status = " << lp_status_to_string(solver->get_status()) <<  std::endl;
         return;
     }
-    int begin = get_millisecond_count();
+    stopwatch sw;
+    sw.start();
     lp_status status = solver->solve();
-    std::cout << "status is " <<  lp_status_to_string(status) << ", processed for " << get_millisecond_span(begin) / 1000.0 <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl;
+    std::cout << "status is " <<  lp_status_to_string(status) << ", processed for " << sw.get_current_seconds() <<" seconds, and " << solver->get_total_iterations() << " iterations" << std::endl;
     if (solver->get_status() == INFEASIBLE) {
         vector<std::pair<lean::mpq, constraint_index>> evidence;
         solver->get_infeasibility_explanation(evidence);
diff --git a/src/util/lp/lp_primal_simplex.h b/src/util/lp/lp_primal_simplex.h
index fcddb4eb1..715d76408 100644
--- a/src/util/lp/lp_primal_simplex.h
+++ b/src/util/lp/lp_primal_simplex.h
@@ -55,10 +55,6 @@ public:
     
     void set_core_solver_bounds();
 
-    void update_time_limit_from_starting_time(int start_time) {
-        this->m_settings.time_limit -= (get_millisecond_span(start_time) / 1000.);
-    }
-
     void find_maximal_solution();
 
     void fill_A_x_and_basis_for_stage_one_total_inf();
diff --git a/src/util/lp/lp_primal_simplex.hpp b/src/util/lp/lp_primal_simplex.hpp
index 9e1af2bbe..b6b6006e5 100644
--- a/src/util/lp/lp_primal_simplex.hpp
+++ b/src/util/lp/lp_primal_simplex.hpp
@@ -152,7 +152,6 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::set_core_solver_
 
 
 template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_solution() {
-    int preprocessing_start_time = get_millisecond_count();
     if (this->problem_is_empty()) {
         this->m_status = lp_status::EMPTY;
         return;
@@ -169,7 +168,6 @@ template <typename T, typename X> void lp_primal_simplex<T, X>::find_maximal_sol
     fill_acceptable_values_for_x();
     this->count_slacks_and_artificials();
     set_core_solver_bounds();
-    update_time_limit_from_starting_time(preprocessing_start_time);
     solve_with_total_inf();
 }
 
diff --git a/src/util/lp/lp_settings.h b/src/util/lp/lp_settings.h
index 6b6aba2ad..aac3692f9 100644
--- a/src/util/lp/lp_settings.h
+++ b/src/util/lp/lp_settings.h
@@ -8,9 +8,9 @@
 #include <string>
 #include <algorithm>
 #include <limits>
-#include <sys/timeb.h>
 #include <iomanip>
 #include "util/lp/lp_utils.h"
+#include "util/stopwatch.h"
 
 namespace lean {
 typedef unsigned var_index;
@@ -69,10 +69,6 @@ enum non_basic_column_value_position { at_low_bound, at_upper_bound, at_fixed, f
 
 template <typename X> bool is_epsilon_small(const X & v, const double& eps);    // forward definition
 
-int get_millisecond_count();
-int get_millisecond_span(int start_time);
-
-
 class lp_resource_limit {
 public:
     virtual bool get_cancel_flag() = 0;
@@ -92,12 +88,13 @@ struct lp_settings {
 private:
     class default_lp_resource_limit : public lp_resource_limit {
         lp_settings& m_settings;
-        int m_start_time;
+        stopwatch    m_sw;
     public:
-        default_lp_resource_limit(lp_settings& s): m_settings(s), m_start_time(get_millisecond_count()) {}
+        default_lp_resource_limit(lp_settings& s): m_settings(s) {
+            m_sw.start();
+        }
         virtual bool get_cancel_flag() {
-            int span_in_mills = get_millisecond_span(m_start_time);
-            return (span_in_mills / 1000.0  > m_settings.time_limit);
+            return (m_sw.get_current_seconds()  > m_settings.time_limit);
         }
     };
 
diff --git a/src/util/lp/lp_settings.hpp b/src/util/lp/lp_settings.hpp
index b57a3acda..b27d837e0 100644
--- a/src/util/lp/lp_settings.hpp
+++ b/src/util/lp/lp_settings.hpp
@@ -52,19 +52,6 @@ lp_status lp_status_from_string(std::string status) {
     lean_unreachable();
     return lp_status::UNKNOWN; // it is unreachable
 }
-int get_millisecond_count() {
-    timeb tb;
-    ftime(&tb);
-    return tb.millitm + (tb.time & 0xfffff) * 1000;
-}
-
-int get_millisecond_span(int start_time) {
-    int span = get_millisecond_count() - start_time;
-    if (span < 0)
-        span += 0x100000 * 1000;
-    return span;
-}
-
 
 
 template <typename T>
diff --git a/src/util/lp/matrix.hpp b/src/util/lp/matrix.hpp
index 27cdabd3e..d032cab8c 100644
--- a/src/util/lp/matrix.hpp
+++ b/src/util/lp/matrix.hpp
@@ -58,8 +58,8 @@ unsigned get_width_of_column(unsigned j, vector<vector<std::string>> & A) {
     unsigned r = 0;
     for (unsigned i = 0; i < A.size(); i++) {
         vector<std::string> & t = A[i];
-        std::string str= t[j];
-        unsigned s = str.size();
+        std::string str = t[j];
+        unsigned s = static_cast<unsigned>(str.size());
         if (r < s) {
             r = s;
         }
@@ -69,8 +69,8 @@ unsigned get_width_of_column(unsigned j, vector<vector<std::string>> & A) {
 
 void print_matrix_with_widths(vector<vector<std::string>> & A, vector<unsigned> & ws, std::ostream & out) {
     for (unsigned i = 0; i < A.size(); i++) {
-        for (unsigned j = 0; j < A[i].size(); j++) {
-            print_blanks(ws[j] - A[i][j].size(), out);
+        for (unsigned j = 0; j < static_cast<unsigned>(A[i].size()); j++) {
+            print_blanks(ws[j] - static_cast<unsigned>(A[i][j].size()), out);
             out << A[i][j] << " ";
         }
         out << std::endl;
diff --git a/src/util/lp/sparse_matrix.hpp b/src/util/lp/sparse_matrix.hpp
index ff6ac9997..32bb8ed4e 100644
--- a/src/util/lp/sparse_matrix.hpp
+++ b/src/util/lp/sparse_matrix.hpp
@@ -1050,8 +1050,8 @@ bool sparse_matrix<T, X>::get_pivot_for_column(unsigned &i, unsigned &j, int c_p
         if (i_inv < k) continue;
         unsigned j_inv = adjust_column_inverse(j);
         if (j_inv < k) continue;
-        int small = elem_is_too_small(i, j, c_partial_pivoting);
-        if (!small) {
+        int _small = elem_is_too_small(i, j, c_partial_pivoting);
+        if (!_small) {
 #ifdef LEAN_DEBUG
             // if (!really_best_pivot(i, j, c_partial_pivoting, k)) {
             //     print_active_matrix(k);
@@ -1063,7 +1063,7 @@ bool sparse_matrix<T, X>::get_pivot_for_column(unsigned &i, unsigned &j, int c_p
             j = j_inv;
             return true;
         }
-        if (small != 2) { // 2 means that the pair is not in the matrix
+        if (_small != 2) { // 2 means that the pair is not in the matrix
             pivots_candidates_that_are_too_small.push_back(std::make_pair(i, j));
         }
     }