~/Work/tools/cbmc-4.3/cbmc main.c mc146818rtc.c qemu-timer.c qverify.c rtc-verify.c --unwind 1 -D__CBMC_TEST_HW__ -D__NO_TIMER__ -DRTC_BENCHMARK_PROP_6 -D__EXPOSE_BUG__ 
file main.c: Parsing
file mc146818rtc.c: Parsing
file qemu-timer.c: Parsing
file qverify.c: Parsing
file rtc-verify.c: Parsing
Converting
Type-checking main
Type-checking mc146818rtc
Type-checking qemu-timer
Type-checking qverify
Type-checking rtc-verify
Generating GOTO Program
Adding CPROVER library
Function Pointer Removal
Partial Inlining
Generic Property Instrumentation
Starting Bounded Model Checking
**** WARNING: no body for function c::gettimeofday
Unwinding loop c::cmos_ioport_write.1 iteration 1 file mc146818rtc.c line 604 function cmos_ioport_write thread 0
Unwinding loop c::cmos_ioport_write.1 iteration 1 file mc146818rtc.c line 604 function cmos_ioport_write thread 0
Unwinding loop c::cmos_ioport_write.1 iteration 1 file mc146818rtc.c line 604 function cmos_ioport_write thread 0
Unwinding loop c::cmos_ioport_write.1 iteration 1 file mc146818rtc.c line 604 function cmos_ioport_write thread 0
Unwinding loop c::cmos_ioport_write.1 iteration 1 file mc146818rtc.c line 604 function cmos_ioport_write thread 0
size of program expression: 23177 assignments
simple slicing removed 56 assignments
Generated 7 VCC(s), 7 remaining after simplification
Passing problem to propositional reduction
Running propositional reduction
Solving with MiniSAT2 with simplifier
3692677 variables, 10821606 clauses
SAT checker inconsistent: negated claim is UNSATISFIABLE, i.e., holds
Runtime decision procedure: 6.128s
VERIFICATION SUCCESSFUL