diff --git a/src/ast/pattern/expr_pattern_match.cpp b/src/ast/pattern/expr_pattern_match.cpp
index d688c840c..c441fb4ce 100644
--- a/src/ast/pattern/expr_pattern_match.cpp
+++ b/src/ast/pattern/expr_pattern_match.cpp
@@ -387,7 +387,7 @@ expr_pattern_match::initialize(char const * spec_string) {
     m_instrs.push_back(instr(BACKTRACK));
 
     std::istringstream is(spec_string);
-    cmd_context      ctx(true, &m_manager);
+    cmd_context      ctx(true, &m_manager);	
     bool ps = ctx.print_success_enabled();
     ctx.set_print_success(false);
     VERIFY(parse_smt2_commands(ctx, is));
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 6ae63a1a6..11f800b25 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -718,8 +718,8 @@ void cmd_context::init_manager_core(bool new_manager) {
     }
     m_dt_eh = alloc(dt_eh, *this);
     m_pmanager->set_new_datatype_eh(m_dt_eh.get());
-    if (!has_logic()) {
-        TRACE("cmd_context", tout << "init manager\n";);
+    if (!has_logic() && new_manager) {
+        TRACE("cmd_context", tout << "init manager " << m_logic << "\n";);
         // add list type only if the logic is not specified.
         // it prevents clashes with builtin types.
         insert(pm().mk_plist_decl());
@@ -757,6 +757,7 @@ void cmd_context::init_external_manager() {
 }
 
 bool cmd_context::set_logic(symbol const & s) {
+    TRACE("cmd_context", tout << s << "\n";);
     if (has_logic())
         throw cmd_exception("the logic has already been set");
     if (has_manager() && m_main_ctx)
@@ -1240,7 +1241,7 @@ void cmd_context::insert_aux_pdecl(pdecl * p) {
     m_aux_pdecls.push_back(p);
 }
 
-void cmd_context::reset(bool finalize) {
+void cmd_context::reset(bool finalize) {    
     m_processing_pareto = false;
     m_logic = symbol::null;
     m_check_sat_result = nullptr;
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 94841603d..ff5bb4486 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1473,7 +1473,7 @@ bool theory_seq::add_solution(expr* l, expr* r, dependency* deps)  {
     if (l == r) {
         return false;
     }
-    TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n";);
+    TRACE("seq", tout << mk_pp(l, m) << " ==> " << mk_pp(r, m) << "\n"; display_deps(tout, deps););
     m_new_solution = true;
     m_rep.update(l, r, deps);
     enode* n1 = ensure_enode(l);
@@ -1513,7 +1513,9 @@ bool theory_seq::solve_eq(expr_ref_vector const& l, expr_ref_vector const& r, de
     change = canonize(r, rs, dep2) || change;
     deps = m_dm.mk_join(dep2, deps);
     TRACE("seq", tout << l << " = " << r << " ==> ";
-          tout << ls << " = " << rs << "\n";);
+          tout << ls << " = " << rs << "\n";
+          display_deps(tout, deps);
+          );
     if (!ctx.inconsistent() && simplify_eq(ls, rs, deps)) {
         return true;
     }
@@ -2674,7 +2676,12 @@ void theory_seq::init_model(expr_ref_vector const& es) {
     }
 }
 
+void theory_seq::finalize_model(model_generator& mg) {
+    m_rep.pop_scope(1);
+}
+
 void theory_seq::init_model(model_generator & mg) {
+    m_rep.push_scope();
     m_factory = alloc(seq_factory, get_manager(), get_family_id(), mg.get_model());
     mg.register_factory(m_factory);
     for (ne const& n : m_nqs) {
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 21aedd7e3..a17b29eba 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -64,14 +64,14 @@ namespace smt {
         // + a cache for normalization.
         class solution_map {
             enum map_update { INS, DEL };
-            ast_manager&                      m;
+            ast_manager&           m;
             dependency_manager&    m_dm;
-            eqdep_map_t                       m_map;            
-            eval_cache                        m_cache;
-            expr_ref_vector                   m_lhs, m_rhs;
+            eqdep_map_t            m_map;            
+            eval_cache             m_cache;
+            expr_ref_vector        m_lhs, m_rhs;
             ptr_vector<dependency> m_deps;
-            svector<map_update>               m_updates;
-            unsigned_vector                   m_limit;
+            svector<map_update>    m_updates;
+            unsigned_vector        m_limit;
 
             void add_trail(map_update op, expr* l, expr* r, dependency* d);
         public:
@@ -362,6 +362,7 @@ namespace smt {
         void collect_statistics(::statistics & st) const override;
         model_value_proc * mk_value(enode * n, model_generator & mg) override;
         void init_model(model_generator & mg) override;
+        void finalize_model(model_generator & mg) override;
         void init_search_eh() override;
 
         void init_model(expr_ref_vector const& es);