From 6d5e09e2fa19095a940bd323f27e4ce4b0cd6f50 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 3 Jul 2026 11:22:33 -0700 Subject: [PATCH] polymorphism: prevent cyclic substitutions in unify to fix stack overflow When merging two type substitutions, util::unify(substitution, substitution, substitution) inserted bindings without an occurs-check. Merging maps such as A |-> list(B) and B |-> list(A) produced a self-referential binding B |-> list(list(B)), and applying that substitution recursed forever, causing a stack overflow during the first polymorphic instantiation round. This was exposed by encoding TPTP $tType quantification as polymorphism (8ee8a3cda): mutually-recursive polymorphic types in THF problems (e.g. COM/DAT/ITP Coq-derived files) triggered 60 stack-overflow crashes during check_sat. Add occurs-checks so a binding that would make the substitution cyclic causes the merge to fail (the instantiation is soundly skipped). Values are resolved against the current substitution before insertion, preserving the acyclic invariant. Verified: the 60 previously-crashing TPTP files now terminate cleanly; 92/92 unit tests pass. Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com> --- src/ast/polymorphism_util.cpp | 16 +++++++++++++--- 1 file changed, 13 insertions(+), 3 deletions(-) diff --git a/src/ast/polymorphism_util.cpp b/src/ast/polymorphism_util.cpp index 555c697b34..35054346d1 100644 --- a/src/ast/polymorphism_util.cpp +++ b/src/ast/polymorphism_util.cpp @@ -244,15 +244,25 @@ namespace polymorphism { bool util::unify(substitution const& s1, substitution const& s2, substitution& sub) { sort* v2; - for (auto const& [k, v] : s1) + 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 + // means the two substitutions are not simultaneously unifiable. + if (occurs(k, v)) + return false; sub.insert(k, v); + } for (auto const& [k, v] : s2) { if (sub.find(k, v2)) { if (!sub.unify(sub(v), v2)) return false; } - else - sub.insert(k, sub(v)); + else { + sort_ref vr = sub(v); + if (occurs(k, vr)) + return false; + sub.insert(k, vr); + } } return true; }