diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index 9ec6f708f..3619a142a 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -18,8 +18,8 @@ Revision History:
 
 --*/
 #include<typeinfo>
-#include "api/api_context.h"
 #include "util/z3_version.h"
+#include "api/api_context.h"
 #include "ast/ast_pp.h"
 #include "ast/ast_ll_pp.h"
 #include "api/api_log_macros.h"
@@ -432,7 +432,7 @@ extern "C" {
 
     void Z3_API Z3_finalize_memory(void) {
         LOG_Z3_finalize_memory();
-        memory::finalize();
+        memory::finalize(true);
     }
 
     Z3_error_code Z3_API Z3_get_error_code(Z3_context c) {
diff --git a/src/cmd_context/check_logic.cpp b/src/cmd_context/check_logic.cpp
index f3c9176e3..9a69d4e6d 100644
--- a/src/cmd_context/check_logic.cpp
+++ b/src/cmd_context/check_logic.cpp
@@ -108,10 +108,13 @@ struct check_logic::imp {
             m_uf        = true;
             m_bvs       = true;
         }
-        else if (logic == "QF_DT") {
+        else if (logic == "QF_UFDT") {
             m_uf        = true;            
             m_dt        = true;
         }
+        else if (logic == "QF_DT") {
+            m_dt        = true;
+        }
         else if (logic == "QF_AUFLIA") {
             m_uf     = true;
             m_arrays = true;
@@ -505,7 +508,7 @@ struct check_logic::imp {
         try {
             unsigned arity = f->get_arity();
             if (arity > 0) {
-                if (!m_uf)
+                if (!m_uf && f->get_family_id() == null_family_id)
                     fail("logic does not support uninterpreted functions");
                 for (unsigned i = 0; i < arity; i++)
                     check_sort(f->get_domain(i));
diff --git a/src/math/lp/lp_core_solver_base.h b/src/math/lp/lp_core_solver_base.h
index 7f861ff5f..673ef2404 100644
--- a/src/math/lp/lp_core_solver_base.h
+++ b/src/math/lp/lp_core_solver_base.h
@@ -590,11 +590,16 @@ public:
             return out;
         }
 
-        out << "[" << j << "] " << std::setw(6) << " := " << m_x[j];
+        std::stringstream strm;
+        strm << m_x[j];
+        std::string j_val = strm.str();
+        out << "[" << j << "] " << std::setw(6) << " := " << j_val;
         if (m_basis_heading[j] >= 0)
-            out << " base\t";
+            out << " base ";
         else 
-            out << "     \t";
+            out << "      ";
+        for (auto k = j_val.size(); k < 15; ++k)
+            out << " ";
         switch (m_column_types[j]) {
         case column_type::fixed:
         case column_type::boxed:
diff --git a/src/sat/sat_extension.h b/src/sat/sat_extension.h
index 24e22d312..a05f7d163 100644
--- a/src/sat/sat_extension.h
+++ b/src/sat/sat_extension.h
@@ -96,6 +96,8 @@ namespace sat {
         virtual void push() = 0;
         void push_scopes(unsigned n) { for (unsigned i = 0; i < n; ++i) push(); }
         virtual void pop(unsigned n) = 0;
+        virtual void user_push() { push(); }
+        virtual void user_pop(unsigned n) { pop(n); }
         virtual void pre_simplify() {}
         virtual void simplify() {}
         // have a way to replace l by r in all constraints
diff --git a/src/sat/sat_solver.cpp b/src/sat/sat_solver.cpp
index 791973661..93942e21e 100644
--- a/src/sat/sat_solver.cpp
+++ b/src/sat/sat_solver.cpp
@@ -109,7 +109,13 @@ namespace sat {
 
     void solver::set_extension(extension* ext) {
         m_ext = ext;
-        if (ext) ext->set_solver(this);
+        if (ext) {
+            ext->set_solver(this);
+            for (unsigned i = num_user_scopes(); i-- > 0;)
+                ext->user_push();
+            for (unsigned i = num_scopes(); i-- > 0;)
+                ext->push();
+        }
     }
 
     void solver::copy(solver const & src, bool copy_learned) {
@@ -3622,6 +3628,8 @@ namespace sat {
         lit = literal(new_v, false);
         m_user_scope_literals.push_back(lit);
         m_cut_simplifier = nullptr; // for simplicity, wipe it out
+        if (m_ext)
+            m_ext->user_push();
         TRACE("sat", tout << "user_push: " << lit << "\n";);
     }
 
@@ -3704,6 +3712,8 @@ namespace sat {
     void solver::user_pop(unsigned num_scopes) {
         pop_to_base_level();
         TRACE("sat", display(tout););
+        if (m_ext)
+            m_ext->user_pop(num_scopes);
         while (num_scopes > 0) {
             literal lit = m_user_scope_literals.back();
             m_user_scope_literals.pop_back();
diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp
index 6d4579225..727fbc1e3 100644
--- a/src/sat/sat_solver/inc_sat_solver.cpp
+++ b/src/sat/sat_solver/inc_sat_solver.cpp
@@ -257,9 +257,8 @@ public:
     }
 
     void push_internal() {
+        m_goal2sat.user_push();
         m_solver.user_push();
-        if (get_euf())
-            get_euf()->user_push();
         ++m_num_scopes;
         m_mcs.push_back(m_mcs.back());
         m_fmls_lim.push_back(m_fmls.size());
@@ -279,6 +278,7 @@ public:
         m_map.pop(n);
         SASSERT(n <= m_num_scopes);
         m_solver.user_pop(n);
+        m_goal2sat.user_pop(n);
         m_num_scopes -= n;
         // ? m_internalized_converted = false;
         m_has_uninterpreted.pop(n);
@@ -339,12 +339,8 @@ public:
         m_params.set_sym("pb.solver", p1.pb_solver());
         m_solver.updt_params(m_params);
         m_solver.set_incremental(is_incremental() && !override_incremental());
-        if (p1.euf() && !get_euf()) {
-            ensure_euf();
-            for (unsigned i = 0; i < m_num_scopes; ++i)
-                get_euf()->user_push();
-        }
-
+        if (p1.euf() && !get_euf()) 
+            ensure_euf();        
     }
     void collect_statistics(statistics & st) const override {
         if (m_preprocess) m_preprocess->collect_statistics(st);
diff --git a/src/sat/smt/arith_axioms.cpp b/src/sat/smt/arith_axioms.cpp
index f1ebe7d79..14cd8b23b 100644
--- a/src/sat/smt/arith_axioms.cpp
+++ b/src/sat/smt/arith_axioms.cpp
@@ -332,8 +332,6 @@ namespace arith {
             le = mk_literal(a.mk_le(diff, zero));
             ge = mk_literal(a.mk_ge(diff, zero));
         }
-        // std::cout << "eq " << mk_pp(e1, m) << " " << mk_pp(e2, m) << " ";
-        // std::cout << le << " " << ge << "\n";
         add_clause(~eq, le);
         add_clause(~eq, ge);
         add_clause(~le, ~ge, eq);
diff --git a/src/sat/smt/arith_diagnostics.cpp b/src/sat/smt/arith_diagnostics.cpp
index 82ff03f04..026568e08 100644
--- a/src/sat/smt/arith_diagnostics.cpp
+++ b/src/sat/smt/arith_diagnostics.cpp
@@ -39,14 +39,27 @@ namespace arith {
             auto t = get_tv(v);
             auto vi = lp().external_to_column_index(v);
             out << "v" << v << " ";
-            if (t.is_null()) out << "null"; else out << (t.is_term() ? "t" : "j") << vi;
-            if (m_nla && m_nla->use_nra_model() && can_get_ivalue(v)) {
-                scoped_anum an(m_nla->am());
-                m_nla->am().display(out << " = ", nl_value(v, an));
+            if (is_bool(v)) {
+                euf::enode* n = var2enode(v);
+                api_bound* b = nullptr;
+                if (m_bool_var2bound.find(n->bool_var(), b)) {
+                    sat::literal lit = b->get_lit();
+                    out << lit << " " << s().value(lit);
+                }
+            }
+            else {
+                if (t.is_null()) 
+                    out << "null"; 
+                else 
+                    out << (t.is_term() ? "t" : "j") << vi;
+                if (m_nla && m_nla->use_nra_model() && can_get_ivalue(v)) {
+                    scoped_anum an(m_nla->am());
+                    m_nla->am().display(out << " = ", nl_value(v, an));
+                }
+                else if (can_get_value(v)) out << " = " << get_value(v);
+                if (is_int(v)) out << ", int";
+                if (ctx.is_shared(var2enode(v))) out << ", shared";
             }
-            else if (can_get_value(v)) out << " = " << get_value(v);
-            if (is_int(v)) out << ", int";
-            if (ctx.is_shared(var2enode(v))) out << ", shared";
             out << " := " << mk_bounded_pp(var2expr(v), m) << "\n";
         }
         return out; 
diff --git a/src/sat/smt/arith_internalize.cpp b/src/sat/smt/arith_internalize.cpp
index 7f8daa0db..4f5c1f9cf 100644
--- a/src/sat/smt/arith_internalize.cpp
+++ b/src/sat/smt/arith_internalize.cpp
@@ -21,7 +21,7 @@ Author:
 namespace arith {
 
     sat::literal solver::internalize(expr* e, bool sign, bool root, bool learned) {
-        force_push();
+        init_internalize();
         flet<bool> _is_learned(m_is_redundant, learned);
         internalize_atom(e);
         literal lit = ctx.expr2literal(e);
@@ -31,7 +31,7 @@ namespace arith {
     }
 
     void solver::internalize(expr* e, bool redundant) {
-        force_push();
+        init_internalize();
         flet<bool> _is_learned(m_is_redundant, redundant);
         if (m.is_bool(e))
             internalize_atom(e);
@@ -39,6 +39,19 @@ namespace arith {
             internalize_term(e);
     }
 
+    void solver::init_internalize() {
+        force_push();
+        // initialize 0, 1 variables:
+        if (!m_internalize_initialized) {
+            get_one(true);
+            get_one(false);
+            get_zero(true);
+            get_zero(false);
+            ctx.push(value_trail<euf::solver, bool>(m_internalize_initialized));
+            m_internalize_initialized = true;
+        }
+    }
+
     lpvar solver::get_one(bool is_int) {
         return add_const(1, is_int ? m_one_var : m_rone_var, is_int);
     }
@@ -113,11 +126,11 @@ namespace arith {
         if (var != UINT_MAX) {
             return var;
         }
+        ctx.push(value_trail<euf::solver, lpvar>(var));
         app_ref cnst(a.mk_numeral(rational(c), is_int), m);
         mk_enode(cnst);
         theory_var v = mk_evar(cnst);
         var = lp().add_var(v, is_int);
-        lp().push();
         add_def_constraint_and_equality(var, lp::GE, rational(c));
         add_def_constraint_and_equality(var, lp::LE, rational(c));
         TRACE("arith", tout << "add " << cnst << ", var = " << var << "\n";);
@@ -540,11 +553,15 @@ namespace arith {
         enode* n = ctx.get_enode(e);
         if (n)
             return n;
-        ptr_buffer<enode> args;
-        if (reflect(e))
-            for (expr* arg : *to_app(e))
-                args.push_back(e_internalize(arg));
-        n = ctx.mk_enode(e, args.size(), args.c_ptr());
+        if (!a.is_arith_expr(e))
+            n = e_internalize(e);
+        else {
+            ptr_buffer<enode> args;
+            if (reflect(e))
+                for (expr* arg : *to_app(e))
+                    args.push_back(e_internalize(arg));
+            n = ctx.mk_enode(e, args.size(), args.c_ptr());
+        }
         return n;
     }
 
@@ -597,7 +614,7 @@ namespace arith {
     }
 
     bool solver::reflect(expr* n) const {
-        return get_config().m_arith_reflect || a.is_underspecified(n);
+        return get_config().m_arith_reflect || a.is_underspecified(n) || !a.is_arith_expr(n);
     }
 
     lpvar solver::get_lpvar(theory_var v) const {
diff --git a/src/sat/smt/arith_solver.cpp b/src/sat/smt/arith_solver.cpp
index d1eddf1a7..0b0359530 100644
--- a/src/sat/smt/arith_solver.cpp
+++ b/src/sat/smt/arith_solver.cpp
@@ -32,11 +32,6 @@ namespace arith {
     {
         reset_variable_values();
         m_solver = alloc(lp::lar_solver);
-        // initialize 0, 1 variables:
-        get_one(true);
-        get_one(false);
-        get_zero(true);
-        get_zero(false);
 
         smt_params_helper lpar(ctx.s().params());
         lp().settings().set_resource_limit(m_resource_limit);
@@ -556,8 +551,35 @@ namespace arith {
         return end;
     }
 
-    void solver::init_model() {
-        init_variable_values();
+    void solver::dbg_finalize_model(model& mdl) {
+        bool found_bad = false;
+        for (unsigned v = 0; v < get_num_vars(); ++v) {
+            if (!is_bool(v))
+                continue;
+            euf::enode* n = var2enode(v);
+            api_bound* b = nullptr;
+            if (!m_bool_var2bound.find(n->bool_var(), b)) {
+                IF_VERBOSE(0, verbose_stream() << "no boolean variable\n";);
+                continue;
+            }
+            lbool value = n->value();
+            expr_ref eval = mdl(var2expr(v));
+            if (m.is_true(eval) && l_false == value)
+                found_bad = true;
+            if (m.is_false(eval) && l_true == value)
+                found_bad = true;
+
+            if (b->get_lit().sign())
+                value = ~value;
+            if (!found_bad && value == get_phase(n->bool_var()))
+                continue;
+            IF_VERBOSE(0, 
+                       verbose_stream() << eval << " " << value << " " << ctx.bpp(n) << "\n";
+                       verbose_stream() << n->bool_var() << " " << n->value() << " " << get_phase(n->bool_var()) << " " << ctx.bpp(n) << "\n";
+                       verbose_stream() << *b << "\n";);
+            IF_VERBOSE(0, ctx.display(verbose_stream()));
+            UNREACHABLE();
+        }
     }
 
     void solver::add_value(euf::enode* n, model& mdl, expr_ref_vector& values) {
diff --git a/src/sat/smt/arith_solver.h b/src/sat/smt/arith_solver.h
index 2e1eff67c..f0b084c9a 100644
--- a/src/sat/smt/arith_solver.h
+++ b/src/sat/smt/arith_solver.h
@@ -208,9 +208,7 @@ namespace arith {
         svector<enode_pair> m_eqs;
         vector<parameter>   m_params;
         nla::lemma          m_lemma;
-
-
-        arith_util        a;
+        arith_util          a;
 
         bool is_int(theory_var v) const { return is_int(var2enode(v)); }
         bool is_int(euf::enode* n) const { return a.is_int(n->get_expr()); }
@@ -221,6 +219,8 @@ namespace arith {
         
 
         // internalize
+        bool m_internalize_initialized { false };
+        void init_internalize();
         lpvar add_const(int c, lpvar& var, bool is_int);
         lpvar get_one(bool is_int);
         lpvar get_zero(bool is_int);
@@ -408,6 +408,7 @@ namespace arith {
         void assign(literal lit, literal_vector const& core, svector<enode_pair> const& eqs, vector<parameter> const& params);
 
         void false_case_of_check_nla(const nla::lemma& l);        
+        void dbg_finalize_model(model& mdl);
 
     public:
         solver(euf::solver& ctx, theory_id id);
@@ -426,7 +427,8 @@ namespace arith {
         void new_eq_eh(euf::th_eq const& eq) override { mk_eq_axiom(true, eq.v1(), eq.v2()); }
         void new_diseq_eh(euf::th_eq const& de) override { mk_eq_axiom(false, de.v1(), de.v2()); }
         bool unit_propagate() override;
-        void init_model() override;
+        void init_model() override { init_variable_values(); }
+        void finalize_model(model& mdl) override { DEBUG_CODE(dbg_finalize_model(mdl);); }
         void add_value(euf::enode* n, model& mdl, expr_ref_vector& values) override;
         sat::literal internalize(expr* e, bool sign, bool root, bool learned) override;
         void internalize(expr* e, bool redundant) override;
diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index eab04ff42..b52b58f83 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -60,7 +60,6 @@ namespace euf {
         SASSERT(get_enode(e));
         if (m.is_bool(e))
             return literal(si.to_bool_var(e), sign);
-        std::cout << "internalize-non-bool\n";
         return sat::null_literal;
     }
 
diff --git a/src/sat/smt/euf_relevancy.cpp b/src/sat/smt/euf_relevancy.cpp
index 2ffaa7827..795c83108 100644
--- a/src/sat/smt/euf_relevancy.cpp
+++ b/src/sat/smt/euf_relevancy.cpp
@@ -31,8 +31,11 @@ namespace euf {
     }
 
     void solver::ensure_dual_solver() {
-        if (!m_dual_solver)
+        if (!m_dual_solver) {
             m_dual_solver = alloc(sat::dual_solver, s().rlimit());
+            for (unsigned i = s().num_user_scopes(); i-- > 0; )
+                m_dual_solver->push();
+        }
     }
 
     void solver::add_root(unsigned n, sat::literal const* lits) {
@@ -79,7 +82,6 @@ namespace euf {
                 continue;
             expr* c = nullptr, *th = nullptr, *el = nullptr;
             if (m.is_ite(e, c, th, el)) {
-                std::cout << mk_pp(c, m) << "\n";
                 sat::literal lit = expr2literal(c);
                 todo.push_back(c);
                 switch (s().value(lit)) {
diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index 17f8dc2fa..b103df9d3 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -126,7 +126,7 @@ namespace euf {
         if (use_drat())
             s().get_drat().add_theory(fid, th->name());
         th->set_solver(m_solver);
-        th->push_scopes(s().num_scopes());
+        th->push_scopes(s().num_scopes() + s().num_user_scopes());
         m_solvers.push_back(th);
         m_id2solver.setx(fid, th, nullptr);
         if (th->use_diseqs())
@@ -430,18 +430,6 @@ namespace euf {
         m_egraph.push();
     }
 
-    void solver::user_push() {
-        push();
-        if (m_dual_solver)
-            m_dual_solver->push();
-    }
-
-    void solver::user_pop(unsigned n) {
-        pop(n);
-        if (m_dual_solver)
-            m_dual_solver->pop(n);
-    }
-
     void solver::pop(unsigned n) {
         start_reinit(n);
         m_trail.pop_scope(n);
@@ -455,7 +443,19 @@ namespace euf {
         m_var_trail.shrink(s.m_var_lim);        
         m_scopes.shrink(m_scopes.size() - n);
         SASSERT(m_egraph.num_scopes() == m_scopes.size());
-        TRACE("euf", display(tout << "pop to: " << m_scopes.size() << "\n"););
+        TRACE("euf_verbose", display(tout << "pop to: " << m_scopes.size() << "\n"););
+    }
+
+    void solver::user_push() {
+        push();
+        if (m_dual_solver)
+            m_dual_solver->push();
+    }
+
+    void solver::user_pop(unsigned n) {
+        pop(n);
+        if (m_dual_solver)
+            m_dual_solver->pop(n);
     }
 
     void solver::start_reinit(unsigned n) {
@@ -487,6 +487,8 @@ namespace euf {
             }
         };
         scoped_set_replay replay(*this);
+        scoped_suspend_rlimit suspend_rlimit(m.limit());
+
         unsigned i = 0;
         for (sat::bool_var v : s().get_vars_to_reinit()) {
             expr* e = m_reinit_exprs.get(i++);
@@ -696,7 +698,7 @@ namespace euf {
     unsigned solver::max_var(unsigned w) const { 
         for (auto* e : m_solvers)
             w = e->max_var(w);
-        for (unsigned sz = m_bool_var2expr.size(); sz-- > 0; ) {
+        for (unsigned sz = m_bool_var2expr.size(); sz > w && sz-- > 0; ) {
             expr* n = m_bool_var2expr[sz];
             if (n && m.is_bool(n)) {
                 w = std::max(w, sz);
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 2ab0b6d78..d8f10c992 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -261,8 +261,8 @@ namespace euf {
         sat::check_result check() override;
         void push() override;
         void pop(unsigned n) override;
-        void user_push();
-        void user_pop(unsigned n);
+        void user_push() override;
+        void user_pop(unsigned n) override;
         void pre_simplify() override;
         void simplify() override;
         // have a way to replace l by r in all constraints
diff --git a/src/sat/smt/q_mbi.cpp b/src/sat/smt/q_mbi.cpp
index 6aa326ffb..2fc1a9e23 100644
--- a/src/sat/smt/q_mbi.cpp
+++ b/src/sat/smt/q_mbi.cpp
@@ -158,6 +158,7 @@ namespace q {
         mbody = subst(mbody, result->vars);
         if (is_forall(q))
             mbody = mk_not(m, mbody);
+        TRACE("q", tout << "specialize " << mbody << "\n";);
         return result;
     }
 
@@ -187,9 +188,11 @@ namespace q {
     expr_ref mbqi::solver_project(model& mdl, q_body& qb) {
         for (app* v : qb.vars)
             m_model->register_decl(v->get_decl(), mdl(v));
-        std::cout << "Project\n";
-        std::cout << *m_model << "\n";
-        std::cout << qb.vbody << "\n";
+        TRACE("q",
+              tout << "Project\n";
+              tout << *m_model << "\n";
+              tout << qb.vbody << "\n";
+              tout << "model of projection\n" << mdl << "\n";);
         expr_ref_vector fmls(qb.vbody);
         app_ref_vector vars(qb.vars);
         mbp::project_plugin proj(m);
diff --git a/src/sat/smt/q_model_fixer.cpp b/src/sat/smt/q_model_fixer.cpp
index 94dde44c7..b3678aa94 100644
--- a/src/sat/smt/q_model_fixer.cpp
+++ b/src/sat/smt/q_model_fixer.cpp
@@ -71,6 +71,7 @@ namespace q {
         if (univ.empty())
             return;
 
+        TRACE("q", tout << "start: " << mdl << "\n";);
         m_dependencies.reset();
         m_projection_data.reset();
         m_projection_pinned.reset();
@@ -88,6 +89,7 @@ namespace q {
 
         univ.append(residue);
         add_projection_functions(mdl, univ);
+        TRACE("q", tout << "end: " << mdl << "\n";);
     }
 
     quantifier_macro_info* model_fixer::operator()(quantifier* q) {
@@ -103,11 +105,9 @@ namespace q {
 
     void model_fixer::add_projection_functions(model& mdl, ptr_vector<quantifier> const& qs) {
         func_decl_set fns;
-        TRACE("q", tout << mdl << "\n";);
         collect_partial_functions(qs, fns);
         for (func_decl* f : fns)
             add_projection_functions(mdl, f);
-        TRACE("q", tout << mdl << "\n";);
     }
 
     void model_fixer::add_projection_functions(model& mdl, func_decl* f) {
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 131adabc3..8b8e87bcf 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -606,8 +606,6 @@ struct goal2sat::imp : public sat::sat_internalizer {
         if (!ext) {
             euf = alloc(euf::solver, m, *this);
             m_solver.set_extension(euf);
-            for (unsigned i = m_solver.num_scopes(); i-- > 0; )
-                euf->push();
 #if 0
             std::function<solver*(void)> mk_solver = [&]() {
                 return mk_inc_sat_solver(m, m_params, true);
@@ -911,6 +909,14 @@ struct goal2sat::imp : public sat::sat_internalizer {
             ext->update_model(mdl);
     }
 
+    void user_push() {
+        
+    }
+
+    void user_pop(unsigned n) {
+        m_true = sat::null_literal;
+    }
+
 };
 
 struct unsupported_bool_proc {
@@ -984,6 +990,16 @@ void goal2sat::update_model(model_ref& mdl) {
         m_imp->update_model(mdl);
 }
 
+void goal2sat::user_push() {
+    if (m_imp)
+        m_imp->user_push();
+}
+    
+void goal2sat::user_pop(unsigned n) {
+    if (m_imp)
+        m_imp->user_pop(n);
+}
+
 
 sat::sat_internalizer& goal2sat::si(ast_manager& m, params_ref const& p, sat::solver_core& t, atom2bool_var& a2b, dep2asm_map& dep2asm, bool default_external) {
     if (!m_imp)
diff --git a/src/sat/tactic/goal2sat.h b/src/sat/tactic/goal2sat.h
index e55b856ab..ba9270f5a 100644
--- a/src/sat/tactic/goal2sat.h
+++ b/src/sat/tactic/goal2sat.h
@@ -69,6 +69,10 @@ public:
 
     void update_model(model_ref& mdl);
 
+    void user_push();
+    
+    void user_pop(unsigned n);
+
 };
 
 
diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp
index 0421c5f46..9e240e102 100644
--- a/src/smt/theory_lra.cpp
+++ b/src/smt/theory_lra.cpp
@@ -1437,13 +1437,15 @@ public:
     }
         
     rational get_value(theory_var v) const {
+        TRACE("arith", tout << "get_value v" << v << "\n";);
         if (v == null_theory_var || !lp().external_is_used(v)) {
             return rational::zero();
         }
 
         auto t = get_tv(v);
+        auto E = m_variable_values.end();
         auto I = m_variable_values.find(t.index());
-        if (I != m_variable_values.end())
+        if (I != E)
             return I->second;
 
         if (!t.is_term() && lp().is_fixed(t.id())) 
@@ -1462,7 +1464,7 @@ public:
                 for (const auto & i : term) {
                     auto tv = lp().column2tv(i.column());
                     auto I = m_variable_values.find(tv.index());
-                    if (I != m_variable_values.end()) {
+                    if (I != E) {
                         result += I->second * coeff * i.coeff();
                     }
                     else {
@@ -1471,7 +1473,9 @@ public:
                 }                    
             }
             else {
-                result += m_variable_values.at(t2.index()) * coeff;
+                auto I = m_variable_values.find(t2.index());
+                if (I != E)
+                    result += I->second * coeff;
             }
         }
         m_variable_values.emplace(t.index(), result);
@@ -1481,8 +1485,8 @@ public:
     void init_variable_values() {
         reset_variable_values();
         if (m.inc() && m_solver.get() && th.get_num_vars() > 0) {            
-            TRACE("arith", display(tout << "update variable values\n"););
             lp().get_model(m_variable_values);
+            TRACE("arith", display(tout << "update variable values " << m_variable_values.size() << "\n"););            
         }
     }
 
@@ -3698,8 +3702,7 @@ public:
             b = m.mk_not(b);
         }
         TRACE("arith", tout << b << "\n";);
-        return expr_ref(b, m);
-            
+        return expr_ref(b, m);            
     }
 
 
diff --git a/src/solver/smt_logics.cpp b/src/solver/smt_logics.cpp
index 9b77bca6d..bf0651a95 100644
--- a/src/solver/smt_logics.cpp
+++ b/src/solver/smt_logics.cpp
@@ -22,10 +22,10 @@ Revision History:
 
 
 bool smt_logics::supported_logic(symbol const & s) {
-    return logic_has_uf(s) || logic_is_allcsp(s) || logic_has_fd(s) || 
+    return logic_has_uf(s) || logic_is_all(s) || logic_has_fd(s) || 
         logic_has_arith(s) || logic_has_bv(s) ||
         logic_has_array(s) || logic_has_seq(s) || logic_has_str(s) ||
-        logic_has_horn(s) || logic_has_fpa(s);
+        logic_has_horn(s) || logic_has_fpa(s) || logic_has_datatype(s);
 }
 
 bool smt_logics::logic_has_reals_only(symbol const& s) {
@@ -86,7 +86,7 @@ bool smt_logics::logic_has_arith(symbol const & s) {
         s == "QF_BVFP" ||
         s == "QF_S" ||
         s == "QF_SLIA" ||
-        logic_is_allcsp(s) ||
+        logic_is_all(s) ||
         s == "QF_FD" ||
         s == "HORN" ||
         s == "QF_FPLRA";
@@ -106,7 +106,7 @@ bool smt_logics::logic_has_bv(symbol const & s) {
         s == "QF_FPBV" ||
         s == "FP" ||
         s == "QF_BVFP" ||
-        logic_is_allcsp(s) ||
+        logic_is_all(s) ||
         s == "QF_FD" ||
         s == "SMTFD" ||
         s == "HORN";
@@ -128,7 +128,7 @@ bool smt_logics::logic_has_array(symbol const & s) {
         s == "AUFNIRA" ||
         s == "AUFBV" ||
         s == "ABV" ||
-        logic_is_allcsp(s) ||
+        logic_is_all(s) ||
         s == "QF_ABV" ||
         s == "QF_AUFBV" ||
         s == "SMTFD" ||
@@ -136,15 +136,15 @@ bool smt_logics::logic_has_array(symbol const & s) {
 }
 
 bool smt_logics::logic_has_seq(symbol const & s) {
-    return s == "QF_BVRE" || s == "QF_S" || s == "QF_SLIA" || logic_is_allcsp(s);
+    return s == "QF_BVRE" || s == "QF_S" || s == "QF_SLIA" || logic_is_all(s);
 }
 
 bool smt_logics::logic_has_str(symbol const & s) {
-    return s == "QF_S" || s == "QF_SLIA" || logic_is_allcsp(s);
+    return s == "QF_S" || s == "QF_SLIA" || logic_is_all(s);
 }
 
 bool smt_logics::logic_has_fpa(symbol const & s) {
-    return s == "FP" || s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA"  || logic_is_allcsp(s);
+    return s == "FP" || s == "QF_FP" || s == "QF_FPBV" || s == "QF_BVFP" || s == "QF_FPLRA"  || logic_is_all(s);
 }
 
 bool smt_logics::logic_has_uf(symbol const & s) {
@@ -156,10 +156,10 @@ bool smt_logics::logic_has_horn(symbol const& s) {
 }
 
 bool smt_logics::logic_has_pb(symbol const& s) {
-    return s == "QF_FD" || logic_is_allcsp(s) || logic_has_horn(s);
+    return s == "QF_FD" || logic_is_all(s) || logic_has_horn(s);
 }
 
 bool smt_logics::logic_has_datatype(symbol const& s) {
-    return s == "QF_FD" || logic_is_allcsp(s) || s == "QF_DT";
+    return s == "QF_FD" || s == "QF_UFDT" || logic_is_all(s) || s == "QF_DT";
 }
 
diff --git a/src/solver/smt_logics.h b/src/solver/smt_logics.h
index 14fdffc06..3e6dd9098 100644
--- a/src/solver/smt_logics.h
+++ b/src/solver/smt_logics.h
@@ -24,8 +24,6 @@ public:
     static bool supported_logic(symbol const & s);
     static bool logic_has_reals_only(symbol const& l);       
     static bool logic_is_all(symbol const& s) { return s == "ALL"; }
-    static bool logic_is_csp(symbol const& s) { return s == "CSP"; }
-    static bool logic_is_allcsp(symbol const& s) { return logic_is_all(s) || logic_is_csp(s); }
     static bool logic_has_uf(symbol const& s);
     static bool logic_has_arith(symbol const & s);
     static bool logic_has_bv(symbol const & s);
diff --git a/src/util/memory_manager.cpp b/src/util/memory_manager.cpp
index 37b2ea716..4fdf20c3a 100644
--- a/src/util/memory_manager.cpp
+++ b/src/util/memory_manager.cpp
@@ -12,6 +12,7 @@ Copyright (c) 2015 Microsoft Corporation
 #include "util/memory_manager.h"
 #include "util/error_codes.h"
 #include "util/debug.h"
+#include "util/scoped_timer.h"
 // The following two function are automatically generated by the mk_make.py script.
 // The script collects ADD_INITIALIZER and ADD_FINALIZER commands in the .h files.
 // For example, rational.h contains
@@ -27,7 +28,6 @@ Copyright (c) 2015 Microsoft Corporation
 //    rational::finalize();
 void mem_initialize();
 void mem_finalize();
-void finalize_scoped_timer();
 
 // If PROFILE_MEMORY is defined, Z3 will display the amount of memory used, and the number of synchronization steps during finalization
 // #define PROFILE_MEMORY
@@ -142,7 +142,7 @@ void memory::finalize(bool shutdown) {
         g_finalizing = false;
 
         if (shutdown) {
-            finalize_scoped_timer();
+            scoped_timer::finalize();
         }
     }
 }
diff --git a/src/util/scoped_timer.cpp b/src/util/scoped_timer.cpp
index bfef8ba04..c8273b3bf 100644
--- a/src/util/scoped_timer.cpp
+++ b/src/util/scoped_timer.cpp
@@ -116,7 +116,7 @@ scoped_timer::~scoped_timer() {
     dealloc(m_imp);
 }
 
-void finalize_scoped_timer() {
+void scoped_timer::finalize() {
     unsigned deleted = 0;
 
     while (deleted < num_workers) {
diff --git a/src/util/scoped_timer.h b/src/util/scoped_timer.h
index 41dcce7b3..f54cba558 100644
--- a/src/util/scoped_timer.h
+++ b/src/util/scoped_timer.h
@@ -26,4 +26,5 @@ class scoped_timer {
 public:
     scoped_timer(unsigned ms, event_handler * eh);
     ~scoped_timer();
+    static void finalize();
 };