Repository navigation

Cut per-round overhead of the executor and explorer - #82

Closed

nils-loose wants to merge 7 commits into

svcomp27/integrationfrom

perf/round-overhead

Closed

Cut per-round overhead of the executor and explorer#82
nils-loose wants to merge 7 commits into
svcomp27/integrationfrom
perf/round-overhead

Commits on Oct 18, 2026
- Extract constraint variables without recursion, each subterm once
  
  nils-loose
  and
  claude
  committed
  5d7de94
- Do not close the solver context at the end of an SV-COMP execution
  
  nils-loose
  and
  claude
  committed
  ab37625
- Encode the trace with one Z3 solver for all formulas, compact JSON
  
  nils-loose
  and
  claude
  committed
  f67f39d
- Create the solver contexts with java-smt's null log manager
  
  nils-loose
  and
  claude
  committed
  d1ac405
- Run the executor JVM with C1 only
  
  nils-loose
  and
  claude
  committed
  2dcd94c
- Select the next branch without copying the execution tree
  
  nils-loose
  and
  claude
  committed
  e4305de
Commits on Oct 19, 2026
- Test variable extraction on shared and deep constraint terms
  
  nils-loose
  and
  claude
  committed
  d757d7f