--stop-on-fail generates a trace even though --trace is omitted

[lou1306]

If I run cbmc --unwind 2 --unwinding-assertions count_by_1.i I only get a summary of the results, as expected:

** Results:
count_by_1.i function main
[main.unwind.0] line 26 unwinding assertion loop 0: FAILURE

count_by_1.i function reach_error
[reach_error.assertion.1] line 12 assertion 0: SUCCESS

** 1 of 2 failed (2 iterations)
VERIFICATION FAILED

However, if I add --stop-on-fail, CBMC will also generate a counterexample trace, even though I did not specify --trace. Is this expected behaviour? I would expect to see a summary similar to the one above, containing only the failed assertion.

Please find attached a copy of count_by_1.i. This program is part of the sv-benchmarks library and can also be found at this URL: https://github.com/sosy-lab/sv-benchmarks/blob/master/c/loop-new/count_by_1.i

---

Details about my setup:

CBMC version: 5.20.1
Operating system: Ubuntu 20.04
Exact command line resulting in the issue: cbmc --stop-on-fail --unwind 2 --unwinding-assertions count_by_1.i
What behaviour did you expect: CBMC reports an assertion failure and exits
What happened instead: CBMC also prints a counterexample, even though I didn't specify --trace

Program: count_by_1.i.txt

[kroening]

Debatable -- I'd say that most users will want to have the trace when using --stop-on-fail.

[lou1306]

Debatable -- I'd say that most users will want to have the trace when using --stop-on-fail.

I'm not denying that this is the common way one uses --stop-on-fail. Still, it's a bit surprising (to me, at least), since the CBMC documentation states that you can only get a trace by adding --trace to the command line.

Maybe having cbmc -h say something like "--stop-on-fail implies --trace" would make this behaviour clearer?