Tool	CBMC 4.6			CPAchecker 1.3			ESBMC 1.23
Limits	timelimit: 900 s, memlimit: 15360 MB, CPU core limit: 8
OS	Linux 3.2.0-58-generic x86_64						Linux 3.2.0-57-generic x86_64
System	CPU: Intel Core i7-2600 CPU @ 3.40GHz with 8 cores, frequency: 3401 MHz; RAM: 32827636 kB						CPU: Intel Core i7-2600 CPU @ 3.40GHz with 8 cores, frequency: 3401 MHz; RAM: 32827640 kB
Date of execution	14-01-12 13:27			14-01-12 13:28			14-01-12 13:23
Options	--propertyfile ${sourcefile_path}/ALL.prp --64			-sv-comp14-challenge -disable-java-assertions -heap 10000m -spec ${sourcefile_path}/ALL.prp -64			-c ${sourcefile_path}/ALL.prp
../../sv-benchmarks/c/ldv-challenges/	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)
linux-3.10-rc1-43_1a-bitvector-drivers--net--ethernet--broadcom--b44.ko--ldv_main0.cil.out.c	true	850	1100	timeout	900	4500	true	72	1500
linux-3.8-rc1-32_7a-drivers--md--md-mod.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	unknown	1.7	150	false(label)	180	2400	unknown	16	960
linux-3.8-rc1-32_7a-drivers--media--dvb-frontends--stv090x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	unknown	850	780	false(label)	16	610	unknown	120	810
linux-3.8-rc1-32_7a-drivers--net--ethernet--broadcom--bnx2x--bnx2x.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	unknown	850	1300	timeout	900	6000	unknown	5.2	1400
linux-3.8-rc1-32_7a-drivers--net--ethernet--broadcom--bnx2x--bnx2x.ko-ldv_main3_sequence_infinite_withcheck_stateful.cil.out.c	unknown	850	1300	timeout	900	5900	unknown	3.5	1200
linux-3.8-rc1-32_7a-drivers--net--ethernet--broadcom--tg3.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	unknown	850	720	timeout	900	8700	unknown	2.9	390
linux-3.8-rc1-32_7a-drivers--net--ethernet--emulex--benet--be2net.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	unknown	39	13000	timeout	900	4200	unknown	180	1300
linux-3.8-rc1-32_7a-drivers--net--fddi--skfp--skfp.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	unknown	850	2200	timeout	900	5500	unknown	900	4400
linux-3.8-rc1-32_7a-drivers--scsi--mpt2sas--mpt2sas.ko-ldv_main4_sequence_infinite_withcheck_stateful.cil.out.c	true	850	11000	true	74	1800	unknown	900	4100
linux-3.8-rc1-32_7a-drivers--scsi--osst.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	unknown	1.1	84	timeout	900	9500	unknown	900	3700
linux-3.8-rc1-32_7a-drivers--usb--core--usbcore.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	unknown	850	1900	exception	38	1300	unknown	900	2700
linux-3.8-rc1-32_7a-drivers--usb--core--usbcore.ko-ldv_main11_sequence_infinite_withcheck_stateful.cil.out.c	unknown	850	2000	exception	74	1800	unknown	3.3	460
linux-3.8-rc1-32_7a-drivers--usb--core--usbcore.ko-ldv_main1_sequence_infinite_withcheck_stateful.cil.out.c	unknown	850	3000	exception	74	1800	unknown	2.6	380
linux-3.8-rc1-32_7a-drivers--usb--misc--sisusbvga--sisusbvga.ko-ldv_main0_sequence_infinite_withcheck_stateful.cil.out.c	true	5.4	95	timeout	900	4200	true	3.8	250
main7-linux-3.10-rc1-43_1a-bitvector-drivers--net--ethernet--mellanox--mlx4--mlx4_en.ko.cil.out.c	unknown	1.7	130	false(label)	74	2800	unknown	2.8	540
../../sv-benchmarks/c/ldv-challenges/	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)
total files	15	8600	39000	15	7700	61000	15	4000	24000
correct results	3	0	0	4	0	0	2	0	0
false negatives	0	0	0	0	0	0	0	0	0
false positives	0	0	0	0	0	0	0	0	0
false properties	0	0	0	0	0	0	0	0	0