diff --git a/src/api/api_context.cpp b/src/api/api_context.cpp
index abc02fc68..bd0967ab2 100644
--- a/src/api/api_context.cpp
+++ b/src/api/api_context.cpp
@@ -27,6 +27,7 @@ Revision History:
 #include "ast/reg_decl_plugins.h"
 #include "math/realclosure/realclosure.h"
 
+
 // The install_tactics procedure is automatically generated
 void install_tactics(tactic_manager & ctx);
 
@@ -383,7 +384,6 @@ extern "C" {
         if (a) {
             mk_c(c)->m().dec_ref(to_ast(a));
         }
-
         Z3_CATCH;
     }
 
diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py
index 540a2b728..2bc055b6f 100644
--- a/src/api/python/z3/z3.py
+++ b/src/api/python/z3/z3.py
@@ -1630,7 +1630,7 @@ def Xor(a, b, ctx=None):
     >>> Xor(p, q)
     Xor(p, q)
     >>> simplify(Xor(p, q))
-    q == Not(p) 
+    q == Not(p)
     """
     ctx = _get_ctx(_ctx_from_ast_arg_list([a, b], ctx))
     s = BoolSort(ctx)
diff --git a/src/ast/ast.cpp b/src/ast/ast.cpp
index a0ee29130..d7b81b424 100644
--- a/src/ast/ast.cpp
+++ b/src/ast/ast.cpp
@@ -169,28 +169,6 @@ bool family_manager::has_family(symbol const & s) const {
     return m_families.contains(s);
 }
 
-#if 0
-static unsigned s_count = 0;
-void ast::inc_ref() {
-    SASSERT(m_ref_count < UINT_MAX);
-    m_ref_count ++;
-    if (get_id() == 1) {
-        s_count++;
-        if (s_count >= 36530) {
-            TRACE("rc", tout << "inc_ref " << m_ref_count << "\n";);
-        }
-    }
-}
-
-void ast::dec_ref() {
-    SASSERT(m_ref_count > 0);
-    m_ref_count --;
-    if (get_id() == 1 && s_count >= 36530) {
-        TRACE("rc", tout << "dec_ref " << m_ref_count << "\n";);
-        // IF_VERBOSE(0, verbose_stream() << "dec_rc " << s_count << "\n";);
-    }
-}
-#endif
 
 // -----------------------------------
 //
diff --git a/src/ast/ast.h b/src/ast/ast.h
index 05b4c241e..a551b8928 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -482,7 +482,6 @@ protected:
     void *   m_mark2_owner;
 #endif
 
-#if 1
     void inc_ref() {
         SASSERT(m_ref_count < UINT_MAX);
         m_ref_count ++;
@@ -492,12 +491,6 @@ protected:
         SASSERT(m_ref_count > 0);
         m_ref_count --;
     }
-#else
-    void inc_ref();
-
-    void dec_ref();
-
-#endif
 
     ast(ast_kind k):m_id(UINT_MAX), m_kind(k), m_mark1(false), m_mark2(false), m_mark_shared_occs(false), m_ref_count(0) {
         DEBUG_CODE({
diff --git a/src/ast/expr_substitution.cpp b/src/ast/expr_substitution.cpp
index 61bd9370c..d53b14840 100644
--- a/src/ast/expr_substitution.cpp
+++ b/src/ast/expr_substitution.cpp
@@ -121,9 +121,9 @@ void expr_substitution::erase(expr * c) {
     }
     expr * def = nullptr;
     if (m_subst.find(c, def)) {
-        m_manager.dec_ref(c);
         m_manager.dec_ref(def);
         m_subst.erase(c);
+        m_manager.dec_ref(c);
     }
 }
 
diff --git a/src/ast/justified_expr.h b/src/ast/justified_expr.h
index 8aa961686..d9a6fc629 100644
--- a/src/ast/justified_expr.h
+++ b/src/ast/justified_expr.h
@@ -43,6 +43,8 @@ public:
     ~justified_expr() {
         m.dec_ref(m_fml);
         m.dec_ref(m_proof);
+		m_fml = nullptr;
+		m_proof = nullptr;
     }
     
     expr* get_fml() const { return m_fml; }
diff --git a/src/sat/tactic/goal2sat.cpp b/src/sat/tactic/goal2sat.cpp
index 76578ebf5..c38e7020c 100644
--- a/src/sat/tactic/goal2sat.cpp
+++ b/src/sat/tactic/goal2sat.cpp
@@ -107,9 +107,9 @@ struct goal2sat::imp {
         m_solver.add_clause(l1, l2, m_is_lemma);
     }
 
-    void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3) {
+    void mk_clause(sat::literal l1, sat::literal l2, sat::literal l3, bool is_lemma = false) {
         TRACE("goal2sat", tout << "mk_clause: " << l1 << " " << l2 << " " << l3 << "\n";);
-        m_solver.add_clause(l1, l2, l3, m_is_lemma);
+        m_solver.add_clause(l1, l2, l3, m_is_lemma || is_lemma);
     }
 
     void mk_clause(unsigned num, sat::literal * lits) {
@@ -337,8 +337,8 @@ struct goal2sat::imp {
             mk_clause(l,  ~c, ~t);
             mk_clause(l,   c, ~e);
             if (m_ite_extra) {
-                mk_clause(~t, ~e, l);
-                mk_clause(t,  e, ~l);
+                mk_clause(~t, ~e, l, true);
+                mk_clause(t,  e, ~l, true);
             }
             m_result_stack.shrink(sz-3);
             if (sign)
diff --git a/src/smt/asserted_formulas.cpp b/src/smt/asserted_formulas.cpp
index b1e89f72e..2a162c1f6 100644
--- a/src/smt/asserted_formulas.cpp
+++ b/src/smt/asserted_formulas.cpp
@@ -216,6 +216,11 @@ void asserted_formulas::reset() {
     m_inconsistent = false;
 }
 
+void asserted_formulas::finalize() {
+    reset();
+    m_substitution.cleanup();
+}
+
 bool asserted_formulas::check_well_sorted() const {
     for (justified_expr const& je : m_formulas) {
         if (!is_well_sorted(m, je.get_fml())) return false;
diff --git a/src/smt/asserted_formulas.h b/src/smt/asserted_formulas.h
index e2411e03a..32e1fabc7 100644
--- a/src/smt/asserted_formulas.h
+++ b/src/smt/asserted_formulas.h
@@ -223,6 +223,7 @@ class asserted_formulas {
 public:
     asserted_formulas(ast_manager & m, smt_params & smtp, params_ref const& p);
     ~asserted_formulas();
+    void finalize();
 
     void updt_params(params_ref const& p);
     bool has_quantifiers() const { return m_has_quantifiers; }
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index a80c6b5aa..d240ebb1e 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -232,6 +232,7 @@ namespace smt {
 
     context::~context() {
         flush();
+        m_asserted_formulas.finalize();
     }
 
     void context::copy_plugins(context& src, context& dst) {