diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp
index be91c8f5e3..c34f03585c 100644
--- a/src/ast/polymorphism_inst.cpp
+++ b/src/ast/polymorphism_inst.cpp
@@ -107,13 +107,14 @@ namespace polymorphism {
         auto const& [tv, fns, substs] = m_instances[e];
                 
         for (auto* f2 : fns) {
-            substitution sub1(m), new_sub(m);
+            substitution sub1(m);
             if (!u.unify(f1, f2, sub1))
                 continue;
             if (substs->contains(&sub1))
                 continue;
             substitutions new_substs;
             for (auto* sub2 : *substs) {
+                substitution new_sub(m);
                 if (!u.unify(sub1, *sub2, new_sub))
                     continue;
                 if (substs->contains(&new_sub))
@@ -128,7 +129,7 @@ namespace polymorphism {
                     new_substs.insert(new_sub1);
                     m_from_instantiation.insert(e_inst);
                     m.inc_ref(e_inst);
-                    t.push(insert_ref_map(m, m_from_instantiation, e_inst));
+                    t.push(insert_ref_map(m, m_from_instantiation, e_inst.get()));
                 }
             }
             for (auto* sub2 : new_substs) {
diff --git a/src/ast/polymorphism_util.cpp b/src/ast/polymorphism_util.cpp
index 35054346d1..a0c2bad502 100644
--- a/src/ast/polymorphism_util.cpp
+++ b/src/ast/polymorphism_util.cpp
@@ -244,6 +244,8 @@ namespace polymorphism {
     bool util::unify(substitution const& s1, substitution const& s2,
                      substitution& sub) {
         sort* v2;
+        SASSERT(&s1 != &sub);
+        SASSERT(&s2 != &sub);
         for (auto const& [k, v] : s1) {
             // Guard against building a cyclic substitution (e.g. A |-> list(A)),
             // which would make substitution application diverge. Such a binding
diff --git a/src/smt/theory_polymorphism.h b/src/smt/theory_polymorphism.h
index a10f9aa84e..613c1a8dd5 100644
--- a/src/smt/theory_polymorphism.h
+++ b/src/smt/theory_polymorphism.h
@@ -96,6 +96,14 @@ namespace smt {
             theory(ctx, poly_family_id),
             m_inst(ctx.get_manager(), m_trail),
             m_assumption(ctx.get_manager()) {}
+
+        ~theory_polymorphism() override {
+            // Undo level-0 trail items (e.g. the inc_ref balancing entries that
+            // m_inst pushes for m_from_instantiation). trail_stack's destructor
+            // does not call reset(), so without this the references those items
+            // hold would leak when the theory is destroyed.
+            m_trail.reset();
+        }
         
         void init_model(model_generator & mg) override { }
     };