Chenfeng Wei

https://github.com/esbmc/esbmc-ai/issues/149

Test comp (will not merge)

1

We need to avoid generate test-case for array-type, struct-type... in test-comp. Considering this C program from Test-Comp Cover-Branch. ```C int main() { int i; int j=__VERIFIER_nondet_int(); int n=__VERIFIER_nondet_int(); assume_abort_if_not(n <...

[multi-property] Incorrect counterexample when using unwind

3

```c #include int main() { int valve = nondet_int(); // environment int input = nondet_int(); // user input while (input) { if (!valve) { assert(valve == 0); // "privacy" valve...

Draft