diff --git a/src/smt/smt_clause_proof.cpp b/src/smt/smt_clause_proof.cpp
index 390a54029..fde08fea8 100644
--- a/src/smt/smt_clause_proof.cpp
+++ b/src/smt/smt_clause_proof.cpp
@@ -99,7 +99,7 @@ namespace smt {
     }
 
     void clause_proof::update(status st, expr_ref_vector& v, proof* p) {
-        TRACE("clause_proof", tout << st << " " << v << "\n";);
+        TRACE("clause_proof", tout << m_trail.size() << " " << st << " " << v << "\n";);
         IF_VERBOSE(3, verbose_stream() << st << " " << v << "\n");
         m_trail.push_back(info(st, v, p));
     }
diff --git a/src/smt/smt_solver.cpp b/src/smt/smt_solver.cpp
index ea21bc329..e7ce999df 100644
--- a/src/smt/smt_solver.cpp
+++ b/src/smt/smt_solver.cpp
@@ -88,24 +88,24 @@ namespace smt {
             smt_solver * result = alloc(smt_solver, m, p, m_logic);
             smt::kernel::copy(m_context, result->m_context);
 
-
             if (mc0()) 
                 result->set_model_converter(mc0()->translate(translator));
 
             for (auto & kv : m_name2assertion) { 
                 expr* val = translator(kv.m_value);
-                expr* t = translator(kv.m_key);
-                result->m_name2assertion.insert(t, val);
-                result->solver_na2as::assert_expr(val, t);
-                m.inc_ref(val);
+                expr* key = translator(kv.m_key);
+                result->assert_expr(val, key);
             }
 
             return result;
         }
 
         ~smt_solver() override {
-            dec_ref_values(get_manager(), m_name2assertion);
             dealloc(m_cuber);
+            for (auto& kv : m_name2assertion) {
+                get_manager().dec_ref(kv.m_key);
+                get_manager().dec_ref(kv.m_value);
+            }
         }
 
         void updt_params(params_ref const & p) override {
@@ -159,6 +159,7 @@ namespace smt {
             }
             solver_na2as::assert_expr_core2(t, a);
             get_manager().inc_ref(t);
+            get_manager().inc_ref(a);
             m_name2assertion.insert(a, t);
         }
 
@@ -173,13 +174,12 @@ namespace smt {
                 SASSERT(n <= lvl);
                 unsigned new_lvl = lvl - n;
                 unsigned old_sz = m_scopes[new_lvl];
-                for (unsigned i = cur_sz; i > old_sz; ) {
-                    --i;
-                    expr * key = m_assumptions[i].get();
-                    SASSERT(m_name2assertion.contains(key));
+                for (unsigned i = cur_sz; i-- > old_sz; ) {
+                    expr * key = m_assumptions.get(i);
                     expr * value = m_name2assertion.find(key);
-                    m.dec_ref(value);
                     m_name2assertion.erase(key);
+                    m.dec_ref(value);
+                    m.dec_ref(key);
                 }
             }
             m_context.pop(n);
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 79c596b18..1b906c8f6 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -5632,17 +5632,10 @@ void theory_seq::add_axiom(literal l1, literal l2, literal l3, literal l4, liter
     TRACE("seq", ctx.display_literals_verbose(tout << "assert:", lits) << "\n";);
     m_new_propagation = true;
     ++m_stats.m_add_axiom;
-    {
-        std::function<expr*(void)> fn = [&]() { return m.mk_or(exprs.size(), exprs.c_ptr()); };
-        scoped_trace_stream _sts(*this, fn);
-        ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());
-    }
-
-#if 0
-    if (!ctx.at_base_level() && l2 == null_literal) {
-        m_trail_stack.push(push_replay(alloc(replay_unit_literal, m, ctx.bool_var2expr(l1.var()), l1.sign())));        
-    }
-#endif
+    
+    std::function<expr*(void)> fn = [&]() { return m.mk_or(exprs.size(), exprs.c_ptr()); };
+    scoped_trace_stream _sts(*this, fn);
+    ctx.mk_th_axiom(get_id(), lits.size(), lits.c_ptr());    
 }