mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-05 06:46:11 +00:00
Code Activity

polymorphism: prevent cyclic substitutions in unify to fix stack overflow

Browse source 
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>
This commit is contained in:
Nikolaj Bjorner 2026-07-03 11:22:33 -07:00
parent 5bd485eb03
commit 6d5e09e2fa
1 changed files with 13 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

16
src/ast/polymorphism_util.cpp
View file

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