Inconsistency in the results by different CBMC versions for --incremental-loop command

[ArpitaDutta]

When I run the below program on cbmc-5.95.1 using this command line : cbmc Prgm1In.c --incremental-loop main.0 --unwind-min 1

#include <assert.h>

void main (void)
{
  int x = 0;
  while(1){
		x += 2; 
	        assert(x != 5);
	}
}

I get this output:

CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing Prgm1In.c
Converting
Type-checking Prgm1In
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
Current unwinding: 1
Unwinding loop main.0 iteration 1 file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 2
Unwinding loop main.0 iteration 2 file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 3
Unwinding loop main.0 iteration 3 file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 4
Unwinding loop main.0 iteration 4 file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 5
Unwinding loop main.0 iteration 5 file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE

.....

However, for cbmc-6.6.0, it does not do anything

CBMC version 6.6.0 (cbmc-6.6.0) 64-bit x86_64 linux
Type-checking Prgm1In
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking

Similarly, when I add --unwind-max 5 (can take any number), on cbmc-5.95.1, it verifies the program successfully,

Command line: cbmc Prgm1In.c --incremental-loop main.0 --unwind-min 1 --unwind-max 5

Output:

CBMC version 5.95.1 (cbmc-5.95.1) 64-bit x86_64 linux
Parsing Prgm1In.c
Converting
Type-checking Prgm1In
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
Current unwinding: 1
Unwinding loop main.0 iteration 1 (5 max) file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 2
Unwinding loop main.0 iteration 2 (5 max) file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 3
Unwinding loop main.0 iteration 3 (5 max) file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 4
Unwinding loop main.0 iteration 4 (5 max) file Prgm1In.c line 6 function main thread 0
Incremental status: INCONCLUSIVE
Current unwinding: 5
Not unwinding loop main.0 iteration 5 (5 max) file Prgm1In.c line 6 function main thread 0

** Results:
Prgm1In.c function main
[main.assertion.1] line 8 assertion x != 5: SUCCESS

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

On the other hand, cbmc-6.6.0 gives the VERIFICATION FAILED

CBMC version 6.6.0 (cbmc-6.6.0) 64-bit x86_64 linux
Type-checking Prgm1In
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Starting Bounded Model Checking
Passing problem to refinement loop with MiniSAT 2.2.1 with simplifier
converting SSA
Running refinement loop with MiniSAT 2.2.1 with simplifier
SAT checker: instance is SATISFIABLE
BV-Refinement: got SAT, and it simulates => SAT
Runtime decision procedure: 0.000150481s

** Results:
Prgm1In.c function main
[main.unwind.0] line 5 unwinding assertion loop 0: FAILURE
[main.overflow.1] line 6 arithmetic overflow on signed + in x + 2: SUCCESS
[main.assertion.1] line 7 assertion x!=5: SUCCESS

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

Questions:

1. Was there an intentional change in how --incremental-loop + --unwind-min works between 5.95.1 and 6.6.0?

2. Why does 6.6.0 fail with an unwinding assertion where 5.95.1 passes?

[tautschnig]

With CBMC 6, we chose to turn on unwinding assertions by default (alongside several other checks to guard against undefined behaviour). You can disable them with --no-unwinding-assertions. We also changed the default verbosity and no longer print unwinding status information by default. You may wish to re-run with, e.g., --verbosity 9 and you should see incremental unwinding updates also with CBMC 6.6.