diff --git a/src/ackermannization/ackr_bound_probe.cpp b/src/ackermannization/ackr_bound_probe.cpp
index c6cdaf268..4c18a3f7e 100644
--- a/src/ackermannization/ackr_bound_probe.cpp
+++ b/src/ackermannization/ackr_bound_probe.cpp
@@ -65,7 +65,7 @@ public:
             for_each_expr_core<proc, expr_fast_mark1, true, true>(p, visited, g.form(i));
         }
         const double total = ackr_helper::calculate_lemma_bound(p.m_fun2terms);
-        TRACE("ackr_bound_probe", tout << "total=" << total << std::endl;);
+        TRACE("ackermannize", tout << "total=" << total << std::endl;);
         return result(total);
     }
 
diff --git a/src/ackermannization/ackr_model_converter.cpp b/src/ackermannization/ackr_model_converter.cpp
index c5e04ab23..4815d5a2c 100644
--- a/src/ackermannization/ackr_model_converter.cpp
+++ b/src/ackermannization/ackr_model_converter.cpp
@@ -84,7 +84,7 @@ void ackr_model_converter::convert(model * source, model * destination) {
 }
 
 void ackr_model_converter::convert_constants(model * source, model * destination) {
-    TRACE("ackr_model", tout << "converting constants\n";);
+    TRACE("ackermannize", tout << "converting constants\n";);
     obj_map<func_decl, func_interp*> interpretations;
     model_evaluator evaluator(*source);
     evaluator.set_model_completion(true);
@@ -113,7 +113,7 @@ void ackr_model_converter::convert_constants(model * source, model * destination
 void ackr_model_converter::add_entry(model_evaluator & evaluator,
                                      app* term, expr* value,
                                      obj_map<func_decl, func_interp*>& interpretations) {
-    TRACE("ackr_model", tout << "add_entry"
+    TRACE("ackermannize", tout << "add_entry"
           << mk_ismt2_pp(term, m, 2)
           << "->"
           << mk_ismt2_pp(value, m, 2) << "\n";
@@ -137,7 +137,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
         args.push_back(std::move(arg_value));
     }
     if (fi->get_entry(args.c_ptr()) == nullptr) {
-        TRACE("ackr_model",
+        TRACE("ackermannize",
               tout << mk_ismt2_pp(declaration, m) << " args: " << std::endl;
                 for (unsigned i = 0; i < args.size(); i++)
                     tout << mk_ismt2_pp(args.get(i), m) << std::endl;
@@ -145,7 +145,7 @@ void ackr_model_converter::add_entry(model_evaluator & evaluator,
         fi->insert_new_entry(args.c_ptr(), value);
     }
     else {
-        TRACE("ackr_model", tout << "entry already present\n";);
+        TRACE("ackermannize", tout << "entry already present\n";);
     }
 
 }
diff --git a/src/ackermannization/lackr.cpp b/src/ackermannization/lackr.cpp
index 9130d628c..a965fc261 100644
--- a/src/ackermannization/lackr.cpp
+++ b/src/ackermannization/lackr.cpp
@@ -56,7 +56,7 @@ lbool lackr::operator() () {
     if (!init()) return l_undef;
     const lbool rv = m_eager ? eager() : lazy();
     if (rv == l_true) m_sat->get_model(m_model);
-    CTRACE("lackr", rv == l_true,
+    CTRACE("ackermannize", rv == l_true,
         model_smt2_pp(tout << "abstr_model(\n", m_m, *(m_model.get()), 2); tout << ")\n"; );
     return rv;
 }
@@ -89,7 +89,7 @@ bool lackr::init() {
 // Introduce ackermann lemma for the two given terms.
 //
 bool lackr::ackr(app * const t1, app * const t2) {
-    TRACE("lackr", tout << "ackr "
+    TRACE("ackermannize", tout << "ackr "
             << mk_ismt2_pp(t1, m_m, 2) << " , " << mk_ismt2_pp(t2, m_m, 2) << "\n";);
     const unsigned sz = t1->get_num_args();
     SASSERT(t2->get_num_args() == sz);
@@ -99,7 +99,7 @@ bool lackr::ackr(app * const t1, app * const t2) {
         expr * const arg2 = t2->get_arg(i);
         if (m_m.are_equal(arg1, arg2)) continue; // quickly skip syntactically equal
         if (m_m.are_distinct(arg1, arg2)){ // quickly abort if there are two distinct (e.g. numerals)                    
-            TRACE("lackr", tout << "never eq\n";);
+            TRACE("ackermannize", tout << "never eq\n";);
             return false;
         }
         eqs.push_back(m_m.mk_eq(arg1, arg2));
@@ -107,19 +107,19 @@ bool lackr::ackr(app * const t1, app * const t2) {
     app * const a1 = m_info->get_abstr(t1);
     app * const a2 = m_info->get_abstr(t2);
     SASSERT(a1 && a2);
-    TRACE("lackr", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";);
-    TRACE("lackr", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";);
+    TRACE("ackermannize", tout << "abstr1 " << mk_ismt2_pp(a1, m_m, 2) << "\n";);
+    TRACE("ackermannize", tout << "abstr2 " << mk_ismt2_pp(a2, m_m, 2) << "\n";);
     expr_ref lhs(m_m);
     lhs = (eqs.size() == 1) ? eqs.get(0) : m_m.mk_and(eqs.size(), eqs.c_ptr());
-    TRACE("lackr", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";);
+    TRACE("ackermannize", tout << "ackr constr lhs" << mk_ismt2_pp(lhs, m_m, 2) << "\n";);
     expr_ref rhs(m_m.mk_eq(a1, a2),m_m);
-    TRACE("lackr", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";);
+    TRACE("ackermannize", tout << "ackr constr rhs" << mk_ismt2_pp(rhs, m_m, 2) << "\n";);
     expr_ref cg(m_m.mk_implies(lhs, rhs), m_m);
-    TRACE("lackr", tout << "ackr constr" << mk_ismt2_pp(cg, m_m, 2) << "\n";);
+    TRACE("ackermannize", tout << "ackr constr" << mk_ismt2_pp(cg, m_m, 2) << "\n";);
     expr_ref cga(m_m);
     m_info->abstract(cg, cga); // constraint needs abstraction due to nested applications
     m_simp(cga);
-    TRACE("lackr", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
+    TRACE("ackermannize", tout << "ackr constr abs:" << mk_ismt2_pp(cga, m_m, 2) << "\n";);
     if (m_m.is_true(cga)) return false;
     m_st.m_ackrs_sz++;
     m_ackrs.push_back(cga);
@@ -130,11 +130,10 @@ bool lackr::ackr(app * const t1, app * const t2) {
 // Introduce the ackermann lemma for each pair of terms.
 //
 void lackr::eager_enc() {
-    TRACE("lackr", tout << "#funs: " << m_fun2terms.size() << std::endl;);
-    const fun2terms_map::iterator e = m_fun2terms.end();
-    for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
+    TRACE("ackermannize", tout << "#funs: " << m_fun2terms.size() << std::endl;);
+    for (auto const& kv : m_fun2terms) {
         checkpoint();
-        app_set * const  ts = i->get_value();
+        app_set * const  ts = kv.get_value();
         const app_set::iterator r = ts->end();
         for (app_set::iterator j = ts->begin(); j != r; ++j) {
             app_set::iterator k = j;
@@ -142,10 +141,11 @@ void lackr::eager_enc() {
             for (;  k != r; ++k) {
                 app * const t1 = *j;
                 app * const t2 = *k;
-                SASSERT(t1->get_decl() == i->m_key);
-                SASSERT(t2->get_decl() == i->m_key);
-                if (t1 == t2) continue;
-                ackr(t1,t2);
+                SASSERT(t1->get_decl() == kv.m_key);
+                SASSERT(t2->get_decl() == kv.m_key);
+                if (t1 != t2) {
+                    ackr(t1,t2);
+                }
             }
         }
     }
@@ -153,18 +153,15 @@ void lackr::eager_enc() {
 
 
 void lackr::abstract() {
-    const fun2terms_map::iterator e = m_fun2terms.end();
-    for (fun2terms_map::iterator i = m_fun2terms.begin(); i != e; ++i) {
-        func_decl* const fd = i->m_key;
-        app_set * const ts = i->get_value();
+    for (auto const& kv : m_fun2terms) {
+        func_decl* const fd = kv.m_key;
+        app_set * const ts = kv.get_value();
         sort* const s = fd->get_range();
-        const app_set::iterator r = ts->end();
-        for (app_set::iterator j = ts->begin(); j != r; ++j) {
+        for (app * t : (*ts)) {
             app * const fc = m_m.mk_fresh_const(fd->get_name().str().c_str(), s);
-            app * const t = *j;
             SASSERT(t->get_decl() == fd);
             m_info->set_abstr(t, fc);
-            TRACE("lackr", tout << "abstr term "
+            TRACE("ackermannize", tout << "abstr term "
                     << mk_ismt2_pp(t, m_m, 2)
                     << " -> "
                     << mk_ismt2_pp(fc, m_m, 2)
@@ -189,7 +186,7 @@ void lackr::add_term(app* a) {
         ts = alloc(app_set);
         m_fun2terms.insert(fd, ts);
     }
-    TRACE("lackr", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
+    TRACE("ackermannize", tout << "term(" << mk_ismt2_pp(a, m_m, 2) << ")\n";);
     ts->insert(a);
 }
 
@@ -203,7 +200,7 @@ void  lackr::push_abstraction() {
 lbool lackr::eager() {
     SASSERT(m_is_init);
     push_abstraction();
-    TRACE("lackr", tout << "run sat 0\n"; );
+    TRACE("ackermannize", tout << "run sat 0\n"; );
     const lbool rv0 = m_sat->check_sat(0, nullptr);
     if (rv0 == l_false) return l_false;
     eager_enc();
@@ -211,7 +208,7 @@ lbool lackr::eager() {
     all = m_m.mk_and(m_ackrs.size(), m_ackrs.c_ptr());
     m_simp(all);
     m_sat->assert_expr(all);
-    TRACE("lackr", tout << "run sat all\n"; );
+    TRACE("ackermannize", tout << "run sat all\n"; );
     return m_sat->check_sat(0, nullptr);
 }
 
@@ -223,7 +220,7 @@ lbool lackr::lazy() {
     while (true) {
         m_st.m_it++;
         checkpoint();
-        TRACE("lackr", tout << "lazy check: " << m_st.m_it << "\n";);
+        TRACE("ackermannize", tout << "lazy check: " << m_st.m_it << "\n";);
         const lbool r = m_sat->check_sat(0, nullptr);
         if (r == l_undef) return l_undef; // give up
         if (r == l_false) return l_false; // abstraction unsat
@@ -264,16 +261,15 @@ bool lackr::collect_terms() {
                 visited.mark(curr, true);
                 stack.pop_back();
                 break;
-            case AST_APP:
-            {
+            case AST_APP: {
                 app * const a = to_app(curr);
                 if (for_each_expr_args(stack, visited, a->get_num_args(), a->get_args())) {
                     visited.mark(curr, true);
                     stack.pop_back();
                     add_term(a);
                 }
-            }
                 break;
+            }
             case AST_QUANTIFIER:
                 return false; // quantifiers not supported
             default:
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index 47c919d4a..35bbde2b2 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -237,10 +237,12 @@ struct check_logic::imp {
                 return;
             }
             else if (m_bv_arrays) {
-                if (get_array_arity(s) != 1)
-                    fail("logic supports only unidimensional arrays");
-                if (!m_bv_util.is_bv_sort(get_array_range(s)) || !m_bv_util.is_bv_sort(get_array_domain(s, 0)))
-                    fail("logic supports only arrays from bitvectors to bitvectors");
+                unsigned sz = get_array_arity(s);
+                for (unsigned i = 0; i < sz; ++i) {
+                    if (!m_bv_util.is_bv_sort(get_array_domain(s, i)))
+                        fail("logic supports only arrays from bitvectors to bitvectors");
+                }
+                check_sort(get_array_range(s));
             }
             else {
                 fail("logic does not support arrays");
diff --git a/src/opt/maxres.cpp b/src/opt/maxres.cpp
index 86eab4eea..b507d6f54 100644
--- a/src/opt/maxres.cpp
+++ b/src/opt/maxres.cpp
@@ -383,6 +383,7 @@ public:
             }
             if (core.empty()) {
                 IF_VERBOSE(100, verbose_stream() << "(opt.maxres core is empty)\n";);
+                TRACE("opt", tout << "empty core\n";);
                 cores.reset();
                 m_lower = m_upper;
                 return l_true;
@@ -517,6 +518,10 @@ public:
         max_resolve(core, w);
         fml = mk_not(m, mk_and(m, core.size(), core.c_ptr()));
         add(fml);
+        // save small cores such that lex-combinations of maxres can reuse these cores.
+        if (core.size() <= 2) {
+            m_defs.push_back(fml);
+        }
         m_lower += w;
         if (m_st == s_primal_dual) {
             m_lower = std::min(m_lower, m_upper);
@@ -847,7 +852,10 @@ public:
         _solver->assert_expr(s().get_assertions());
         _solver->assert_expr(core);
         lbool is_sat = _solver->check_sat(0, nullptr);
-        IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << "\n");
+        IF_VERBOSE(0, verbose_stream() << "core status (l_false:) " << is_sat << " core size " << core.size() << "\n");
+        CTRACE("opt", is_sat != l_false, 
+               for (expr* c : core) tout << "core: " << mk_pp(c, m) << "\n";
+               _solver->display(tout););
         VERIFY(is_sat == l_false);
     }
 
diff --git a/src/opt/opt_context.cpp b/src/opt/opt_context.cpp
index 50b61a8e2..ffb8754a2 100644
--- a/src/opt/opt_context.cpp
+++ b/src/opt/opt_context.cpp
@@ -383,7 +383,7 @@ namespace opt {
     lbool context::execute_min_max(unsigned index, bool committed, bool scoped, bool is_max) {
         if (scoped) get_solver().push();            
         lbool result = m_optsmt.lex(index, is_max);
-        if (result == l_true) m_optsmt.get_model(m_model, m_labels);
+        if (result == l_true) { m_optsmt.get_model(m_model, m_labels); SASSERT(m_model); }
         if (scoped) get_solver().pop(1);        
         if (result == l_true && committed) m_optsmt.commit_assignment(index);
         if (result == l_true && m_optsmt.is_unbounded(index, is_max) && contains_quantifiers()) {
@@ -1604,6 +1604,7 @@ namespace opt {
     void context::validate_lex() {
         rational r1;
         expr_ref val(m);
+        SASSERT(m_model);
         for (unsigned i = 0; i < m_objectives.size(); ++i) {
             objective const& obj = m_objectives[i];
             switch(obj.m_type) {
diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp
index a461d4a22..7feb8f615 100644
--- a/src/opt/optsmt.cpp
+++ b/src/opt/optsmt.cpp
@@ -171,6 +171,7 @@ namespace opt {
     }
 
     lbool optsmt::geometric_lex(unsigned obj_index, bool is_maximize) {
+        TRACE("opt", tout << "index: " << obj_index << " is-max: " << is_maximize << "\n";);
         arith_util arith(m);
         bool is_int = arith.is_int(m_objs[obj_index].get());
         lbool is_sat = l_true;
@@ -189,9 +190,11 @@ namespace opt {
             SASSERT(delta_per_step.is_int());
             SASSERT(delta_per_step.is_pos());
             is_sat = m_s->check_sat(0, nullptr);
+            TRACE("opt", tout << "check " << is_sat << "\n";);
             if (is_sat == l_true) {                
                 m_s->maximize_objective(obj_index, bound);
                 m_s->get_model(m_model);
+                SASSERT(m_model);
                 m_s->get_labels(m_labels);
                 inf_eps obj = m_s->saved_objective_value(obj_index);
                 update_lower_lex(obj_index, obj, is_maximize);
@@ -220,13 +223,17 @@ namespace opt {
                 delta_per_step = rational::one();
                 SASSERT(num_scopes > 0);
                 --num_scopes;
-                m_s->pop(1);             
+                m_s->pop(1);                             
             }
             else {
                 break;
             }
         }
         m_s->pop(num_scopes);        
+
+        if (is_sat == l_false && !m_model) {
+            return l_false;
+        }
         
         if (m.canceled() || is_sat == l_undef) {
             return l_undef;
@@ -574,7 +581,7 @@ namespace opt {
         return m_upper[i];
     }
 
-    void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {
+    void optsmt::get_model(model_ref& mdl, svector<symbol> & labels) {        
         mdl = m_model.get();
         labels = m_labels;
     }
diff --git a/src/smt/smt_context_pp.cpp b/src/smt/smt_context_pp.cpp
index c79068298..20a084c81 100644
--- a/src/smt/smt_context_pp.cpp
+++ b/src/smt/smt_context_pp.cpp
@@ -567,12 +567,9 @@ namespace smt {
         case b_justification::AXIOM:
             out << "axiom";
             break;
-        case b_justification::BIN_CLAUSE: {
-            literal l2 = j.get_literal();
-            out << "bin-clause ";
-            display_literal(out, l2);
+        case b_justification::BIN_CLAUSE: 
+            out << "bin " << j.get_literal();
             break;
-        }
         case b_justification::CLAUSE: {
             clause * cls = j.get_clause();
             out << "clause ";
@@ -580,10 +577,9 @@ namespace smt {
             break;
         }
         case b_justification::JUSTIFICATION: {
-            out << "justification " << j.get_justification()->get_from_theory() << ": ";
             literal_vector lits;
             const_cast<conflict_resolution&>(*m_conflict_resolution).justification2literals(j.get_justification(), lits);
-            display_literals(out, lits);
+            out << "justification " << j.get_justification()->get_from_theory() << ": " << lits;
             break;
         }
         default:
diff --git a/src/smt/theory_pb.cpp b/src/smt/theory_pb.cpp
index 03f4b62c3..86d84c60a 100644
--- a/src/smt/theory_pb.cpp
+++ b/src/smt/theory_pb.cpp
@@ -1836,8 +1836,6 @@ namespace smt {
             return false;
         }
 
-        // std::cout << c.lit() << "\n";
-
         reset_coeffs();
         m_num_marks = 0;
         m_bound = c.k();
@@ -1936,7 +1934,10 @@ namespace smt {
                 }
                 if (pbj == nullptr) {
                     TRACE("pb", tout << "skip justification for " << conseq << "\n";);
-                    inc_coeff(conseq, offset);
+                    // this is possible when conseq is an assumption.
+                    // The justification of conseq is itself, 
+                    // don't increment the cofficient here because it assumes
+                    // conseq is justified further. it isnt'. conseq becomes part of the lemma.
                 }
                 else {
                     card& c2 = pbj->get_card();
@@ -1944,7 +1945,6 @@ namespace smt {
                     bound = c2.k();
                 }
                 
-                // std::cout << " offset: " << offset << " bound: " << bound << "\n";
                 break;
             }
             default:
@@ -2020,6 +2020,7 @@ namespace smt {
         SASSERT(slack < 0);
 
         SASSERT(validate_antecedents(m_antecedents));
+        TRACE("pb", tout << "antecedents " << m_antecedents << "\n";);
         ctx.assign(alit, ctx.mk_justification(theory_propagation_justification(get_id(), ctx.get_region(), m_antecedents.size(), m_antecedents.c_ptr(), alit, 0, nullptr)));
 
         DEBUG_CODE(
@@ -2127,7 +2128,7 @@ namespace smt {
                 break;
             }
         }
-        TRACE("pb", display(tout << "validate: ", c, true);
+        TRACE("pb_verbose", display(tout << "validate: ", c, true);
               tout << "sum: " << sum << " " << maxsum << " ";
               tout << ctx.get_assignment(c.lit()) << "\n";);
 
@@ -2215,15 +2216,11 @@ namespace smt {
 
     void theory_pb::display_resolved_lemma(std::ostream& out) const {
         context& ctx = get_context();
-        bool_var v;
-        unsigned lvl;
         out << "num marks: " << m_num_marks << "\n";
         out << "conflict level: " << m_conflict_lvl << "\n";
-        for (unsigned i = 0; i < m_resolved.size(); ++i) {
-            v = m_resolved[i].var();
-            lvl = ctx.get_assign_level(v);
-            out << lvl << ": " << m_resolved[i] << " ";
-            ctx.display(out, ctx.get_justification(v));
+        for (literal r : m_resolved) {
+            out << ctx.get_assign_level(r) << ": " << r << " ";
+            ctx.display(out, ctx.get_justification(r.var()));
         }
 
         if (!m_antecedents.empty()) {
diff --git a/src/tactic/core/propagate_values_tactic.cpp b/src/tactic/core/propagate_values_tactic.cpp
index 14c715f03..f9712120f 100644
--- a/src/tactic/core/propagate_values_tactic.cpp
+++ b/src/tactic/core/propagate_values_tactic.cpp
@@ -23,7 +23,6 @@ Revision History:
 #include "ast/ast_smt2_pp.h"
 #include "ast/expr_substitution.h"
 #include "tactic/goal_shared_occs.h"
-#include "ast/pb_decl_plugin.h"
 
 namespace {
 class propagate_values_tactic : public tactic {
@@ -117,23 +116,10 @@ class propagate_values_tactic : public tactic {
         TRACE("shallow_context_simplifier_bug", tout << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n";);
         if (new_curr != curr) {
             m_modified = true;
-            //if (has_pb(curr))
-            //    IF_VERBOSE(0, verbose_stream() << mk_ismt2_pp(curr, m) << "\n---->\n" << mk_ismt2_pp(new_curr, m) << "\n");
         }
         push_result(new_curr, new_pr);
     }
 
-    bool has_pb(expr* e) {
-        pb_util pb(m);
-        if (pb.is_ge(e)) return true;
-        if (m.is_or(e)) {
-            for (expr* a : *to_app(e)) {
-                if (pb.is_ge(a)) return true;
-            }
-        }
-        return false;
-    }
-
     void run(goal_ref const & g, goal_ref_buffer & result) {
         SASSERT(g->is_well_sorted());
         tactic_report report("propagate-values", *g);
diff --git a/src/tactic/core/solve_eqs_tactic.cpp b/src/tactic/core/solve_eqs_tactic.cpp
index f665fe509..1ed230886 100644
--- a/src/tactic/core/solve_eqs_tactic.cpp
+++ b/src/tactic/core/solve_eqs_tactic.cpp
@@ -16,14 +16,15 @@ Author:
 Revision History:
 
 --*/
-#include "tactic/tactical.h"
 #include "ast/rewriter/expr_replacer.h"
-#include "tactic/generic_model_converter.h"
-#include "ast/occurs.h"
 #include "util/cooperate.h"
-#include "tactic/goal_shared_occs.h"
+#include "ast/occurs.h"
+#include "ast/ast_util.h"
 #include "ast/ast_pp.h"
 #include "ast/pb_decl_plugin.h"
+#include "tactic/goal_shared_occs.h"
+#include "tactic/tactical.h"
+#include "tactic/generic_model_converter.h"
 
 class solve_eqs_tactic : public tactic {
     struct imp {
@@ -384,6 +385,20 @@ class solve_eqs_tactic : public tactic {
             
             return false;
         }
+
+        void insert_solution(goal const& g, unsigned idx, expr* f, app* var, expr* def, proof* pr) {
+            m_vars.push_back(var);
+            m_candidates.push_back(f);
+            m_candidate_set.mark(f);
+            m_candidate_vars.mark(var);
+            if (m_produce_proofs) {
+                if (!pr)
+                    pr = g.pr(idx);
+                else
+                    pr = m().mk_modus_ponens(g.pr(idx), pr);
+            }
+            m_subst->insert(var, def, pr, g.dep(idx));
+        }
         
         /**
            \brief Start collecting candidates
@@ -408,17 +423,7 @@ class solve_eqs_tactic : public tactic {
                 checkpoint();
                 expr * f = g.form(idx);
                 if (solve(f, var, def, pr)) {
-                    m_vars.push_back(var);
-                    m_candidates.push_back(f);
-                    m_candidate_set.mark(f);
-                    m_candidate_vars.mark(var);
-                    if (m_produce_proofs) {
-                        if (pr == 0)
-                            pr = g.pr(idx);
-                        else
-                            pr = m().mk_modus_ponens(g.pr(idx), pr);
-                    }
-                    m_subst->insert(var, def, pr, g.dep(idx));
+                    insert_solution(g, idx, f, var, def, pr);
                 }
                 m_num_steps++;
             }
@@ -430,6 +435,163 @@ class solve_eqs_tactic : public tactic {
                   }
                   tout << "\n";);
         }
+
+        struct nnf_context {
+            bool m_is_and;
+            expr_ref_vector m_args;
+            unsigned m_index;
+            nnf_context(bool is_and, expr_ref_vector const& args, unsigned idx):
+                m_is_and(is_and),
+                m_args(args),
+                m_index(idx)
+            {}
+        };
+
+        bool is_compatible(goal const& g, unsigned idx, vector<nnf_context> const & path, expr* v, expr* eq) {
+            return is_goal_compatible(g, idx, v, eq) && is_path_compatible(path, v, eq);
+        }
+
+        bool is_goal_compatible(goal const& g, unsigned idx, expr* v, expr* eq) {
+            bool all_e = false;
+            for (unsigned j = 0; j < g.size(); ++j) {              
+                if (j != idx && !check_eq_compat(g.form(j), v, eq, all_e)) {
+                    TRACE("solve_eqs", tout << "occurs goal " << mk_pp(eq, m()) << "\n";);
+                    return false;
+                }
+            }
+            return true;
+        }
+
+        // 
+        // all_e := all disjunctions contain eq
+        //
+        // or, all_e -> skip if all disjunctions contain eq
+        // or, all_e -> fail if some disjunction contains v but not eq
+        // or, all_e -> all_e := false if some disjunction does not contain v
+        // and, all_e -> all_e
+        //
+
+        bool is_path_compatible(vector<nnf_context> const & path, expr* v, expr* eq) {
+            bool all_e = true;
+            for (unsigned i = path.size(); i-- > 0; ) {
+                auto const& p = path[i];
+                auto const& args = p.m_args;
+                if (p.m_is_and && !all_e) {
+                    for (unsigned j = 0; j < args.size(); ++j) {
+                        if (j != p.m_index && occurs(v, args[j])) {
+                            TRACE("solve_eqs", tout << "occurs and " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
+                            return false;
+                        }
+                    }
+                }
+                else if (!p.m_is_and) {
+                    for (unsigned j = 0; j < args.size(); ++j) {
+                        if (j != p.m_index) {
+                            if (occurs(v, args[j])) {
+                                if (!check_eq_compat(args[j], v, eq, all_e)) {
+                                    TRACE("solve_eqs", tout << "occurs or " << mk_pp(eq, m()) << " " << mk_pp(args[j], m()) << "\n";);
+                                    return false;
+                                }
+                            }
+                            else {
+                                all_e = false;
+                            }
+                        }
+                    }
+                }
+            }
+            return true;
+        }
+
+        bool check_eq_compat(expr* f, expr* v, expr* eq, bool& all) {
+            expr_ref_vector args(m());
+            expr* f1 = nullptr;
+            if (!occurs(v, f)) {
+                all = false;
+                return true;
+            }
+            if (m().is_not(f, f1) && m().is_or(f1)) {
+                flatten_and(f, args);
+                for (expr* arg : args) {
+                    if (arg == eq) {
+                        return true;
+                    }
+                }                
+            }
+            else if (m().is_or(f)) {
+                flatten_or(f, args);
+            }
+            else {
+                return false;
+            }
+
+            for (expr* arg : args) {
+                if (!check_eq_compat(arg, v, eq, all)) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
+        void hoist_nnf(goal const& g, expr* f, vector<nnf_context> & path, unsigned idx, unsigned depth) {
+            if (depth > 4) {
+                return;
+            }
+            app_ref var(m());
+            expr_ref def(m());
+            proof_ref pr(m());
+            expr_ref_vector args(m());
+            expr* f1 = nullptr;
+
+            if (m().is_not(f, f1) && m().is_or(f1)) {
+                flatten_and(f, args);
+                for (unsigned i = 0; i < args.size(); ++i) {
+                    expr* arg = args.get(i), *lhs = nullptr, *rhs = nullptr;
+                    if (m().is_eq(arg, lhs, rhs)) { 
+                        if (trivial_solve1(lhs, rhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
+                            insert_solution(g, idx, arg, var, def, pr);
+                        }
+                        else if (trivial_solve1(rhs, lhs, var, def, pr) && is_compatible(g, idx, path, var, arg)) {
+                            insert_solution(g, idx, arg, var, def, pr);
+                        }
+                        else {
+                            IF_VERBOSE(0, 
+                                       verbose_stream() << "eq not solved " << mk_pp(arg, m()) << "\n";
+                                       verbose_stream() << is_uninterp_const(lhs) << " " << !m_candidate_vars.is_marked(lhs) << " " 
+                                       << !occurs(lhs, rhs) << " " << check_occs(lhs) << "\n";);
+                        }
+                    }
+                    else {
+                        path.push_back(nnf_context(true, args, i));
+                        hoist_nnf(g, arg, path, idx, depth + 1);
+                        path.pop_back();
+                    }                             
+                }
+            }
+            else if (m().is_or(f)) {
+                flatten_or(f, args);
+                //std::cout << "hoist or " << args.size() << "\n";
+                for (unsigned i = 0; i < args.size(); ++i) {
+                    path.push_back(nnf_context(false, args, i));
+                    hoist_nnf(g, args.get(i), path, idx, depth + 1);
+                    path.pop_back();
+                }
+            }
+            else {
+                // std::cout << "no hoist " << mk_pp(f, m()) << "\n";
+            }
+        }
+
+        bool collect_hoist(goal const& g) {
+            bool change = false;
+            unsigned size = g.size();
+            vector<nnf_context> path;
+            for (unsigned idx = 0; idx < size; idx++) {
+                checkpoint();
+                hoist_nnf(g, g.form(idx), path, idx, 0);
+            }
+            return change;
+        }
         
         void sort_vars() {
             SASSERT(m_candidates.size() == m_vars.size());
@@ -564,6 +726,10 @@ class solve_eqs_tactic : public tactic {
                 ++idx;
             }
             
+            IF_VERBOSE(10, 
+                       verbose_stream() << "ordered vars: ";
+                       for (app* v : m_ordered_vars) verbose_stream() << mk_pp(v, m()) << " ";
+                       verbose_stream() << "\n";);
             TRACE("solve_eqs", 
                   tout << "ordered vars:\n";
                   for (app* v : m_ordered_vars) {
@@ -756,6 +922,8 @@ class solve_eqs_tactic : public tactic {
                 while (true) {
                     collect_num_occs(*g);
                     collect(*g);
+                    // TBD Disabled until tested more:
+                    // collect_hoist(*g);
                     if (m_subst->empty()) 
                         break;
                     sort_vars();
@@ -773,6 +941,7 @@ class solve_eqs_tactic : public tactic {
             g->inc_depth();
             g->add(mc.get());
             result.push_back(g.get());
+            //IF_VERBOSE(0, g->display(verbose_stream()));
             TRACE("solve_eqs", g->display(tout););
             SASSERT(g->is_well_sorted());
         }
diff --git a/src/tactic/smtlogics/qfaufbv_tactic.cpp b/src/tactic/smtlogics/qfaufbv_tactic.cpp
index b35bc1f20..e3d7ec953 100644
--- a/src/tactic/smtlogics/qfaufbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfaufbv_tactic.cpp
@@ -24,13 +24,10 @@ Notes:
 #include "tactic/bv/max_bv_sharing_tactic.h"
 #include "tactic/bv/bv_size_reduction_tactic.h"
 #include "tactic/core/ctx_simplify_tactic.h"
-#include "sat/tactic/sat_tactic.h"
+#include "ackermannization/ackermannize_bv_tactic.h"
 #include "smt/tactic/smt_tactic.h"
 
-tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
-    params_ref main_p;
-    main_p.set_bool("elim_and", true);
-    main_p.set_bool("sort_store", true);
+static tactic * mk_qfaufbv_preamble(ast_manager & m, params_ref const & p) {
 
     params_ref simp2_p = p;
     simp2_p.set_bool("som", true);
@@ -39,26 +36,27 @@ tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
     simp2_p.set_bool("local_ctx", true);
     simp2_p.set_uint("local_ctx_limit", 10000000);
 
-    params_ref ctx_simp_p;
-    ctx_simp_p.set_uint("max_depth", 32);
-    ctx_simp_p.set_uint("max_steps", 5000000);
 
-    params_ref solver_p;
-    solver_p.set_bool("array.simplify", false); // disable array simplifications at old_simplify module
+    return and_then(mk_simplify_tactic(m),
+                    mk_propagate_values_tactic(m),
+                    mk_solve_eqs_tactic(m),
+                    mk_elim_uncnstr_tactic(m),
+                    // sound to use? if_no_proofs(if_no_unsat_cores(mk_reduce_args_tactic(m))),
+                    if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
+                    using_params(mk_simplify_tactic(m), simp2_p),
+                    mk_max_bv_sharing_tactic(m),
+                    if_no_proofs(if_no_unsat_cores(mk_ackermannize_bv_tactic(m, p)))
+                    );
+}
 
-    tactic * preamble_st = and_then(mk_simplify_tactic(m),
-                                    mk_propagate_values_tactic(m),
-                                    // using_params(mk_ctx_simplify_tactic(m), ctx_simp_p),
-                                    mk_solve_eqs_tactic(m),
-                                    mk_elim_uncnstr_tactic(m),
-                                    if_no_proofs(if_no_unsat_cores(mk_bv_size_reduction_tactic(m))),
-                                    using_params(mk_simplify_tactic(m), simp2_p),
-                                    mk_max_bv_sharing_tactic(m)
-                                    );
+tactic * mk_qfaufbv_tactic(ast_manager & m, params_ref const & p) {
+    params_ref main_p;
+    main_p.set_bool("elim_and", true);
+    main_p.set_bool("sort_store", true);
 
-    tactic * st = using_params(and_then(preamble_st,
-                                        using_params(mk_smt_tactic(m), solver_p)),
-                               main_p);
+    tactic * preamble_st = mk_qfaufbv_preamble(m, p);
+
+    tactic * st = using_params(and_then(preamble_st, mk_smt_tactic(m)), main_p);
     
     st->updt_params(p);
     return st;
diff --git a/src/tactic/tactic.cpp b/src/tactic/tactic.cpp
index 4a51c701a..95eeaa251 100644
--- a/src/tactic/tactic.cpp
+++ b/src/tactic/tactic.cpp
@@ -39,13 +39,14 @@ struct tactic_report::imp {
     ~imp() {
         m_watch.stop();
         double end_memory = static_cast<double>(memory::get_allocation_size())/static_cast<double>(1024*1024);
-        verbose_stream() << "(" << m_id
-                         << " :num-exprs " << m_goal.num_exprs()
-                         << " :num-asts " << m_goal.m().get_num_asts()
-                         << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
-                         << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
-                         << " :after-memory " << std::fixed << std::setprecision(2) << end_memory
-                         << ")" << std::endl;
+        IF_VERBOSE(0, 
+                   verbose_stream() << "(" << m_id
+                   << " :num-exprs " << m_goal.num_exprs()
+                   << " :num-asts " << m_goal.m().get_num_asts()
+                   << " :time " << std::fixed << std::setprecision(2) << m_watch.get_seconds()
+                   << " :before-memory " << std::fixed << std::setprecision(2) << m_start_memory
+                   << " :after-memory " << std::fixed << std::setprecision(2) << end_memory
+                   << ")" << std::endl);
     }
 };