Tool	CBMC 4.5			CPAchecker 1.2.11-svcomp14b			ESBMC 1.22.1			LLBMC			Predator 2013-10-30			Symbiotic			UltimateAutomizer			UltimateKojak
Limits	timelimit: 900 s, memlimit: 15360 MB, CPU core limit: 8
OS	Linux 3.2.0-56-generic x86_64
System	CPU: Intel Core i7-2600 CPU @ 3.40GHz with 8 cores, frequency: 3401 MHz; RAM: 32827640 kB
Date of execution	13-11-18 23:43			13-11-18 14:59			13-11-18 23:26			13-11-21 13:28			13-11-19 22:09			13-11-25 00:14			13-11-19 23:49			13-11-21 12:52
Options	--propertyfile ${sourcefile_path}/ALL.prp --32			-sv-comp14 -heap 10000M -spec ${sourcefile_path}/ALL.prp -disable-java-assertions			-c ${sourcefile_path}/ALL.prp			-spec ${sourcefile_path}/ALL.prp -witness ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt			--propertyfile ${sourcefile_path}/ALL.prp --trace ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt -m32						${sourcefile_path}/ALL.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt			${sourcefile_path}/ALL.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
../../sv-benchmarks/c/	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)
bitvector/byte_add_false.i	false(label)	0.30	17	false(label)	47	1200	false(label)	0.65	17	false(label)	0.19	3.0	unknown	38	20	false(label)	0.42	4.0	unknown	2.0	110	unknown	2.5	110
bitvector/byte_add_1_true.i	true	0.86	19	true	55	1100	true	0.49	16	true	0.16	4.0	unknown	2.9	9.0	true	0.24	3.0	unknown	2.0	110	unknown	2.2	110
bitvector/byte_add_2_true.i	true	0.90	19	true	53	1100	true	0.50	16	true	0.16	4.0	unknown	3.1	9.0	true	0.23	4.0	unknown	2.0	110	unknown	2.5	110
bitvector/gcd_1_true.i	true	2.6	62	true	9.7	170	true	13	58	true	0.15	3.0	false(label)	0.09	3.0	true	0.20	2.0	unknown	11	250	unknown	22	260
bitvector/gcd_2_true.i	true	2.8	61	true	85	180	true	170	60	true	1.5	8.0	false(label)	0.09	3.0	true	0.20	2.0	timeout	900	240	timeout	900	290
bitvector/gcd_3_true.i	true	2.9	61	true	67	200	true	250	61	true	2.3	8.0	false(label)	0.13	3.0	true	0.19	2.0	timeout	900	280	timeout	900	370
bitvector/gcd_4_true.i	true	0.53	16	true	1.6	95	true	0.23	12	true	0.12	2.0	false(label)	0.10	4.0	true	0.20	2.0	unknown	390	2400	timeout	920	500
bitvector/interleave_bits_true.i	true	0.61	16	true	15	270	true	0.24	12	true	0.11	2.0	false(label)	0.11	4.0	true	0.20	3.0	unknown	60	290	false(label)	43	350
bitvector/jain_1_true.i	true	1.0	68	true	2.1	140	true	0.37	19	true	0.19	2.0	false(label)	0.09	3.0	timeout	900	38	true	26	730	true	4.4	200
bitvector/jain_2_true.i	true	1.5	140	true	2.1	140	true	0.45	28	true	0.20	2.0	false(label)	0.09	3.0	timeout	900	51	unknown	29	2300	timeout	910	370
bitvector/jain_4_true.i	true	1.9	200	true	2.2	140	true	1.6	41	true	0.23	2.0	false(label)	0.09	3.0	timeout	900	59	true	250	750	unknown	170	8200
bitvector/jain_5_true.i	true	0.53	16	timeout	900	2000	true	0.25	11	true	0.18	2.0	false(label)	0.11	3.0	timeout	900	2.0	timeout	920	410	timeout	920	1100
bitvector/jain_6_true.i	true	1.6	140	true	2.2	140	true	2.1	41	true	0.22	2.0	false(label)	0.09	3.0	timeout	900	59	true	37	480	timeout	910	1500
bitvector/jain_7_true.i	true	1.1	58	true	2.2	140	true	0.41	19	true	0.22	2.0	false(label)	0.10	3.0	timeout	900	46	timeout	900	800	timeout	900	680
bitvector/modulus_true.i	true	380	1100	true	4.7	150	true	32	150	true	6.9	53	false(label)	0.09	4.0	true	210	34	unknown	2.5	150	false(label)	2.8	190
bitvector/num_conversion_1_true.i	true	0.53	16	true	1.6	95	true	0.24	12	true	0.12	2.0	true	0.13	3.0	true	0.16	2.0	unknown	2.0	100	unknown	2.3	110
bitvector/num_conversion_2_true.i	true	0.53	16	true	25	390	true	0.29	12	true	0.10	2.0	false(label)	0.11	3.0	true	0.21	2.0	unknown	2.3	100	unknown	2.3	110
bitvector/parity_true.i	true	4.6	19	true	76	230	true	25	41	true	0.49	4.0	false(label)	0.09	3.0	true	1.3	5.0	unknown	2.7	170	false(label)	2.6	160
bitvector/sum02_true.i	true	0.64	18	timeout	900	3800	true	0.32	13	true	0.24	5.0	false(label)	0.10	3.0	timeout	900	150	timeout	920	430	timeout	920	810
bitvector/s3_clnt_1_false.BV.c.cil.c	false(label)	6.1	180	false(label)	6.6	250	false(label)	16	120	false(label)	0.37	11	false(label)	12	31	timeout	900	1300	unknown	18	650	false(label)	210	1200
bitvector/s3_clnt_2_false.BV.c.cil.c	false(label)	5.2	150	false(label)	6.2	240	false(label)	12	82	false(label)	0.69	20	false(label)	15	36	timeout	900	1200	unknown	21	640	false(label)	410	1200
bitvector/s3_clnt_3_false.BV.c.cil.c	false(label)	1.3	53	false(label)	3.4	190	false(label)	13	83	false(label)	0.30	12	false(label)	0.12	5.0	false(label)	0.65	5.0	unknown	12	380	false(label)	33	400
bitvector/s3_clnt_1_true.BV.c.cil.c	true	86	1500	true	3.7	180	true	4.7	110	true	0.88	25	false(label)	16	44	true	1.3	10.0	unknown	18	650	false(label)	210	1200
bitvector/s3_clnt_2_true.BV.c.cil.c	true	75	1300	true	3.7	180	true	3.3	80	true	0.91	25	false(label)	27	48	true	1.3	10.0	unknown	20	680	false(label)	390	1100
bitvector/s3_clnt_3_true.BV.c.cil.c	true	73	1200	true	4.7	200	true	3.2	77	true	1.1	28	false(label)	6.7	27	true	1.3	10.0	true	40	1200	timeout	920	1600
bitvector/s3_srvr_1_alt_true.BV.c.cil.c	true	850	640	timeout	900	530	true	900	190	true	5.6	95	false(label)	3.5	24	timeout	900	580	timeout	920	4400	timeout	920	1200
bitvector/s3_srvr_1_true.BV.c.cil.c	true	170	1800	true	15	260	true	3.9	100	true	1.00	29	false(label)	3.7	27	timeout	900	700	true	51	1800	timeout	920	1600
bitvector/s3_srvr_2_alt_true.BV.c.cil.c	true	160	1700	true	16	640	true	5.0	90	true	1.9	35	false(label)	14	37	timeout	900	1100	true	46	980	timeout	920	1600
bitvector/s3_srvr_2_true.BV.c.cil.c	true	170	1700	true	17	640	true	5.3	93	true	2.1	37	false(label)	14	37	timeout	900	1100	true	46	820	timeout	920	1200
bitvector/s3_srvr_3_alt_true.BV.c.cil.c	true	150	1600	true	15	250	true	6.7	130	true	1.9	60	false(label)	7.3	30	timeout	900	930	true	50	1600	true	250	1100
bitvector/s3_srvr_3_true.BV.c.cil.c	true	150	1600	true	15	250	true	7.6	130	true	1.9	64	false(label)	3.5	24	timeout	900	930	true	51	1700	true	230	1100
bitvector/soft_float_1_true.c.cil.c	true	3.3	38	true	23	720	true	1.2	23	true	0.97	8.0	false(label)	0.11	4.0	unknown	0.73	5.0	unknown	8.4	250	unknown	8.5	270
bitvector/soft_float_2_true.c.cil.c	true	1.7	38	true	8.8	240	true	0.25	14	true	0.21	4.0	unknown	0.10	4.0	timeout	900	130	unknown	8.1	360	timeout	920	540
bitvector/soft_float_3_true.c.cil.c	true	1.7	38	timeout	900	6300	true	0.28	14	true	0.23	4.0	unknown	0.10	4.0	timeout	900	140	unknown	5.8	240	timeout	920	500
bitvector/soft_float_4_true.c.cil.c	true	6.5	44	true	70	290	true	16	29	true	3.1	9.0	false(label)	0.11	4.0	unknown	0.62	5.0	unknown	5.6	250	unknown	7.8	270
bitvector/soft_float_5_true.c.cil.c	true	1.7	38	true	8.8	240	true	0.26	14	true	0.23	4.0	unknown	0.10	4.0	timeout	900	130	unknown	9.3	250	timeout	920	640
bitvector-regression/implicitfloatconversion_false.i	false(label)	0.18	16	false(label)	1.7	120	false(label)	0.26	11	false(label)	0.11	2.0	false(label)	0.08	3.0	false(label)	0.34	2.0	unknown	2.0	100	unknown	2.2	110
bitvector-regression/implicitunsignedconversion_false.i	false(label)	0.17	16	false(label)	1.8	120	false(label)	0.27	11	false(label)	0.10	2.0	false(label)	0.10	3.0	false(label)	0.19	2.0	true	2.2	130	true	2.4	140
bitvector-regression/integerpromotion_false.i	false(label)	0.18	18	false(label)	2.0	130	false(label)	0.33	17	false(label)	0.10	2.0	false(label)	0.10	3.0	false(label)	0.22	2.0	unknown	2.0	110	unknown	2.2	110
bitvector-regression/pointer_extension2_false.i	false(label)	0.18	18	false(label)	2.0	130	true	0.30	16	false(label)	0.12	2.0	unknown	0.13	3.0	true	0.21	2.0	unknown	2.0	110	unknown	2.3	110
bitvector-regression/pointer_extension3_false.i	false(label)	0.21	18	false(label)	2.0	120	false(label)	0.33	17	false(label)	0.10	2.0	unknown	0.10	3.0	false(label)	0.21	2.0	unknown	2.0	110	unknown	2.2	110
bitvector-regression/pointer_extension_false.i	false(label)	0.18	18	false(label)	2.0	130	false(label)	0.32	17	false(label)	0.11	2.0	unknown	0.10	3.0	false(label)	0.20	2.0	unknown	2.0	110	unknown	2.2	110
bitvector-regression/signextension2_false.i	false(label)	0.17	18	false(label)	2.0	120	false(label)	0.35	16	false(label)	0.10	2.0	unknown	0.10	4.0	false(label)	0.20	2.0	unknown	2.0	100	unknown	2.3	110
bitvector-regression/signextension_false.i	false(label)	0.17	18	false(label)	2.0	130	false(label)	0.34	17	false(label)	0.13	2.0	unknown	0.16	4.0	false(label)	0.21	2.0	unknown	2.0	110	unknown	2.2	110
bitvector-regression/implicitunsignedconversion_true.i	true	0.57	16	true	1.6	94	true	0.21	11	true	0.10	2.0	true	0.15	3.0	true	0.19	2.0	false(label)	2.1	120	false(label)	2.4	140
bitvector-regression/integerpromotion_true.i	true	0.60	18	true	2.3	140	true	0.36	16	true	0.11	2.0	true	0.12	3.0	true	0.21	2.0	unknown	2.0	110	unknown	2.2	110
bitvector-regression/pointer_extension_true.i	true	0.57	18	true	2.2	130	true	0.31	16	true	0.10	2.0	unknown	0.10	3.0	true	0.21	2.0	unknown	2.0	110	unknown	2.2	110
bitvector-regression/signextension2_true.i	true	0.58	18	true	1.7	97	true	0.27	16	true	0.11	2.0	unknown	0.09	4.0	true	0.19	2.0	unknown	2.0	110	unknown	2.2	110
bitvector-regression/signextension_true.i	true	0.57	18	true	1.7	97	true	0.28	16	true	0.11	2.0	unknown	0.15	4.0	true	0.20	2.0	unknown	2.0	110	unknown	2.2	110
../../sv-benchmarks/c/	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)	status	time(s)	memory(MB)
total files	49	2300	16000	49	4300	25000	49	1500	2200	49	39	610	49	170	520	49	16000	8700	49	6700	28000	49	17000	34000
correct results	49	2300	16000	45	690	12000	48	1500	2200	49	39	610	9	28	90	28	220	130	9	590	10000	6	1100	5300
false negatives	0	0	0	0	0	0	1	0.30	16	0	0	0	0	0	0	1	0.21	2.0	1	2.2	130	1	2.4	140
false positives	0	0	0	0	0	0	0	0	0	0	0	0	26	97	360	0	0	0	1	2.1	120	6	650	3100
score (49 files, max score: 86)	86			78			77			86			-92			39			6			-23