From 6b7725dcb8c71b59a2ffc87282559b89f203ee7f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 09:06:54 -0700 Subject: [PATCH] Fix use-after-free in polymorphism substitution over sorts In polymorphism::substitution::operator()(sort*), each substituted sub-sort was held only in a local sort_ref that was destroyed at the end of the loop iteration, while its raw pointer was retained in the parameter vector passed to mk_sort. When the sub-sort's refcount dropped to zero, its memory was freed and then reused by the next allocation, producing a self-referential sort. Structural sort traversals such as has_type_var (which has no cycle detection) then recursed infinitely, manifesting as a stack overflow. Pin each intermediate sub-sort in a sort_ref_vector so it stays alive until after mk_sort has taken its own references. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/polymorphism_util.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/ast/polymorphism_util.cpp b/src/ast/polymorphism_util.cpp index 62dd4e9494..555c697b34 100644 --- a/src/ast/polymorphism_util.cpp +++ b/src/ast/polymorphism_util.cpp @@ -39,11 +39,13 @@ namespace polymorphism { } unsigned n = s->get_num_parameters(); vector ps; + sort_ref_vector pin(m); // keep substituted sub-sorts alive until mk_sort below for (unsigned i = 0; i < n; ++i) { auto &p = s->get_parameter(i); if (p.is_ast() && is_sort(p.get_ast())) { - sort_ref s = (*this)(to_sort(p.get_ast())); - ps.push_back(parameter(s.get())); + sort_ref ss = (*this)(to_sort(p.get_ast())); + pin.push_back(ss); + ps.push_back(parameter(ss.get())); } else ps.push_back(p);