util: make irept destruction depth-safe without recursion

[tautschnig]

Deeply nested ireps (e.g. a deep SMT-LIB let chain) overflow the call stack when the recursive destructor unwinds them. Bound the destruction recursion: remove_ref still deletes recursively -- which is as cheap as the natural recursive destructor for the shallow trees that dominate -- but tracks the recursion depth in a thread-local counter and, once it reaches a fixed bound, collapses the remainder of the subtree with an explicit work stack instead. Only the deep tail pays the cost of detaching children and allocating a work stack; shallow destruction (the overwhelmingly common case) is unaffected, so this avoids the regression on destruction-heavy workloads (symbolic execution and simplification churn) that an always-iterative destructor incurs.

Add a unit test that builds and destroys a chain of ireps far deeper than any plausible call stack; it passes with the bounded destructor and segfaults with a purely recursive one.

Chose a bounded-recursive (hybrid) destructor over an always-iterative one to avoid a regression on destruction-heavy work. SAT-free, destruction-heavy benchmark (cbmc --program-only over a tight struct-update loop — symex/simplification churn), median user CPU: recursive baseline 1.71 s, always-iterative 1.84 s (+~8%), this hybrid 1.73 s (+~1%).

• Each commit message has a non-empty body, explaining why the change was made.
• n/a Methods or procedures I have added are documented, following the guidelines provided in CODING_STANDARD.md.
• n/a The feature or user visible behaviour I have added or modified has been documented in the User Guide in doc/cprover-manual/
• Regression or unit tests are included, or existing tests cover the modified code (in this case I have detailed which ones those are in the commit message).
• My commit message includes data points confirming performance improvements (if claimed).
• My PR is restricted to a single feature or bugfix.
• n/a White-space or formatting changes outside the feature-related changed lines are in commits of their own.

[Copilot]

Pull request overview

This PR makes irept destruction depth-safe by bounding recursive deletion in sharing_treet::remove_ref and switching to an explicit work stack when a recursion-depth threshold is reached, preventing stack overflows on deeply nested ireps (e.g., deep SMT-LIB let chains). It also adds a unit test that constructs and destroys an extremely deep irep chain to exercise the new destruction behavior.

Changes:

• Add a thread-local recursion-depth counter in sharing_treet::remove_ref and fall back to iterative subtree deletion beyond a fixed depth bound.
• Remove the unused nonrecursive_destructor helper and embed the iterative deletion logic directly in remove_ref.
• Add a unit test that builds a deeply nested irep chain and verifies destruction completes without a stack overflow.

Reviewed changes

Copilot reviewed 2 out of 2 changed files in this pull request and generated 3 comments.

File	Description
src/util/irep.h	Bounds recursive destruction and introduces an iterative deep-subtree deletion path inside remove_ref.
unit/util/irep.cpp	Adds a unit test that constructs a very deep irep chain and validates destruction doesn’t overflow the stack.

---

💡 Add Copilot custom instructions for smarter, more guided reviews. Learn how to get started.

[codecov]

Codecov Report

✅ All modified and coverable lines are covered by tests.
✅ Project coverage is 80.69%. Comparing base (321ba11) to head (89801c5).

Additional details and impacted files

@@           Coverage Diff            @@
##           develop    #9043   +/-   ##
========================================
  Coverage    80.68%   80.69%           
========================================
  Files         1714     1714           
  Lines       189501   189556   +55     
  Branches        73       73           
========================================
+ Hits        152902   152959   +57     
+ Misses       36599    36597    -2     

☔ View full report in Codecov by Harness.
📢 Have feedback on the report? Share it here.

🚀 New features to boost your workflow:

• ❄️ Test Analytics: Detect flaky tests, report on failures, and find test suite problems.
• 📦 JS Bundle Analysis: Save yourself from yourself by tracking and limiting bundle sizes in JS merges.