file checkiftrans.c: Parsing
Converting
Type-checking checkiftrans
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
size of program expression: 166 assignments
simple slicing removed 1 assignments
Generated 18 VCC(s), 16 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 without simplifier
4061 variables, 11441 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 0.1s
VERIFICATION SUCCESSFUL