goto-symex: keep composite quantifier bound variables as symbols

[tautschnig]

Field sensitivity decomposes struct- and array-typed symbols into struct/array expressions built from per-field SSA symbols. When this is applied to the bound variable of a forall/exists quantifier, the bound variable is turned into a non-symbol expression, violating the invariant that quantifier bound variables must be symbols (validate_expr in mathematical_expr.h: "quantified variable shall be a symbol"). As a result, any quantifier with a struct- or array-typed bound variable triggered an invariant violation, in both the assertion (forall) and the assumption (exists) code paths.

Restrict field sensitivity to the body of a quantifier:

• field_sensitivityt::apply now descends only into the body (operand 1) of a quantifier, leaving the bound variables (operand 0) untouched. This covers the assertion path, where the quantifier is field-sensitised by clean_expr before rewrite_quantifiers removes it.

• goto_symex_statet::rename renames the bound-variable symbols individually via the symbol path (which assigns L2 indices but does not apply field sensitivity) and renames the body normally. This covers the assumption path, where renaming happens before rewrite_quantifiers and was decomposing the binding via field sensitivity.

The body is still renamed with field sensitivity so that references to program variables remain connected to their SSA values.

• Each commit message has a non-empty body, explaining why the change was made.
• 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).
• n/a 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

Note

Copilot couldn't run its full agentic review because no GitHub Actions runner was available. Make sure your repository has a runner available to run Copilot's review, or add a copilot-setup-steps.yml file specifying one with the runs-on attribute. See the docs for more details.

Fixes invariant violations caused by field sensitivity decomposing composite-typed quantifier bound variables into non-symbol expressions during symex/renaming.

Changes:

• Restricts field sensitivity to only the quantifier body (operand 1), leaving bound variables (operand 0) untouched.
• Updates goto_symex_statet::rename to rename quantifier bound variables via the symbol path while still renaming the body normally.
• Adds regression tests covering struct-typed and array-typed quantifier bound variables for both forall/assertion and exists/assumption paths.

Reviewed changes

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

File	Description
src/goto-symex/goto_symex_state.cpp	Special-cases quantifier renaming to keep bound variables as symbols while still field-sensitising the body.
src/goto-symex/field_sensitivity.cpp	Prevents field sensitivity from descending into quantifier bindings; only processes the body.
regression/cbmc/Quantifiers-struct-bound-var/*	Adds regression cases for struct-typed quantified bound variables (forall, exists, and a refutation case).
regression/cbmc/Quantifiers-array-bound-var/*	Adds regression case for array-typed quantified bound variables.

---

💡 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.68%. Comparing base (7483d0d) to head (71d1823).

Additional details and impacted files

@@             Coverage Diff             @@
##           develop    #9077      +/-   ##
===========================================
- Coverage    80.68%   80.68%   -0.01%     
===========================================
  Files         1714     1714              
  Lines       189593   189604      +11     
  Branches        73       73              
===========================================
+ Hits        152979   152987       +8     
- Misses       36614    36617       +3     

☔ 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.