Floats – BenchExec results

Tool	2LS 0.3.4			CBMC			Ceagle 1.0			Ceagle AbsRef 1.0.0			CPAchecker 1.4-svcomp16c						CPAchecker 1.4-svn 18373			CPAchecker 1.4-svcomp16c			ESBMC ESBMC version 2.0.0 64-bit x86_64 linux			DepthK ESBMC+DepthK version 2.1			impara 0.45			PAC-MAN			SeaHorn-F16 0.1.0			SMACK+Corral 1.5.2			symbiotic 3.0.1			ULTIMATE Automizer cfb9fd9e			ULTIMATE Kojak fd30d3d8
Limits	timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host	[zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]						[zeus02; zeus04; zeus05; zeus06; zeus07; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus17; zeus19; zeus20; zeus21; zeus24]			[zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS	Linux 4.2.0-22-generic																								Linux 4.2.0-23-generic			Linux 4.2.0-22-generic			Linux 4.2.0-23-generic
System	CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution	2016-01-02 22:42:27 CET [[ 2016-01-15 08:01:51 CET ]] [[ 2016-01-15 21:37:22 CET ]]			2016-01-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]			2016-01-03 23:39:46 CET [[ 2016-01-15 08:27:56 CET ]] [[ 2016-01-15 21:58:29 CET ]]			2016-01-04 05:59:47 CET [[ 2016-01-15 08:28:20 CET ]] [[ 2016-01-15 21:58:46 CET ]]			2016-01-04 06:25:51 CET [[ 2016-01-15 08:31:02 CET ]] [[ 2016-01-15 21:59:57 CET ]]			2016-01-04 01:42:53 CET [[ 2016-01-15 08:36:34 CET ]] [[ 2016-01-15 22:02:40 CET ]]			2016-01-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]]			2016-01-04 13:17:38 CET [[ 2016-01-15 08:48:20 CET ]] [[ 2016-01-15 22:10:37 CET ]]			2016-01-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]]			2016-01-05 14:06:34 CET [[ 2016-01-15 09:00:06 CET ]] [[ 2016-01-15 22:17:52 CET ]]			2016-01-13 07:41:14 CET [[ 2016-01-15 09:11:00 CET ]] [[ 2016-01-15 22:23:23 CET ]]			2016-01-13 07:33:23 CET [[ 2016-01-15 09:22:08 CET ]] [[ 2016-01-15 22:28:32 CET ]]			2016-01-11 21:35:00 [[ 2016-01-15 18:20:27 CET ]] [[ 2016-01-15 22:30:28 CET ]]			2016-01-07 09:05:16 CET [[ 2016-01-15 09:34:34 CET ]] [[ 2016-01-15 22:36:10 CET ]]			2016-01-07 09:04:54 CET [[ 2016-01-15 09:39:10 CET ]] [[ 2016-01-15 22:39:28 CET ]]			2016-01-14 23:51:13 CET [[ 2016-01-15 09:43:48 CET ]] [[ 2016-01-15 22:41:15 CET ]]			2016-01-08 15:10:30 CET [[ 2016-01-15 09:49:48 CET ]] [[ 2016-01-15 22:43:29 CET ]]
Run set	2ls.sv-comp16.Floats			cbmc.sv-comp16.Floats			ceagle.sv-comp16			ceagle-absref.sv-comp16.Floats			cpa-bam.sv-comp16.Floats			cpa-kind.sv-comp16.Floats			cpa-refsel.sv-comp16.Floats			cpa-seq.sv-comp16.Floats			esbmc.sv-comp16.Floats			esbmcdepthk.sv-comp16.Floats			impara.sv-comp16.Floats			pacman.sv-comp16.Floats			seahorn.sv-comp16.Floats			smack.sv-comp16.Floats			symbiotic3.sv-comp16.Floats			uautomizer.sv-comp16.Floats			ukojak.sv-comp16.Floats
Options	--k-induction --competition-mode --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/2ls.2016-01-02_2242.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			--graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			[[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ceagle.2016-01-03_2339.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ceagle.2016-01-03_2339.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			[[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ceagle-absref.2016-01-04_0559.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ceagle-absref.2016-01-04_0559.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			-sv-comp16-bam -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-bam.2016-01-04_0625.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			-sv-comp16--k-induction -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-kind.2016-01-04_0142.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			-sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			-sv-comp16 -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-seq.2016-01-04_1317.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			[[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			[[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmcdepthk.2016-01-05_1406.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			--eager --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/impara.2016-01-13_0741.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			[[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/pacman.2016-01-13_0733.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/pacman.2016-01-13_0733.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			--cex=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/seahorn.2016-01-11_2135.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			-w error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/smack.2016-01-07_0905.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			[[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/symbiotic3.2016-01-07_0904.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			[[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/uautomizer.2016-01-14_2351.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]			[[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/ukojak.2016-01-08_1510.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)
floats-cdfpl/newton_1_4_false-unreach-call.i	false(reach)	3.1	55	false(reach)	9.3	54	false(reach)	.46	8.0	false(reach)	.089	5.7	false(reach)	370	8600	false(reach)	92	440	false(reach)	120	3000	false(reach)	16	300	false(reach)	51	340	unknown	.20	21	false(reach)	9.2	73	true	680	210	failure	.031	5.5	error (1)	.063	7.1	unknown	18	5.9	unknown	9.7	350	unknown	8.4	330
floats-cdfpl/newton_1_5_false-unreach-call.i	false(reach)	2.8	55	false(reach)	4.3	48	false(reach)	.55	8.0	false(reach)	.10	5.9	false(reach)	56	480	false(reach)	320	650	false(reach)	160	4200	false(reach)	16	300	false(reach)	33	340	unknown	.23	21	false(reach)	10	76	true	670	210	failure	.037	5.4	error (1)	.077	7.1	unknown	18	6.2	unknown	9.0	360	unknown	9.1	330
floats-cdfpl/newton_1_6_false-unreach-call.i	false(reach)	3.2	56	false(reach)	7.2	52	false(reach)	.40	8.1	false(reach)	.091	5.9	false(reach)	43	1200	false(reach)	220	580	false(reach)	15	490	false(reach)	7.4	300	false(reach)	18	330	unknown	.21	21	false(reach)	15	85	true	680	210	failure	.051	5.4	error (1)	.047	7.2	unknown	18	6.0	unknown	7.9	320	unknown	9.9	340
floats-cdfpl/newton_1_7_false-unreach-call.i	false(reach)	4.5	57	false(reach)	8.5	53	false(reach)	.33	8.0	false(reach)	.14	5.7	false(reach)	11	420	false(reach)	100	490	false(reach)	34	980	false(reach)	8.5	300	false(reach)	7.9	340	unknown	.18	21	false(reach)	12	80	true	670	200	failure	.038	5.4	error (1)	.078	7.3	unknown	18	6.0	unknown	8.8	340	unknown	8.3	320
floats-cdfpl/newton_1_8_false-unreach-call.i	false(reach)	2.4	54	false(reach)	9.3	55	false(reach)	.30	8.2	false(reach)	.093	5.9	false(reach)	11	400	false(reach)	20	440	false(reach)	12	470	false(reach)	7.1	300	false(reach)	8.3	330	unknown	.16	21	false(reach)	20	92	true	670	200	failure	.025	5.5	error (1)	.034	7.2	unknown	18	5.8	unknown	8.8	330	unknown	8.6	320
floats-cdfpl/newton_2_6_false-unreach-call.i	false(reach)	14	120	false(reach)	20	99	false(reach)	.57	9.2	false(reach)	.38	7.8	false(reach)	160	2900	false(reach)	120	650	false(reach)	140	3100	false(reach)	12	400	false(reach)	630	7500	unknown	.13	21	false(reach)	180	350	true	680	210	failure	.048	5.5	error (1)	.047	7.3	unknown	18	6.0	unknown	9.7	330	unknown	8.2	330
floats-cdfpl/newton_2_7_false-unreach-call.i	false(reach)	20	140	false(reach)	80	180	false(reach)	.86	9.3	false(reach)	.28	8.1	false(reach)	360	8800	false(reach)	120	700	false(reach)	74	2000	false(reach)	8.2	400	false(reach)	310	2500	unknown	.17	21	false(reach)	92	240	true	690	210	failure	.032	5.6	error (1)	.045	7.2	unknown	18	6.1	unknown	9.2	320	unknown	8.7	330
floats-cdfpl/newton_2_8_false-unreach-call.i	false(reach)	18	130	false(reach)	23	100	false(reach)	.88	9.5	false(reach)	.37	7.8	false(reach)	470	11000	false(reach)	640	890	false(reach)	22	720	false(reach)	8.4	400	false(reach)	24	600	unknown	.17	21	false(reach)	50	180	true	680	200	failure	.047	5.5	error (1)	.042	7.2	unknown	18	5.9	unknown	8.7	320	unknown	9.1	320
floats-cdfpl/newton_3_6_false-unreach-call.i	false(reach)	35	190	false(reach)	140	300	false(reach)	150	45	timeout	900	150	false(reach)	870	14000	timeout	900	890	out of memory	580	15000	false(reach)	21	510	out of memory	770	15000	unknown	.15	21	false(reach)	680	1000	true	680	210	failure	.043	5.5	error (1)	.067	7.3	unknown	18	6.2	unknown	9.5	350	unknown	9.3	330
floats-cdfpl/newton_3_7_false-unreach-call.i	false(reach)	39	190	false(reach)	150	290	false(reach)	150	45	timeout	900	150	out of memory	580	15000	false(reach)	230	1000	false(reach)	59	1500	false(reach)	19	510	false(reach)	92	1100	unknown	.20	21	false(reach)	530	870	true	670	200	failure	.027	5.6	error (1)	.077	7.3	unknown	18	6.0	unknown	9.8	350	unknown	8.8	320
floats-cdfpl/newton_3_8_false-unreach-call.i	false(reach)	13	140	false(reach)	120	250	false(reach)	150	44	timeout	900	180	false(reach)	74	1500	false(reach)	270	1000	false(reach)	140	2200	false(reach)	68	530	false(reach)	48	1100	unknown	.22	21	false(reach)	310	650	true	680	210	failure	.041	5.6	error (1)	.080	7.2	unknown	18	6.1	unknown	8.5	330	unknown	8.4	320
floats-cdfpl/sine_1_false-unreach-call.i	false(reach)	1.6	41	false(reach)	.43	35	unknown	.047	6.1	false(reach)	4.0	110	false(reach)	77	350	false(reach)	77	430	false(reach)	140	4700	false(reach)	39	300	false(reach)	16	290	unknown	.13	21	false(reach)	3.2	46	true	670	200	failure	.020	5.6	error (1)	.080	7.2	unknown	18	6.1	unknown	8.0	320	unknown	8.8	330
floats-cdfpl/sine_2_false-unreach-call.i	false(reach)	.50	37	false(reach)	1.6	35	unknown	.051	6.2	false(reach)	52	380	false(reach)	160	5800	false(reach)	11	340	false(reach)	160	6700	false(reach)	4.4	270	false(reach)	24	300	unknown	.15	21	false(reach)	7.1	62	true	680	210	failure	.035	5.5	error (1)	.069	7.2	unknown	17	6.0	unknown	8.2	320	unknown	8.2	320
floats-cdfpl/sine_3_false-unreach-call.i	false(reach)	2.3	40	false(reach)	1.8	35	unknown	.086	5.9	false(reach)	50	380	false(reach)	320	11000	false(reach)	52	390	false(reach)	36	320	false(reach)	33	280	false(reach)	6.5	280	unknown	.16	21	false(reach)	7.4	53	true	670	210	failure	.030	5.6	error (1)	.077	7.1	unknown	18	5.8	unknown	8.4	330	unknown	8.3	320
floats-cdfpl/square_1_false-unreach-call.i	false(reach)	1.5	39	false(reach)	1.2	35	false(reach)	21	110	false(reach)	55	140	false(reach)	96	2200	false(reach)	45	420	exception	26	770	false(reach)	87	500	false(reach)	28	420	unknown	.17	21	false(reach)	4.3	49	true	670	200	failure	.050	5.5	error (1)	.044	7.2	unknown	18	6.2	unknown	9.2	330	unknown	8.4	320
floats-cdfpl/square_2_false-unreach-call.i	false(reach)	1.5	37	false(reach)	1.8	34	false(reach)	8.0	100	false(reach)	65	140	false(reach)	79	1900	false(reach)	44	400	exception	34	770	false(reach)	87	490	false(reach)	70	480	unknown	.17	21	false(reach)	5.2	50	true	690	210	failure	.030	5.5	error (1)	.049	7.2	unknown	18	5.9	unknown	9.7	320	unknown	8.7	330
floats-cdfpl/square_3_false-unreach-call.i	false(reach)	1.1	38	false(reach)	8.5	45	false(reach)	81	110	false(reach)	60	140	false(reach)	83	2000	false(reach)	35	390	exception	42	770	false(reach)	78	480	false(reach)	27	430	unknown	.15	21	false(reach)	6.4	53	true	680	210	failure	.022	5.5	error (1)	.067	7.2	unknown	18	6.1	unknown	8.3	330	unknown	8.0	320
floats-cdfpl/newton_1_1_true-unreach-call.i	true	7.6	60	true	850	150	true	.19	8.1	true	.099	5.7	out of memory	660	15000	timeout	900	510	out of memory	720	15000	timeout	900	530	true	200	52	unknown	.18	21	true	16	66	true	660	200	failure	.048	5.5	error (1)	.033	7.1	unknown	18	8.0	unknown	9.6	340	unknown	8.9	330
floats-cdfpl/newton_1_2_true-unreach-call.i	true	9.8	65	true	850	120	true	.15	7.9	true	.078	5.9	out of memory	660	15000	timeout	900	530	out of memory	660	15000	timeout	900	640	true	320	57	unknown	.17	21	true	22	69	true	680	210	failure	.030	5.5	error (1)	.034	7.1	unknown	18	8.1	unknown	9.3	330	unknown	8.4	310
floats-cdfpl/newton_1_3_true-unreach-call.i	true	10	73	true	520	96	true	.14	8.0	true	.18	21	out of memory	610	15000	timeout	900	740	out of memory	680	15000	timeout	900	640	true	590	57	unknown	.16	21	true	22	82	true	690	210	failure	.031	5.5	error (1)	.059	7.2	unknown	17	5.7	unknown	8.0	310	unknown	9.0	320
floats-cdfpl/newton_2_1_true-unreach-call.i	true	23	130	true	850	210	true	.43	9.6	true	.40	8.9	out of memory	600	15000	timeout	900	740	out of memory	590	15000	timeout	900	590	true	410	100	unknown	.17	21	true	100	150	true	670	200	failure	.026	5.5	error (1)	.073	7.2	unknown	18	5.8	unknown	8.1	310	unknown	8.1	320
floats-cdfpl/newton_2_2_true-unreach-call.i	true	22	130	true	850	270	true	.41	9.5	true	.43	8.9	out of memory	650	15000	timeout	900	720	out of memory	620	15000	timeout	900	690	true	840	120	unknown	.18	21	true	120	180	true	670	210	failure	.041	5.6	error (1)	.045	7.4	unknown	18	6.0	unknown	7.7	320	unknown	8.9	330
floats-cdfpl/newton_2_3_true-unreach-call.i	true	26	130	true	850	330	true	.29	11	true	.46	8.9	out of memory	610	15000	timeout	900	720	out of memory	630	15000	timeout	900	700	unknown	890	120	unknown	.14	21	true	120	200	true	680	210	failure	.030	5.5	error (1)	.062	7.4	unknown	18	6.0	unknown	8.6	320	unknown	9.2	320
floats-cdfpl/newton_2_4_true-unreach-call.i	true	36	130	true	850	590	true	.41	9.3	true	.40	9.0	out of memory	630	15000	timeout	900	730	out of memory	430	15000	timeout	900	740	unknown	900	120	unknown	.22	21	true	120	180	true	670	200	failure	.052	5.6	error (1)	.045	7.2	unknown	18	6.0	unknown	8.2	320	unknown	9.6	330
floats-cdfpl/newton_2_5_true-unreach-call.i	true	38	130	true	850	620	true	.10	6.4	true	.41	8.9	out of memory	620	15000	timeout	900	670	out of memory	620	15000	timeout	900	600	unknown	890	120	unknown	.18	21	true	200	300	true	670	210	failure	.041	5.4	error (1)	.046	7.2	unknown	18	6.0	unknown	9.7	330	unknown	9.3	350
floats-cdfpl/newton_3_1_true-unreach-call.i	true	57	220	true	850	470	true	150	42	timeout	900	150	out of memory	600	15000	timeout	900	770	out of memory	620	15000	timeout	900	730	true	680	150	unknown	.22	21	true	340	430	true	680	210	failure	.046	5.6	error (1)	.076	7.4	unknown	18	5.9	unknown	9.8	350	unknown	8.1	330
floats-cdfpl/newton_3_2_true-unreach-call.i	true	85	220	true	850	400	true	150	43	timeout	900	150	out of memory	630	15000	timeout	900	730	out of memory	620	15000	timeout	900	710	unknown	890	150	unknown	.15	22	true	270	440	true	660	200	failure	.051	5.4	error (1)	.048	7.3	unknown	18	5.9	unknown	8.9	330	unknown	9.3	320
floats-cdfpl/newton_3_3_true-unreach-call.i	true	80	190	true	850	600	true	150	43	timeout	900	150	out of memory	570	15000	timeout	900	790	out of memory	580	15000	timeout	900	800	unknown	890	150	unknown	.13	21	true	190	320	true	690	210	failure	.036	5.5	error (1)	.037	7.1	unknown	18	5.8	unknown	9.5	310	unknown	9.0	320
floats-cdfpl/newton_3_4_true-unreach-call.i	true	77	190	true	850	510	true	150	44	timeout	900	150	out of memory	620	15000	timeout	900	730	out of memory	620	15000	timeout	900	660	unknown	890	150	unknown	.22	21	true	340	460	true	670	210	failure	.042	5.5	error (1)	.051	7.2	unknown	18	5.9	unknown	8.8	340	unknown	9.3	330
floats-cdfpl/newton_3_5_true-unreach-call.i	true	79	210	true	850	610	true	150	46	timeout	900	160	out of memory	610	15000	timeout	900	680	out of memory	610	15000	timeout	900	680	unknown	890	150	unknown	.22	21	true	400	480	true	680	210	failure	.026	5.4	error (1)	.050	7.4	unknown	18	6.3	unknown	8.8	330	unknown	8.6	320
floats-cdfpl/sine_4_true-unreach-call.i	true	38	49	true	850	96	true	350	200	true	470	400	timeout	900	500	timeout	900	490	out of memory	410	15000	timeout	900	580	unknown	890	60	unknown	.16	21	true	740	130	true	660	200	failure	.050	5.6	error (1)	.075	7.2	unknown	18	5.8	unknown	9.2	330	unknown	8.6	320
floats-cdfpl/sine_5_true-unreach-call.i	true	2.0	40	true	510	71	true	380	200	true	240	400	timeout	900	480	timeout	900	470	out of memory	460	15000	timeout	900	450	unknown	890	65	unknown	.21	21	true	73	90	true	670	210	failure	.041	5.4	error (1)	.048	7.1	unknown	18	6.1	unknown	9.3	320	unknown	8.8	330
floats-cdfpl/sine_6_true-unreach-call.i	true	2.6	41	true	330	74	true	390	200	true	220	400	true	260	370	true	260	350	exception	410	14000	true	410	400	unknown	890	60	unknown	.22	21	true	8.9	53	true	670	210	failure	.047	5.4	error (1)	.046	7.2	unknown	18	6.0	unknown	7.8	320	unknown	9.0	340
floats-cdfpl/sine_7_true-unreach-call.i	true	1.9	39	true	850	100	true	220	190	true	160	400	timeout	900	500	timeout	900	480	exception	150	5900	timeout	900	540	unknown	890	58	unknown	.22	21	true	4.5	47	true	680	200	failure	.044	5.5	error (1)	.045	7.3	unknown	18	5.8	unknown	8.6	310	unknown	10	350
floats-cdfpl/sine_8_true-unreach-call.i	true	1.6	40	true	530	100	true	240	190	true	180	390	true	500	450	true	510	430	exception	260	9400	timeout	900	570	unknown	890	57	unknown	.22	21	true	150	130	true	660	200	failure	.048	5.4	error (1)	.044	7.4	unknown	18	6.2	unknown	8.5	320	unknown	8.9	330
floats-cdfpl/square_4_true-unreach-call.i	true	190	90	true	850	120	true	250	120	true	210	150	true	340	410	true	340	400	exception	30	760	true	680	470	false(reach)	800	680	unknown	.22	21	true	200	170	true	680	210	failure	.051	5.5	error (1)	.058	7.1	unknown	18	5.8	unknown	8.0	310	unknown	8.9	330
floats-cdfpl/square_5_true-unreach-call.i	true	200	81	true	850	110	true	200	120	true	170	140	true	670	490	true	660	470	exception	42	770	timeout	900	620	true	2.2	16	unknown	.19	21	true	190	200	true	670	210	failure	.035	5.5	error (1)	.068	7.3	unknown	18	6.1	unknown	8.2	320	unknown	8.1	320
floats-cdfpl/square_6_true-unreach-call.i	true	72	78	true	420	78	true	150	120	true	200	140	true	270	410	true	270	390	exception	44	770	true	310	430	true	4.4	18	unknown	.21	21	true	56	120	true	670	200	failure	.033	5.5	error (1)	.036	7.0	unknown	18	5.8	unknown	9.1	320	unknown	9.3	330
floats-cdfpl/square_7_true-unreach-call.i	true	6.9	45	true	630	110	true	150	110	true	160	140	true	290	470	true	290	460	exception	51	770	true	330	500	true	3.8	18	unknown	.17	21	true	58	120	true	680	210	failure	.040	5.4	error (1)	.045	7.0	unknown	18	6.0	unknown	9.0	330	unknown	8.1	330
floats-cdfpl/square_8_true-unreach-call.i	true	1.1	37	true	14	36	true	59	110	true	77	130	true	32	310	true	33	290	timeout	900	860	true	73	340	true	.064	15	unknown	.18	21	true	2.2	40	true	690	210	failure	.027	5.6	error (1)	.081	7.3	unknown	18	5.7	unknown	8.5	330	unknown	9.5	350
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i	true	.67	52	true	3.3	40	true	.19	6.6	true	1.5	19	false(reach)	10	460	false(reach)	300	800	false(reach)	8.7	480	false(reach)	300	930	unknown	.18	28	unknown	.62	41	true	.57	38	unknown	.46	18	failure	.039	5.7	error (1)	.095	7.1	false(reach)	.36	6.7	unknown	8.2	310	unknown	7.2	310
floats-cbmc-regression/float-no-simp1_true-unreach-call.i	true	.10	22	true	1.1	24	true	.11	7.6	true	.082	5.9	true	3.5	210	true	3.4	190	true	3.4	210	true	2.6	180	true	.090	13	true	.35	21	true	.10	22	true	690	210	failure	.023	5.6	error (1)	.077	7.3	true	.12	5.8	unknown	9.2	330	unknown	9.7	330
floats-cbmc-regression/float-no-simp2_true-unreach-call.i	true	2.2	37	true	14	35	true	.58	32	true	4.4	120	true	7.1	260	true	11	260	exception	5.1	250	true	15	350	true	.25	24	unknown	.51	36	true	1.6	34	true	670	210	failure	.025	5.5	error (1)	.055	7.2	unknown	53	7.0	unknown	8.6	320	unknown	9.2	320
floats-cbmc-regression/float-no-simp3_true-unreach-call.i	true	.12	24	true	1.1	24	true	.13	7.7	true	.077	5.7	true	3.5	220	true	3.5	190	true	2.8	210	true	3.2	180	error (1)	3.4	200	unknown	.16	21	true	.14	22	true	670	210	failure	.022	5.5	error (1)	.077	7.3	true	.056	5.7	unknown	7.8	320	unknown	8.7	310
floats-cbmc-regression/float-no-simp4_true-unreach-call.i	true	.29	31	true	2.6	31	true	.82	18	true	1.1	11	true	4.5	240	true	4.5	230	error	6.1	270	true	9.8	370	unknown	.11	24	unknown	.53	36	true	.35	30	unknown	.33	17	failure	.051	5.7	error (1)	.051	7.5	false(reach)	18	7.3	unknown	7.2	310	unknown	8.1	300
floats-cbmc-regression/float-no-simp6_true-unreach-call.i	true	.081	23	true	1.1	24	true	.14	7.6	true	.094	5.9	true	3.1	220	true	3.6	200	true	3.5	210	true	3.1	180	unknown	.0085	2.9	unknown	.12	11	true	.14	23	true	680	210	failure	.033	5.6	error (1)	.078	6.9	true	.12	5.7	unknown	8.7	340	unknown	8.9	320
floats-cbmc-regression/float-no-simp7_true-unreach-call.i	true	.11	23	true	.99	24	true	.085	7.5	true	.072	5.9	true	3.5	210	true	3.5	190	true	3.5	200	true	3.1	180	unknown	.0098	2.8	unknown	.11	11	true	.095	22	true	670	210	failure	.052	5.4	error (1)	.071	7.1	true	.082	5.5	unknown	8.5	320	unknown	8.4	320
floats-cbmc-regression/float-no-simp8_true-unreach-call.i	true	.28	29	true	2.0	30	true	.23	7.5	true	.17	6.1	true	4.8	240	true	5.0	220	true	4.3	230	true	7.4	330	unknown	.032	10	unknown	.33	22	true	.23	29	true	690	210	failure	.031	5.7	error (1)	.050	7.1	true	.30	5.6	error	9.0	330	error	9.2	330
floats-cbmc-regression/float-rounding1_true-unreach-call.i	true	.26	29	true	2.3	31	true	.083	6.6	unknown	.10	6.1	unknown	4.1	220	error	5.0	220	error	4.7	230	unknown	9.7	400	unknown	.030	11	unknown	.36	23	true	.33	29	unknown	.16	11	failure	.047	5.6	error (1)	.059	7.2	false(reach)	.34	6.6	unknown	8.8	320	unknown	8.9	320
floats-cbmc-regression/float-to-double1_true-unreach-call.i	true	.27	29	true	2.4	31	true	.49	8.1	true	.23	31	true	4.2	230	true	5.1	220	true	5.4	240	true	8.5	370	true	.10	23	unknown	.40	35	true	.34	29	unknown	.21	17	failure	.050	5.6	error (1)	.085	7.1	unknown	.27	5.8	unknown	7.7	310	unknown	7.4	320
floats-cbmc-regression/float-to-double2_true-unreach-call.i	true	.10	22	true	1.1	24	true	.065	7.3	true	.058	5.9	true	3.5	210	true	2.9	190	true	2.8	210	true	3.1	180	unknown	.010	2.7	unknown	.14	11	true	.14	23	true	670	210	failure	.051	5.5	error (1)	.048	7.4	true	.084	5.6	unknown	8.6	320	unknown	8.5	330
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i	true	.13	23	true	1.2	24	true	.081	6.2	true	.078	5.7	true	4.0	230	true	3.0	200	true	3.1	210	true	3.2	190	unknown	.0091	3.2	unknown	.12	11	true	.11	23	true	690	210	failure	.051	5.4	error (1)	.070	7.1	true	.14	5.6	unknown	7.4	300	unknown	7.7	320
floats-cbmc-regression/float11_true-unreach-call.i	true	.12	23	true	1.1	24	true	.073	6.2	true	.082	6.0	true	3.0	210	true	3.4	190	true	3.5	210	true	3.2	190	true	.10	13	unknown	.20	22	true	.15	23	true	660	200	failure	.037	5.6	error (1)	.054	7.3	true	.17	5.8	unknown	8.7	330	unknown	10	330
floats-cbmc-regression/float12_true-unreach-call.i	true	.15	23	true	1.2	24	true	.32	15	true	.54	54	true	2.8	220	true	2.9	200	true	3.1	210	true	4.4	230	true	.099	13	unknown	.15	21	true	.17	23	true	670	200	failure	.029	5.6	error (1)	.042	7.1	unknown	18	5.8	unknown	8.7	320	unknown	8.4	320
floats-cbmc-regression/float13_true-unreach-call.i	true	.13	24	true	1.1	24	true	.47	8.0	true	.23	5.9	true	3.6	220	true	3.1	200	true	3.7	210	true	3.2	180	error (1)	3.8	200	unknown	.16	21	true	.16	23	true	680	210	failure	.028	5.6	error (1)	.067	7.3	true	.082	5.4	unknown	8.1	320	unknown	10	350
floats-cbmc-regression/float14_true-unreach-call.i	true	.18	29	true	2.1	30	true	.37	7.8	true	.12	6.0	true	4.1	230	true	5.1	220	true	4.8	220	true	4.3	200	false(reach)	12	370	unknown	.47	34	true	.17	29	true	680	210	failure	.048	5.7	error (1)	.057	7.3	true	.15	5.7	unknown	9.1	330	unknown	8.0	320
floats-cbmc-regression/float18_true-unreach-call.i	timeout	900	1200	true	1.4	30	true	.59	8.4	true	.15	6.0	true	5.8	260	exception	6.5	330	true	4.9	230	true	4.5	210	error (1)	12	340	unknown	.40	34	true	4.7	33	unknown	.33	17	failure	.056	5.6	error (1)	.076	7.4	timeout	870	15000	unknown	8.0	300	unknown	8.2	320
floats-cbmc-regression/float19_true-unreach-call.i	true	.24	29	true	1.8	31	true	.22	7.5	true	.32	17	true	4.0	230	true	4.9	220	true	4.7	230	true	8.4	330	unknown	.062	14	unknown	.38	26	true	.28	30	true	670	210	failure	.059	5.6	error (1)	.067	7.4	unknown	.30	5.9	unknown	8.6	320	unknown	8.3	320
floats-cbmc-regression/float1_true-unreach-call.i	true	.13	23	true	1.0	24	true	.15	7.7	true	.076	5.9	true	3.0	210	true	3.4	190	true	3.5	210	true	3.1	180	true	.096	13	true	.36	21	true	.11	23	true	680	210	failure	.054	5.6	error (1)	.044	7.3	true	.13	5.6	unknown	9.7	340	unknown	8.5	310
floats-cbmc-regression/float20_true-unreach-call.i	true	.15	28	true	1.2	26	true	.49	25	true	.35	17	true	3.9	240	true	3.7	190	true	3.7	210	true	3.3	180	unknown	.015	3.0	unknown	.18	11	true	.28	25	true	680	210	failure	.025	5.4	error (1)	1.8	37	unknown	.15	6.0	unknown	8.6	320	unknown	8.1	330
floats-cbmc-regression/float22_true-unreach-call.i	true	.11	23	true	1.1	24	true	.11	6.3	true	.19	5.9	true	4.1	230	true	4.0	200	true	3.8	210	true	3.4	190	unknown	.065	14	unknown	.20	22	true	.15	23	true	670	210	failure	.027	5.5	error (1)	1.7	35	true	18	5.8	error	14	360	error	16	350
floats-cbmc-regression/float2_true-unreach-call.i	true	.079	22	true	1.1	24	true	.22	7.7	true	.070	6.1	true	3.6	210	true	3.4	200	true	3.6	210	true	3.2	180	unknown	.010	2.9	unknown	.17	11	true	.11	23	true	680	210	failure	.048	5.5	error (1)	.074	7.2	true	.070	5.3	error	8.2	320	error	8.0	300
floats-cbmc-regression/float3_true-unreach-call.i	true	.13	25	true	1.4	27	true	.18	7.8	true	.49	94	false(reach)	3.8	240	true	3.8	220	true	3.6	210	true	2.7	180	true	.062	13	unknown	.17	21	true	.14	22	true	670	170	failure	.045	5.6	error (1)	.067	7.3	true	.082	5.8	unknown	8.5	330	unknown	9.1	330
floats-cbmc-regression/float4_true-unreach-call.i	true	25	65	true	64	51	true	3.1	97	true	44	150	true	14	260	true	43	290	exception	7.3	230	true	48	380	true	.17	24	unknown	.48	36	true	7.3	37	true	690	210	failure	.032	5.7	error (1)	.089	7.1	unknown	53	7.2	unknown	7.9	310	unknown	7.5	320
floats-cbmc-regression/float5_true-unreach-call.i	true	.17	26	true	1.1	27	true	.46	17	true	.17	32	true	3.1	220	true	3.7	200	true	3.7	210	true	2.8	180	true	.069	13	unknown	.15	21	true	.14	26	true	680	200	failure	.020	5.4	error (1)	.044	7.1	unknown	18	5.8	unknown	8.1	330	unknown	8.6	330
floats-cbmc-regression/float6_true-unreach-call.i	true	.11	24	true	1.1	27	true	1.0	16	true	1.7	12	true	3.9	220	true	3.3	210	true	3.6	220	true	3.4	190	error (1)	4.0	200	unknown	.19	22	true	.30	25	true	670	200	failure	.050	5.6	error (1)	.078	7.1	unknown	.096	6.1	unknown	8.9	330	unknown	10	330
floats-cbmc-regression/float7_true-unreach-call.i	true	.12	23	true	1.0	24	true	.093	7.4	true	.13	17	false(reach)	3.7	230	true	3.4	200	false(reach)	3.3	220	true	3.2	190	true	.066	13	unknown	.15	21	true	.12	22	true	680	210	failure	.028	5.4	error (1)	.061	7.4	true	.18	5.7	unknown	7.4	320	unknown	8.0	320
floats-cbmc-regression/float8_true-unreach-call.i	true	.65	29	true	5.0	30	true	.16	9.0	true	.15	6.5	true	4.7	230	true	5.6	220	true	4.7	230	true	10	370	true	.11	23	unknown	.42	34	true	.73	31	true	680	200	failure	.031	5.6	error (1)	.055	7.4	unknown	.15	6.0	unknown	8.2	300	unknown	8.1	300
float-benchs/float_int_inv_square_false-unreach-call.c	false(reach)	.15	29	false(reach)	.16	25	false(reach)	.14	7.6	false(reach)	.085	5.6	false(reach)	3.7	240	false(reach)	4.4	260	false(reach)	4.5	240	false(reach)	3.9	210	false(reach)	5.2	250	false(reach)	3.2	160	false(reach)	.24	25	unknown	.15	12	failure	.046	5.5	error (1)	.080	7.1	unknown	.095	6.2	unknown	8.5	330	unknown	9.7	340
float-benchs/inv_square_false-unreach-call.c	false(reach)	.18	28	false(reach)	.14	25	false(reach)	.46	12	false(reach)	.083	9.3	false(reach)	4.2	240	false(reach)	4.4	260	false(reach)	3.7	250	false(reach)	3.8	210	false(reach)	5.1	250	unknown	.18	21	false(reach)	.19	24	timeout	900	110	failure	.025	5.4	error (1)	.045	7.1	unknown	18	5.7	unknown	8.4	320	unknown	9.0	340
float-benchs/nan_double_false-unreach-call.c	false(reach)	.11	23	false(reach)	.13	24	false(reach)	.14	7.9	false(reach)	.055	5.9	false(reach)	3.3	230	false(reach)	4.1	240	false(reach)	3.2	230	false(reach)	3.6	210	false(reach)	4.0	220	unknown	.23	21	false(reach)	.13	23	unknown	.24	17	failure	.051	5.6	error (1)	.059	7.2	unknown	.14	5.9	false(reach)	7.9	330	unknown	8.7	330
float-benchs/nan_float_false-unreach-call.c	false(reach)	.11	23	false(reach)	.11	24	false(reach)	.18	7.8	false(reach)	.076	5.9	false(reach)	3.8	230	false(reach)	4.1	240	false(reach)	4.0	240	false(reach)	3.6	210	false(reach)	4.0	220	unknown	.19	21	false(reach)	.10	23	false(reach)	1.5	110	failure	.019	5.4	error (1)	.075	7.3	unknown	.087	6.0	false(reach)	8.7	330	unknown	8.5	320
float-benchs/sin_interpolated_index_false-unreach-call.c	false(reach)	5.9	270	false(reach)	3.5	200	unknown	.12	6.4	unknown	.24	6.1	unknown	3.8	220	error	3.5	200	error	3.2	210	unknown	6.6	310	false(reach)	72	2700	unknown	.30	24	false(reach)	.32	27	unknown	.26	17	failure	.050	5.5	error (1)	.050	7.3	unknown	18	6.0	error	7.5	310	error	8.2	310
float-benchs/inv_square_int_true-unreach-call.c	true	.12	28	true	1.3	27	true	.30	14	true	.13	5.7	true	3.0	220	true	3.4	210	true	3.1	220	true	5.1	240	true	.066	13	true	.47	22	true	.21	27	unknown	.17	12	failure	.043	5.5	error (1)	.065	7.2	unknown	.13	5.9	unknown	8.1	320	unknown	8.3	310
float-benchs/inv_square_true-unreach-call.c	true	.17	26	true	1.1	27	true	.84	14	true	.33	11	true	3.1	220	true	3.8	200	exception	3.2	230	true	4.4	250	error (1)	13	470	unknown	.24	21	true	.18	24	timeout	900	110	failure	.022	5.5	error (1)	.042	7.4	unknown	18	5.8	unknown	8.7	330	unknown	8.9	320
float-benchs/nan_double_range_true-unreach-call.c	true	.14	23	true	.97	24	true	.18	8.5	true	.11	6.4	true	3.0	210	true	3.6	200	true	3.6	210	true	4.3	240	error (1)	5.8	270	unknown	.17	21	true	.098	23	unknown	.29	17	failure	.032	5.6	error (1)	.049	7.2	unknown	.072	5.7	unknown	8.7	320	unknown	8.2	320
float-benchs/nan_float_range_true-unreach-call.c	true	.13	23	true	1.0	24	true	.18	13	true	.16	28	true	2.8	210	true	3.0	200	true	3.5	210	true	4.5	240	error (1)	5.9	270	unknown	.15	21	true	.17	23	true	690	210	failure	.033	5.5	error (1)	.064	7.4	unknown	.081	5.7	unknown	8.3	310	unknown	8.5	320
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c	true	870	320	error	850	670	true	.10	6.0	true	.20	6.0	unknown	4.0	210	error	3.1	200	error	3.8	210	unknown	7.4	390	false(reach)	260	3900	unknown	.28	23	timeout	900	220	unknown	.27	17	failure	.048	5.4	error (1)	.071	6.9	unknown	18	6.1	error	8.4	320	error	8.0	310
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c	true	760	320	error	850	650	true	.17	6.4	true	.29	5.7	unknown	3.4	210	error	4.1	200	error	3.8	210	unknown	7.3	390	false(reach)	270	3100	unknown	.25	24	timeout	900	230	unknown	.29	17	failure	.032	5.6	error (1)	.044	6.9	unknown	18	5.9	error	8.5	310	error	7.9	320
float-benchs/sin_interpolated_index_true-unreach-call.c	true	650	310	error	850	640	true	.20	6.2	true	.26	5.6	unknown	3.3	210	error	3.9	200	error	3.7	210	unknown	6.9	320	false(reach)	71	3000	unknown	.22	23	timeout	900	180	unknown	.30	17	failure	.030	5.6	error (1)	.038	7.1	unknown	18	6.1	error	9.4	340	error	7.2	320
float-benchs/sin_interpolated_smallrange_true-unreach-call.c	timeout	900	310	true	850	4400	true	.10	6.1	true	.26	6.0	unknown	3.4	210	error	4.8	230	error	3.8	210	unknown	6.9	390	unknown	900	11000	unknown	.22	23	timeout	900	380	unknown	.29	17	failure	.040	5.6	error (1)	.061	7.3	unknown	.10	6.1	error	8.4	310	error	9.1	330
../../sv-benchmarks/c/	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)	status	cputime (s)	memUsage (MB)
total tasks	81	5300	7500	81	21000	15000	81	3700	2900	81	9600	6100	81	17000	300000	81	21000	33000	81	13000	320000	81	19000	31000	81	18000	62000	81	21	1900	81	9300	10000	81	45000	14000	81	3.1	450	81	8.2	640	81	1900	15000	81	700	26000	81	710	26000
correct results	79	3500	6000	78	18000	13000	77	3700	2900	71	2400	4900	55	5700	83000	56	4900	19000	42	1200	37000	56	2500	17000	43	4500	21000	4	4.3	220	77	5700	9400	48	32000	9800	0			0			15	19	85	2	17	660	0
correct true	57	3400	4200	56	18000	11000	59	3200	2300	53	2100	3500	35	2500	9200	36	2500	8800	25	94	5400	35	2000	9200	22	3100	810	3	1.2	64	55	3800	5300	47	32000	9700	0			0			15	19	85	0			0
correct false	22	170	1800	22	600	2000	18	570	560	18	290	1400	20	3200	73000	20	2400	10000	17	1100	31000	21	540	7400	21	1500	20000	1	3.2	160	22	1900	4200	1	1.5	110	0			0			0			2	17	660	0
incorrect results	0			0			0			0			3	18	930	1	300	800	2	12	700	1	300	930	5	1400	11000	0			0			17	11000	3500	0			0			3	19	21	0			0
incorrect true	0			0			0			0			0			0			0			0			0			0			0			17	11000	3500	0			0			0			0			0
incorrect false	0			0			0			0			3	18	930	1	300	800	2	12	700	1	300	930	5	1400	11000	0			0			0			0			0			3	19	21	0			0
score (81 tasks, max score: 140)	136			134			136			124			42			76			35			75			-15			7			132			-449			0			0			-18			2			0
Run set	2ls.sv-comp16.Floats			cbmc.sv-comp16.Floats			ceagle.sv-comp16			ceagle-absref.sv-comp16.Floats			cpa-bam.sv-comp16.Floats			cpa-kind.sv-comp16.Floats			cpa-refsel.sv-comp16.Floats			cpa-seq.sv-comp16.Floats			esbmc.sv-comp16.Floats			esbmcdepthk.sv-comp16.Floats			impara.sv-comp16.Floats			pacman.sv-comp16.Floats			seahorn.sv-comp16.Floats			smack.sv-comp16.Floats			symbiotic3.sv-comp16.Floats			uautomizer.sv-comp16.Floats			ukojak.sv-comp16.Floats