SV-COMP 2018: diff "CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr: Fixing `bitvector/modulus_true-unreach-call_true-no-overflow.i`

[marek-trtik]

The goal is to fix the benchmark bitvector/modulus_true-unreach-call_true-no-overflow.i in the CBMC version (left tool)

https://github.com/marek-trtik/cbmc/tree/sv-comp-2018-patches

The original CBMC version (right tool) is here:

https://github.com/tautschnig/cbmc/tree/sv-comp-2017

Here is the diff file:

diff_CBMC-sv-comp-2017-pr-rebase_CBMC-sv-comp-2017-pr.json.zip

And here is the CBMC package of SV-COMP 2017:

CBMC-sv-comp-2017.tar.gz

[marek-trtik]

• The evaluation of the latest cbmc binary of the benchmark produces the correct result true. This was also confirmed by the direct evaluation in the benchexec tool.

• The re-evaluation of old binary on the benchmark also produced correct result true (in both the framework and benchexec)

• I've double-checked original results from the machine on Google cloud. The resulting XML files indeed claim ERROR state. I also performed binary compare of CBMC binary on the Google count with the one tested locally. They are equal. Equal are also shell script calling CBMC.

The major difference is that on Google cloud the benchmark was evaluated together with many others, while locally I have created a new category consisting only of that benchmark.

[peterschrammel]

Can you run the bitvector reach safety category again with the sv-comp-2018 branch to check whether this problem is solved?

[marek-trtik]

And another re-evaluation in benchexec produced correct result again. Here is the log:

./xtest --graphml-witness witness.graphml --32 --propertyfile ../sv-benchmarks/c/ReachSafety.prp ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i

--------------------------------------------------------------------------------

./xtest-binary --graphml-witness /tmp/BenchExec_run_4r0njzhb/tmp/xtest-log.ETimsE.witness --unwind 2 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --unwinding-assertions --unwind 2 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --graphml-witness /tmp/BenchExec_run_4r0njzhb/tmp/xtest-log.ETimsE.witness --unwind 6 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --unwinding-assertions --unwind 6 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --graphml-witness /tmp/BenchExec_run_4r0njzhb/tmp/xtest-log.ETimsE.witness --unwind 12 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --unwinding-assertions --unwind 12 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --graphml-witness /tmp/BenchExec_run_4r0njzhb/tmp/xtest-log.ETimsE.witness --unwind 17 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --unwinding-assertions --unwind 17 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --graphml-witness /tmp/BenchExec_run_4r0njzhb/tmp/xtest-log.ETimsE.witness --unwind 21 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --unwinding-assertions --unwind 21 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --graphml-witness /tmp/BenchExec_run_4r0njzhb/tmp/xtest-log.ETimsE.witness --unwind 40 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
./xtest-binary --unwinding-assertions --unwind 40 --stop-on-fail --32 --function main ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
Unwind: 40
CBMC version 5.8 64-bit x86_64 linux
Parsing ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i
Converting
Type-checking modulus_true-unreach-call_true-no-overflow
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 24 offset bits (default)
Starting Bounded Model Checking
Unwinding loop main.0 iteration 1 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 2 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 3 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 4 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 5 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 6 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 7 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 8 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 9 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 10 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 11 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 12 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 13 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 14 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 15 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 16 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 17 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 18 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 19 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 20 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 21 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 22 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 23 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 24 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 25 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 26 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 27 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 28 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 29 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 30 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 31 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 32 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 33 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 34 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 35 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 36 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 37 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 38 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 39 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Not unwinding loop main.0 iteration 40 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.1 iteration 1 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 32 function main thread 0
Unwinding loop main.0 iteration 1 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 2 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 3 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 4 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 5 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 6 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 7 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 8 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 9 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 10 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 11 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 12 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 13 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 14 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 15 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 16 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 17 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 18 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 19 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 20 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 21 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 22 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 23 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 24 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 25 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 26 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 27 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 28 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 29 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 30 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 31 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 32 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 33 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 34 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 35 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 36 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 37 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 38 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 39 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Not unwinding loop main.0 iteration 40 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.1 iteration 2 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 32 function main thread 0
Unwinding loop main.0 iteration 1 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 2 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 3 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 4 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 5 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 6 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 7 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 8 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 9 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 10 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 11 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 12 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 13 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 14 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 15 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 16 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main 

...........

thread 0
Unwinding loop main.0 iteration 23 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 24 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 25 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 26 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 27 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 28 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 29 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 30 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 31 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 32 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 33 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 34 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 35 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 36 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 37 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 38 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Unwinding loop main.0 iteration 39 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Not unwinding loop main.0 iteration 40 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 34 function main thread 0
Not unwinding loop main.1 iteration 40 (40 max) file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 32 function main thread 0
aborting path on assume(false) at file ../sv-benchmarks/c/bitvector/modulus_true-unreach-call_true-no-overflow.i line 7 function __VERIFIER_assert thread 0
size of program expression: 11577 steps
simple slicing removed 9 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with Glucose Syrup with simplifier
1956792 variables, 6688405 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 318.636s
VERIFICATION SUCCESSFUL
EC=0
TRUE

[marek-trtik]

Closing the issue, because I cannot reproduce the wrong result from the Google cloud evaluation.