3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-28 09:52:46 +00:00

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>
This commit is contained in:
Nikolaj Bjorner 2026-07-03 15:00:10 -07:00
parent 6d5e09e2fa
commit 348bb3b6a4
3 changed files with 13 additions and 2 deletions

View file

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