--stop-on-fail suppresses output of proof objectives status when analysis is successfull.

[remi-delmas-3000]

The terminal output does not print individual PO statuses when --stop-on-fail is used, making it hard to see what was actually analysed.

CBMC version: 5.62
Operating system: Linux, macOS
Exact command line resulting in the issue: cbmc --stop-on-fail main.c
What behaviour did you expect: status of POs printed in terminal
What happened instead: no status printed

int main()
{
  int x;
  assert((x==0) ==> (2*x == 0));
}

❯ cbmc --stop-on-fail main.c
CBMC version 5.62.0 (cbmc-5.62.0-52-ga1d9f75c2d-dirty) 64-bit x86_64 macos
Parsing main.c
Converting
Type-checking main
file main.c line 4 function main: function 'assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000902692s
size of program expression: 37 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.3229e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.00036133s
Running propositional reduction
Post-processing
Runtime Post-process: 3.4564e-05s
Solving with MiniSAT 2.2.1 with simplifier
241 variables, 33 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 6.6318e-05s
Runtime decision procedure: 0.000482911s
VERIFICATION SUCCESSFUL

Without stop on fail:

❯ cbmc main.c
CBMC version 5.62.0 (cbmc-5.62.0-52-ga1d9f75c2d-dirty) 64-bit x86_64 macos
Parsing main.c
Converting
Type-checking main
file main.c line 4 function main: function 'assert' is not declared
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
Runtime Symex: 0.000974558s
size of program expression: 37 steps
simple slicing removed 5 assignments
Generated 1 VCC(s), 1 remaining after simplification
Runtime Postprocess Equation: 1.3696e-05s
Passing problem to propositional reduction
converting SSA
Runtime Convert SSA: 0.000350669s
Running propositional reduction
Post-processing
Runtime Post-process: 2.3313e-05s
Solving with MiniSAT 2.2.1 with simplifier
241 variables, 33 clauses
SAT checker inconsistent: instance is UNSATISFIABLE
Runtime Solver: 4.2389e-05s
Runtime decision procedure: 0.000427057s

** Results:
main.c function main
[main.assertion.1] line 4 assertion x == 0 ==> 2 * x == 0: SUCCESS

** 0 of 1 failed (1 iterations)
VERIFICATION SUCCESSFUL