CBMC version 5.5 64-bit x86_64 linux
Parsing Z6.3_tso.c
Converting
Type-checking Z6.3_tso
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Unwinding loop sysinit.0 iteration 1 file Z6.3_tso.h line 29 function sysinit thread 0
Unwinding loop sysinit.0 iteration 2 file Z6.3_tso.h line 29 function sysinit thread 0
Unwinding loop sysinit.0 iteration 3 file Z6.3_tso.h line 29 function sysinit thread 0
Unwinding loop sysinit.1 iteration 1 file Z6.3_tso.h line 36 function sysinit thread 0
Unwinding loop sysinit.1 iteration 2 file Z6.3_tso.h line 36 function sysinit thread 0
Unwinding loop sysinit.1 iteration 3 file Z6.3_tso.h line 36 function sysinit thread 0
Unwinding loop sysinit.1 iteration 4 file Z6.3_tso.h line 36 function sysinit thread 0
Unwinding loop sysinit.2 iteration 1 file Z6.3_tso.h line 48 function sysinit thread 0
Unwinding loop sysinit.2 iteration 2 file Z6.3_tso.h line 48 function sysinit thread 0
Unwinding loop sysinit.2 iteration 3 file Z6.3_tso.h line 48 function sysinit thread 0
Unwinding loop sysinit.3 iteration 1 file Z6.3_tso.h line 53 function sysinit thread 0
Unwinding loop sysinit.3 iteration 2 file Z6.3_tso.h line 53 function sysinit thread 0
Unwinding loop sysinit.3 iteration 3 file Z6.3_tso.h line 53 function sysinit thread 0
Unwinding loop sysinit.3 iteration 4 file Z6.3_tso.h line 53 function sysinit thread 0
Unwinding loop sysinit.4 iteration 1 file Z6.3_tso.h line 66 function sysinit thread 0
Unwinding loop sysinit.4 iteration 2 file Z6.3_tso.h line 66 function sysinit thread 0
Unwinding loop sysinit.4 iteration 3 file Z6.3_tso.h line 66 function sysinit thread 0
Unwinding loop sysinit.5 iteration 1 file Z6.3_tso.h line 71 function sysinit thread 0
Unwinding loop sysinit.5 iteration 2 file Z6.3_tso.h line 71 function sysinit thread 0
Unwinding loop sysinit.5 iteration 3 file Z6.3_tso.h line 71 function sysinit thread 0
Unwinding loop sysinit.5 iteration 4 file Z6.3_tso.h line 71 function sysinit thread 0
size of program expression: 954 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
12658 variables, 27981 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 0.049s

** Results:
[main.assertion.1] assertion !(y == 2 && r1 == 1 && r2 == 0): SUCCESS

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