Michael Tautschnig

I believe #765 finally fixes this problem for all remaining folders.

I'd say the key difference is whether you want the benchmark to be meaningful for termination analysis?!

@danieldietsch Would you mind elaborating? To what extent is `abort()` a problem, and how is `__VERIFIER_assume()` fine with regard to termination? @PhilippWendler I'm not sure I agree with the removal...

In my opinion, the sole difference lies in termination. Quoting the rules: > **__VERIFIER_assume(expression):** A verification tool can assume that a function call __VERIFIER_assume(expression) has the following meaning: If 'expression'...

@PhilippWendler If the answer to both your questions is "no", what is then the semantics? If `__VERIFIER_assume(false)` would cause termination, then the answer to the second question can't be "no",...

Let me try to work out an example: ````c 1: int main() { 2: __VERIFIER_assume(0); 3: return 0; 4: } ```` Let me try to define a program execution as...

@danielsn ?

Still WIP, but https://github.com/diffblue/cbmc/pull/7230 might help here: the example at the top of this issue takes 18 seconds instead of 428 on my machine.

Yes, that’s CBMC’s doing: one peculiarity of ARM64 is that the char type is unsigned. That makes CBMC print ASCII characters here.

Should we resolve this now that #2370 has been merged?