Tool	BLAST 2.7		CPAchecker ABE r4569		CPAchecker ABM r4573		ESBMC 1.17		FShell 1.3		LLBMC 0.9		Predator		QARMC-HSF		SatAbs 3.0		WOLVERINE 0.5c
Limits	timelimit: 900 s, memlimit: 15000 MB
System	os: Linux 2.6.35-30-generic x86_64 cpu: Intel(R) Core(TM) i7-2600K CPU @ 3.40GHz cores: 4, frequency: 3401 MHz, ram: 16375440 kB
Date of run	2011-12-06 03:06		2011-12-03 10:32		2011-12-04 14:36		2011-12-04 08:46		2011-12-05 01:14		2011-12-07 02:12		2011-12-04 23:44		2011-12-05 10:09		2011-12-05 13:41		2011-12-06 08:38
Benchmark	control		control		control		control		control		control		control		control		control		control
Options	-alias bdd -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb		-heap 12500m -sv-comp12		-heap 12500m -sv-comp12-abm		--64 --error-label ERROR --no-bounds-check --no-div-by-zero-check --no-assertions --no-pointer-check --no-unwinding-assertions --partial-loops --unwind 8		--unwind 10 --query-file benchmarks/fshell_query --no-unwinding-assertions --32				-m32				--full-inlining --iterations 500 --error-label ERROR --32		--error-label ERROR --32
../sv-benchmarks/	status	runtime	status	runtime	status	runtime	status	runtime	status	runtime	status	runtime	status	runtime	status	runtime	status	runtime	status	runtime
total files	93	43000	93	2800	93	4300	93	19000	93	4100	93	2700	93	15000	93	6600	93	18000	93	62000
correct results	51	9900	91	1000	91	3200	70	4500	67	580	79	2400	24	1100	91	4800	47	5400	25	580
false negatives	0	0	0	0	0	0	4	1700	22	310	3	140	0	0	0	0	0	0	0	0
false positives	0	0	0	0	0	0	0	0	0	0	5	140	8	710	0	0	0	0	0	0
score (93 files, max score: 144)	71		141		140		102		28		100		17		140		75		39
ntdrivers-simplified/cdaudio_simpl1_BUG.cil.c	unsafe	240	unsafe	5.0	unsafe	10.0	safe	1.1	unsafe	2.2	unsafe	0.67	unsafe	0.63	unsafe	390	timeout	910	unsafe	3.1
ntdrivers-simplified/floppy_simpl3_BUG.cil.c	unsafe	31	unsafe	2.6	unsafe	5.6	unsafe	0.32	unsafe	0.36	unsafe	0.11	unknown	0.71	unsafe	260	unsafe	170	unsafe	1.6
ntdrivers-simplified/floppy_simpl4_BUG.cil.c	unsafe	46	unsafe	3.6	unsafe	6.4	unsafe	0.52	unsafe	0.65	unsafe	0.12	unsafe	0.66	unsafe	740	unsafe	460	unsafe	1.7
ntdrivers-simplified/kbfiltr_simpl2_BUG.cil.c	unsafe	4.8	unsafe	3.0	unsafe	3.9	unsafe	0.24	unsafe	0.31	unsafe	0.08	unsafe	0.13	unsafe	12	unsafe	54	unsafe	0.62
ntdrivers-simplified/cdaudio_simpl1.cil.c	timeout	910	safe	4.5	safe	9.8	safe	1.1	safe	2.5	safe	0.25	unsafe	0.62	safe	380	timeout	910	safe	11
ntdrivers-simplified/diskperf_simpl1.cil.c	safe	160	safe	3.1	safe	8.0	safe	0.43	safe	0.8	safe	1.3	unsafe	1.4	safe	330	timeout	910	safe	7.7
ntdrivers-simplified/floppy_simpl3.cil.c	safe	180	safe	2.5	safe	7.7	safe	0.28	safe	0.6	safe	0.16	unknown	0.72	safe	420	safe	260	safe	6.3
ntdrivers-simplified/floppy_simpl4.cil.c	safe	350	safe	2.9	safe	8.6	safe	0.49	safe	0.87	safe	0.2	unsafe	0.67	safe	790	safe	760	safe	7.5
ntdrivers-simplified/kbfiltr_simpl1.cil.c	safe	2.3	safe	1.7	safe	2.9	safe	0.11	safe	0.14	safe	0.09	safe	0.12	safe	4.0	safe	13	safe	1.5
ntdrivers-simplified/kbfiltr_simpl2.cil.c	safe	2.4	safe	2.2	safe	3.9	safe	0.23	safe	0.29	safe	0.11	safe	0.16	safe	9.2	safe	37	safe	2.1
ntdrivers/cdaudio.BUG.i.cil.c	unsafe	34	unsafe	6.9	unsafe	12	unknown	4.8	safe	0.81	unsafe	3.5	unknown	1.0	unsafe	58	failure	760	unsafe	1.0
ntdrivers/diskperf.BUG.i.cil.c	unsafe	9.1	unsafe	4.1	unsafe	7.6	unsafe	3.5	safe	0.54	unknown	0.26	unknown	0.19	unsafe	4.3	unsafe	46	unsafe	0.86
ntdrivers/floppy.BUG.i.cil.c	unsafe	6.2	unsafe	7.2	unsafe	9.5	unknown	360	error	720	unknown	0.24	unknown	0.2	unsafe	30	unsafe	210	unsafe	0.9
ntdrivers/kbfiltr.BUG.i.cil.c	unsafe	90	unsafe	3.4	unsafe	4.7	unsafe	1.3	safe	0.53	unsafe	5.7	unknown	0.13	unsafe	20	timeout	910	timeout	900
ntdrivers/parport.BUG.i.cil.c	unsafe	9.3	out of memory	900	unsafe	15	unknown	120	timeout	900	unknown	0.39	unknown	0.82	unsafe	58	timeout	910	unsafe	0.49
ntdrivers/cdaudio.i.cil.c	safe	510	safe	7.9	safe	13	unknown	4.8	safe	0.81	unsafe	3.6	unknown	1.0	safe	360	failure	710	safe	15
ntdrivers/diskperf.i.cil.c	safe	180	safe	3.8	safe	8.4	safe	3.0	safe	0.54	unknown	0.25	unknown	0.19	timeout	900	timeout	910	safe	10
ntdrivers/floppy.i.cil.c	unknown	140	safe	8.5	safe	11	unknown	370	error	720	unknown	0.25	unknown	0.2	safe	220	failure	28	safe	310
ntdrivers/parport.i.cil.c	timeout	910	timeout	900	safe	24	unknown	120	timeout	900	unknown	0.4	unknown	0.78	timeout	910	timeout	910	timeout	900
ssh-simplified/s3_clnt_1_BUG.cil.c	unsafe	22	unsafe	3.1	unsafe	3.8	unsafe	4.3	unsafe	9.2	unsafe	0.23	unsafe	3.9	unsafe	1.7	unsafe	6.0	timeout	900
ssh-simplified/s3_clnt_2_BUG.cil.c	unsafe	22	unsafe	3.0	unsafe	3.5	unsafe	4.3	unsafe	11	unsafe	0.24	unsafe	3.9	unsafe	1.7	unsafe	5.9	timeout	900
ssh-simplified/s3_clnt_3_BUG.cil.c	unsafe	22	unsafe	3.0	unsafe	4.0	unsafe	4.6	unsafe	12	unsafe	0.24	unsafe	4.1	unsafe	2.0	unsafe	6.2	timeout	900
ssh-simplified/s3_clnt_4_BUG.cil.c	unsafe	22	unsafe	4.0	unsafe	3.9	unsafe	4.3	unsafe	10	unsafe	0.25	unsafe	3.9	unsafe	1.8	unsafe	6.0	timeout	900
ssh-simplified/s3_srvr_10_BUG.cil.c	unsafe	0.07	unsafe	2.1	unsafe	44	unsafe	5.8	unsafe	11	unsafe	0.05	unsafe	0.06	unsafe	1.2	unsafe	1.6	timeout	900
ssh-simplified/s3_srvr_11_BUG.cil.c	unknown	2.8	unsafe	6.6	unsafe	360	unsafe	7.6	unsafe	13	unsafe	0.47	unsafe	120	unsafe	9.4	unsafe	330	timeout	900
ssh-simplified/s3_srvr_12_BUG.cil.c	unknown	3.0	unsafe	4.8	unsafe	18	unsafe	9.4	unsafe	16	unsafe	0.34	unsafe	1.1	unsafe	33	unsafe	580	timeout	900
ssh-simplified/s3_srvr_13_BUG.cil.c	unknown	2.5	unsafe	3.7	unsafe	87	unsafe	7.7	unsafe	15	unsafe	0.16	unsafe	0.82	unsafe	7.5	unsafe	55	timeout	900
ssh-simplified/s3_srvr_14_BUG.cil.c	unknown	4.9	unsafe	2.4	unsafe	12	unsafe	7.3	unsafe	13	unsafe	0.06	unsafe	0.11	unsafe	3.7	unsafe	27	timeout	900
ssh-simplified/s3_srvr_1_BUG.cil.c	unsafe	4.1	unsafe	3.0	unsafe	3.7	unsafe	6.8	unsafe	13	unsafe	0.14	unsafe	1.9	unsafe	2.2	unsafe	8.3	timeout	900
ssh-simplified/s3_srvr_2_BUG.cil.c	unsafe	4.2	unsafe	2.8	unsafe	3.3	unsafe	6.6	unsafe	12	unsafe	0.14	unsafe	2.1	unsafe	2.3	unsafe	6.9	timeout	900
ssh-simplified/s3_srvr_6_BUG.cil.c	unsafe	0.06	unsafe	1.7	unsafe	1.8	unsafe	7.7	unsafe	14	unsafe	0.05	unsafe	0.04	unsafe	1.4	unsafe	1.1	unsafe	1.1
ssh-simplified/s3_clnt_1.cil.c	safe	140	safe	7.9	safe	12	safe	3.7	safe	7.9	safe	0.51	unsafe	320	safe	6.3	safe	42	timeout	900
ssh-simplified/s3_clnt_2.cil.c	timeout	910	safe	6.7	safe	8.3	safe	3.8	safe	7.9	safe	0.57	unsafe	94	safe	3.8	safe	300	timeout	900
ssh-simplified/s3_clnt_3.cil.c	safe	350	safe	9.9	safe	6.9	safe	4.1	safe	9.7	safe	0.58	unsafe	130	safe	7.3	safe	160	timeout	900
ssh-simplified/s3_clnt_4.cil.c	timeout	910	safe	6.3	safe	13	safe	3.8	safe	7.9	safe	0.59	unsafe	160	safe	5.8	safe	180	timeout	900
ssh-simplified/s3_srvr_1.cil.c	unknown	0.04	safe	22	safe	8.1	safe	5.7	safe	15	safe	0.57	timeout	900	safe	0.97	safe	120	timeout	900
ssh-simplified/s3_srvr_1a.cil.c	safe	1.1	safe	2.9	safe	5.0	safe	0.34	safe	0.29	safe	0.24	unsafe	0.06	safe	0.67	safe	0.59	safe	2.6
ssh-simplified/s3_srvr_1b.cil.c	safe	1.1	safe	1.5	safe	1.7	safe	0.14	safe	0.12	safe	0.24	safe	0.05	safe	0.33	safe	0.22	safe	0.3
ssh-simplified/s3_srvr_2.cil.c	safe	410	safe	65	safe	120	safe	5.7	safe	11	safe	0.6	timeout	900	safe	8.4	safe	110	timeout	900
ssh-simplified/s3_srvr_3.cil.c	safe	430	safe	17	safe	22	safe	5.7	safe	11	safe	0.6	timeout	900	safe	30	safe	91	timeout	900
ssh-simplified/s3_srvr_4.cil.c	safe	440	safe	6.6	safe	14	safe	5.7	safe	11	safe	0.63	timeout	900	safe	7.6	safe	130	timeout	900
ssh-simplified/s3_srvr_6.cil.c	timeout	910	safe	180	out of memory	230	safe	6.7	safe	11	safe	1.1	timeout	900	safe	42	safe	480	timeout	900
ssh-simplified/s3_srvr_7.cil.c	timeout	910	safe	24	safe	110	safe	5.9	safe	11	safe	0.71	timeout	900	safe	110	safe	340	timeout	900
ssh-simplified/s3_srvr_8.cil.c	safe	220	safe	19	safe	8.7	safe	6.1	safe	11	safe	0.65	timeout	900	safe	20	safe	350	timeout	900
ssh/s3_clnt.blast.01.BUG.i.cil.c	unsafe	560	unsafe	4.5	unsafe	4.7	timeout	900	safe	58	unsafe	110	unknown	0.07	unsafe	2.4	timeout	910	timeout	900
ssh/s3_clnt.blast.02.BUG.i.cil.c	unsafe	520	unsafe	3.5	unsafe	5.4	timeout	900	safe	57	unsafe	63	unknown	0.07	unsafe	2.0	failure	150	timeout	900
ssh/s3_clnt.blast.03.BUG.i.cil.c	unsafe	300	unsafe	3.7	unsafe	4.2	timeout	900	safe	57	unsafe	62	unknown	0.07	unsafe	1.9	failure	150	timeout	900
ssh/s3_clnt.blast.04.BUG.i.cil.c	unsafe	560	unsafe	3.1	unsafe	4.6	timeout	900	safe	57	unsafe	64	unknown	0.07	unsafe	1.9	failure	150	timeout	900
ssh/s3_srvr.blast.01.BUG.i.cil.c	unsafe	89	unsafe	3.4	unsafe	4.9	timeout	900	safe	5.9	unsafe	0.56	unknown	0.95	unsafe	2.9	failure	0.61	timeout	900
ssh/s3_srvr.blast.02.BUG.i.cil.c	unsafe	7.1	unsafe	3.2	unsafe	4.2	unsafe	710	safe	5.0	unsafe	0.39	unknown	2.8	unsafe	2.4	failure	0.46	timeout	900
ssh/s3_srvr.blast.03.BUG.i.cil.c	unsafe	7.0	unsafe	3.1	unsafe	4.2	timeout	900	safe	5.1	unsafe	0.39	unknown	2.8	unsafe	2.4	failure	0.53	timeout	900
ssh/s3_srvr.blast.04.BUG.i.cil.c	unsafe	7.1	unsafe	3.2	unsafe	3.7	timeout	900	safe	5.0	unsafe	0.37	unknown	2.8	unsafe	2.0	failure	0.53	timeout	900
ssh/s3_srvr.blast.06.BUG.i.cil.c	unsafe	610	unsafe	5.4	unsafe	12	timeout	900	safe	5.5	unsafe	1.4	unknown	0.38	unsafe	4.5	failure	0.7	timeout	900
ssh/s3_srvr.blast.07.BUG.i.cil.c	timeout	910	unsafe	4.5	unsafe	110	unsafe	800	safe	5.2	unsafe	2.3	unknown	2.8	unsafe	5.4	failure	0.64	timeout	900
ssh/s3_srvr.blast.08.BUG.i.cil.c	timeout	910	unsafe	5.4	unsafe	13	safe	560	safe	5.2	safe	45	unknown	0.43	unsafe	6.4	failure	0.61	timeout	900
ssh/s3_srvr.blast.09.BUG.i.cil.c	timeout	910	unsafe	4.0	unsafe	260	timeout	900	safe	5.2	unsafe	2.1	unknown	2.9	unsafe	4.7	failure	0.64	timeout	900
ssh/s3_srvr.blast.10.BUG.i.cil.c	timeout	910	unsafe	5.7	unsafe	12	safe	550	safe	5.1	safe	53	unknown	0.43	unsafe	6.1	failure	0.61	timeout	900
ssh/s3_srvr.blast.11.BUG.i.cil.c	unsafe	460	unsafe	4.0	unsafe	3.8	timeout	900	safe	5.2	unsafe	1.4	unknown	2.9	unsafe	3.1	failure	0.57	timeout	900
ssh/s3_srvr.blast.12.BUG.i.cil.c	unsafe	840	unsafe	4.7	unsafe	7.9	timeout	900	safe	5.2	unsafe	2.0	unknown	0.43	unsafe	3.2	failure	0.65	timeout	900
ssh/s3_srvr.blast.13.BUG.i.cil.c	timeout	910	unsafe	5.0	unsafe	47	timeout	900	safe	5.2	unsafe	1.9	unknown	2.9	unsafe	5.8	failure	0.56	timeout	900
ssh/s3_srvr.blast.14.BUG.i.cil.c	unsafe	900	unsafe	4.9	unsafe	8.9	unsafe	880	safe	5.3	unsafe	2.0	unknown	0.43	unsafe	3.7	failure	0.65	timeout	900
ssh/s3_srvr.blast.15.BUG.i.cil.c	timeout	910	unsafe	7.0	unsafe	14	safe	630	safe	5.3	safe	43	unknown	0.41	unsafe	6.5	failure	0.63	timeout	900
ssh/s3_srvr.blast.16.BUG.i.cil.c	timeout	910	unsafe	4.5	unsafe	7.4	timeout	900	safe	5.4	unsafe	1.3	unknown	0.41	unsafe	4.4	failure	0.68	timeout	900
ssh/s3_clnt.blast.01.i.cil.c	timeout	910	safe	8.5	safe	8.7	safe	52	safe	56	safe	340	unknown	0.06	safe	6.6	timeout	910	timeout	900
ssh/s3_clnt.blast.02.i.cil.c	timeout	910	safe	7.4	safe	9.5	safe	53	safe	57	safe	370	unknown	0.07	safe	4.1	timeout	910	timeout	900
ssh/s3_clnt.blast.03.i.cil.c	timeout	910	safe	9.1	safe	11	safe	53	safe	57	safe	490	unknown	0.07	safe	6.4	timeout	910	timeout	900
ssh/s3_clnt.blast.04.i.cil.c	timeout	910	safe	12	safe	9.5	safe	53	safe	57	safe	320	unknown	0.07	safe	6.0	timeout	910	timeout	900
ssh/s3_srvr.blast.01.i.cil.c	timeout	910	safe	22	safe	36	safe	150	safe	5.9	safe	46	unknown	0.95	safe	3.9	failure	0.68	timeout	900
ssh/s3_srvr.blast.02.i.cil.c	timeout	910	safe	15	safe	13	safe	410	safe	5.0	unsafe	42	unknown	2.8	safe	8.3	failure	0.47	timeout	900
ssh/s3_srvr.blast.06.i.cil.c	timeout	910	safe	25	safe	19	safe	200	safe	5.6	safe	69	unknown	3.1	safe	15	failure	0.73	timeout	900
ssh/s3_srvr.blast.07.i.cil.c	timeout	910	safe	35	timeout	900	safe	190	safe	5.2	unsafe	39	unknown	2.8	safe	35	failure	0.65	timeout	900
ssh/s3_srvr.blast.08.i.cil.c	timeout	910	safe	17	safe	140	safe	49	safe	5.2	safe	47	unknown	2.9	safe	14	failure	0.62	timeout	900
ssh/s3_srvr.blast.09.i.cil.c	timeout	910	safe	30	safe	36	safe	100	safe	5.2	unsafe	40	unknown	2.9	safe	23	failure	0.65	timeout	900
ssh/s3_srvr.blast.10.i.cil.c	timeout	910	safe	10	safe	13	safe	46	safe	5.2	safe	72	unknown	2.9	safe	14	failure	0.62	timeout	900
ssh/s3_srvr.blast.11.i.cil.c	timeout	910	safe	22	safe	310	safe	120	safe	5.2	safe	51	unknown	2.8	safe	42	failure	0.58	timeout	900
ssh/s3_srvr.blast.12.i.cil.c	timeout	910	safe	25	safe	32	safe	180	safe	5.2	safe	73	unknown	3.0	safe	20	failure	0.65	timeout	900
ssh/s3_srvr.blast.13.i.cil.c	timeout	910	safe	24	safe	680	safe	61	safe	5.2	unsafe	16	unknown	2.9	safe	36	failure	0.63	timeout	900
ssh/s3_srvr.blast.14.i.cil.c	timeout	910	safe	12	safe	39	safe	65	safe	5.4	safe	59	unknown	3.0	safe	14	failure	0.6	timeout	900
ssh/s3_srvr.blast.15.i.cil.c	timeout	910	safe	110	safe	68	safe	25	safe	5.4	safe	50	unknown	2.9	safe	15	failure	0.71	timeout	900
ssh/s3_srvr.blast.16.i.cil.c	timeout	910	safe	59	safe	130	safe	130	safe	5.5	safe	48	unknown	3.0	safe	14	failure	0.93	timeout	900
locks/test_locks_14.BUG.c	unsafe	0.08	unsafe	1.6	unsafe	2.7	unsafe	0.75	unsafe	0.7	unsafe	0.04	timeout	900	unsafe	0.41	unsafe	0.26	unsafe	0.03
locks/test_locks_15.BUG.c	unsafe	0.08	unsafe	2.0	unsafe	2.8	unsafe	0.85	unsafe	0.79	unsafe	0.04	timeout	900	unsafe	0.42	unsafe	0.33	unsafe	0.03
locks/test_locks_10.c	timeout	910	safe	1.4	safe	1.8	safe	0.31	safe	0.35	safe	0.32	safe	800	safe	0.39	safe	1.7	timeout	900
locks/test_locks_11.c	timeout	910	safe	1.5	safe	1.9	safe	0.36	safe	0.41	safe	0.33	timeout	900	safe	0.42	safe	2.6	timeout	900
locks/test_locks_12.c	timeout	910	safe	2.0	safe	2.5	safe	0.41	safe	0.47	safe	0.35	timeout	900	safe	0.46	safe	4.0	timeout	900
locks/test_locks_13.c	timeout	910	safe	1.5	safe	2.1	safe	0.47	safe	0.54	safe	0.36	timeout	900	safe	0.5	safe	4.8	timeout	900
locks/test_locks_14.c	timeout	910	safe	1.5	safe	2.2	safe	0.55	safe	0.61	safe	0.38	timeout	900	safe	0.53	safe	8.2	timeout	900
locks/test_locks_15.c	timeout	910	safe	2.0	safe	2.2	safe	0.59	safe	0.67	safe	0.4	timeout	900	safe	0.58	safe	9.4	timeout	900
locks/test_locks_5.c	safe	22	safe	1.4	safe	1.7	safe	0.13	safe	0.14	safe	0.24	safe	0.32	safe	0.25	safe	0.28	safe	1.8
locks/test_locks_6.c	safe	43	safe	1.9	safe	2.1	safe	0.16	safe	0.18	safe	0.25	safe	1.4	safe	0.26	safe	0.4	safe	12
locks/test_locks_7.c	safe	140	safe	1.9	safe	1.6	safe	0.19	safe	0.21	safe	0.27	safe	6.4	safe	0.28	safe	0.61	safe	180
locks/test_locks_8.c	safe	270	safe	1.4	safe	2.2	safe	0.22	safe	0.26	safe	0.28	safe	31	safe	0.3	safe	0.84	timeout	900
locks/test_locks_9.c	safe	600	safe	1.9	safe	1.7	safe	0.32	safe	0.29	safe	0.3	safe	150	safe	0.33	safe	1.2	timeout	900