Zsófia Ádám

State Machine Triggers / Actions missing

7

### Is your feature request related to a problem? The state machine diagram feels really nice to use with composite states, guards, etc., but the lack of actions and triggers...

- missing create threads - ??

This commit adds a fix for a few typos in the portfolio (which caused the output to be wrong in certain cases) and a two additional portfolio configuration YAMLs.

Support SV-COMP ReachSafety-Combined with BMC

1

I'll need to take a look at exactly what the problem is here. It could be a performance issue, but it probably can be handled so that this issue is...

Limitation due to semantics of undef causes SVComp incorrect false results

5

I came across more than one SVComp task, that gives back incorrect false values, because the call of the error function depends on the value of a global variable, which...

Task with floats: bmc incorrect false, with somehow correct test harness

5

**Describe the bug** gazer-bmc produces an incorrect false result when run on the following SV-Comp task (besides other, similar tasks) : [float-no-simp8.i](https://github.com/sosy-lab/sv-benchmarks/blob/master/c/floats-cbmc-regression/float-no-simp8.i) [float-no-simp8.c](https://github.com/sosy-lab/sv-benchmarks/blob/master/c/floats-cbmc-regression/float-no-simp8.c) [float-no-simp8.yml ](https://github.com/sosy-lab/sv-benchmarks/blob/master/c/floats-cbmc-regression/float-no-simp8.yml) As stated in the YAML...

Solver executables - permission and packaging issues

1

## Issues with owner only permissions: In SolverInstallers (e.g., `BitwuzlaSmtLibSolverInstaller`) in the `installSolver` method `setExecutable` is called with `ownerOnly = true`. This is usually enough, but e.g., on docker it...

`--witness-only` is deprecated, so we need to change it to: ``` --enable-output --disable-arg-generation --disable-chc-serialization --disable-xcfa-serialization --disable-c-serialization --only-svcomp-witness ```

Flags to reproduce: ``` --input simple.c --backend portfolio --portfolio COMPLEX --loglevel RESULT --enable-output --disable-arg-generation --disable-xcfa-serialization --disable-c-serialization --property ../../../sw-verifiers/unreach-call.prp --architecture LP64 ``` [simple.c.txt](https://github.com/user-attachments/files/16801940/simple.c.txt) [witness.graphml.txt](https://github.com/user-attachments/files/16801945/witness.graphml.txt) I am not sure if this went...

Output files and flags of xsts-cli

1

The number of output file types and files is growing and the current `--cex-file` flag will not scale to that. I had similar problems when working on trace generation (and...