Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop t1.0 iteration 1 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
Unwinding loop t1.0 iteration 2 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
Unwinding loop t1.0 iteration 3 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
Unwinding loop t1.0 iteration 4 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
Unwinding loop t1.0 iteration 5 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
Unwinding loop t1.0 iteration 6 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
Unwinding loop t1.0 iteration 7 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
Unwinding loop t1.0 iteration 8 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 196 function t1 thread 0
Unwinding loop t2.0 iteration 1 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
Unwinding loop t2.0 iteration 2 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
Unwinding loop t2.0 iteration 3 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
Unwinding loop t2.0 iteration 4 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
Unwinding loop t2.0 iteration 5 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
Unwinding loop t2.0 iteration 6 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
Unwinding loop t2.0 iteration 7 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
Unwinding loop t2.0 iteration 8 (9 max) file CBMC5.5/MUCSeq/_cs_ID-S-Num8-lc.c line 218 function t2 thread 0
size of program expression: 6673 steps
simple slicing removed 3 assignments
Generated 1 VCC(s), 1 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
259564 variables, 1147015 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 44.482s

** Results:
[main.assertion.1] assertion (signed int)__CS_error != 1: SUCCESS

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