From 334f4fa32b48c354eba7f2ee77baa64d7e798a1e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 7 Jul 2026 11:30:33 -0700 Subject: [PATCH] reduce leaks for sorts --- src/ast/polymorphism_inst.cpp | 4 +++- src/cmd_context/tptp_frontend.cpp | 6 +++++- 2 files changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ast/polymorphism_inst.cpp b/src/ast/polymorphism_inst.cpp index c34f03585c..5070f66d67 100644 --- a/src/ast/polymorphism_inst.cpp +++ b/src/ast/polymorphism_inst.cpp @@ -57,9 +57,11 @@ namespace polymorphism { m_assertions.push_back(e); t.push(push_back_vector(m_assertions)); u.collect_type_vars(e, inst.m_tvs); + auto* init = alloc(substitution, m); inst.m_subst = alloc(substitutions); - inst.m_subst->insert(alloc(substitution, m)); + inst.m_subst->insert(init); m_instances.insert(e, inst); + t.push(new_obj_trail(init)); t.push(new_obj_trail(inst.m_subst)); t.push(insert_map(m_instances, e)); } diff --git a/src/cmd_context/tptp_frontend.cpp b/src/cmd_context/tptp_frontend.cpp index 8ab6b31672..ff656b7ef4 100644 --- a/src/cmd_context/tptp_frontend.cpp +++ b/src/cmd_context/tptp_frontend.cpp @@ -553,8 +553,10 @@ class tptp_parser { // Multi-argument A * B > C is represented as Array(A, Array(B, C)) (curried). sort* get_ho_sort(ptr_vector const& domain, sort* range) { sort* s = range; - for (int i = (int)domain.size() - 1; i >= 0; --i) + for (int i = (int)domain.size() - 1; i >= 0; --i) { s = m_array.mk_array_sort(domain[i], s); + m_pinned_sorts.push_back(s); + } return s; } @@ -1369,6 +1371,7 @@ class tptp_parser { sort* arg_sort = arg->get_sort(); sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ; sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort); + m_pinned_sorts.push_back(arr_sort); e = coerce_arg(e, arr_sort); } else { // Array but domain may not match arg sort — coerce arg @@ -2217,6 +2220,7 @@ class tptp_parser { // If arg is Bool-sorted, result is likely Bool too (modal/connective application) sort* result_sort = m.is_bool(arg_sort) ? m.mk_bool_sort() : m_univ; sort* arr_sort = m_array.mk_array_sort(arg_sort, result_sort); + m_pinned_sorts.push_back(arr_sort); e = coerce_arg(e, arr_sort); } else { // Array but domain may not match arg sort — coerce arg