Simmo Saan
Simmo Saan
Discovered in https://github.com/goblint/analyzer/pull/1838#discussion_r2571447038. Should be redundant due to #1764. Especially because this only trigger for must division by zero, not may. It's strange because it's the only warning/error emitted during...
Based on my observation in PR #1885, we lost a few tasks with PR #1777 not being configured for SV-COMP 2026. For SV-COMP 2027 one of the following should happen:...
While benchmarking #1752 I noticed that there's no real difference between cputime and walltime, even when I switched Goblint from 1 core to 4 cores. After some profiling I realized...
> Another thing that I noticed a while ago, but what's relevant to the case from the issue description (where the deadlock is during warning output): > We never turn...
> > But the other worrying point is that we're apparently printing something during solving itself. That's unusual, because usually it's just one solver stats printout after another. Perhaps there's...
While working on witness IDE integration, @karoliineh has looked at some of our witness invariants, which has revealed some questionable ones: - [x] Seemingly pointless reflexive equality: ``` - invariant:...
While checking https://github.com/goblint/analyzer/pull/1821#issuecomment-3342492386, I found out the following surprising thing: the autotuner only enables relational analysis for _at most 2_ globals: https://github.com/goblint/analyzer/blob/529013137ad4de9d020b47dcfc7a553d1e677766/src/autoTune.ml#L435-L447 We should really look into this because we...
The knightly runs always have some Intel TDX tasks from sv-benchmarks where the result spuriously flips between `unknown` and `OUT OF MEMORY` (in either direction). I find this suspicious. It's...
YAML witness 2.1 has `loop_transition_invariant`s for describing proofs of termination. I think it will be a demo in SV-COMP 2026 but I was still wondering if we could generate something...
While abstractly debugging some of our own sv-benchmarks coreutils instrumented programs, I realized that we're very bad at indexing constant string literals. This PR includes my quick hacky attempts at...