CBMC version 5.0 64-bit linux
Parsing fake.c
Converting
Type-checking fake
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
Adding SC constraints
size of program expression: 7433 steps
no slicing due to threads
Generated 7 VCC(s), 7 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
69050 variables, 287548 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 9.129s
VERIFICATION SUCCESSFUL

real    0m10.155s
user    0m9.994s
sys     0m0.156s