From 348bb3b6a46275c8b38c3c2250c6541e10028339 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 3 Jul 2026 15:00:10 -0700
Subject: [PATCH] Fix memory leaks in polymorphism instantiation engine

The polymorphism theory routed polymorphic (\) problems through
theory_polymorphism, which instantiated axioms during search. Two leaks:

1. In inst::instantiate, insert_ref_map was constructed with an expr_ref
   argument, so its template parameter D deduced to expr_ref instead of
   expr*. Trail objects are region-allocated and freed without running
   destructors, so the embedded expr_ref never released its reference,
   leaking one AST subtree per instantiation. Pass e_inst.get() so D is
   expr*, matching the raw hashtable + manual inc_ref/dec_ref pattern.

2. trail_stack's destructor does not call reset(), so level-0 trail items
   (including the inc_ref balancing entries for m_from_instantiation) were
   never undone when the theory was destroyed. Added a ~theory_polymorphism
   destructor that calls m_trail.reset().

Also keeps a defensive alias check in util::unify and a fresh per-iteration
substitution in inst::instantiate.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/ast/polymorphism_inst.cpp | 5 +++--
 src/ast/polymorphism_util.cpp | 2 ++
 src/smt/theory_polymorphism.h | 8 ++++++++
 3 files changed, 13 insertions(+), 2 deletions(-)

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 { }
     };