sv-benchmarks unsoundness pre-SV-COMP 2025 #1578
Labels
benchmarking
bug
in progress
sv-benchmarks-MR
This tracks an MR in the`sv-benchmarks` repo that will solve issue
sv-comp
SV-COMP (analyses, results), witnesses
unsound
Milestone
nla-digbench-scaling/geo1-ll2_unwindbound1
withno-overflow
property: something to do with unrolling, because disablingloopUnrollHeuristic
makes us sound again. Incorrect expected verdicts? https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1415, https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1558.termination-restricted-15/IntPath
withtermination
property: the verdict is technically right, but we have "Both branches dead" (ERROR
verdict for both branches dead in SV-COMP #1576). This also has something to do with unrolling, because disablingloopUnrollHeuristic
makes us sound again. Issue from Apron normalization: Try to fix sv-benchmarks termination-restricted-15/IntPath Apron normalization #1585.The text was updated successfully, but these errors were encountered: