$ cmbc test1.c

CBMC version 5.10 (n/a) 64-bit x86_64 linux
Parsing test1.c
Converting
Type-checking test1
Generating GOTO Program
Adding CPROVER library (x86_64)
Removal of function pointers and virtual functions
Generic Property Instrumentation
Running with 8 object bits, 56 offset bits (default)
Starting Bounded Model Checking
**** WARNING: no body for function reader
size of program expression: 48 steps
simple slicing removed 5 assignments
Generated 2 VCC(s), 2 remaining after simplification
Passing problem to propositional reduction
converting SSA
Running propositional reduction
Post-processing
Solving with MiniSAT 2.2.1 with simplifier
361 variables, 562 clauses
SAT checker: instance is SATISFIABLE
Solving with MiniSAT 2.2.1 with simplifier
361 variables, 336 clauses
SAT checker: instance is UNSATISFIABLE
Runtime decision procedure: 0.00121097s

** Results:
[main.assertion.1] postcondition1: SUCCESS
[main.assertion.2] postcondition2: FAILURE

** 1 of 2 failed (2 iterations)
VERIFICATION FAILED