Simmo Saan
Simmo Saan
I'm trying to use multiple refcontexts with the same sorting, but different subsets of entries in various places (by refsegment). It seems that biblatex considers all refcontexts with same sorting...
There are countless StackExchange posts about hyperref links going to wrong bibliography: * https://tex.stackexchange.com/q/513409/383946 * https://tex.stackexchange.com/q/142632/35864 * https://tex.stackexchange.com/q/303503/35864 * https://tex.stackexchange.com/q/140048/35864 * https://tex.stackexchange.com/q/448694/35864 It would make sense to allow this choice...
I just happened to look into a witness we now produce with the portfolio at a level which enables the bitfield domain and saw lots of trivial invariants like `(i...
This is currently on top of #1895. It combines that with #1894. ### TODO - [ ] Add non-`Unknown` cast kinds.
In SV-COMP 2026 (first) final result, we have a `witness invalid (true)` verdict for five tasks: * goblint-coreutils/instrumented_cksum_comb * goblint-coreutils/instrumented_cut_comb * goblint-coreutils/instrumented_interval_cksum_comb * goblint-coreutils/instrumented_interval_nohup_comb * goblint-coreutils/instrumented_nohup_comb The error from witnesslint...
This does nothing on the surface itself, but will be useful for #1895. This will also be useful for https://github.com/goblint/analyzer/pull/1838#discussion_r2571468662 to possibly avoid emitting (or even performing) some unnecessary internal...
Closes #1795. This probably isn't all of it, but hopefully is most that I quickly found with some simple searches.
~~This is on top of #1886 because I got the idea there.~~ `GobList.cartesian_map` unifies two kinds of patterns I found in various places: 1. `List.map` on `BatList.cartesian_product`. 2. `List.map` inside...
According to C11, incrementing an _atomic_ signed integer to overflow is not undefined behavior, but defined to wrap around. Therefore, it doesn't violate SV-COMP's no-overflow property.
This is on top of #1880. Instead of writing ```ocaml f @@ fun x -> e ``` (which is a bit odd indentaiton-wise), this provides a neat way to write...