Tool	BLAST 2.7		CPAchecker ABE r4569		CPAchecker ABM r4573		ESBMC 1.17		FShell 1.3		LLBMC 0.9		Predator		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 13:41		2011-12-06 08:38
Benchmark	drivers		drivers		drivers		drivers		drivers		drivers		drivers		drivers		drivers
Options	-alias bdd -enable-recursion -noprofile -cref -sv-comp -lattice -include-lattice symb		-heap 12500m -sv-comp12 -setprop cpa.predicate.handlePointerAliasing=true		-heap 12500m -setprop cpa.predicate.handlePointerAliasing=true -setprop cpa.abm.blockHeuristic=LoopPartitioning -sv-comp12-abm-funpoint		--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 --modelchecker boom --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
total files	59	300	59	120	59	110	59	310	59	5.2	59	2200	59	3.7	59	1600	59	99
correct results	51	30	46	97	46	93	43	160	40	3.5	46	1.6	46	1.9	43	140	48	65
false negatives	1	1.2	0	0	0	0	0	0	15	1.7	0	0	0	0	1	0.17	3	34
false positives	6	0.34	13	22	13	22	6	0.27	0	0	0	0	0	0	0	0	2	0.06
score (59 files, max score: 103)	72		51		51		63		20		80		80		71		68
ldv-regression/1_3.c-unsafe.cil.c	unsafe	0.06	unsafe	1.4	unsafe	1.7	unsafe	0.06	safe	0.07	unsafe	0.03	unsafe	0.03	failure	0.07	unsafe	0.03
ldv-regression/alt_test.c-unsafe.cil.c	unsafe	0.96	unsafe	1.4	unsafe	1.5	unsafe	0.07	safe	0.07	unsafe	0.03	unsafe	0.03	failure	3.5	unsafe	0.09
ldv-regression/callfpointer.c-unsafe.cil.c	unsafe	0.05	unsafe	1.8	unsafe	1.9	unsafe	0.05	safe	0.03	unsafe	0.03	unsafe	0.03	unsafe	0.05	unsafe	0.02
ldv-regression/fo_test.c-unsafe.cil.c	unsafe	0.06	unsafe	1.4	unsafe	1.4	unsafe	0.05	safe	0.09	unsafe	0.03	unsafe	0.03	unsafe	0.11	unsafe	0.03
ldv-regression/mutex_lock_int.c-unsafe.cil.c	unsafe	0.05	unsafe	1.9	unsafe	1.4	unsafe	0.04	safe	0.02	unsafe	0.03	unsafe	0.03	unsafe	0.09	unsafe	0.03
ldv-regression/mutex_lock_struct.c-unsafe.cil.c	unsafe	0.05	unsafe	1.9	unsafe	1.4	unsafe	0.04	safe	0.03	unsafe	0.03	unsafe	0.03	unsafe	0.09	unsafe	0.03
ldv-regression/recursive_list.c-unsafe.cil.c	unsafe	0.09	unsafe	1.9	unsafe	1.4	unsafe	0.06	safe	0.07	unsafe	0.03	unsafe	0.04	failure	0.08	unsafe	0.03
ldv-regression/rule57_ebda_blast.c-unsafe.cil.c	unsafe	0.06	unsafe	1.9	unsafe	1.4	unknown	0.06	safe	0.05	unsafe	0.04	unsafe	0.06	unsafe	0.11	unsafe	0.05
ldv-regression/rule60_list2.c-unsafe_1.cil.c	unsafe	3.4	unsafe	1.6	unsafe	1.6	unsafe	0.07	safe	0.05	unsafe	0.04	unsafe	0.03	unsafe	34	unsafe	1.1
ldv-regression/stateful_check-unsafe.cil.c	safe	1.2	unsafe	1.8	unsafe	1.8	unsafe	0.27	safe	0.38	unsafe	0.15	unsafe	0.04	safe	0.17	unsafe	1.4
ldv-regression/test_while_int.c-unsafe.cil.c	unsafe	0.55	unsafe	1.9	unsafe	1.9	unsafe	0.04	safe	0.02	unsafe	0.03	unsafe	0.03	unsafe	0.17	unsafe	0.10
ldv-regression/test_while_int.c-unsafe_1.cil.c	unsafe	0.42	unsafe	1.9	unsafe	1.7	unsafe	0.04	safe	0.03	unsafe	0.03	unsafe	0.03	unsafe	0.15	unsafe	0.07
ldv-regression/alias_of_return.c-safe.cil.c	safe	0.04	safe	1.4	safe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.13	safe	0.02
ldv-regression/alias_of_return.c-safe_1.cil.c	safe	0.04	safe	1.8	safe	1.4	safe	0.04	safe	0.02	safe	0.03	safe	0.04	safe	0.10	safe	0.03
ldv-regression/alias_of_return_2.c-safe.cil.c	safe	0.04	safe	1.8	safe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.11	safe	0.03
ldv-regression/alias_of_return_2.c-safe_1.cil.c	safe	0.04	safe	1.4	safe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.09	safe	0.02
ldv-regression/ex3_forlist.c-safe.cil.c	unknown	270	unsafe	2.0	unsafe	1.9	unknown	0.08	safe	0.06	safe	0.05	safe	0.05	timeout	1400	safe	58
ldv-regression/just_assert.c-safe.cil.c	safe	0.04	safe	1.8	safe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.05	safe	0.02
ldv-regression/mutex_lock_int.c-safe_1.cil.c	safe	0.04	unsafe	1.4	unsafe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.28	safe	0.03
ldv-regression/mutex_lock_struct.c-safe_1.cil.c	safe	0.04	unsafe	1.4	unsafe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.32	safe	0.03
ldv-regression/nested_structure-safe.cil.c	unsafe	0.06	unsafe	1.9	unsafe	1.9	unsafe	0.05	safe	0.03	safe	0.03	safe	0.04	failure	0.04	safe	0.03
ldv-regression/nested_structure.c-safe.cil.c	safe	0.04	unsafe	1.9	unsafe	1.4	safe	0.05	safe	0.03	safe	0.03	safe	0.04	safe	0.33	safe	0.03
ldv-regression/nested_structure_noptr-safe.cil.c	safe	0.04	safe	1.8	safe	1.8	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.07	safe	0.03
ldv-regression/nested_structure_noptr.c-safe.cil.c	safe	0.04	safe	1.8	safe	1.8	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.07	safe	0.03
ldv-regression/nested_structure_ptr-safe.cil.c	unsafe	0.08	unsafe	1.6	unsafe	1.6	unsafe	0.04	safe	0.03	safe	0.03	safe	0.04	failure	0.05	failure	0.03
ldv-regression/nested_structure_ptr.c-safe.cil.c	safe	0.04	unsafe	1.9	unsafe	1.9	safe	0.04	safe	0.02	safe	0.03	safe	0.04	safe	0.95	safe	0.03
ldv-regression/oomInt.c-safe.cil.c	safe	0.04	safe	1.8	safe	1.4	safe	0.04	safe	0.02	safe	0.03	safe	0.04	out of memory	0.02	safe	0.03
ldv-regression/oomInt.c-safe_1.cil.c	safe	0.04	safe	1.4	safe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.08	safe	0.03
ldv-regression/rule57_ebda_blast.c-safe_1.cil.c	safe	0.99	unsafe	1.9	unsafe	1.9	unknown	0.05	safe	0.05	safe	0.05	safe	0.09	safe	0.12	safe	0.13
ldv-regression/rule60_list.c-safe.cil.c	safe	0.04	unsafe	1.9	unsafe	1.4	unsafe	0.04	safe	0.07	safe	0.03	safe	0.07	failure	0.07	unsafe	0.03
ldv-regression/rule60_list2.c-safe.cil.c	safe	3.3	safe	1.5	safe	1.9	unsafe	0.06	safe	0.05	safe	0.06	safe	0.05	safe	29	safe	0.89
ldv-regression/sizeofparameters_test.c-safe.cil.c	safe	0.04	safe	1.8	safe	1.4	safe	0.04	safe	0.02	safe	0.03	safe	0.04	safe	0.05	safe	0.03
ldv-regression/structure_assignment.c-safe.cil.c	safe	0.04	unsafe	1.4	unsafe	1.9	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.06	safe	0.03
ldv-regression/test_address.c-safe.cil.c	unsafe	0.05	unsafe	1.8	unsafe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	failure	0.13	safe	0.03
ldv-regression/test_cut_trace.c-safe.cil.c	safe	0.05	safe	1.4	safe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.09	safe	0.03
ldv-regression/test_malloc-1-safe.cil.c	unsafe	0.05	safe	1.8	safe	1.4	unsafe	0.04	safe	0.07	safe	0.03	safe	0.04	failure	1.8	unsafe	0.03
ldv-regression/test_malloc-2-safe.cil.c	unsafe	0.05	safe	1.8	safe	1.4	unsafe	0.04	safe	0.02	safe	0.03	safe	0.04	safe	0.14	safe	0.03
ldv-regression/test_overflow.c-safe.cil.c	safe	0.04	safe	1.8	safe	1.4	safe	0.04	safe	0.03	safe	0.04	safe	0.04	safe	0.08	safe	0.03
ldv-regression/test_union.c-safe.cil.c	safe	0.04	safe	1.4	safe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.07	safe	0.03
ldv-regression/test_union.c-safe_1.cil.c	unsafe	0.05	unsafe	1.4	unsafe	1.9	safe	0.04	safe	0.03	safe	0.03	safe	0.04	failure	0.07	failure	0.02
ldv-regression/test_union_cast-1-safe.cil.c	safe	0.04	safe	1.8	safe	1.9	parsing error	0.01	parsing error	0.02	safe	0.03	safe	0.04	parsing error	0.02	parsing error	0.02
ldv-regression/test_union_cast-2-safe.cil.c	safe	0.04	safe	1.4	safe	1.4	parsing error	0.01	parsing error	0.02	safe	0.03	safe	0.04	parsing error	0.02	parsing error	0.02
ldv-regression/test_union_cast.c-safe.cil.c	safe	0.04	unsafe	1.9	unsafe	1.9	parsing error	0.01	parsing error	0.02	safe	0.03	safe	0.04	parsing error	0.02	parsing error	0.02
ldv-regression/test_union_cast.c-safe_1.cil.c	safe	0.04	safe	1.8	safe	1.4	parsing error	0.01	parsing error	0.02	safe	0.03	safe	0.04	parsing error	0.02	parsing error	0.02
ldv-regression/volatile_alias.c-safe.cil.c	safe	0.04	safe	1.4	safe	1.8	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.18	safe	0.03
ldv-regression/volatile_alias.c-safe_1.cil.c	safe	0.03	safe	1.4	safe	1.4	safe	0.04	safe	0.03	safe	0.03	safe	0.04	safe	0.14	safe	0.03
ddv-machzwd/ddv_machzwd_all_BUG.cil.c	unsafe	4.4	unsafe	3.3	unsafe	3.2	unknown	68	safe	0.25	unknown	0.10	unknown	0.12	unsafe	33	safe	16
ddv-machzwd/ddv_machzwd_inw_BUG.cil.c	unsafe	4.4	unsafe	3.1	unsafe	3.4	unknown	31	safe	0.25	unknown	0.09	unknown	0.12	unsafe	13	safe	6.7
ddv-machzwd/ddv_machzwd_outb_BUG.cil.c	unsafe	4.3	unsafe	3.9	unsafe	3.6	unknown	52	safe	0.25	unknown	0.09	unknown	0.12	unsafe	28	safe	11
ddv-machzwd/ddv_machzwd_inb.cil.c	safe	0.61	safe	3.6	safe	3.1	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.27	safe	0.2
ddv-machzwd/ddv_machzwd_inb_p.cil.c	safe	0.61	safe	3.6	safe	3.5	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.27	safe	0.2
ddv-machzwd/ddv_machzwd_inl.cil.c	safe	0.61	safe	2.9	safe	3.0	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.28	safe	0.19
ddv-machzwd/ddv_machzwd_inl_p.cil.c	safe	0.61	safe	2.9	safe	3.1	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.28	safe	0.2
ddv-machzwd/ddv_machzwd_inw_p.cil.c	safe	0.61	safe	3.0	safe	3.0	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.27	safe	0.2
ddv-machzwd/ddv_machzwd_outb_p.cil.c	safe	0.61	safe	3.0	safe	3.5	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.27	safe	0.2
ddv-machzwd/ddv_machzwd_outl.cil.c	safe	0.61	safe	2.9	safe	3.5	safe	16	safe	0.24	unknown	220	unknown	0.15	safe	0.28	safe	0.19
ddv-machzwd/ddv_machzwd_outl_p.cil.c	safe	0.6	safe	3.5	safe	3.0	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.27	safe	0.2
ddv-machzwd/ddv_machzwd_outw_p.cil.c	safe	0.61	safe	3.6	safe	3.1	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.27	safe	0.2
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock.cil.c	safe	0.61	safe	3.0	safe	3.0	safe	16	safe	0.25	unknown	220	unknown	0.15	safe	0.27	safe	0.2