Simmo Saan
Simmo Saan
This branch contains development and integration for SV-COMP 2025. This branch is used for creating verifier archives for preruns. ### PRs It includes some not-yet merged PRs: 1. #1593 2....
It looks like TD3 populates the `dep` table along with `infl`. If I recall correctly, `dep` is just used for some incremental things, so it's useless during non-incremental runs and...
- [x] `nla-digbench-scaling/geo1-ll2_unwindbound1` with `no-overflow` property: something to do with unrolling, because disabling `loopUnrollHeuristic` 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. - [x] `termination-restricted-15/IntPath` with `termination` property: the...
Closes #1299. The widening tokens are no longer just the YAML witness entry UUID, but also contain an optional index for `invariant_set`s.
When widening thresholds are collected from the program, we do use a `Set` to avoid duplicates, but then it's just converted to a list with `elements`: https://github.com/goblint/analyzer/blob/bb6f9aa1a2a4f38d022112e1ab840a4bdb382286/src/cdomain/value/util/wideningThresholds.ml#L103-L108 Later, `IntDomain` uses...
This is a bit silly but the threadflag analysis `may_race` did not exclude `main`-`main` races even though it has all the information to do so. It almost never makes a...
I inspected the first `ERROR (both branches dead)` result after #1579 on sv-benchmarks and it lead to unsound congruence domain arithmetic which presents itself as both branches dead in a...
Regarding the [question whether casts are overflows in SV-COMP](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/issues/1413), I ran Goblint both ways and inspected the verdict differences. There are a bunch of tasks where it seems that we...
As identified in https://github.com/goblint/analyzer/issues/1576#issuecomment-2378939924, this SV-COMP task causes a weird both branches dead situation which actually is sound. With both octagon and polyhedra, there are constraints like `2x=1` where `x`...
In the same vein as #1577, when our deadlock analysis proves the program deadlock-free, there's no explanation or proof of the fact. Whereas in the case of possible deadlocks we...