diff --git a/src/ast/simplifiers/extract_eqs.h b/src/ast/simplifiers/extract_eqs.h
index 724425d6a..b88a3e8a5 100644
--- a/src/ast/simplifiers/extract_eqs.h
+++ b/src/ast/simplifiers/extract_eqs.h
@@ -31,8 +31,9 @@ namespace euf {
         expr* orig;       // original expression that encoded equation
         app* var;         // isolated variable
         expr_ref term;    // defined term
-        expr_dependency* dep;
-        dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : orig(orig), var(var), term(term), dep(d) {}
+        expr_dependency_ref dep;
+        dependent_eq(expr* orig, app* var, expr_ref const& term, expr_dependency* d) : 
+            orig(orig), var(var), term(term), dep(d, term.get_manager()) {}
     };
 
     typedef vector<dependent_eq> dep_eq_vector;
diff --git a/src/ast/sls/bv_sls_eval.cpp b/src/ast/sls/bv_sls_eval.cpp
index 486b33445..d7ce8e703 100644
--- a/src/ast/sls/bv_sls_eval.cpp
+++ b/src/ast/sls/bv_sls_eval.cpp
@@ -1996,11 +1996,7 @@ namespace bv {
             out << e->get_id() << ": " << mk_bounded_pp(e, m, 1) << " ";
             if (is_fixed0(e))
                 out << "f ";
-            if (bv.is_bv(e))
-                out << wval(e);
-            else if (m.is_bool(e))
-                out << (bval0(e) ? "T" : "F");
-            out << "\n";
+            display_value(out, e) << "\n";
         }
         terms.reset();
         return out;
diff --git a/src/math/lp/lar_solver.h b/src/math/lp/lar_solver.h
index ec40fcb24..f223b5cc5 100644
--- a/src/math/lp/lar_solver.h
+++ b/src/math/lp/lar_solver.h
@@ -393,6 +393,7 @@ public:
     bool external_is_used(unsigned) const;
     void pop(unsigned k);
     unsigned num_scopes() const { return m_trail.get_num_scopes(); }
+    trail_stack& trail() { return m_trail; }
     bool compare_values(lpvar j, lconstraint_kind kind, const mpq& right_side);
     lpvar add_term(const vector<std::pair<mpq, lpvar>>& coeffs, unsigned ext_i);
     void register_existing_terms();
diff --git a/src/tactic/portfolio/smt_strategic_solver.cpp b/src/tactic/portfolio/smt_strategic_solver.cpp
index 138c6e646..09e7aa047 100644
--- a/src/tactic/portfolio/smt_strategic_solver.cpp
+++ b/src/tactic/portfolio/smt_strategic_solver.cpp
@@ -49,8 +49,18 @@ Notes:
 #include "parsers/smt2/smt2parser.h"
 #include "sat/sat_params.hpp"
 
+tactic* mk_tactic_for_logic(ast_manager& m, params_ref const& p, symbol const& logic);
 
 
+class smt_nested_solver_factory : public solver_factory {
+public:
+    solver* operator()(ast_manager& m, params_ref const& p, bool proofs_enabled, bool models_enabled, bool unsat_core_enabled, symbol const& logic) override {
+        auto t = mk_tactic_for_logic(m, p, logic);
+        auto s = mk_tactic2solver(m, t, p, proofs_enabled, models_enabled, unsat_core_enabled, logic);
+        return s;
+    }
+};
+
 tactic * mk_tactic_for_logic(ast_manager & m, params_ref const & p, symbol const & logic) {
     if (logic=="QF_UF")
         return mk_qfuf_tactic(m, p);