~/Work/tools/cbmc-4.3/cbmc irq.c  tmp105.c  tmp105-test.c --unwind 4 -D__CBMC_TEST_HW__ -DI2C_BENCHMARK_PROP_13 #-D__EXPOSE_BUG__
file irq.c: Parsing
file tmp105.c: Parsing
file tmp105-test.c: Parsing
Converting
Type-checking irq
Type-checking tmp105
Type-checking tmp105-test
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
**** WARNING: no body for function c::fprintf
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 2 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 2 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 2 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 3 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 2 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 3 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 2 file tmp105-test.c line 50 function write thread 0
Unwinding loop c::write.0 iteration 1 file tmp105-test.c line 50 function write thread 0
size of program expression: 8613 assignments
simple slicing removed 4 assignments
Generated 127 VCC(s), 127 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 with simplifier
105183 variables, 180449 clauses
SAT checker: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 1.416s
VERIFICATION SUCCESSFUL