* /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 2 --partial-loops version 4.2 results *
Timeout: - Memory limit: unlimitedkb
Thu May 23 06:47:40 2013
Benchmark Result commandline date dec-procedure exitcode expected maxmem mt_atomic-block (**) mt_fr (**) mt_max_per_address mt_num_unique_addresses mt_po (**) mt_rf (**) mt_rf-at-least-one (**) mt_rfi (**) mt_thread-spawn (*) (**) mt_tot_subevent_count mt_ws (**) mt_ws-preceding (**) ssa-size time_dec_proc user usertime wallclock
ethoc_hw_m32_prop1_prop2 Property HOLDS /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 2 --partial-loops ../ethoc_hw_m32_prop1_prop2.gb Thu May 23 06:44:20 BST 2013 MiniSAT2 with simplifier 0 unknown 171888kb 8 2 25 9 9 9 1 27 4 1036 1.444 mictau 1.66 0:01.72
ethoc_hw_m32_prop1_prop3 Property VIOLATED /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 2 --partial-loops ../ethoc_hw_m32_prop1_prop3.gb Thu May 23 06:44:23 BST 2013 MiniSAT2 with simplifier 10 unknown 2448316kb 184 116 18 8 73 135 37 37 12 86 249 220 4633 45.216 mictau 46.14 0:47.15
ethoc_hw_m32_prop1_prop4 Property HOLDS /nas/mictau/SVNS/cbmc-r2030+concurrency --unwind 2 --partial-loops ../ethoc_hw_m32_prop1_prop4.gb Thu May 23 06:45:12 BST 2013 MiniSAT2 with simplifier 0 unknown 4023552kb 343 169 24 7 90 173 48 48 16 107 109 304 6073 144.265 mictau 145.68 2:27.37

The benchmarks were run on a Linux 3.5.0-26-generic 8x Intel(R) Xeon(R) CPU X5667 (3.07GHz) system equipped with 49453040kb RAM.

(*) This is the total number of extra threads spawned in addition to the main thread. In the paper we report that total number, i.e., mt_thread-spawn + 1.
(**) The number of concurrency constraints reported in the paper is the sum of all columns marked (**).