Implement solver-based branch pruning

[tautschnig]

Query the SAT solver at each branch point to eliminate infeasible branches. Works in both --paths mode (push/pop scoping) and monolithic mode (incremental conversion with converted_for_pruning flag). Uses a non-simplifying MiniSat solver to avoid backwardSubsumptionCheck overhead; falls back to solver_factoryt when MiniSat is not available (e.g., CaDiCaL builds).

Adaptive pruning: cumulative 2-second time budget auto-disables pruning when overhead exceeds benefit.

Assumes are explicitly asserted as guard => cond. Includes fix for symex::args name collisions across paths via a static type registry.

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

Note

Copilot was unable to run its full agentic suite in this review.

Adds solver-assisted feasibility checks at branch points to prune unreachable branches during symbolic execution, reducing path explosion.

Changes:

• Introduces a shared, push/pop-capable SAT solver for branch pruning (with MiniSat-no-simplifier fast path and solver-factory fallback).
• Implements pruning in both --paths and monolithic modes, with an adaptive time-budget auto-disable.
• Adds CLI toggle --no-branch-pruning, regression tests, and an architecture note.

Reviewed changes

Copilot reviewed 34 out of 34 changed files in this pull request and generated 4 comments.

Show a summary per file

File	Description
src/goto-symex/symex_target_equation.cpp	Avoids argument symbol name/type collisions across shared solver conversions
src/goto-symex/symex_goto.cpp	Adds solver queries to prune infeasible branches in paths + monolithic execution
src/goto-symex/ssa_step.h	Adds converted_for_pruning flag for incremental pruning conversions
src/goto-symex/goto_symex.h	Stores pruning solver pointer and pruning budget state; exposes setter
src/goto-checker/single_path_symex_only_checker.h	Adds persistent pruning solver member and setup_symex hook
src/goto-checker/single_path_symex_only_checker.cpp	Builds/configures pruning solver and wires it into symex
src/goto-checker/multi_path_symex_only_checker.h	Adds persistent pruning solver member
src/goto-checker/multi_path_symex_only_checker.cpp	Builds/configures pruning solver and wires it into symex
src/cbmc/cbmc_parse_options.h	Adds no-branch-pruning command-line option
src/cbmc/cbmc_parse_options.cpp	Parses --no-branch-pruning and documents it in --help
regression/cbmc/unwind_counters4/test.desc	Updates expected output regex
regression/cbmc/paths-branch-pruning/*.c/.desc	Adds new regression tests covering pruning behavior and refine-soundness
doc/architectural/branch-pruning.md	Documents pruning architecture and limitations

Comments suppressed due to low confidence (4)

src/goto-symex/symex_goto.cpp:1

• In monolithic pruning, assignments/constraints are asserted unconditionally via set_to_true(step.cond_expr). SSA steps are typically guarded, and the normal conversion asserts them as guard => cond_expr; dropping the guard can over-constrain the pruning solver and incorrectly mark branches infeasible. Fix by asserting guarded steps as implies_exprt{step.guard, step.cond_expr} (or the equivalent used by the normal equation conversion) for assignments and constraints as well.
  src/goto-symex/symex_goto.cpp:1
• SSA_stept::converted is documented/used for incremental conversion. Resetting it here for pruning risks interfering with later conversions into other solvers (and can force repeated reconversion), which can change performance and potentially duplicate constraints depending on how conversion is orchestrated downstream. Prefer tracking pruning conversion exclusively with converted_for_pruning (already added) and avoid mutating converted in the pruning path.
  src/goto-symex/symex_target_equation.cpp:1
• This function-local static registry is shared across all runs/instances and is not thread-safe. It also grows monotonically with every unique symex::args::<n> ever produced, which can create unbounded memory growth in long-running or multi-check workflows. A more robust approach is to make the registry solver- or symex-instance scoped (or incorporate a type-derived discriminator into the identifier) so state doesn’t leak globally and can be managed/reset deterministically.
  src/goto-symex/symex_goto.cpp:1
• The pruning query is checking satisfiability under the converted equation, but it doesn’t appear to assert the current path condition explicitly (e.g., state.guard). That can significantly reduce pruning power (SAT models can satisfy implications by setting earlier guards false). Consider adding the current path guard as an assumption (or conjoining it with new_guard / !new_guard) when calling push(...) so the solver checks feasibility under the active path condition.

---

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