Zsófia Ádám

@RipplB has there been progress with this?

I looked at count_up_down-2 locally, simply with `--backend BOUNDED`. - On the `trace-generation` branch it just seemed to not be solved even after quite a while (I'll run it again...

**Solution to bounded issues:** We found the cause of the bounded false positives: there was a synthetic loop added to the error location, so bmc finds the shorter error paths...

Yes, the example has a `reach_error()` call, thus we have an error location in the xcfa. Which, in the termination case, should be regarded simply as a program exit. So...

> Some wrong results (@mondokm, @AdamZsofi): > ASG: > > * [loops/for_infinite_loop_1.yml](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/loops/for_infinite_loop_1.yml) > * [loops/for_infinite_loop_2.yml](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/loops/for_infinite_loop_2.yml) > * [loops/while_infinite_loop_1.yml](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/loops/while_infinite_loop_1.yml) > * [loops/while_infinite_loop_2.yml](https://gitlab.com/sosy-lab/benchmarking/sv-benchmarks/-/blob/main/c/loops/while_infinite_loop_2.yml) Unfortunately these still persist, also on `trace-generation`.

**ASG wrong true issue solution:** RemoveDeadEnds works too well and removes the infinite loop (pass was implemented with reachability in mind). Will remove it from pass list in case of...

Additions from this PR were merged into and will be merged to master in https://github.com/ftsrg/theta/pull/401

Thanks for the changes! Can you maybe mark this PR as a draft for now? I approved the CI checks - if those work, we'll benchmark and compare the results....

Also, you can use `gradlew spotlessApply` locally for formatting or manually run the formatting action on github on your fork. There is also an action for bumping the version, although...

@KlevisImeri will work on this. :)