-
Notifications
You must be signed in to change notification settings - Fork 84
Closed
Labels
benchmarkingbugsv-benchmarks-MRThis tracks an MR in the`sv-benchmarks` repo that will solve issueThis tracks an MR in the`sv-benchmarks` repo that will solve issuesv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnessesunsound
Milestone
Description
-
nla-digbench-scaling/geo1-ll2_unwindbound1withno-overflowproperty: something to do with unrolling, because disablingloopUnrollHeuristicmakes 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/IntPathwithterminationproperty: the verdict is technically right, but we have "Both branches dead" (ERRORverdict for both branches dead in SV-COMP #1576). This also has something to do with unrolling, because disablingloopUnrollHeuristicmakes us sound again. Issue from Apron normalization: Try to fix sv-benchmarks termination-restricted-15/IntPath Apron normalization #1585.
Metadata
Metadata
Assignees
Labels
benchmarkingbugsv-benchmarks-MRThis tracks an MR in the`sv-benchmarks` repo that will solve issueThis tracks an MR in the`sv-benchmarks` repo that will solve issuesv-compSV-COMP (analyses, results), witnessesSV-COMP (analyses, results), witnessesunsound