Simmo Saan

This really needs to be fixed. I had to independently realize the same thing that the current behavior makes smart_importer completely useless: https://github.com/beancount/smart_importer/issues/149.

PCRE completely fails the tests because the regex flag handling works a bit differently. Also, PCRE has a different idea of [newline handling](http://www.pcre.org/original/doc/html/pcreposix.html#SEC4). Not only the behavioral change but PCRE...

I know I could but that basically means ditching most of the existing regex tests with PCRE as `string_regex_flags` is only needed to force some flags for pcreposix, while letting...

Is TCL's regex engine available as a separate C library? Does it act as a drop-in replacement for POSIX? These are two fundamental features that PCRE has which makes the...

This is with just mutex-meet, not the experimental mutex-meet-atomic, so there should be no special handling of SV-COMP atomics. The same behavior should be observable when replacing them with a...

Thanks for the minimized test case, it indeed highlights the problem. Turns out it's the same issue as https://github.com/goblint/analyzer/pull/1407#issuecomment-2037220588, but now with soundness consequences. I'll see if a quick fix...

The remaining task here was also mentioned in #1498, which should be fixed by #1492. Its initialization issue should be fixed in sv-benchmarks (https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1551), but that is unrelated to our...

There's now progress in sv-benchmarks to replace some `__VERIFIER_atomic`s with C11/GCC atomics: * https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1548, * https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1549, * https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1554, * https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1556, * https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/merge_requests/1557. I haven't checked how much it affects our...

I cherry-picked and generalized the configurability of the assert transformation to `master`. Also a few of the test parameter and annotation improvements, but not the new annotations.

I guess we could also reject GraphML violation witnesses based on verdict, but it's probably kind of pointless. GraphML witnesses might become unused in SV-COMP sometime anyway.