smack.results.sv-comp19.All – BenchExec results

Tool		SMACK 1.9.3								CPAchecker 1.7-svn 29852								ULTIMATE Automizer 0.1.23-635dfa2a								CPA-witness2test 1.7-svn 29852								CProver witness2test 0.1								CPAchecker 1.7-svn 29852								ULTIMATE Automizer 0.1.23-635dfa2a
Limits		timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8								timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2																																timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host		apollon*
OS		Linux 4.15.0-42-generic
System		CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33546 MB
Date of execution		2018-12-07 19:13:55 CET								2018-12-08 22:05:35 CET								2018-12-08 23:40:49 CET								2018-12-08 23:45:33 CET								2018-12-12 21:01:56 CET								2018-12-08 20:48:05 CET								2018-12-08 22:13:47 CET
Run set		smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other]								cpa-seq-validate-violation-witnesses-smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.ConcurrencySafety-Main; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other]								uautomizer-validate-violation-witnesses-smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows; sv-comp19_prop-termination.Termination-MainControlFlow; sv-comp19_prop-termination.Termination-MainHeap; sv-comp19_prop-termination.Termination-Other]								cpa-witness2test-validate-violation-witnesses-smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows]								fshell-witness2test-validate-violation-witnesses-smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows]								cpa-seq-validate-correctness-witnesses-smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety]								uautomizer-validate-correctness-witnesses-smack.[sv-comp19_prop-reachsafety.ReachSafety-Arrays; sv-comp19_prop-reachsafety.ReachSafety-BitVectors; sv-comp19_prop-reachsafety.ReachSafety-ControlFlow; sv-comp19_prop-reachsafety.ReachSafety-ECA; sv-comp19_prop-reachsafety.ReachSafety-Floats; sv-comp19_prop-reachsafety.ReachSafety-Heap; sv-comp19_prop-reachsafety.ReachSafety-Loops; sv-comp19_prop-reachsafety.ReachSafety-ProductLines; sv-comp19_prop-reachsafety.ReachSafety-Recursive; sv-comp19_prop-reachsafety.ReachSafety-Sequentialized; sv-comp19_prop-reachsafety.Systems_DeviceDriversLinux64_ReachSafety; sv-comp19_prop-memsafety.MemSafety-Arrays; sv-comp19_prop-memsafety.MemSafety-Heap; sv-comp19_prop-memsafety.MemSafety-LinkedLists; sv-comp19_prop-memsafety.MemSafety-Other; sv-comp19_prop-memsafety.MemSafety-MemCleanup; sv-comp19_prop-memsafety.Systems_BusyBox_MemSafety; sv-comp19_prop-nooverflow.NoOverflows-BitVectors; sv-comp19_prop-nooverflow.NoOverflows-Other; sv-comp19_prop-nooverflow.Systems_BusyBox_NoOverflows]
Options		-w error-witness.graphml								-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const -witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml								--full-output --validate ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml								-setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true -witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml								--graphml-witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml								-witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -witness ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml								--full-output --validate ../../results-verified/smack.2018-12-07_1913.logfiles/${rundefinition_name}.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/		status	score	cpu (s)	wall (s)	mem (MB)	energy (J)	blkio-w (MB)	blkio-r (MB)	status	score	cpu (s)	wall (s)	mem (MB)	energy	blkio-w (MB)	blkio-r (MB)	status	score	cpu (s)	wall (s)	mem (MB)	energy	blkio-w (MB)	blkio-r (MB)	status	score	cpu (s)	wall (s)	mem (MB)	energy	blkio-w (MB)	blkio-r (MB)	status	score	cpu (s)	wall (s)	mem (MB)	energy	blkio-w (MB)	blkio-r (MB)	status	score	cpu (s)	wall (s)	mem (MB)	energy	blkio-w (MB)	blkio-r (MB)	status	score	cpu (s)	wall (s)	mem (MB)	energy	blkio-w (MB)	blkio-r (MB)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i	unreach-call	disqualified	0	4.1	3.9	120	45	.62	0	true	-32	6.3	4.0	440		0	0	true	-32	7.0	4.0	310		.62	0	false(unreach-call)	1	4.4	2.5	260		0	0	false(unreach-call)	1	.69	.68	20		.061	0	-								-
array-examples/sorting_bubblesort_false-unreach-call2_ground.i	unreach-call	disqualified	0	3.6	3.4	91	43	.69	0	timeout	0	97	83	2000		0	0	true	-32	8.1	4.7	310		.62	0	false(unreach-call)	1	29	28	250		0	.0041	false(unreach-call)	1	24	24	20		.049	0	-								-
array-examples/sorting_bubblesort_false-unreach-call_ground.i	unreach-call	disqualified	0	3.6	3.4	90	44	.69	0	timeout	0	97	83	2000		0	.11	true	-32	11	6.4	320		.66	0	false(unreach-call)	1	36	34	240		0	0	false(unreach-call)	1	25	25	20		.049	0	-								-
array-examples/sorting_selectionsort_false-unreach-call2_ground.i	unreach-call	disqualified	0	880	930	500	10000	.76	2.2	error (invalid witness file)	0	.68	.42	41		0	0	error (2)	0	.021	.022	5.6		0	0	error (invalid witness file)	0	.90	.57	47		0	0	error (invalid witness file)	0	.0055	.0067	.53		0	0	-								-
array-examples/sorting_selectionsort_false-unreach-call_ground.i	unreach-call	disqualified	0	350	350	830	3800	1.8	0	timeout	0	98	86	2000		0	0	true	-32	42	27	830		.66	0	false(unreach-call)	1	3.8	2.2	250		0	0	false(unreach-call)	1	.58	.58	20		.049	0	-								-
array-examples/standard_allDiff2_false-unreach-call_ground.i	unreach-call	disqualified	0	17	17	130	220	.59	0	timeout	0	96	81	2000		0	0	out of memory	0	69	43	7000		.64	0	false(unreach-call)	1	18	15	270		0	0	false(unreach-call)	1	13	13	21		.049	0	-								-
array-examples/standard_copy1_false-unreach-call_ground.i	unreach-call	disqualified	0	3.6	3.4	91	43	.65	0	timeout	0	97	84	1900		0	0	true	-32	7.5	4.7	320		.62	0	true	-32	3.4	2.0	250		0	0	false(unreach-call)	1	.58	.58	20		.049	0	-								-
array-examples/standard_copy2_false-unreach-call_ground.i	unreach-call	disqualified	0	3.7	3.9	120	45	.70	0	timeout	0	98	86	2000		0	0	true	-32	7.9	4.4	300		.66	0	true	-32	3.6	2.1	250		0	0	false(unreach-call)	1	.57	.57	20		.049	0	-								-
array-examples/standard_copy3_false-unreach-call_ground.i	unreach-call	disqualified	0	3.7	3.9	95	48	.75	0	timeout	0	98	85	2000		0	0	true	-32	6.9	4.3	310		.66	0	true	-32	3.7	2.1	250		0	0	false(unreach-call)	1	.59	.59	20		.049	0	-								-
array-examples/standard_copy4_false-unreach-call_ground.i	unreach-call	disqualified	0	3.9	3.9	120	51	.78	0	timeout	0	97	85	2000		0	0	true	-32	8.8	5.3	310		.66	0	true	-32	3.5	2.1	250		0	0	false(unreach-call)	1	.59	.59	20		.057	0	-								-
array-examples/standard_copy5_false-unreach-call_ground.i	unreach-call	disqualified	0	3.9	4.0	110	49	.83	0	timeout	0	97	85	2000		0	0	true	-32	6.8	4.3	300		.66	0	true	-32	3.5	2.0	240		0	0	false(unreach-call)	1	.60	.60	20		.057	0	-								-
array-examples/standard_copy6_false-unreach-call_ground.i	unreach-call	disqualified	0	4.2	4.0	100	48	.87	0	timeout	0	97	86	2200		0	0	true	-32	7.2	4.5	310		.62	0	true	-32	3.5	2.1	250		0	0	false(unreach-call)	1	.59	.59	20		.057	0	-								-
array-examples/standard_copy7_false-unreach-call_ground.i	unreach-call	disqualified	0	4.1	4.0	130	48	.91	2.3	timeout	0	98	85	2100		0	0	true	-32	6.9	4.4	300		.66	0	true	-32	4.1	2.4	250		0	0	false(unreach-call)	1	.60	.60	20		.053	0	-								-
array-examples/standard_copy8_false-unreach-call_ground.i	unreach-call	disqualified	0	4.3	4.0	120	49	.95	0	timeout	0	98	84	2100		0	0	true	-32	7.5	4.2	310		.66	0	true	-32	3.8	2.2	250		0	0	false(unreach-call)	1	.61	.61	20		.057	.0041	-								-
array-examples/standard_copy9_false-unreach-call_ground.i	unreach-call	disqualified	0	4.4	4.0	120	66	.99	0	timeout	0	97	86	2100		0	0	true	-32	7.1	4.5	310		.62	0	true	-32	4.1	2.4	250		0	0	false(unreach-call)	1	.60	.59	20		.057	0	-								-
array-examples/standard_copyInitSum2_false-unreach-call_ground.i	unreach-call	disqualified	0	3.3	3.3	85	43	.65	0	timeout	0	97	88	900		0	0	true	-32	7.3	4.6	310		.66	0	false(unreach-call)	1	4.4	2.6	250		0	0	false(unreach-call)	1	.59	.59	20		.049	0	-								-
array-examples/standard_init1_false-unreach-call_ground.i	unreach-call	disqualified	0	3.1	3.3	78	39	.56	0	timeout	0	97	88	910		0	0	true	-32	9.0	5.6	320		.62	0	false(unreach-call)	1	4.1	2.3	250		0	0	false(unreach-call)	1	.57	.57	20		.045	0	-								-
array-examples/standard_init2_false-unreach-call_ground.i	unreach-call	disqualified	0	3.1	3.3	82	38	.58	0	timeout	0	97	89	940		0	0	true	-32	8.0	4.8	310		.66	0	false(unreach-call)	1	4.6	2.6	250		0	0	false(unreach-call)	1	.56	.58	20		.045	.0041	-								-
array-examples/standard_init3_false-unreach-call_ground.i	unreach-call	disqualified	0	3.2	3.3	84	38	.60	0	timeout	0	97	89	880		0	0	true	-32	7.6	4.7	320		.62	0	false(unreach-call)	1	3.5	2.1	250		0	0	false(unreach-call)	1	.57	.58	20		.045	0	-								-
array-examples/standard_init4_false-unreach-call_ground.i	unreach-call	disqualified	0	3.2	3.3	83	38	.61	0	timeout	0	97	88	920		0	0	true	-32	6.8	3.8	300		.66	0	false(unreach-call)	1	3.9	2.2	250		0	0	false(unreach-call)	1	.59	.59	20		.045	0	-								-
array-examples/standard_init5_false-unreach-call_ground.i	unreach-call	disqualified	0	3.2	3.4	82	39	.63	0	timeout	0	97	89	720		0	0	true	-32	6.9	4.0	310		.094	0	false(unreach-call)	1	3.7	2.1	250		0	0	false(unreach-call)	1	.58	.58	20		.045	0	-								-
array-examples/standard_init6_false-unreach-call_ground.i	unreach-call	disqualified	0	3.2	3.4	84	42	.67	0	timeout	0	97	88	920		0	0	true	-32	8.8	5.1	300		.66	0	false(unreach-call)	1	3.4	2.0	240		0	0	false(unreach-call)	1	.57	.59	20		.045	0	-								-
array-examples/standard_init7_false-unreach-call_ground.i	unreach-call	disqualified	0	3.3	3.4	87	41	.68	0	timeout	0	97	89	850		0	0	true	-32	7.4	4.2	310		.62	0	false(unreach-call)	1	3.9	2.3	250		0	0	false(unreach-call)	1	.58	.58	20		.045	0	-								-
array-examples/standard_init8_false-unreach-call_ground.i	unreach-call	disqualified	0	3.3	3.4	85	45	.71	0	timeout	0	97	89	920		0	0	true	-32	7.3	4.3	310		.66	0	false(unreach-call)	1	3.6	2.1	250		0	0	false(unreach-call)	1	.57	.57	20		.045	0	-								-
array-examples/standard_init9_false-unreach-call_ground.i	unreach-call	disqualified	0	3.4	3.4	110	37	.72	0	timeout	0	97	89	910		0	0	true	-32	7.4	4.1	310		.62	0	false(unreach-call)	1	3.4	2.0	240		0	0	false(unreach-call)	1	.57	.57	20		.045	0	-								-
array-examples/standard_minInArray_false-unreach-call_ground.i	unreach-call	disqualified	0	3.2	3.3	83	37	.61	0	timeout	0	97	82	2000		0	0	true	-32	8.8	4.9	320		.66	0	false(unreach-call)	1	3.9	2.3	250		0	0	false(unreach-call)	1	.58	.58	20		.049	0	-								-
array-examples/standard_partition_false-unreach-call_ground.i	unreach-call	disqualified	0	4.1	4.0	93	50	.79	0	timeout	0	96	82	2000		0	0	true	-32	9.8	5.8	300		.66	0	false(unreach-call)	1	3.9	2.3	250		0	0	false(unreach-call)	1	.59	.59	20		.057	0	-								-
array-examples/standard_running_false-unreach-call.i	unreach-call	disqualified	0	3.0	3.3	85	37	.79	0	timeout	0	97	84	2100		0	0	true	-32	9.2	5.4	310		.62	0	false(unreach-call)	1	3.6	2.1	250		0	0	true	-32	.57	.57	20		.045	0	-								-
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i	unreach-call	disqualified	0	3.4	3.4	100	51	.66	0	-								-								-								-								out of memory	0	630	550	7000		0	0	true	2	9.2	5.2	310		.66	0
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i	unreach-call	disqualified	0	880	880	210	14000	.64	0	-								-								-								-								out of memory	0	780	730	7000		0	0	timeout	0	960	930	2200		.64	0
array-examples/relax_true-unreach-call.i	unreach-call	disqualified	0	880	880	340	9800	.73	0	-								-								-								-								timeout	0	900	870	4600		0	0	timeout	0	960	890	2700		.63	0
array-examples/sanfoundry_02_true-unreach-call_ground.i	unreach-call	disqualified	0	2.7	2.8	80	30	.81	0	-								-								-								-								timeout	0	900	890	2600		0	0	timeout	0	960	830	1900		.63	0
array-examples/sanfoundry_10_true-unreach-call_ground.i	unreach-call	disqualified	0	5.7	5.8	94	73	.60	0	-								-								-								-								timeout	0	900	890	4800		0	0	timeout	0	960	930	1700		.63	0
array-examples/sanfoundry_24_true-unreach-call_true-termination.i	unreach-call	disqualified	0	880	880	350	11000	.59	0	-								-								-								-								true	2	8.3	5.0	500		0	0	true	2	9.6	5.7	310		.66	0
array-examples/sanfoundry_27_true-unreach-call_ground.i	unreach-call	disqualified	0	3.0	2.9	83	41	.61	0	-								-								-								-								timeout	0	900	890	2400		0	0	timeout	0	960	810	1700		1.6	0
array-examples/sanfoundry_43_true-unreach-call_ground.i	unreach-call	disqualified	0	2.0	2.2	73	25	.62	0	-								-								-								-								true	2	4.5	2.5	270		0	0	true	2	9.1	5.3	310		.66	0
array-examples/sorting_bubblesort_true-unreach-call_ground.i	unreach-call	disqualified	0	22	21	140	310	.69	0	-								-								-								-								timeout	0	900	890	3100		0	1.8	timeout	0	960	890	2000		.68	0
array-examples/sorting_selectionsort_true-unreach-call_ground.i	unreach-call	disqualified	0	880	930	780	9600	1.3	0	-								-								-								-								error (invalid witness file)	0	.61	.37	41		0	0	error (2)	0	.026	.027	5.6		0	0
array-examples/standard_compareModified_true-unreach-call_ground.i	unreach-call	disqualified	0	2.5	2.8	81	34	.77	0	-								-								-								-								timeout	0	900	890	4700		0	0	timeout	0	960	920	860		1.0	0
array-examples/standard_compare_true-unreach-call_ground.i	unreach-call	disqualified	0	2.7	2.8	84	36	.61	0	-								-								-								-								timeout	0	910	890	4700		0	0	timeout	0	960	890	1200		1.5	0
array-examples/standard_copy1_true-unreach-call_ground.i	unreach-call	disqualified	0	3.2	3.3	82	38	.62	0	-								-								-								-								timeout	0	900	890	4200		0	0	timeout	0	960	930	660		.63	0
array-examples/standard_copy2_true-unreach-call_ground.i	unreach-call	disqualified	0	3.3	3.4	85	39	.66	0	-								-								-								-								timeout	0	900	890	4100		0	0	timeout	0	960	930	650		.62	0
array-examples/standard_copy3_true-unreach-call_ground.i	unreach-call	disqualified	0	3.5	3.4	89	47	.72	0	-								-								-								-								timeout	0	900	890	3600		0	0	timeout	0	960	940	790		.63	0
array-examples/standard_copy4_true-unreach-call_ground.i	unreach-call	disqualified	0	3.7	3.9	93	47	.76	0	-								-								-								-								timeout	0	900	890	3600		0	0	timeout	0	960	940	810		.63	0
array-examples/standard_copy5_true-unreach-call_ground.i	unreach-call	disqualified	0	3.8	3.9	95	54	.79	.049	-								-								-								-								timeout	0	900	890	3800		0	0	timeout	0	960	940	800		.63	0
array-examples/standard_copy6_true-unreach-call_ground.i	unreach-call	disqualified	0	4.0	3.9	100	50	.84	0	-								-								-								-								timeout	0	900	890	4400		0	0	timeout	0	960	930	850		.62	0
array-examples/standard_copy7_true-unreach-call_ground.i	unreach-call	disqualified	0	4.2	4.5	100	53	.88	0	-								-								-								-								timeout	0	900	890	4100		0	0	timeout	0	960	940	850		.63	0
array-examples/standard_copy8_true-unreach-call_ground.i	unreach-call	disqualified	0	4.4	4.5	100	58	.92	0	-								-								-								-								timeout	0	900	890	3900		0	0	timeout	0	960	930	750		.63	0
array-examples/standard_copy9_true-unreach-call_ground.i	unreach-call	disqualified	0	4.6	4.5	110	58	.96	0	-								-								-								-								timeout	0	900	890	4300		0	0	timeout	0	960	930	840		.63	0
array-examples/standard_copyInitSum2_true-unreach-call_ground.i	unreach-call	disqualified	0	3.2	3.3	87	39	.65	0	-								-								-								-								timeout	0	900	890	2900		0	0	timeout	0	960	940	830		.63	0
array-examples/standard_copyInitSum3_true-unreach-call_ground.i	unreach-call	disqualified	0	3.9	3.8	92	50	.73	0	-								-								-								-								timeout	0	900	890	2500		0	0	timeout	0	960	940	740		.64	0
array-examples/standard_copyInitSum_true-unreach-call_ground.i	unreach-call	disqualified	0	3.0	2.8	83	35	.66	0	-								-								-								-								timeout	0	900	890	2700		0	0	timeout	0	960	940	800		.63	0
array-examples/standard_copyInit_true-unreach-call_ground.i	unreach-call	disqualified	0	2.8	2.8	84	33	.60	0	-								-								-								-								timeout	0	900	890	4100		0	0	timeout	0	960	930	650		.63	0
array-examples/standard_find_true-unreach-call_ground.i	unreach-call	disqualified	0	3.5	3.4	89	41	.60	0	-								-								-								-								timeout	0	910	890	4500		0	0	timeout	0	960	880	1300		1.6	0
array-examples/standard_init1_true-unreach-call_ground.i	unreach-call	disqualified	0	2.6	2.8	79	37	.56	0	-								-								-								-								timeout	0	900	890	5000		0	0	timeout	0	960	930	680		.68	0
array-examples/standard_init2_true-unreach-call_ground.i	unreach-call	disqualified	0	2.7	2.8	77	29	.58	0	-								-								-								-								timeout	0	900	890	3900		0	0	timeout	0	960	930	760		1.6	0
array-examples/standard_init3_true-unreach-call_ground.i	unreach-call	disqualified	0	2.7	2.8	80	40	.60	0	-								-								-								-								timeout	0	910	890	4700		0	0	timeout	0	960	940	660		.63	0
array-examples/standard_init4_true-unreach-call_ground.i	unreach-call	disqualified	0	2.9	2.8	84	36	.61	0	-								-								-								-								timeout	0	900	890	4600		0	0	timeout	0	960	930	660		.64	0
array-examples/standard_init5_true-unreach-call_ground.i	unreach-call	disqualified	0	2.9	2.8	85	39	.63	0	-								-								-								-								timeout	0	900	890	4700		0	0	timeout	0	960	940	800		.66	0
array-examples/standard_init6_true-unreach-call_ground.i	unreach-call	disqualified	0	3.0	2.9	88	37	.66	.049	-								-								-								-								timeout	0	900	890	5000		0	0	timeout	0	960	930	810		1.4	0
array-examples/standard_init7_true-unreach-call_ground.i	unreach-call	disqualified	0	3.0	2.8	86	42	.68	0	-								-								-								-								timeout	0	900	890	4800		0	0	timeout	0	960	930	780		.68	0
array-examples/standard_init8_true-unreach-call_ground.i	unreach-call	disqualified	0	3.1	3.4	91	38	.71	0	-								-								-								-								timeout	0	900	890	4500		0	0	timeout	0	960	930	800		.64	0
array-examples/standard_init9_true-unreach-call_ground.i	unreach-call	disqualified	0	3.2	3.4	91	38	.72	0	-								-								-								-								timeout	0	900	880	5200		0	0	timeout	0	960	930	790		.63	0
array-examples/standard_maxInArray_true-unreach-call_ground.i	unreach-call	disqualified	0	3.0	2.8	83	36	.61	0	-								-								-								-								timeout	0	900	890	2400		0	0	timeout	0	960	810	1800		.65	0
array-examples/standard_minInArray_true-unreach-call_ground.i	unreach-call	disqualified	0	3.0	2.9	83	37	.61	0	-								-								-								-								timeout	0	900	890	3900		0	0	timeout	0	960	810	1900		.63	0
array-examples/standard_palindrome_true-unreach-call_ground.i	unreach-call	disqualified	0	2.5	2.8	77	28	.56	0	-								-								-								-								timeout	0	910	900	6300		0	0	timeout	0	960	940	800		.65	0
array-examples/standard_partial_init_true-unreach-call_ground.i	unreach-call	disqualified	0	140	140	110	1900	.66	0	-								-								-								-								timeout	0	900	890	2600		0	0	timeout	0	960	930	810		.63	0
array-examples/standard_partition_original_true-unreach-call_ground.i	unreach-call	disqualified	0	68	68	100	910	.70	0	-								-								-								-								timeout	0	900	890	3700		0	0	timeout	0	960	920	870		.63	0
array-examples/standard_partition_true-unreach-call_ground.i	unreach-call	disqualified	0	24	24	93	340	.73	0	-								-								-								-								timeout	0	910	890	5700		0	0	timeout	0	960	920	1700		.70	0
array-examples/standard_password_true-unreach-call_ground.i	unreach-call	disqualified	0	2.7	2.8	85	32	.62	0	-								-								-								-								timeout	0	900	880	4500		0	0	timeout	0	960	900	1200		.66	0
array-examples/standard_reverse_true-unreach-call_ground.i	unreach-call	disqualified	0	2.7	2.8	82	36	.59	.34	-								-								-								-								timeout	0	910	890	5500		0	0	timeout	0	960	900	860		1.1	0
array-examples/standard_running_true-unreach-call.i	unreach-call	disqualified	0	2.7	2.8	80	34	.79	0	-								-								-								-								timeout	0	900	890	3000		0	0	timeout	0	960	940	1300		1.6	0
array-examples/standard_sentinel_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.7	2.9	75	28	.56	0	-								-								-								-								timeout	0	900	890	1500		0	0	true	2	15	9.1	470		.66	0
array-examples/standard_seq_init_true-unreach-call_ground.i	unreach-call	disqualified	0	2.8	2.8	82	36	.59	0	-								-								-								-								timeout	0	900	890	2100		0	0	timeout	0	960	920	640		.63	0
array-examples/standard_strcmp_true-unreach-call_ground.i	unreach-call	disqualified	0	2.7	2.8	82	37	.61	0	-								-								-								-								timeout	0	900	880	4600		0	0	timeout	0	960	890	1100		.63	0
array-examples/standard_strcpy_original_true-unreach-call.i	unreach-call	disqualified	0	7.6	7.4	100	100	.60	0	-								-								-								-								timeout	0	900	890	3700		0	0	timeout	0	960	900	700		1.5	0
array-examples/standard_strcpy_true-unreach-call_ground.i	unreach-call	disqualified	0	5.7	5.8	98	76	.60	0	-								-								-								-								timeout	0	900	890	4800		0	0	timeout	0	960	920	860		.62	0
array-examples/standard_two_index_01_true-unreach-call.i	unreach-call	disqualified	0	880	930	870	9100	.57	0	-								-								-								-								error (invalid witness file)	0	.61	.37	42		0	0	error (2)	0	.023	.024	5.6		0	0
array-examples/standard_two_index_02_true-unreach-call.i	unreach-call	disqualified	0	2.7	2.9	81	34	.60	0	-								-								-								-								timeout	0	900	890	4300		0	.025	timeout	0	960	930	640		.64	0
array-examples/standard_two_index_03_true-unreach-call.i	unreach-call	disqualified	0	900	890	4400	13000	26	0	-								-								-								-								error (invalid witness file)	0	.76	.46	42		0	0	error (2)	0	.026	.027	5.6		0	0
array-examples/standard_two_index_04_true-unreach-call.i	unreach-call	disqualified	0	2.6	2.9	82	37	.60	0	-								-								-								-								timeout	0	900	890	4700		0	0	timeout	0	960	920	810		.66	0
array-examples/standard_two_index_05_true-unreach-call.i	unreach-call	disqualified	0	2.5	2.8	81	37	.59	0	-								-								-								-								timeout	0	900	890	4600		0	0	timeout	0	960	920	840		.63	0
array-examples/standard_two_index_06_true-unreach-call.i	unreach-call	disqualified	0	890	930	1100	11000	13	0	-								-								-								-								error (invalid witness file)	0	.77	.46	41		0	0	error (2)	0	.026	.027	5.7		0	0
array-examples/standard_two_index_07_true-unreach-call.i	unreach-call	disqualified	0	2.5	2.8	81	39	.59	0	-								-								-								-								timeout	0	900	890	4700		0	0	timeout	0	960	920	830		.63	0
array-examples/standard_two_index_08_true-unreach-call.i	unreach-call	disqualified	0	2.5	2.8	81	32	.59	0	-								-								-								-								timeout	0	900	890	4700		0	0	timeout	0	960	910	910		.63	0
array-examples/standard_two_index_09_true-unreach-call.i	unreach-call	disqualified	0	2.4	2.8	74	29	.59	0	-								-								-								-								timeout	0	910	890	5000		0	0	timeout	0	960	920	860		.66	0
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i	unreach-call	disqualified	0	880	880	380	11000	.57	0	-								-								-								-								out of memory	0	750	730	7000		0	0	timeout	0	960	920	1100		.64	0
array-examples/standard_vector_difference_true-unreach-call_ground.i	unreach-call	disqualified	0	2.9	2.8	86	39	.61	0	-								-								-								-								timeout	0	910	900	4000		0	0	timeout	0	960	930	620		.64	0
array-examples/standard_sentinel_true-unreach-call.i.v+cfa-reducer.c	unreach-call	disqualified	0	2.7	2.8	75	33	.56	0	-								-								-								-								timeout	0	900	890	1600		0	0	true	2	20	13	570		.66	0
array-industry-pattern/array_assert_loop_dep_false-unreach-call_true-termination.i	unreach-call	disqualified	0	3.1	3.3	82	38	.57	0	timeout	0	98	89	940		0	0	true	-32	9.0	5.6	320		.62	0	false(unreach-call)	1	3.6	2.1	250		0	0	false(unreach-call)	1	.58	.58	20		.049	0	-								-
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i	unreach-call	disqualified	0	3.2	3.3	82	38	.56	0	timeout	0	97	87	1800		0	0	true	-32	14	7.5	610		.62	0	false(unreach-call)	1	3.6	2.1	250		0	0	false(unreach-call)	1	.58	.58	20		.049	0	-								-
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call_true-termination.i	unreach-call	disqualified	0	4.4	4.4	110	53	.79	0	timeout	0	96	81	2200		0	0	true	-32	12	7.3	460		.62	0	false(unreach-call)	1	3.8	2.2	240		0	0	false(unreach-call)	1	.58	.58	20		.057	0	-								-
array-industry-pattern/array_range_init_false-unreach-call.i	unreach-call	disqualified	0	3.1	3.3	85	38	.61	0	timeout	0	97	86	1800		0	0	true	-32	12	6.5	580		.62	0	false(unreach-call)	1	4.1	2.4	250		0	.082	false(unreach-call)	1	.59	.59	20		.049	0	-								-
array-industry-pattern/array_single_elem_init_false-unreach-call_true-termination.i	unreach-call	disqualified	0	4.5	4.4	120	58	.79	0	timeout	0	97	83	2200		0	0	true	-32	12	7.2	460		.66	0	true	-32	3.8	2.2	250		0	1.5	true	-32	.61	.61	20		.057	.0041	-								-
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i	unreach-call	disqualified	0	5.9	5.9	110	76	.63	0	true	-32	4.0	2.2	260		0	0	true	-32	7.2	4.5	300		.66	0	false(unreach-call)	1	4.2	2.4	250		0	0	error (2)	0	.60	.59	20		.066	0	-								-
array-industry-pattern/array_monotonic_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.7	2.9	84	40	.61	0	-								-								-								-								timeout	0	900	890	3500		0	0	timeout	0	960	930	660		1.5	0
array-industry-pattern/array_mul_init_true-unreach-call_true-termination.i	unreach-call	disqualified	0	880	930	260	12000	.73	0	-								-								-								-								error (invalid witness file)	0	.75	.46	41		0	0	error (2)	0	.023	.025	5.6		0	0
array-industry-pattern/array_of_struct_break_true-unreach-call.i	unreach-call	disqualified	0	2.7	2.8	84	30	.60	.053	-								-								-								-								timeout	0	900	900	3900		0	0	timeout	0	960	920	2000		.65	1.6
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i	unreach-call	disqualified	0	8.6	8.4	100	120	.59	0	-								-								-								-								timeout	0	900	900	3900		0	0	timeout	0	960	940	1400		.62	0
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i	unreach-call	disqualified	0	3.0	2.9	83	35	.63	0	-								-								-								-								timeout	0	900	880	4200		0	0	true	2	14	8.5	510		.66	0
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i	unreach-call	disqualified	0	2.9	2.8	80	37	.63	0	-								-								-								-								timeout	0	900	900	4000		0	0	timeout	0	960	940	1100		.70	0
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i	unreach-call	disqualified	0	880	930	440	9300	.65	0	-								-								-								-								error (invalid witness file)	0	.82	.50	40		0	0	error (2)	0	.023	.024	5.6		0	0
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i	unreach-call	disqualified	0	5.9	5.9	97	84	.69	0	-								-								-								-								out of memory	0	680	680	7000		0	0	timeout	0	960	930	1500		1.0	0
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i	unreach-call	disqualified	0	2.7	2.8	84	34	.58	0	-								-								-								-								timeout	0	900	900	3800		0	0	timeout	0	960	940	1400		.62	0
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i	unreach-call	disqualified	0	19	19	120	250	.80	0	-								-								-								-								timeout	0	900	900	3900		0	0	timeout	0	960	930	1500		.63	0
array-industry-pattern/array_shadowinit_true-unreach-call_true-termination.i	unreach-call	disqualified	0	880	880	380	12000	.57	0	-								-								-								-								timeout	0	910	890	5600		0	0	timeout	0	960	840	960		.68	0
reducercommutativity/rangesum05_false-unreach-call_true-termination.i	unreach-call	disqualified	0	2.8	2.7	84	36	.66	0	false(unreach-call)	1	7.8	5.4	350		0	.0041	true	-32	8.4	4.8	320		.62	0	unknown	0	4.5	2.6	250		0	.0041	false(unreach-call)	1	.61	.61	20		.061	.0041	-								-
reducercommutativity/rangesum10_false-unreach-call_true-termination.i	unreach-call	disqualified	0	3.0	3.2	84	37	.73	0	false(unreach-call)	1	10	7.4	370		0	0	true	-32	7.4	4.3	320		.62	0	unknown	0	4.4	2.6	250		0	0	false(unreach-call)	1	.63	.63	20		.061	0	-								-
reducercommutativity/rangesum20_false-unreach-call.i	unreach-call	disqualified	0	3.7	3.9	120	50	.87	0	false(unreach-call)	1	21	18	450		0	0	true	-32	7.3	4.6	310		.62	.0041	unknown	0	4.1	2.4	250		0	0	false(unreach-call)	1	.60	.60	20		.061	0	-								-
reducercommutativity/rangesum40_false-unreach-call.i	unreach-call	disqualified	0	5.0	5.0	140	72	1.2	.0041	timeout	0	93	90	750		0	0	true	-32	7.8	4.8	320		.66	0	unknown	0	3.6	2.1	250		0	0	false(unreach-call)	1	.63	.62	20		.061	0	-								-
reducercommutativity/rangesum60_false-unreach-call.i	unreach-call	disqualified	0	7.4	7.3	220	110	1.5	0	timeout	0	93	89	800		0	0	true	-32	9.1	5.1	320		.66	0	unknown	0	3.7	2.1	260		0	.54	false(unreach-call)	1	.62	.62	20		.061	0	-								-
reducercommutativity/rangesum_false-unreach-call_true-termination.i	unreach-call	disqualified	0	3.7	3.9	88	48	.63	0	true	-32	4.0	2.2	250		0	0	false(unreach-call)	1	15	8.7	490		.62	0	unknown	0	4.4	2.5	250		0	0	false(unreach-call)	1	.61	.61	20		.061	0	-								-
reducercommutativity/avg05_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.1	2.2	72	26	.62	0	-								-								-								-								timeout	0	900	900	2000		0	.14	timeout	0	960	940	780		.63	.0041
reducercommutativity/avg10_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.1	2.2	76	29	.68	0	-								-								-								-								timeout	0	900	890	3200		0	0	timeout	0	960	930	1700		.63	0
reducercommutativity/avg20_true-unreach-call.i	unreach-call	disqualified	0	2.4	2.3	90	34	.78	0	-								-								-								-								timeout	0	900	890	3000		0	0	timeout	0	960	910	4900		.67	0
reducercommutativity/avg40_true-unreach-call.i	unreach-call	disqualified	0	3.3	3.4	140	43	1.0	0	-								-								-								-								timeout	0	900	890	4000		0	0	timeout	0	960	920	970		.65	0
reducercommutativity/avg60_true-unreach-call.i	unreach-call	disqualified	0	5.0	5.1	220	70	1.2	0	-								-								-								-								timeout	0	900	890	4000		0	0	timeout	0	960	920	970		.63	0
reducercommutativity/avg_true-unreach-call_true-termination.i	unreach-call	disqualified	0	880	930	180	11000	.62	0	-								-								-								-								error (invalid witness file)	0	.75	.46	40		0	0	error (2)	0	.027	.029	5.6		0	0
reducercommutativity/max05_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.1	2.2	73	30	.65	0	-								-								-								-								true	2	540	530	1200		0	0	timeout	0	960	910	2300		.72	.016
reducercommutativity/max10_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.4	2.8	81	38	.74	0	-								-								-								-								timeout	0	900	890	1700		0	0	timeout	0	960	840	5900		.63	0
reducercommutativity/max20_true-unreach-call.i	unreach-call	disqualified	0	3.5	3.8	110	39	.89	0	-								-								-								-								timeout	0	900	890	1800		0	0	timeout	0	960	920	2700		.68	0
reducercommutativity/max40_true-unreach-call.i	unreach-call	disqualified	0	12	12	200	100	1.2	0	-								-								-								-								timeout	0	900	890	1200		0	0	timeout	0	960	920	1700		.68	0
reducercommutativity/max60_true-unreach-call.i	unreach-call	disqualified	0	38	38	340	270	1.5	0	-								-								-								-								timeout	0	900	890	1400		0	0	timeout	0	960	910	900		.63	0
reducercommutativity/max_true-unreach-call_true-termination.i	unreach-call	disqualified	0	880	880	380	11000	.61	0	-								-								-								-								timeout	0	900	890	2500		0	0	timeout	0	960	940	4600		.63	0
reducercommutativity/sep05_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.1	2.2	72	25	.65	0	-								-								-								-								true	2	400	390	1200		0	0	timeout	0	960	900	3700		.63	0
reducercommutativity/sep10_true-unreach-call.i	unreach-call	disqualified	0	3.0	3.3	81	39	.71	0	-								-								-								-								timeout	0	900	890	1100		0	0	timeout	0	960	810	6800		1.4	0
reducercommutativity/sep20_true-unreach-call.i	unreach-call	disqualified	0	880	930	110	12000	.86	0	-								-								-								-								error (invalid witness file)	0	.65	.41	40		0	0	error (2)	0	.034	.035	5.7		0	0
reducercommutativity/sep40_true-unreach-call.i	unreach-call	disqualified	0	880	930	170	12000	1.2	0	-								-								-								-								error (invalid witness file)	0	.77	.48	41		0	0	error (2)	0	.021	.022	5.6		0	0
reducercommutativity/sep60_true-unreach-call.i	unreach-call	disqualified	0	880	930	270	13000	1.4	0	-								-								-								-								error (invalid witness file)	0	.67	.40	42		0	0	error (2)	0	.025	.026	5.6		0	0
reducercommutativity/sep_true-unreach-call_true-termination.i	unreach-call	disqualified	0	880	880	180	11000	.61	0	-								-								-								-								timeout	0	900	890	2500		0	0	timeout	0	960	890	2100		.64	0
reducercommutativity/sum05_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.1	2.2	73	23	.62	0	-								-								-								-								timeout	0	900	900	1300		0	0	timeout	0	960	940	4600		.65	0
reducercommutativity/sum10_true-unreach-call_true-termination.i	unreach-call	disqualified	0	2.1	2.2	76	26	.68	0	-								-								-								-								timeout	0	900	890	3100		0	0	timeout	0	960	920	970		.67	0
reducercommutativity/sum20_true-unreach-call.i	unreach-call	disqualified	0	2.3	2.3	90	33	.78	2.3	-								-								-								-								timeout	0	900	890	2900		0	0	timeout	0	960	910	4900		1.1	0
reducercommutativity/sum40_true-unreach-call.i	unreach-call	disqualified	0	2.8	2.9	140	35	1.0	0	-								-								-								-								timeout	0	900	890	4400		0	0	timeout	0	960	920	930		.65	0
reducercommutativity/sum60_true-unreach-call.i	unreach-call	disqualified	0	4.8	5.0	220	61	1.2	1.9	-								-								-								-								timeout	0	900	890	4400		0	0	timeout	0	960	920	940		.63	0
reducercommutativity/sum_true-unreach-call_true-termination.i	unreach-call	disqualified	0	880	880	380	10000	.61	0	-								-								-								-								timeout	0	900	890	2700		0	0	timeout	0	960	940	860		.63	0
array-tiling/mlceu_false-unreach-call.i	unreach-call	disqualified	0	880	930	270	7800	.59	2.2	error (invalid witness file)	0	.58	.36	42		0	0	error (2)	0	.022	.023	5.6		0	0	error (invalid witness file)	0	1.2	.76	47		0	0	error (invalid witness file)	0	.0052	.0063	.41		0	0	-								-
array-tiling/skippedu_false-unreach-call.i	unreach-call	disqualified	0	3.2	3.4	82	37	.61	0	true	-32	4.4	2.4	250		0	0	false(unreach-call)	1	11	6.7	380		.62	0	unknown	0	3.6	2.1	250		0	0	true	-32	.58	.58	20		.053	0	-								-
array-tiling/mbpr2_true-unreach-call.i	unreach-call	disqualified	0	880	880	390	11000	.64	0	-								-								-								-								timeout	0	900	880	4200		0	0	timeout	0	960	920	900		.65	0
array-tiling/mbpr3_true-unreach-call.i	unreach-call	disqualified	0	880	880	410	8100	.68	0	-								-								-								-								timeout	0	900	860	4900		0	0	timeout	0	960	920	880		.65	0
array-tiling/mbpr4_true-unreach-call.i	unreach-call	disqualified	0	880	930	500	9000	.74	0	-								-								-								-								error (invalid witness file)	0	1.0	.61	41		0	0	error (2)	0	.021	.022	5.6		0	0
array-tiling/mbpr5_true-unreach-call.i	unreach-call	disqualified	0	880	930	510	9200	.82	0	-								-								-								-								error (invalid witness file)	0	.59	.36	42		0	0	error (2)	0	.021	.021	5.6		0	0
array-tiling/nr2_true-unreach-call.i	unreach-call	disqualified	0	880	880	330	14000	.61	0	-								-								-								-								timeout	0	900	880	5300		0	0	timeout	0	960	940	1100		.64	0
array-tiling/nr3_true-unreach-call.i	unreach-call	disqualified	0	880	880	360	10000	.62	0	-								-								-								-								timeout	0	900	880	4600		0	.053	timeout	0	960	930	910		.65	0
array-tiling/nr4_true-unreach-call.i	unreach-call	disqualified	0	880	880	380	12000	.63	0	-								-								-								-								timeout	0	900	880	4400		0	0	timeout	0	960	920	2300		.70	0
array-tiling/nr5_true-unreach-call.i	unreach-call	disqualified	0	880	880	410	9300	.64	0	-								-								-								-								timeout	0	900	880	4400		0	0	timeout	0	960	920	2100		.71	0
array-tiling/pnr2_true-unreach-call.i	unreach-call	disqualified	0	880	880	210	11000	.62	0	-								-								-								-								timeout	0	900	890	1200		0	.0041	timeout	0	960	930	950		.63	0
array-tiling/pnr3_true-unreach-call.i	unreach-call	disqualified	0	880	880	220	11000	.62	0	-								-								-								-								timeout	0	900	900	870		0	0	timeout	0	960	930	950		.63	.10
array-tiling/pnr4_true-unreach-call.i	unreach-call	disqualified	0	880	880	260	10000	.63	0	-								-								-								-								timeout	0	900	900	570		0	0	timeout	0	960	920	950		.63	0
array-tiling/pnr5_true-unreach-call.i	unreach-call	disqualified	0	880	880	250	11000	.65	0	-								-								-								-								timeout	0	900	900	630		0	0	timeout	0	960	910	2400		.69	.14
array-tiling/poly1_true-unreach-call.i	unreach-call	disqualified	0	880	880	180	11000	.57	0	-								-								-								-								timeout	0	910	890	5200		0	0	timeout	0	960	940	820		.63	.0041
array-tiling/poly2_true-unreach-call.i	unreach-call	disqualified	0	880	880	700	12000	.65	0	-								-								-								-								timeout	0	900	890	4900		0	0	timeout	0	960	950	550		.63	0
array-tiling/pr2_true-unreach-call.i	unreach-call	disqualified	0	880	880	380	11000	.61	0	-								-								-								-								timeout	0	900	890	2200		0	0	timeout	0	960	910	1000		.71	0
array-tiling/pr3_true-unreach-call.i	unreach-call	disqualified	0	880	880	370	10000	.62	0	-								-								-								-								timeout	0	900	890	1900		0	0	timeout	0	960	930	1300		.64	0
array-tiling/pr4_true-unreach-call.i	unreach-call	disqualified	0	880	880	390	11000	.63	0	-								-								-								-								timeout	0	900	890	2000		0	0	timeout	0	960	930	1000		.63	0
array-tiling/pr5_true-unreach-call.i	unreach-call	disqualified	0	880	880	400	10000	.65	0	-								-								-								-								timeout	0	900	890	2000		0	0	timeout	0	960	900	1000		.63	0
array-tiling/revcpyswp2_true-unreach-call.i	unreach-call	disqualified	0	880	880	290	14000	.63	0	-								-								-								-								timeout	0	900	890	2000		0	0	timeout	0	960	930	750		.69	0
array-tiling/rew_true-unreach-call.i	unreach-call	disqualified	0	880	880	390	11000	.58	0	-								-								-								-								timeout	0	900	890	2500		0	0	timeout	0	960	940	1300		.68	0
array-tiling/rewnif_true-unreach-call.i	unreach-call	disqualified	0	880	880	400	12000	.58	0	-								-								-								-								timeout	0	900	890	2400		0	0	timeout	0	960	930	1100		.63	0
array-tiling/rewnifrev2_true-unreach-call.i	unreach-call	disqualified	0	880	880	310	10000	.57	0	-								-								-								-								timeout	0	900	890	2000		0	.10	timeout	0	960	910	2300		.70	0
array-tiling/rewnifrev_true-unreach-call.i	unreach-call	disqualified	0	880	880	320	11000	.58	0	-								-								-								-								timeout	0	900	890	2300		0	.70	timeout	0	960	780	1100		1.1	0
array-tiling/rewrev_true-unreach-call.i	unreach-call	disqualified	0	880	880	280	12000	.58	0	-								-								-								-								timeout	0	900	890	2100		0	0	timeout	0	960	890	1200		.66	1.6
array-tiling/skipped_true-unreach-call.i	unreach-call	disqualified	0	880	880	230	13000	.62	2.2	-								-								-								-								timeout	0	900	890	1100		0	0	timeout	0	960	890	3900		1.7	0
array-tiling/tcpy_true-unreach-call.i	unreach-call	disqualified	0	880	880	240	14000	.60	.049	-								-								-								-								timeout	0	900	900	1200		0	0	timeout	0	960	920	1300		1.5	0
array-programs/copysome1_false-unreach-call.i	unreach-call	disqualified	0	880	930	820	13000	.58	0	error (invalid witness file)	0	.66	.40	41		0	0	error (2)	0	.022	.024	5.7		0	0	error (invalid witness file)	0	1.1	.71	47		0	0	error (invalid witness file)	0	.0050	.0061	.40		0	0	-								-
array-programs/copysome2_false-unreach-call.i	unreach-call	disqualified	0	890	930	860	13000	.60	3.3	error (invalid witness file)	0	.57	.36	40		0	0	error (2)	0	.030	.031	5.7		0	0	error (invalid witness file)	0	.91	.60	47		0	0	error (invalid witness file)	0	.0054	.0068	.41		0	0	-								-
array-programs/copysome1_true-unreach-call.i	unreach-call	disqualified	0	880	930	790	11000	.58	0	-								-								-								-								error (invalid witness file)	0	.83	.52	41		0	0	error (2)	0	.026	.027	5.6		0	0
array-programs/copysome2_true-unreach-call.i	unreach-call	disqualified	0	890	930	820	11000	.60	0	-								-								-								-								error (invalid witness file)	0	.74	.46	40		0	0	error (2)	0	.023	.023	5.6		0	0
array-crafted/bAnd1_true-unreach-call.i	unreach-call	disqualified	0	880	930	1700	7400	1.7	0	-								-								-								-								error (invalid witness file)	0	.59	.36	40		0	0	error (2)	0	.026	.027	5.7		0	0
array-crafted/bAnd2_true-unreach-call.i	unreach-call	disqualified	0	66	65	15000	590	19	0	-								-								-								-								error (invalid witness file)	0	.61	.37	41		0	0	error (2)	0	.023	.024	5.6		0	0
array-crafted/bAnd3_true-unreach-call.i	unreach-call	disqualified	0	880	930	490	13000	.61	0	-								-								-								-								error (invalid witness file)	0	.76	.46	40		0	0	error (2)	0	.027	.028	5.6		0	0
array-crafted/bAnd4_true-unreach-call.i	unreach-call	disqualified	0	3.9	4.2	100	48	.68	0	-								-								-								-								timeout	0	900	890	4300		0	0	timeout	0	960	920	770		.66	0
array-crafted/bAnd5_true-unreach-call.i	unreach-call	disqualified	0	880	880	400	8700	.66	0	-								-								-								-								timeout	0	900	890	3800		0	0	timeout	0	960	940	920		.72	0
array-crafted/bor1_true-unreach-call.i	unreach-call	disqualified	0	880	930	1000	8900	1.7	0	-								-								-								-								error (invalid witness file)	0	.76	.46	41		0	0	error (2)	0	.023	.023	5.6		0	0
array-crafted/bor2_true-unreach-call.i	unreach-call	disqualified	0	65	64	15000	610	19	0	-								-								-								-								error (invalid witness file)	0	.58	.36	40		0	0	error (2)	0	.026	.027	5.6		0	0
array-crafted/bor3_true-unreach-call.i	unreach-call	disqualified	0	880	930	340	9500	.60	0	-								-								-								-								error (invalid witness file)	0	.60	.36	40		0	0	error (2)	0	.021	.022	5.6		0	0
array-crafted/bor4_true-unreach-call.i	unreach-call	disqualified	0	62	63	120	870	.68	0	-								-								-								-								timeout	0	900	890	4200		0	0	timeout	0	960	920	880		1.7	0
array-crafted/bor5_true-unreach-call.i	unreach-call	disqualified	0	880	880	330	8500	.61	0	-								-								-								-								timeout	0	900	890	3600		0	0	timeout	0	960	930	810		.76	17
array-crafted/mapavg1_true-unreach-call.i	unreach-call	disqualified	0	13	13	460	150	1.7	0	-								-								-								-								timeout	0	900	890	3900		0	0	timeout	0	960	920	920		.64	0
array-crafted/mapavg2_true-unreach-call.i	unreach-call	disqualified	0	890	930	8400	2700	21	0	-								-								-								-								error (invalid witness file)	0	.75	.45	40		0	0	error (2)	0	.026	.027	5.7		0	0
array-crafted/mapavg3_true-unreach-call.i	unreach-call	disqualified	0	890	930	690	9700	.60	0	-								-								-								-								error (invalid witness file)	0	.59	.35	41		0	0	error (2)	0	.020	.021	5.6		0	0
array-crafted/mapavg4_true-unreach-call.i	unreach-call	disqualified	0	2.2	2.2	80	26	.68	0	-								-								-								-								timeout	0	900	890	3200		0	0	timeout	0	960	920	910		.63	0
array-crafted/mapavg5_true-unreach-call.i	unreach-call	disqualified	0	880	880	430	12000	.61	0	-								-								-								-								exception	0	7.5	4.7	470		0	0	timeout	0	960	950	600		1.5	0
array-crafted/mapsum1_true-unreach-call.i	unreach-call	disqualified	0	17	17	470	180	1.7	0	-								-								-								-								timeout	0	900	890	4200		0	0	timeout	0	960	910	920		.66	0
array-crafted/mapsum2_true-unreach-call.i	unreach-call	disqualified	0	880	930	8400	3200	24	0	-								-								-								-								error (invalid witness file)	0	.76	.47	40		0	0	error (2)	0	.026	.027	5.6		0	0
array-crafted/mapsum3_true-unreach-call.i	unreach-call	disqualified	0	890	930	700	12000	.61	0	-								-								-								-								error (invalid witness file)	0	.84	.53	43		0	0	error (2)	0	.022	.022	5.6		0	0
array-crafted/mapsum4_true-unreach-call.i	unreach-call	disqualified	0	2.2	2.3	77	25	.68	0	-								-								-								-								timeout	0	900	890	5000		0	0	timeout	0	960	920	930		.63	0
array-crafted/mapsum5_true-unreach-call.i	unreach-call	disqualified	0	880	880	430	14000	.66	0	-								-								-								-								timeout	0	900	890	2000		0	0	timeout	0	960	950	4700		.64	0
array-crafted/xor1_true-unreach-call.i	unreach-call	disqualified	0	880	930	1000	7300	1.7	0	-								-								-								-								error (invalid witness file)	0	.74	.44	40		0	0	error (2)	0	.026	.027	5.5		0	0
array-crafted/xor2_true-unreach-call.i	unreach-call	disqualified	0	62	61	15000	680	15	2.1	-								-								-								-								error (invalid witness file)	0	.77	.47	42		0	0	error (2)	0	.027	.028	5.6		0	0
array-crafted/xor3_true-unreach-call.i	unreach-call	disqualified	0	880	930	370	10000	.61	0	-								-								-								-								error (invalid witness file)	0	.66	.39	40		0	0	error (2)	0	.025	.026	5.6		0	0
array-crafted/xor4_true-unreach-call.i	unreach-call	disqualified	0	7.1	7.2	100	91	.68	0	-								-								-								-								timeout	0	900	890	4900		0	0	timeout	0	960	910	770		1.7	0
array-crafted/xor5_true-unreach-call.i	unreach-call	disqualified	0	880	880	330	8300	.61	0	-								-								-								-								timeout	0	900	880	3700		0	0	timeout	0	960	930	780		.71	0
array-crafted/zero_sum1_true-unreach-call.c	unreach-call	disqualified	0	880	880	360	11000	.64	0	-								-								-								-								timeout	0	900	900	650		0	0	timeout	0	960	860	1600		1.5	0
array-crafted/zero_sum2_true-unreach-call.c	unreach-call	disqualified	0	880	880	480	11000	.68	0	-								-								-								-								timeout	0	900	890	1400		0	0	timeout	0	960	860	1600		.63	0
array-crafted/zero_sum3_true-unreach-call.c	unreach-call	disqualified	0	880	880	420	12000	.66	0	-								-								-								-								timeout	0	900	880	2900		0	0	timeout	0	960	860	1900		.63	0
array-crafted/zero_sum4_true-unreach-call.c	unreach-call	disqualified	0	880	880	480	10000	.74	0	-								-								-								-								timeout	0	900	850	5600		0	0	timeout	0	960	850	2100		.63	1.6
array-crafted/zero_sum5_true-unreach-call.c	unreach-call	disqualified	0	880	880	520	11000	.78	0	-								-								-								-								timeout	0	930	690	6900		0	0	timeout	0	960	860	2500		.64	0
array-crafted/zero_sum_const1_true-unreach-call.c	unreach-call	disqualified	0	880	880	470	11000	.64	0	-								-								-								-								timeout	0	900	880	4600		0	0	timeout	0	960	890	2000		1.5	0
array-crafted/zero_sum_const2_true-unreach-call.c	unreach-call	disqualified	0	880	880	480	10000	.67	0	-								-								-								-								timeout	0	900	870	4500		0	0	out of memory	0	620	500	7000		.63	.0041
array-crafted/zero_sum_const3_true-unreach-call.c	unreach-call	disqualified	0	880	880	610	12000	.71	0	-								-								-								-								out of memory	0	840	760	7000		0	0	out of memory	0	360	270	7000		.63	0
array-crafted/zero_sum_const4_true-unreach-call.c	unreach-call	disqualified	0	880	880	730	12000	.73	0	-								-								-								-								timeout	0	910	630	6200		0	.14	timeout	0	960	860	1600		.63	0
array-crafted/zero_sum_const5_true-unreach-call.c	unreach-call	disqualified	0	880	880	750	12000	.77	0	-								-								-								-								timeout	0	900	620	5900		0	0	timeout	0	960	850	2500		.62	0
array-crafted/zero_sum_const_m2_true-unreach-call.c	unreach-call	disqualified	0	880	880	510	11000	.68	0	-								-								-								-								timeout	0	900	860	6000		0	0	timeout	0	960	900	2600		.63	0
array-crafted/zero_sum_const_m3_true-unreach-call.c	unreach-call	disqualified	0	880	880	610	12000	.72	0	-								-								-								-								out of memory	0	850	770	7000		0	0	timeout	0	960	870	2200		1.3	0
array-crafted/zero_sum_const_m4_true-unreach-call.c	unreach-call	disqualified	0	880	880	750	10000	.74	0	-								-								-								-								timeout	0	900	620	6200		0	0	timeout	0	960	890	2200		.73	0
array-crafted/zero_sum_const_m5_true-unreach-call.c	unreach-call	disqualified	0	880	880	760	9400	.77	0	-								-								-								-								timeout	0	910	630	6000		0	0	timeout	0	960	890	1200		.63	0
array-crafted/zero_sum_m2_true-unreach-call.c	unreach-call	disqualified	0	880	880	440	9800	.68	0	-								-								-								-								timeout	0	900	890	740		0	0	timeout	0	960	880	1300		.65	0
array-crafted/zero_sum_m3_true-unreach-call.c	unreach-call	disqualified	0	880	880	440	12000	.66	0	-								-								-								-								timeout	0	900	890	2100		0	0	timeout	0	960	880	1200		.65	0
array-crafted/zero_sum_m4_true-unreach-call.c	unreach-call	disqualified	0	880	880	480	10000	.68	0	-								-								-								-								timeout	0	900	840	5100		0	0	timeout	0	960	880	1500		.64	0
array-crafted/zero_sum_m5_true-unreach-call.c	unreach-call	disqualified	0	880	880	490	11000	.77	0	-								-								-								-								timeout	0	900	830	5700		0	0	timeout	0	960	890	1300		.65	0
array-multidimensional/add-2-n-u_true-unreach-call.i	unreach-call	disqualified	0	270	260	13000	3800	62	0	-								-								-								-								error (invalid witness file)	0	.77	.48	40		0	0	error (2)	0	.026	.026	5.6		0	0
array-multidimensional/add-3-n-u_true-unreach-call.i	unreach-call	disqualified	0	670	660	14000	7200	92	0	-								-								-								-								error (invalid witness file)	0	.68	.41	41		0	0	error (2)	0	.020	.021	5.6		0	0
array-multidimensional/copy-2-u_true-unreach-call.i	unreach-call	disqualified	0	900	930	8700	13000	21	0	-								-								-								-								error (invalid witness file)	0	.60	.37	40		0	0	error (2)	0	.021	.022	5.7		0	0
array-multidimensional/copy-3-n-u_true-unreach-call.i	unreach-call	disqualified	0	370	370	13000	5100	43	0	-								-								-								-								error (invalid witness file)	0	.62	.38	41		0	0	error (2)	0	.025	.027	5.7		0	0
array-multidimensional/copy-partial-2-n-u_true-unreach-call.i	unreach-call	disqualified	0	900	880	7400	12000	18	0	-								-								-								-								error (invalid witness file)	0	.60	.36	42		0	0	error (2)	0	.023	.024	5.6		0	0
array-multidimensional/copy-partial-3-u_true-unreach-call.i	unreach-call	disqualified	0	890	930	5400	10000	14	0	-								-								-								-								error (invalid witness file)	0	.74	.45	41		0	0	error (2)	0	.022	.022	5.6		0	0
array-multidimensional/diff-2-n-u_true-unreach-call.i	unreach-call	disqualified	0	420	410	14000	5400	80	0	-								-								-								-								error (invalid witness file)	0	.60	.37	40		0	0	error (2)	0	.023	.024	5.6		0	0
array-multidimensional/diff-3-n-u_true-unreach-call.i	unreach-call	disqualified	0	710	700	14000	8400	82	0	-								-								-								-								error (invalid witness file)	0	.76	.47	41		0	0	error (2)	0	.027	.028	5.6		0	0
array-multidimensional/init-2-n-u_true-unreach-call.i	unreach-call	disqualified	0	890	930	2500	11000	11	0	-								-								-								-								error (invalid witness file)	0	.80	.48	40		0	0	error (2)	0	.024	.024	5.6		0	0
array-multidimensional/init-3-u_true-unreach-call.i	unreach-call	disqualified	0	890	930	2500	14000	8.1	0	-								-								-								-								error (invalid witness file)	0	.73	.43	40		0	0	error (2)	0	.024	.024	5.6		0	0
array-multidimensional/init-4-n-u_true-unreach-call.i	unreach-call	disqualified	0	190	180	14000	2600	28	0	-								-								-								-								error (invalid witness file)	0	.65	.39	41		0	0	error (2)	0	.025	.025	5.6		0	0
array-multidimensional/init-non-constant-2-n-u_true-unreach-call.i	unreach-call	disqualified	0	880	880	340	13000	.63	0	-								-								-								-								timeout	0	900	880	5400		0	0	timeout	0	960	930	1000		.64	0
array-multidimensional/init-non-constant-3-u_true-unreach-call.i	unreach-call	disqualified	0	890	930	6700	12000	11	0	-								-								-								-								error (invalid witness file)	0	.60	.36	42		0	0	error (2)	0	.023	.024	5.6		0	0
array-multidimensional/max-2-u_true-unreach-call.i	unreach-call	disqualified	0	190	190	14000	2800	40	0	-								-								-								-								error (invalid witness file)	0	.74	.45	40		0	0	error (2)	0	.022	.022	5.6		0	0
array-multidimensional/max-3-n-u_true-unreach-call.i	unreach-call	disqualified	0	530	530	13000	6300	68	0	-								-								-								-								error (invalid witness file)	0	.77	.46	40		0	0	error (2)	0	.027	.028	5.5		0	0
array-multidimensional/min-2-u_true-unreach-call.i	unreach-call	disqualified	0	200	190	14000	2300	32	0	-								-								-								-								error (invalid witness file)	0	.76	.46	40		0	0	error (2)	0	.022	.023	5.6		0	0
array-multidimensional/min-3-n-u_true-unreach-call.i	unreach-call	disqualified	0	530	530	13000	7300	68	0	-								-								-								-								error (invalid witness file)	0	.65	.39	42		0	0	error (2)	0	.026	.027	5.6		0	0
array-multidimensional/rev-2-n-u_true-unreach-call.i	unreach-call	disqualified	0	150	150	14000	1600	35	0	-								-								-								-								error (invalid witness file)	0	.96	.59	42		0	0	error (2)	0	.022	.022	5.6		0	0
array-multidimensional/rev-3-u_true-unreach-call.i	unreach-call	disqualified	0	210	210	14000	3000	34	0	-								-								-								-								error (invalid witness file)	0	.59	.36	40		0	0	error (2)	0	.026	.027	5.7		0	0
array-multidimensional/transpose-u_true-unreach-call.i	unreach-call	disqualified	0	900	930	7500	9300	20	0	-								-								-								-								error (invalid witness file)	0	.66	.40	41		0	0	error (2)	0	.027	.028	5.6		0	0
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i	unreach-call	disqualified	0	13	13	170	170	.83	0	false(unreach-call)	1	4.7	2.6	260		0	.0041	false(unreach-call)	1	45	27	580		.68	0	false(unreach-call)	1	4.2	2.5	260		0	0	false(unreach-call)	1	.67	.66	20		.094	0	-								-
bitvector/sum02_false-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	880	880	440	11000	.59	0	error (invalid witness file)	0	.57	.34	40		0	0	error (2)	0	.024	.025	5.5		0	0	error (invalid witness file)	0	.94	.62	48		0	0	error (invalid witness file)	0	.0016	.0020	.52		0	0	-								-
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i	unreach-call	disqualified	0	35	34	190	500	.83	0	-								-								-								-								true	2	9.8	5.2	370		0	0	timeout	0	960	920	990		.75	0
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i	unreach-call	disqualified	0	43	43	190	520	.83	0	-								-								-								-								true	2	11	6.0	370		0	0	timeout	0	960	920	1000		.74	15
bitvector/gcd_1_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	2.6	2.9	78	36	.59	0	-								-								-								-								true	2	11	8.5	320		0	0	timeout	0	960	950	670		1.2	.28
bitvector/gcd_2_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	880	880	160	13000	.59	0	-								-								-								-								true	2	160	160	560		0	0	timeout	0	960	950	640		.63	0
bitvector/gcd_3_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	880	930	440	9900	.59	2.0	-								-								-								-								error (invalid witness file)	0	.68	.42	40		0	0	error (2)	0	.021	.023	5.7		0	0
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i	unreach-call	disqualified	0	2.6	2.8	82	30	.57	0	-								-								-								-								true	2	8.9	5.8	320		0	0	true	2	41	32	580		.62	.020
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	3.2	3.2	84	44	.71	0	-								-								-								-								true	2	12	8.2	390		0	0	true	2	200	190	650		.71	0
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i	unreach-call	disqualified	0	900	880	400	11000	.57	0	-								-								-								-								error (invalid witness file)	0	.75	.46	41		0	0	error (2)	0	.027	.028	5.6		0	0
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i	unreach-call	disqualified	0	890	880	390	8300	.57	.0041	-								-								-								-								out of memory	0	610	600	7000		0	0	true	2	17	13	330		.62	0
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i	unreach-call	disqualified	0	890	880	370	7200	.57	0	-								-								-								-								out of memory	0	580	570	7000		0	0	true	2	16	12	330		.66	0
bitvector/jain_5_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	890	880	350	12000	.54	0	-								-								-								-								timeout	0	910	890	6300		0	0	timeout	0	960	940	680		.63	0
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i	unreach-call	disqualified	0	890	880	410	6000	.57	0	-								-								-								-								out of memory	0	630	620	7000		0	0	true	2	20	16	330		.66	0
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i	unreach-call	disqualified	0	890	880	460	8900	.57	0	-								-								-								-								out of memory	0	680	670	7000		0	0	true	2	20	16	330		.66	0
bitvector/modulus_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	3.1	3.3	87	50	.59	0	-								-								-								-								true	2	17	14	340		0	0	true	2	17	12	370		.66	0
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	2.0	2.1	71	28	.59	0	-								-								-								-								true	2	7.0	3.8	280		0	0	true	2	40	26	570		.75	0
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	2.3	2.7	72	31	.63	0	-								-								-								-								true	2	6.8	3.8	290		0	0	timeout	0	960	930	2200		.88	0
bitvector/parity_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	880	880	300	11000	.59	0	-								-								-								-								true	2	36	26	470		0	0	timeout	0	960	950	1000		.72	0
bitvector/sum02_true-unreach-call_true-no-overflow.i	unreach-call	disqualified	0	880	880	260	12000	.57	0	-								-								-								-								out of memory	0	720	710	7000		0	0	unknown	0	380	380	620		.62	0
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	50	49	290	450	1.0	0	false(unreach-call)	1	5.4	2.9	270		0	0	true	-32	8.7	5.3	310		.66	0	unknown	0	4.9	2.8	270		0	0	false(unreach-call)	1	.64	.64	20		.13	0	-								-
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	110	110	360	1100	1.0	0	false(unreach-call)	1	7.0	3.7	270		0	0	true	-32	8.3	5.1	310		.62	0	false(unreach-call)	1	5.0	2.8	260		0	0	true	-32	.65	.65	21		.12	0	-								-
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	27	27	230	300	1.0	0	false(unreach-call)	1	5.2	2.8	270		0	0	true	-32	8.3	5.1	310		.62	0	false(unreach-call)	1	4.8	2.7	270		0	0	false(unreach-call)	1	.65	.65	21		.13	0	-								-
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	290	290	470	2400	1.0	0	-								-								-								-								true	2	93	80	1000		0	0	true	2	54	31	750		.75	.0041
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	260	260	450	2600	1.0	0	-								-								-								-								true	2	21	13	590		0	.0041	true	2	57	32	990		.68	0
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	320	320	480	2200	1.0	0	-								-								-								-								true	2	19	11	550		0	0	true	2	35	20	790		.62	0
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	880	880	730	7200	1.2	0	-								-								-								-								timeout	0	900	890	1600		0	0	timeout	0	960	920	2500		.63	0
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	880	880	720	6400	1.2	0	-								-								-								-								timeout	0	910	890	4400		0	0	true	2	45	25	920		.66	0
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c	unreach-call	disqualified	0	880	880	730	8500	1.2	0	-								-								-								-								timeout	0	900	890	4300		0	0	true	2	42	24	980		.62	0
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c	unreach-call	disqualified	0	880	880	720	9900	1.2	0	-								-								-								-								timeout	0	900	890	4300		0	0	true	2	38	22	1000		.66	0
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	880	880	790	9300	1.1	0	-								-								-								-								timeout	0	910	900	6200		0	0	true	2	39	22	850		.66	0
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c	unreach-call	disqualified	0	880	880	800	6200	1.1	0	-								-								-								-								timeout	0	910	890	6200		0	0	true	2	49	27	940		.66	0
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c	unreach-call	disqualified	0	3.7	3.9	94	52	.76	0	-								-								-								-								timeout	0	900	860	5200		0	0	true	2	190	160	790		.68	0
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c	unreach-call	disqualified	0	2.6	2.9	89	38	.72	0	-								-								-								-								out of memory	0	850	780	7000		0	0	true	2	44	28	550		.66	0
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c	unreach-call	disqualified	0	21	20	150	290	.72	0	-								-								-								-								timeout	0	900	840	6800		0	0	timeout	0	960	890	780		.68	0
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c	unreach-call	disqualified	0	15	15	99	230	.70	0	-								-								-								-								true	2	110	100	550		0	0	true	2	370	340	810		.71	1.7
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c	unreach-call	disqualified	0	2.6	2.9	88	31	.72	0	-								-								-								-								out of memory	0	810	740	7000		0	0	true	2	30	18	510		.66	0
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c	unreach-call	disqualified	0	2.6	2.6	71	30	.53	0	false(unreach-call)	1	3.7	2.1	250		0	0	false(unreach-call)	1	15	9.3	300		.68	0	false(unreach-call)	1	3.4	2.0	250		0	0	false(unreach-call)	1	.57	.57	20		.041	0	-								-
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c	unreach-call	disqualified	0	2.5	2.6	70	39	.54	0	false(unreach-call)	1	4.2	2.3	250		0	0	false(unreach-call)	1	6.5	3.7	290		.62	0	false(unreach-call)	1	3.7	2.2	250		0	0	false(unreach-call)	1	.59	.59	20		.041	0	-								-
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c	unreach-call	disqualified	0	2.6	2.6	71	30	.54	0	false(unreach-call)	1	3.6	2.0	250		0	0	false(unreach-call)	1	15	8.6	300		.75	0	false(unreach-call)	1	3.5	2.1	250		0	0	false(unreach-call)	1	.59	.58	20		.041	0	-								-
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c	unreach-call	disqualified	0	21	21	88	340	.56	0	timeout	0	93	75	1900		0	0	true	-32	13	7.8	300		.71	0	false(unreach-call)	1	3.6	2.1	250		0	0	false(unreach-call)	1	.57	.57	20		.049	0	-								-
bitvector-regression/signextension2_false-unreach-call_true-termination.c	unreach-call	disqualified	0	2.5	2.6	71	33	.54	0	false(unreach-call)	1	3.6	2.1	250		0	0	false(unreach-call)	1	6.8	4.3	310		.62	0	false(unreach-call)	1	4.3	2.5	250		0	.21	false(unreach-call)	1	.58	.58	20		.045	0	-								-
bitvector-regression/signextension_false-unreach-call_true-termination.c	unreach-call	disqualified	0	2.6	2.6	71	30	.55	0	false(unreach-call)	1	4.8	2.7	250		0	0	false(unreach-call)	1	8.4	5.0	300		.66	0	false(unreach-call)	1	3.6	2.1	250		0	0	false(unreach-call)	1	.58	.60	20		.045	.0041	-								-
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c	unreach-call	disqualified	0	1.9	2.1	66	24	.54	0	-								-								-								-								true	2	4.4	2.5	250		0	0	true	2	9.6	5.5	300		.66	0
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c	unreach-call	disqualified	0	1.9	2.1	68	24	.54	1.9	-								-								-								-								true	2	4.2	2.4	250		0	0	true	2	15	8.9	290		.75	0
bitvector-regression/signextension2_true-unreach-call_true-termination.c	unreach-call	disqualified	0	2.0	2.2	67	22	.54	0	-								-								-								-								true	2	3.8	2.1	250		0	0	true	2	9.7	5.7	300		.66	0
bitvector-regression/signextension_true-unreach-call_true-termination.c	unreach-call	disqualified	0	2.0	2.1	67	22	.55	0	-								-								-								-								true	2	5.2	2.9	250		0	0	true	2	8.2	4.5	310		.66	0
bitvector-loops/diamond_false-unreach-call2.i	unreach-call	disqualified	0	3.5	3.3	92	44	.63	0	false(unreach-call)	1	4.9	2.7	250		0	0	false(unreach-call)	1	8.1	4.9	310		.66	.0041	false(unreach-call)	1	3.9	2.3	250		0	0	false(unreach-call)	1	.58	.58	20		.049	0	-								-
bitvector-loops/overflow_false-unreach-call1.i	unreach-call	disqualified	0	880	930	930	12000	.54	0	error (invalid witness file)	0	.63	.39	40		0	0	error (2)	0	.020	.021	5.6		0	0	error (invalid witness file)	0	.95	.63	48		0	0	error (invalid witness file)	0	.0057	.0071	.54		0	0	-								-
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i	unreach-call	disqualified	0	5.7	5.3	110	75	.61	0	false(unreach-call)	1	4.9	2.7	290		0	0	true	-32	10	6.3	470		.66	0	true	-32	3.9	2.3	250		0	0	true	-32	.61	.61	20		.061	0	-								-
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	7.6	7.0	140	100	2.1	0	false(unreach-call)	1	5.8	3.1	270		0	.070	true	-32	13	7.5	430		.62	0	false(unreach-call)	1	5.9	3.3	280		0	0	false(unreach-call)	1	.82	.82	21		.30	0	-								-
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	6.0	5.7	120	71	1.5	0	false(unreach-call)	1	5.7	3.1	270		0	0	false(unreach-call)	1	20	11	520		.66	0	false(unreach-call)	1	5.6	3.1	280		0	.033	false(unreach-call)	1	.74	.74	21		.19	0	-								-
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	8.6	8.4	130	120	1.8	0	false(unreach-call)	1	6.3	3.3	290		0	0	false(unreach-call)	1	17	9.9	480		.62	.11	false(unreach-call)	1	7.4	4.0	280		0	.049	false(unreach-call)	1	.76	.76	21		.25	0	-								-
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	4.6	4.7	110	71	1.4	0	false(unreach-call)	1	5.8	3.1	270		0	0	false(unreach-call)	1	10	6.1	370		.62	0	false(unreach-call)	1	5.4	3.0	280		0	0	false(unreach-call)	1	.70	.70	21		.16	0	-								-
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	19	19	160	250	2.1	0	-								-								-								-								true	2	11	6.0	520		0	0	true	2	120	72	1100		.62	0
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	7.0	6.7	130	110	1.5	0	-								-								-								-								out of memory	0	500	480	7000		0	11	true	2	81	46	710		.62	0
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	5.2	5.2	120	63	1.5	0	-								-								-								-								true	2	9.5	5.1	350		0	0	true	2	76	42	670		.62	0
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	8.5	8.4	140	110	1.8	0	-								-								-								-								true	2	8.5	4.6	430		0	0	true	2	110	59	880		.62	0
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	2.6	3.0	86	31	1.0	0	-								-								-								-								true	2	5.8	3.2	270		0	0	true	2	20	11	480		.66	0
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c	unreach-call	disqualified	0	3.4	3.6	100	44	1.4	0	-								-								-								-								true	2	7.2	3.9	270		0	0	true	2	21	11	480		.66	0
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c	unreach-call	disqualified	0	7.0	6.6	140	92	1.0	0	false(unreach-call)	1	5.3	2.9	270		0	0	true	-32	8.3	4.7	310		.66	0	false(unreach-call)	1	4.9	2.8	270		0	0	false(unreach-call)	1	.66	.67	21		.13	0	-								-
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c	unreach-call	disqualified	0	6.7	6.6	140	86	1.0	0	false(unreach-call)	1	5.9	3.2	270		0	0	true	-32	9.3