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: 6916 steps
no slicing due to threads
Generated 27 VCC(s), 26 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.0 with simplifier
109811 variables, 457344 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 9.496s
VERIFICATION SUCCESSFUL

real    0m10.922s
user    0m10.751s
sys     0m0.168s