Repository navigation

Loop-head state matching for concrete loop states - #84

Closed

nils-loose wants to merge 7 commits into

svcomp27/integrationfrom

feat/loop-state-matching

Closed

Loop-head state matching for concrete loop states#84
nils-loose wants to merge 7 commits into
svcomp27/integrationfrom
feat/loop-state-matching

Commits on Oct 18, 2026
- Report loop-head states with the trace
  
  nils-loose
  and
  claude
  committed
  98e402a
- Leave out branches below a repeated loop-head state
  
  nils-loose
  and
  claude
  committed
  1a4e046
- Enable loop-state matching in the SV-COMP configuration
  
  nils-loose
  and
  claude
  committed
  b138c9d
- Bound the time a run spends on loop-head states
  
  nils-loose
  and
  claude
  committed
  44a5a24
Commits on Oct 19, 2026
- Count a symbolic array length as symbolic
  
  nils-loose
  and
  claude
  committed
  22e3844
- Stop reporting loop states after a call into untracked code
  
  nils-loose
  and
  claude
  committed
  ca0f2a5
- Add loop-state matching soundness tasks
  
  nils-loose
  and
  claude
  committed
  730db3a