results.2016-09-03_1437 differences

Tool	CPAchecker 1.6.1-svn 22870
Limits	timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 2
OS	Linux 4.4.0-34-generic
System	CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135148 MB
Run set	bmc-bitprecise.BMC.ProductLines									k-induction-bitprecise.k-Induction.ProductLines												predicateAnalysis-bitprecise.PredicateAbstraction.ProductLines															impact-bitprecise.Impact.ProductLines
Options	-heap 10000M -noout -bmc -setprop solver.solver=MATHSAT5 -setprop cpa.predicate.encodeBitvectorAs=BITVECTOR -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.bounds.maxLoopIterationsUpperBound=0 -setprop cpa.bounds.maxLoopIterations=1 -setprop cpa.bounds.maxLoopIterationAdjusterFactory=INCREMENT									-heap 10000M -noout -sv-comp16--k-induction -setprop limits.time.cpu.thread=10000s												-heap 10000M -noout -predicateAnalysis-PredAbsRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC															-heap 10000M -noout -predicateAnalysis-ImpactRefiner-ABEl-bitprecise -setprop cpa.predicate.encodeFloatAs=FLOAT -setprop analysis.checkCounterexamples=true -setprop counterexample.checker=CBMC -setprop cpa.forcedCovering=cpa.predicate.PredicateForcedCovering
test/programs/benchmarks/product-lines/	status	cputime (s)	walltime (s)	memUsage	host	k	BMC formula creation (s)	SMT check (s)	Bounds check (s)	status	cputime (s)	walltime (s)	memUsage	host	k	BMC formula creation (s)	SMT check (s)	Invariant generation (s)	Bounds check (s)	Induction formula creation (s)	Induction check (s)	status	cputime (s)	walltime (s)	memUsage	host	Refinement (s)	Precision adjustment (s)	CPA algorithm (s)	Post operator (s)	Prec operator (s)	Abstraction (s)	Solving (s)	Model enumeration (s)	SMT without itp (s)	Boolean abstraction (s)	status	cputime (s)	walltime (s)	memUsage	host	Attempted forced coverings	Refinement (s)	Precision adjustment (s)	CPA algorithm (s)	Post operator (s)	Prec operator (s)	Abstraction (s)	Solving (s)	Model enumeration (s)	SMT without itp (s)	Forced covering (s)	Successful forced coverings	Boolean abstraction (s)
elevator_spec14_productSimulator_false-unreach-call.cil.c	false(reach)	214	190	2360836096		1	11.8	2.57		false(reach)	523	262	5285154816		1	17.7	2.40	200				timeout	1000	967	4689915904												timeout	1000	968	4577275904
elevator_spec1_product18_false-unreach-call.cil.c	false(reach)	18.7	10.1	571920384		3	1.86	.004	.014	false(reach)	96.9	48.9	1659928576		3	3.66	.005	13.2	.023	19.0	3.83	timeout	903	869	1437609984		3.93	833	860	13.5	831	831	13.7	813	827	828	false(reach)	87.7	60.7	1618284544		6	17.4	6.72	32.8	8.58	5.89	5.66	3.42	1.39	4.89	10.8	1	4.82
elevator_spec1_product22_false-unreach-call.cil.c	false(reach)	19.7	10.7	622419968		3	2.03	.018	.009	false(reach)	113	57.1	2000007168		3	3.28	.004	19.2	.028	21.3	5.61	timeout	903	868	1955151872		9.11	817	854	17.9	814	813	32.7	775	807	808	false(reach)	104	76.5	2036858880		4	20.7	9.19	42.7	12.2	8.13	7.84	4.98	1.84	7.06	12.1	1	6.84
elevator_spec1_product24_false-unreach-call.cil.c	false(reach)	18.9	10.4	568958976		3	1.75	.004	.020	false(reach)	130	65.8	2269085696		3	3.31	.006	21.6	.042	25.6	7.90	timeout	903	869	1802854400		5.05	824	859	17.8	822	822	18.8	798	817	818	false(reach)	121	92.7	2087391232		4	22.7	9.57	57.2	11.8	8.46	8.22	4.74	2.41	7.37	25.9	1	7.18
elevator_spec1_product26_false-unreach-call.cil.c	false(reach)	18.6	10.0	571379712		3	1.72	.003	.012	false(reach)	108	54.4	1692684288		3	3.17	.004	15.3	.028	19.4	3.74	timeout	903	869	1624776704		5.95	826	858	14.6	824	823	23.2	795	818	818	false(reach)	92.7	64.9	1685303296		6	18.3	8.06	36.3	9.43	6.94	6.74	4.11	1.76	5.95	11.6	1	5.88
elevator_spec1_product28_false-unreach-call.cil.c	false(reach)	18.7	10.2	586661888		3	1.91	.003	.035	false(reach)	106	53.7	1785593856		3	3.88	.005	15.5	.033	19.6	4.41	timeout	904	868	1719083008		8.18	819	855	16.4	817	816	33.8	776	810	811	false(reach)	96.2	70.2	1891782656		6	17.6	11.1	41.8	10.2	9.70	9.35	5.04	3.21	8.49	12.2	0	8.27
elevator_spec1_product30_false-unreach-call.cil.c	false(reach)	19.8	10.9	722743296		3	2.14	.004	.006	false(reach)	115	58.1	2209026048		3	2.81	.004	19.9	.009	19.4	7.39	timeout	903	870	1689251840		4.93	828	860	15.7	826	825	20.5	801	821	822	false(reach)	145	116	2030002176		6	22.7	9.24	81.2	11.1	7.74	7.53	4.34	2.18	6.62	52.4	1	6.53
elevator_spec1_product32_false-unreach-call.cil.c	false(reach)	18.9	10.3	587161600		3	1.79	.004	.023	false(reach)	129	65.0	2269237248		3	3.32	.006	23.1	.056	23.6	10.8	timeout	903	871	1559007232		5.04	829	861	15.9	827	826	18.7	804	822	823	false(reach)	116	86.3	2078511104		4	22.7	11.9	50.4	11.8	10.1	9.85	5.56	3.24	8.99	17.4	1	8.81
elevator_spec1_productSimulator_false-unreach-call.cil.c	false(reach)	47.8	27.6	1122344960		3	12.1	.346	.771	false(reach)	212	107	4389982208		3	8.56	.554	58.6	1.27	36.1	9.90	timeout	904	867	2549751808		9.12	792	852	28.8	787	786	24.3	756	780	781	timeout	1000	967	4215369728
elevator_spec2_productSimulator_false-unreach-call.cil.c	false(reach)	42.7	24.5	1226792960		3	10.8	.346	.734	false(reach)	199	100	4146581504		3	8.76	.537	.005	1.83	33.2	12.4	timeout	905	872	2794962944		11.4	786	854	34.6	781	780	27.3	747	775	775	timeout	1000	964	4726034432
elevator_spec9_product28_false-unreach-call.cil.c	false(reach)	19.4	10.6	541548544		3	1.97	.004	.007	false(reach)	108	54.5	1867890688		3	4.02	.004	17.6	.030	16.9	4.34	timeout	903	871	1715810304		5.74	834	861	12.3	832	831	20.9	806	827	828	false(reach)	109	81.5	1872302080		6	22.6	13.5	47.8	11.2	12.5	12.2	4.88	6.20	11.5	15.0	0	11.1
elevator_spec9_product32_false-unreach-call.cil.c	false(reach)	20.3	11.1	626827264		3	2.12	.003	.028	false(reach)	120	60.6	2287783936		3	3.14	.006	.004	.034	18.0	6.53	timeout	904	871	1742155776		3.63	828	862	17.4	826	826	18.0	804	822	822	false(reach)	157	126	2402107392		6	25.9	20.6	87.1	15.1	19.2	18.9	7.58	10.2	18.2	39.6	0	17.8
elevator_spec9_productSimulator_false-unreach-call.cil.c	false(reach)	43.9	25.4	1171914752		3	10.8	.465	.773	false(reach)	218	110	3793092608		3	9.37	.575	60.6	1.28	41.6	8.81	timeout	904	871	2564108288		11.3	801	854	25.6	796	795	20.3	771	791	791	timeout	1000	965	4426334208
elevator_spec13_product23_true-unreach-call.cil.c	timeout	903	879	2052317184		8054	83.5	.973	355	timeout	902	452	5578674176		1	4.20	.009	368	.049			true	270	248	2065207296		168	61.9	75.2	6.32	60.9	60.7	46.5	4.33	50.9	47.9	timeout	904	876	2035798016		163	819	2.54	40.8	20.4	.604	.044	.00	.00	1.25	2.46	119
elevator_spec1_product03_true-unreach-call.cil.c	true	20.2	10.6	494444544		9	3.64	.001	.082	true	283	142	4728242176		9	5.23	.00	97.7	.117	20.7	101	timeout	903	874	1583476736		17.0	834	852	7.31	832	832	32.2	793	825	826	true	97.0	75.1	1313669120		13	22.4	9.34	48.1	6.25	8.93	8.83	5.35	2.37	8.05	27.1	1	7.74
elevator_spec1_product09_true-unreach-call.cil.c	true	19.0	9.99	521965568		9	3.00	.002	.112	true	227	114	4608782336		9	4.89	.002	70.8	.092	21.2	70.8	timeout	902	873	1425219584		11.5	842	857	5.98	840	840	24.4	811	835	836	true	104	81.2	1321299968		14	24.7	9.47	51.8	5.74	8.76	8.62	4.83	2.71	7.96	31.5	1	7.56
elevator_spec1_product11_true-unreach-call.cil.c	true	18.7	9.93	509526016		9	2.96	.00	.062	true	267	134	4704636928		9	5.29	.020	.005	.131	21.8	89.7	timeout	903	871	1994153984		15.5	817	851	16.0	815	814	48.6	757	805	806	true	97.4	75.7	1342328832		13	21.5	9.42	49.7	6.08	8.24	8.10	5.16	1.74	7.33	29.0	1	6.95
elevator_spec1_product17_true-unreach-call.cil.c	true	19.3	10.2	506802176		9	3.10	.00	.096	true	220	111	4434677760		9	5.08	.00	64.6	.119	22.4	66.2	timeout	904	871	1803423744		17.2	820	849	12.4	818	817	51.2	757	808	809	true	74.2	52.8	1226637312		9	15.3	7.71	33.0	5.84	7.18	7.08	4.10	1.94	6.21	14.1	1	6.05
elevator_spec1_product21_true-unreach-call.cil.c	true	18.6	9.92	524328960		9	2.83	.00	.065	true	540	271	5255311360		9	4.42	.012	222	.103	25.4	222	timeout	903	871	1555607552		6.73	834	859	11.9	831	831	26.8	799	826	827	timeout	903	877	1868283904		21	44.5	12.8	827	8.64	12.0	11.8	7.63	2.92	12.0	798	1	10.6
elevator_spec1_product23_true-unreach-call.cil.c	true	22.5	11.8	604364800		9	4.13	.001	.116	true	655	328	5547192320		9	4.57	.001	269	.141	28.6	274	timeout	903	872	1337769984		7.19	837	860	11.0	836	835	23.8	807	831	831	timeout	903	878	2147254272		34	127	18.1	746	10.4	16.7	16.4	9.82	4.94	18.5	709	1	14.8
elevator_spec1_product25_true-unreach-call.cil.c	true	19.2	10.1	545824768		9	2.94	.00	.085	true	269	135	4712402944		9	4.99	.002	89.2	.121	21.6	93.0	timeout	902	876	1184313344		9.23	851	862	4.76	850	850	14.7	832	846	847	true	77.3	55.3	1234993152		9	16.6	7.56	34.1	6.22	6.99	6.87	4.39	1.53	6.11	15.3	1	5.95
elevator_spec1_product27_true-unreach-call.cil.c	true	20.7	10.8	506474496		9	3.30	.00	.090	true	350	176	4964069376		9	5.01	.001	127	.127	20.4	134	timeout	902	871	1682411520		15.4	830	851	9.65	828	828	36.1	785	821	822	true	130	107	1400811520		18	23.6	10.6	78.2	7.26	9.92	9.71	6.02	2.52	8.94	54.5	2	8.55
elevator_spec1_product29_true-unreach-call.cil.c	true	18.6	9.96	520687616		9	2.96	.003	.066	true	624	313	5390364672		9	4.41	.001	261	.101	25.3	262	timeout	903	872	1487298560		6.13	836	861	12.0	834	833	30.9	797	828	828	timeout	903	878	2124349440		21	47.6	14.1	826	9.28	13.3	13.1	7.20	4.46	12.6	795	1	11.7
elevator_spec1_product31_true-unreach-call.cil.c	true	20.2	10.7	595464192		9	3.54	.002	.097	true	748	375	5889708032		9	4.68	.001	308	.111	26.3	323	timeout	903	870	1778200576		10.1	827	855	13.0	824	824	43.1	774	817	818	timeout	903	877	2343096320		27	80.1	18.6	792	9.55	17.7	17.5	11.3	4.60	19.8	757	1	15.9
elevator_spec2_product11_true-unreach-call.cil.c	true	17.3	9.11	547913728		5	2.24	.00	.021	true	114	57.3	2312527872		5	4.56	.00	21.2	.059	18.7	19.8	timeout	902	872	1731936256		22.3	828	845	7.00	827	826	34.3	783	817	821	true	132	110	1367408640		11	44.5	15.5	60.8	6.86	14.8	14.6	5.69	7.70	15.6	33.0	1	13.4
elevator_spec2_product21_true-unreach-call.cil.c	true	19.0	10.1	459448320		5	2.53	.001	.027	true	137	68.9	2540482560		5	3.51	.001	.004	.039	17.4	28.6	timeout	903	871	1857015808		23.3	814	843	11.3	812	812	40.6	762	803	805	timeout	903	878	2276995072		8	20.7	13.0	853	8.42	12.2	12.0	6.06	4.94	11.5	824	0	11.0
elevator_spec2_product29_true-unreach-call.cil.c	true	17.0	9.11	511938560		5	2.09	.00	.021	true	172	86.5	3350327296		5	4.32	.002	48.5	.048	17.6	43.0	timeout	903	874	1638486016		8.29	833	860	13.3	831	830	37.2	786	824	825	timeout	903	878	1860743168		17	68.1	21.5	805	10.0	20.6	20.3	8.36	10.6	22.9	765	0	19.0
elevator_spec2_product31_true-unreach-call.cil.c	true	18.0	9.48	526667776		5	2.46	.001	.055	true	185	93.2	3612209152		5	4.34	.001	.007	.052	19.2	49.1	timeout	903	875	1503956992		5.26	841	864	10.7	840	839	24.8	810	835	835	true	437	412	1797488640		16	105	25.8	302	9.71	24.8	24.5	10.3	12.6	31.0	258	1	23.0
elevator_spec3_product09_true-unreach-call.cil.c	true	22.0	11.8	605933568		12	3.88	.001	.199	true	89.6	45.3	1519538176		1	5.35	.008	10.9	.051	9.01	7.32	true	82.1	62.7	1383698432		19.2	29.3	38.7	4.89	28.6	28.5	19.0	6.00	25.0	11.0	timeout	903	881	2678587392		41	492	.979	384	6.97	.185	.001	.00	.00	25.4	368	0
elevator_spec3_product17_true-unreach-call.cil.c	true	20.5	11.1	589606912		12	3.43	.001	.126	true	87.3	44.3	1469468672		1	4.75	.00	11.4	.017	7.26	6.66	true	147	127	1424769024		18.7	88.7	104	7.84	87.8	87.6	33.7	47.8	81.6	57.4	timeout	904	881	2540867584		45	458	.884	418	8.20	.199	.002	.00	.00	23.8	400	0
elevator_spec3_product18_true-unreach-call.cil.c	true	22.6	12.6	719413248		12	3.84	.001	.165	true	97.9	49.4	1732304896		1	3.27	.00	14.9	.042	12.4	3.55	true	132	107	1695625216		28.6	55.5	72.9	8.81	54.3	54.1	25.1	24.0	49.1	31.1	timeout	903	877	3056513024		32	567	1.49	305	12.3	.265	.003	.00	.00	16.3	280	0
elevator_spec3_product21_true-unreach-call.cil.c	true	23.8	13.3	744194048		12	4.19	.00	.127	true	94.2	47.5	1561001984		1	4.12	.00	.005	.024	11.3	2.96	true	125	99.9	1608118272		28.1	51.8	66.9	8.26	50.6	50.4	28.1	17.8	45.9	26.4	timeout	904	880	2379870208		15	320	1.12	555	9.02	.166	.012	.00	.00	3.92	538	0
elevator_spec3_product22_true-unreach-call.cil.c	true	23.9	13.7	753270784		12	3.81	.001	.174	true	130	65.8	2323156992		1	3.04	.00	26.7	.030	14.5	2.72	true	229	204	2128195584		33.6	136	164	15.5	135	134	40.9	86.9	128	102	timeout	904	877	2885001216		17	542	1.69	330	15.5	.301	.003	.00	.00	6.79	300	0
elevator_spec3_product25_true-unreach-call.cil.c	true	21.9	11.9	595304448		12	3.61	.004	.196	true	82.0	41.4	1488314368		1	4.55	.001	9.78	.037	8.42	6.40	true	133	112	1443622912		20.1	72.9	86.5	6.89	72.2	71.9	25.8	41.2	67.0	48.6	timeout	903	881	2976907264		39	523	1.07	352	8.70	.196	.003	.00	.00	29.0	333	0
elevator_spec3_product26_true-unreach-call.cil.c	true	22.3	12.6	754266112		12	3.41	.00	.125	true	96.7	48.8	1833664512		1	3.42	.001	15.0	.008	11.8	3.24	true	212	184	1867034624		27.3	129	152	11.6	128	127	36.0	84.9	121	96.3	timeout	904	878	3054411776		28	628	1.62	245	12.6	.285	.005	.00	.00	9.57	220	0
elevator_spec3_product29_true-unreach-call.cil.c	true	23.1	12.6	723816448		12	3.79	.00	.166	true	102	51.6	1738919936		1	3.65	.00	16.8	.036	10.4	2.28	true	182	159	1733185536		30.4	107	123	7.97	106	106	31.5	69.5	101	78.5	timeout	904	879	2448330752		15	356	.894	518	8.20	.159	.003	.00	.00	4.01	502	0
elevator_spec3_product30_true-unreach-call.cil.c	true	25.6	14.5	782188544		12	3.94	.00	.206	true	111	56.2	3356172288		1	3.69	.001	19.1	.030	14.2	2.66	true	287	262	2101661696		34.2	194	222	15.8	193	192	41.5	144	186	158	timeout	903	876	2707369984		12	448	1.57	422	14.3	.353	.004	.00	.00	4.76	395	0
elevator_spec9_product09_true-unreach-call.cil.c	true	17.3	9.18	483938304		5	2.27	.00	.038	true	104	52.7	1908318208		5	4.05	.00	17.2	.256	18.0	15.6	timeout	903	874	1195073536		6.61	848	862	7.09	847	847	14.7	828	843	844	true	125	103	1346899968		11	40.9	12.7	57.4	6.87	12.1	11.9	5.46	5.28	12.4	32.2	1	10.8
elevator_spec9_product27_true-unreach-call.cil.c	true	17.4	9.30	426369024		5	2.23	.00	.026	true	117	59.1	2160078848		5	4.45	.00	.004	.026	17.6	21.3	timeout	903	876	1176281088		6.82	850	864	6.72	849	849	11.5	834	845	846	true	133	111	1442009088		11	46.5	13.8	60.1	6.80	13.2	13.0	5.71	6.13	13.6	33.6	1	11.9
elevator_spec9_product31_true-unreach-call.cil.c	true	19.0	10.1	517754880		5	2.69	.00	.032	true	159	80.1	3115343872		5	4.55	.001	.004	.050	20.9	34.6	timeout	903	872	1509376000		11.7	833	856	10.3	831	830	32.7	790	823	825	true	768	743	2022514688		16	108	24.6	630	9.55	23.6	23.4	9.88	12.1	29.0	587	1	22.0
email_spec1_product14_false-unreach-call.cil.c	unknown	159	148	2750676992		3	4.28	.564	.413	timeout	1000	734	6509584384									timeout	902	886	794234880		.393	876	881	2.50	876	876	2.02	868	870	875	unknown	185	168	2943733760		6	9.95	.367	7.33	3.04	.083	.002	.00	.00	.769	1.52	1
email_spec1_product15_false-unreach-call.cil.c	unknown	145	134	2617896960		3	3.77	.692	.215	timeout	1000	718	6148550656									timeout	1000	984	2749620224												unknown	169	154	2724945920		6	5.46	.324	5.47	2.18	.059	.001	.00	.00	.103	1.16	1
email_spec1_product16_false-unreach-call.cil.c	unknown	127	117	2618933248		3	3.90	.735	.229	timeout	1000	712	6212640768									timeout	1000	984	2729197568												unknown	160	146	2698522624		6	5.82	.248	5.40	1.82	.037	.00	.00	.00	.084	1.00	1
email_spec1_product20_false-unreach-call.cil.c	unknown	713	690	3074162688		3	5.49	2.21	.283	timeout	1000	501	6362173440									timeout	902	886	819040256		.682	876	881	2.36	876	875	2.73	867	870	874	timeout	1000	978	3146711040
email_spec1_product21_false-unreach-call.cil.c	unknown	762	738	3128766464		3	6.64	3.01	.357	timeout	1000	501	6611165184									timeout	902	881	967720960		1.17	869	875	3.21	868	868	8.19	850	858	861	timeout	1000	976	3187695616
email_spec1_product22_false-unreach-call.cil.c	unknown	169	156	2630201344		3	4.25	.729	.385	timeout	1000	694	6593449984									timeout	1000	979	3025178624												unknown	183	168	2772299776		6	6.32	.755	5.78	2.04	.096	.002	.00	.00	.230	1.29	1
email_spec1_product26_false-unreach-call.cil.c	unknown	800	776	3228188672		3	6.34	3.96	.297	timeout	1000	501	7145947136									timeout	1000	977	3306078208												timeout	1000	976	3248214016
email_spec1_product29_false-unreach-call.cil.c	unknown	169	157	2766667776		3	3.80	.524	.252	timeout	1000	729	6379610112									timeout	1000	977	3155820544												unknown	187	170	3070951424		6	10.1	.983	9.32	3.41	.059	.001	.00	.00	.506	2.32	1
email_spec1_product30_false-unreach-call.cil.c	unknown	155	144	2623008768		3	4.11	.784	.295	timeout	1000	699	6299815936									timeout	1000	981	2832674816												unknown	184	168	2739290112		6	5.36	.251	6.87	2.22	.073	.004	.00	.00	.105	1.95	1
email_spec1_product31_false-unreach-call.cil.c	unknown	145	131	2753433600		3	4.21	.673	.211	timeout	1000	685	6791446528									timeout	1000	976	3024019456												unknown	202	186	2782269440		6	5.69	.386	7.07	2.32	.087	.001	.00	.00	.283	1.89	1
email_spec1_product32_false-unreach-call.cil.c	unknown	655	632	3219218432		3	6.81	3.48	.261	timeout	1000	501	7201665024									timeout	1000	977	3280826368												timeout	1000	977	3281887232
email_spec1_product33_false-unreach-call.cil.c	unknown	174	158	2770472960		3	4.39	.967	.307	timeout	1000	676	6773972992									timeout	1000	979	2988167168												unknown	203	187	2799403008		6	5.33	.297	7.61	2.52	.036	.002	.00	.00	.282	2.00	1
email_spec27_product17_false-unreach-call.cil.c	unknown	357	346	2765504512		3	3.49	.508	.356	timeout	1000	501	6274134016									timeout	902	885	883068928		.692	875	880	2.05	875	875	3.93	862	866	872	unknown	224	208	3021271040		6	11.3	.406	7.16	3.12	.063	.002	.00	.00	.425	1.45	1
email_spec27_product18_false-unreach-call.cil.c	unknown	233	222	2624438272		3	3.75	.658	.237	timeout	1000	556	6429462528									timeout	1000	981	2770452480												unknown	167	153	2749464576		6	6.17	.689	5.24	1.88	.059	.001	.00	.00	.161	.985	1
email_spec27_product19_false-unreach-call.cil.c	unknown	291	279	2618368000		3	3.85	.969	.301	timeout	1000	584	6167572480									timeout	1000	979	2929430528												unknown	187	172	2760302592		6	6.70	.325	5.42	1.96	.054	.001	.00	.00	.168	1.11	1
email_spec27_product24_false-unreach-call.cil.c	unknown	236	224	2677403648		3	4.22	.809	.425	timeout	1000	576	6220177408									timeout	1000	980	3014373376												unknown	195	179	2764591104		6	6.50	.286	6.33	2.58	.052	.001	.00	.00	.220	1.42	1
email_spec27_product29_false-unreach-call.cil.c	unknown	376	360	2929532928		3	3.82	.862	.234	timeout	1000	501	7343742976									timeout	1000	977	3211317248												unknown	226	209	3049218048		6	12.4	.371	7.51	2.86	.075	.008	.00	.00	.259	1.55	1
email_spec27_product30_false-unreach-call.cil.c	unknown	325	313	2728300544		3	4.73	1.07	.251	timeout	1000	513	7200337920									timeout	1000	982	2860871680												unknown	250	235	2754068480		6	5.16	.269	6.41	2.56	.037	.003	.00	.00	.151	1.40	1
email_spec27_product31_false-unreach-call.cil.c	unknown	286	271	2822045696		3	4.40	.941	.267	timeout	1000	538	7102279680									timeout	1000	982	2904842240												unknown	194	177	2871238656		6	6.28	.362	7.27	2.91	.095	.001	.00	.00	.252	1.75	1
email_spec27_product33_false-unreach-call.cil.c	unknown	334	317	2844008448		3	5.19	1.23	.241	timeout	1000	501	7687585792									timeout	1000	978	3042279424												unknown	201	185	2872516608		6	6.12	.713	7.88	2.47	.040	.001	.00	.00	.170	2.39	1
email_spec3_product13_false-unreach-call.cil.c	unknown	14.6	7.92	449478656		1	1.51	.003		timeout	903	806	4685447168		1	5.65	.049	733				timeout	1000	980	2931736576												unknown	287	271	2758402048		6	5.29	.232	4.99	1.68	.043	.002	.00	.00	.111	1.03	1
email_spec3_product17_false-unreach-call.cil.c	unknown	16.7	9.00	452325376		1	1.82	.003		timeout	902	807	4713312256		1	5.42	.029	.004				timeout	905	883	1068785664		3.82	864	870	2.42	863	863	13.0	835	848	851	timeout	1000	975	3194916864
email_spec3_product18_false-unreach-call.cil.c	unknown	15.6	8.44	432087040		1	1.76	.004		timeout	902	803	5662883840		1	3.09	.209	.021				timeout	1000	974	3070562304												timeout	1000	978	2871578624
email_spec3_product19_false-unreach-call.cil.c	unknown	15.6	8.41	459255808		1	1.87	.015		timeout	902	814	5291511808		1	5.53	.036	.005				timeout	1000	974	3089301504												timeout	1000	979	2902622208
email_spec3_product23_false-unreach-call.cil.c	unknown	16.2	8.68	477306880		1	1.79	.003		timeout	908	794	5947121664		1	6.32	.015	706				timeout	902	884	864292864		1.24	873	878	2.32	873	873	4.53	862	867	869	timeout	1000	974	3273195520
email_spec3_product24_false-unreach-call.cil.c	unknown	16.5	8.84	453406720		1	1.83	.002		timeout	903	794	5755281408		1	4.55	.343	711				timeout	1000	974	3078287360												timeout	1000	976	2929307648
email_spec3_product25_false-unreach-call.cil.c	unknown	16.7	9.02	484884480		1	1.82	.003		timeout	903	784	6153580544		1	6.03	.019	685				timeout	1000	974	3420037120												timeout	1000	976	3268833280
email_spec3_product27_false-unreach-call.cil.c	unknown	16.7	9.01	467431424		1	1.70	.002		timeout	902	771	6366494720		1	5.33	.032	661				timeout	902	884	936841216		1.37	873	878	2.27	872	872	5.70	859	865	868	timeout	1000	973	3287515136
email_spec3_product28_false-unreach-call.cil.c	unknown	16.6	8.94	471191552		1	2.29	.004		timeout	902	803	5069561856		1	5.36	.022	.005				timeout	1000	980	2987175936												unknown	289	270	2803924992		6	7.83	.299	5.02	2.17	.074	.001	.00	.00	.191	.934	1
email_spec3_product29_false-unreach-call.cil.c	unknown	17.0	9.14	450338816		1	1.81	.003		timeout	902	801	5921546240		1	5.39	.075	.004				timeout	1000	973	3317268480												timeout	1000	973	3217981440
email_spec3_product30_false-unreach-call.cil.c	unknown	15.5	8.31	468623360		1	1.88	.002		timeout	902	789	6163546112		1	5.37	.021	.004				timeout	1000	973	3116777472												timeout	1000	978	2960285696
email_spec3_product31_false-unreach-call.cil.c	unknown	17.3	9.15	465907712		1	1.82	.004		timeout	903	792	5939171328		1	5.39	.011	707				timeout	1000	977	3005747200												timeout	1000	976	3046612992
email_spec3_product32_false-unreach-call.cil.c	unknown	16.5	8.84	449519616		1	1.77	.003		timeout	902	769	6518104064		1	5.40	.045	.013				timeout	903	883	940625920		2.07	870	876	2.57	870	870	6.39	858	864	865	timeout	1000	974	3315032064
email_spec3_product33_false-unreach-call.cil.c	unknown	16.2	8.76	481583104		1	1.96	.003		timeout	902	765	6475051008		1	5.74	.155	.017				timeout	1000	974	3170349056												timeout	1000	977	3055747072
email_spec3_product34_false-unreach-call.cil.c	unknown	16.9	9.18	464302080		1	1.76	.005		timeout	902	752	7142518784		1	5.28	.021	.004				timeout	902	883	919097344		1.94	871	876	2.04	870	870	6.77	858	865	865	timeout	1000	974	3374116864
email_spec3_product35_false-unreach-call.cil.c	unknown	17.9	9.58	463048704		1	1.87	.002		timeout	902	728	7245975552		1	5.21	.030	575				timeout	902	883	963444736		2.08	871	876	2.65	870	870	7.11	858	865	864	timeout	1000	974	3363684352
email_spec3_productSimulator_false-unreach-call.cil.c	unknown	38.8	24.9	1391112192		1	4.05	.090		timeout	907	695	7687184384		1	5.65	.157	.005				timeout	904	879	1690759168		4.33	848	867	10.2	847	847	29.1	804	833	812	timeout	1000	967	5635235840
email_spec4_product18_false-unreach-call.cil.c	unknown	201	190	2613141504		3	3.67	.632	.209	timeout	1000	573	6701621248									unknown	167	154	2695208960		1.75	4.16	8.58	2.15	3.88	3.79	2.84	.343	3.18	1.50	unknown	174	161	2684792832		6	4.71	.686	5.11	1.77	.040	.00	.00	.00	.054	.897	1
email_spec4_product19_false-unreach-call.cil.c	unknown	257	246	2636759040		3	4.39	.535	.325	timeout	1000	595	6597558272									unknown	206	193	2731372544		2.03	4.58	9.10	2.13	4.29	4.25	2.63	.835	3.47	2.17	unknown	155	140	2772652032		6	6.61	.806	4.95	1.66	.083	.001	.00	.00	.059	1.00	1
email_spec4_product23_false-unreach-call.cil.c	unknown	825	803	3088175104		3	5.21	3.40	.260	timeout	1000	501	7456501760									timeout	1000	980	3197706240												timeout	1000	978	3060568064
email_spec4_product24_false-unreach-call.cil.c	unknown	233	222	2679025664		3	4.47	.529	.284	timeout	1000	595	6980403200									timeout	1000	979	2924163072												unknown	175	159	2752454656		6	6.16	.239	5.71	2.38	.056	.003	.00	.00	.123	1.13	1
email_spec4_product27_false-unreach-call.cil.c	unknown	856	832	3192770560		3	7.38	3.79	.328	timeout	1000	501	7620706304									timeout	1000	978	3216269312												timeout	1000	978	3096064000
email_spec4_product30_false-unreach-call.cil.c	unknown	267	254	2655657984		3	4.55	.728	.452	timeout	1000	582	6884323328									unknown	192	179	2741202944		1.98	4.28	8.77	2.27	4.03	3.95	2.56	.718	3.28	1.89	unknown	188	171	2782785536		6	6.64	.267	6.16	2.04	.073	.003	.00	.00	.059	1.57	1
email_spec4_product31_false-unreach-call.cil.c	unknown	257	241	2759778304		3	4.32	.731	.214	timeout	1000	621	6793084928									timeout	1000	980	2848518144												unknown	207	191	2792366080		6	5.07	.339	7.38	2.89	.083	.003	.00	.00	.109	1.98	1
email_spec4_product32_false-unreach-call.cil.c	unknown	872	849	3239407616		3	6.83	3.11	.262	timeout	1000	501	7285383168									timeout	1000	979	3259334656												timeout	1000	977	3194667008
email_spec4_product33_false-unreach-call.cil.c	unknown	294	277	2783424512		3	4.91	1.01	.266	timeout	1000	577	7205855232									timeout	1000	982	2798256128												unknown	211	195	2777997312		6	4.89	.291	7.72	3.10	.062	.001	.00	.00	.102	1.93	1
email_spec4_product34_false-unreach-call.cil.c	unknown	832	810	3290464256		3	6.45	2.00	.292	timeout	1000	501	7222337536									timeout	1000	975	3409739776												timeout	1000	976	3273359360
email_spec6_product12_false-unreach-call.cil.c	unknown	119	110	2607882240		3	3.38	.520	.228	timeout	1000	742	6246031360									timeout	1000	979	2893045760												unknown	159	145	2630320128		6	3.83	.268	4.82	2.13	.046	.009	.00	.00	.082	.947	1
email_spec6_product14_false-unreach-call.cil.c	unknown	387	376	2752933888		3	3.58	.529	.252	timeout	1000	501	6993567744									timeout	1000	976	3291860992												timeout	1000	979	2932248576
email_spec6_product15_false-unreach-call.cil.c	unknown	259	249	2608467968		3	3.73	.513	.274	timeout	1000	577	6875176960									timeout	1000	978	2980728832												timeout	1000	981	2688831488
email_spec6_product16_false-unreach-call.cil.c	unknown	226	214	2645385216		3	4.29	.751	.297	timeout	1000	578	6776737792									timeout	902	885	951164928		.732	875	880	2.34	874	874	3.20	860	863	873	timeout	1000	980	2730573824
email_spec6_product20_false-unreach-call.cil.c	unknown	894	871	3190968320		3	5.49	3.61	.259	timeout	1000	501	7034945536									timeout	902	880	1126653952		1.13	868	874	3.08	868	867	11.4	840	852	859	timeout	1000	978	3049279488
email_spec6_product22_false-unreach-call.cil.c	unknown	224	213	2637164544		3	4.15	.751	.342	timeout	1000	551	6888525824									timeout	1000	975	3070545920												timeout	1000	980	2750275584
email_spec6_product26_false-unreach-call.cil.c	unknown	897	873	3282997248		3	7.62	3.10	.457	timeout	1000	501	7355011072									timeout	1000	978	3423543296												timeout	1000	979	3072495616
email_spec6_product28_false-unreach-call.cil.c	unknown	110	99.4	2572963840		3	3.79	.538	.193	timeout	1000	735	6256582656									timeout	1000	983	2828218368												unknown	160	144	2762391552		6	5.71	.293	6.24	2.07	.044	.003	.00	.00	.102	1.51	1
email_spec6_product29_false-unreach-call.cil.c	unknown	390	377	2864742400		3	3.87	.676	.239	timeout	1000	501	7253876736									timeout	902	885	1079185408		.557	873	879	3.26	873	872	5.56	848	853	868	timeout	1000	979	3008942080
email_spec6_product30_false-unreach-call.cil.c	unknown	236	223	2657771520		3	4.53	.832	.283	timeout	1000	602	6314737664									timeout	1000	979	2994581504												timeout	1000	980	2719318016
email_spec6_product31_false-unreach-call.cil.c	unknown	284	268	2758430720		3	4.69	.854	.270	timeout	1000	531	7263936512									timeout	1000	980	2989068288												timeout	1000	981	2769297408
email_spec6_product33_false-unreach-call.cil.c	unknown	297	280	2805940224		3	5.36	1.18	.273	timeout	1000	517	7621562368									timeout	1000	976	3106123776												timeout	1000	980	2752442368
email_spec7_product28_false-unreach-call.cil.c	unknown	121	111	2605035520		3	3.16	.657	.197	timeout	1000	728	6147776512									timeout	1000	980	2841423872												unknown	165	151	2683805696		6	3.67	.294	5.11	2.13	.058	.001	.00	.00	.094	1.02	1
email_spec7_product29_false-unreach-call.cil.c	unknown	366	353	2827702272		3	3.89	.788	.235	timeout	1000	501	6651260928									timeout	902	882	1076568064		1.17	869	877	2.99	869	869	9.97	835	845	860	timeout	1000	976	3043328000
email_spec7_product30_false-unreach-call.cil.c	unknown	268	257	2647449600		3	4.15	1.01	.298	timeout	1000	579	6499368960									timeout	1000	979	3007266816												timeout	1000	981	2674917376
email_spec7_product31_false-unreach-call.cil.c	unknown	305	294	2667540480		3	4.44	.865	.216	timeout	1000	535	6692958208									timeout	1000	976	3209498624												timeout	1000	981	2741866496
email_spec7_product33_false-unreach-call.cil.c	unknown	316	298	2778750976		3	5.04	1.46	.256	timeout	1000	576	7010643968									timeout	1000	975	3153543168												timeout	1000	981	2765598720
email_spec8_product15_false-unreach-call.cil.c	unknown	148	137	2621882368		3	3.77	.611	.230	timeout	1000	734	6178148352									unknown	175	162	2717667328		1.82	3.86	8.43	2.22	3.59	3.48	2.13	.727	2.86	1.90	unknown	190	176	2706497536		6	4.62	.298	5.19	1.99	.061	.003	.00	.00	.067	.938	1
email_spec8_product16_false-unreach-call.cil.c	unknown	168	157	2637537280		3	4.08	.587	.332	timeout	1000	710	6181666816									timeout	1000	983	2825650176												unknown	195	179	2737000448		6	5.82	.308	5.74	2.34	.037	.001	.00	.00	.120	1.31	1
email_spec8_product20_false-unreach-call.cil.c	unknown	756	734	3108327424		3	5.13	3.96	.286	timeout	1000	501	7179239424									timeout	1000	974	3267072000												timeout	1000	978	3074490368
email_spec8_product21_false-unreach-call.cil.c	unknown	683	661	3162468352		3	5.22	5.28	.277	timeout	1000	501	7239483392									timeout	1000	979	3185229824												timeout	1000	978	3105669120
email_spec8_product22_false-unreach-call.cil.c	unknown	136	125	2621403136		3	3.76	.686	.302	timeout	1000	707	6674841600									timeout	1000	981	2862792704												unknown	198	183	2739937280		6	5.08	.678	5.60	1.62	.041	.002	.00	.00	.079	1.55	1
email_spec8_product26_false-unreach-call.cil.c	unknown	733	709	3207045120		3	8.14	2.90	.285	timeout	1000	501	8047702016									timeout	902	885	965488640		1.27	874	879	2.64	873	873	7.76	858	866	867	timeout	1000	976	3185905664
email_spec8_product30_false-unreach-call.cil.c	unknown	183	171	2641944576		3	4.28	.760	.281	timeout	1000	720	6637387776									timeout	1000	980	2828988416												unknown	210	194	2778902528		6	6.16	.695	6.59	2.21	.033	.001	.00	.00	.074	1.77	1
email_spec8_product31_false-unreach-call.cil.c	unknown	158	143	2746744832		3	4.38	.769	.299	timeout	1000	700	6958198784									timeout	1000	981	2832850944												unknown	197	182	2762186752		6	5.34	.879	6.61	2.38	.056	.002	.00	.00	.097	1.27	1
email_spec8_product33_false-unreach-call.cil.c	unknown	173	158	2768449536		3	4.54	.914	.269	timeout	1000	682	6665269248									timeout	1000	980	2914361344												unknown	214	199	2801197056		6	5.39	.421	7.34	3.11	.091	.003	.00	.00	.090	1.50	1
email_spec8_product34_false-unreach-call.cil.c	unknown	810	785	3298258944		3	8.54	2.62	.242	timeout	1000	501	7551426560									timeout	902	886	941973504		1.33	876	881	2.68	875	875	5.18	863	868	871	timeout	1000	978	3188875264
email_spec8_product35_false-unreach-call.cil.c	unknown	869	845	3310235648		3	6.60	4.14	.256	timeout	1000	501	7452835840									timeout	902	883	961957888		1.58	870	876	3.25	869	869	9.37	851	860	861	timeout	1000	977	3267440640
email_spec9_product15_false-unreach-call.cil.c	unknown	153	143	2588463104		3	3.80	.587	.232	timeout	1000	737	6094442496									unknown	176	164	2720165888		1.93	4.00	8.15	2.19	3.68	3.61	2.28	.683	2.96	2.01	unknown	193	178	2699468800		6	5.62	.229	5.29	2.35	.053	.011	.00	.00	.074	.972	1
email_spec9_product16_false-unreach-call.cil.c	unknown	124	113	2608177152		3	4.03	.594	.342	timeout	1000	735	6160736256									timeout	1000	982	2838347776												unknown	167	153	2726809600		6	5.36	.290	5.75	2.52	.061	.003	.00	.00	.167	1.28	1
email_spec9_product20_false-unreach-call.cil.c	unknown	694	673	3058413568		3	5.57	3.41	.290	timeout	1000	501	7254003712									timeout	1000	976	3249008640												timeout	1000	978	3087937536
email_spec9_product21_false-unreach-call.cil.c	unknown	761	739	3150684160		3	5.89	4.40	.283	timeout	1000	501	7569272832									timeout	1000	976	3225817088												timeout	1000	977	3132530688
email_spec9_product22_false-unreach-call.cil.c	unknown	144	133	2631749632		3	3.70	.798	.283	timeout	1000	704	6605955072									timeout	1000	983	2860994560												unknown	175	161	2709864448		6	4.38	.619	5.38	1.89	.093	.001	.00	.00	.075	1.15	1
email_spec9_product26_false-unreach-call.cil.c	unknown	864	841	3211108352		3	8.89	2.08	.292	timeout	1000	501	7311872000									timeout	902	884	928473088		1.40	872	878	2.67	871	871	9.38	854	864	863	timeout	1000	977	3176923136
email_spec9_product30_false-unreach-call.cil.c	unknown	139	128	2635005952		3	4.29	.797	.488	timeout	1000	721	6617268224									timeout	1000	981	2801238016												unknown	182	166	2726473728		6	6.56	.279	6.31	2.72	.050	.002	.00	.00	.056	1.22	1
email_spec9_product31_false-unreach-call.cil.c	unknown	158	143	2743599104		3	4.59	.797	.275	timeout	1000	686	6887661568									timeout	1000	980	2846490624												unknown	213	196	2808090624		6	5.32	.436	7.84	2.64	.140	.002	.00	.00	.147	2.15	1
email_spec9_product32_false-unreach-call.cil.c	unknown	627	606	3245625344		3	7.88	2.71	.256	timeout	1000	501	7575748608									timeout	1000	977	3209318400												timeout	1000	977	3187220480
email_spec9_product33_false-unreach-call.cil.c	unknown	148	134	2742902784		3	4.33	.807	.218	timeout	1000	663	6988742656									timeout	1000	981	2898640896												unknown	162	146	2824011776		6	6.13	.493	6.83	3.03	.082	.003	.00	.00	.125	1.27	1
email_spec9_product34_false-unreach-call.cil.c	unknown	735	713	3250339840		3	6.32	1.95	.238	timeout	1000	501	7528787968									timeout	902	884	946257920		1.36	873	878	2.56	872	872	5.46	859	865	868	timeout	1000	976	3252678656
email_spec8_product29_true-unreach-call.cil.c	true	31.2	16.9	712159232		5	5.80	2.98	1.28	true	123	62.2	2545819648		5	9.24	2.54	24.1	2.77	21.1	13.8	timeout	902	883	1035370496		1.97	869	877	3.71	868	868	12.1	841	853	858	true	58.9	43.9	939020288		19	22.7	.552	16.3	3.73	.111	.003	.00	.00	1.85	8.43	1
email_spec9_product29_true-unreach-call.cil.c	true	31.2	17.1	708288512		5	5.67	2.71	1.44	true	122	61.7	2711949312		5	9.35	2.80	23.7	3.00	19.3	12.7	timeout	902	884	1086132224		1.72	872	878	2.71	871	871	11.0	843	854	862	true	62.8	45.5	1004945408		19	23.6	.579	17.1	4.50	.155	.001	.00	.00	1.95	8.67	1
minepump_spec1_product01_true-unreach-call.cil.c	timeout	906	892	5112897536		206	4.87	.022	878	true	10.5	5.64	364756992		1	.669	.00	.005	.089			true	8.01	4.46	332681216		.432	.147	.496	.138	.111	.104	.032	.001	.033	.038	true	7.67	4.26	303235072		2	.093	.062	.815	.177	.004	.002	.00	.00	.002	.450	2
minepump_spec1_product02_true-unreach-call.cil.c	timeout	905	887	3503267840		173	4.68	.015	874	true	10.6	5.67	355479552		1	.555	.00	.005	.071			true	8.00	4.44	330285056		.509	.145	.480	.173	.092	.085	.035	.002	.037	.036	true	7.57	4.22	300810240		2	.093	.053	.390	.178	.007	.001	.00	.00	.003	.025	2
minepump_spec1_product03_true-unreach-call.cil.c	timeout	905	889	3665260544		184	4.74	.010	876	true	11.4	6.14	362536960		1	.695	.00	.008	.082			true	7.99	4.45	332062720		.473	.168	.549	.172	.101	.093	.035	.003	.038	.034	true	8.06	4.48	306511872		2	.101	.069	.410	.164	.012	.003	.00	.00	.003	.038	2
minepump_spec1_product04_true-unreach-call.cil.c	timeout	905	892	3320442880		169	4.75	.012	878	true	10.8	5.79	389267456		1	.663	.001	.005	.374			true	7.57	4.25	338796544		.413	.167	.523	.157	.110	.101	.042	.002	.044	.038	true	8.11	4.51	309809152		2	.095	.058	.380	.141	.009	.001	.00	.00	.002	.030	2
minepump_spec1_product05_true-unreach-call.cil.c	timeout	906	892	5105774592		201	4.87	.010	877	true	10.9	5.85	333643776		1	.475	.00	.004	.106			true	8.81	4.93	357322752		.492	.478	1.04	.229	.378	.368	.210	.010	.220	.160	true	8.60	4.77	312549376		4	.280	.072	1.15	.748	.011	.002	.00	.00	.015	.103	2
minepump_spec1_product06_true-unreach-call.cil.c	timeout	905	891	3511189504		179	4.66	.014	878	true	10.9	5.84	351379456		1	.559	.00	.005	.024			true	8.76	4.94	350150656		.470	.425	.962	.260	.340	.322	.174	.013	.187	.123	true	8.81	4.92	312340480		5	.740	.071	.712	.258	.012	.002	.00	.00	.020	.130	3
minepump_spec1_product07_true-unreach-call.cil.c	timeout	912	898	5123010560		184	4.95	.018	884	true	11.7	6.28	391536640		1	.785	.00	.006	.036			true	9.20	5.06	354828288		.548	.488	1.06	.226	.407	.381	.238	.012	.250	.142	true	8.66	4.87	318222336		4	.248	.093	1.13	.619	.013	.002	.00	.00	.019	.119	2
minepump_spec1_product08_true-unreach-call.cil.c	timeout	906	891	5129388032		185	5.01	.015	877	true	13.6	7.24	427380736		1	.558	.017	.009	.028			true	9.50	5.31	353869824		.563	.587	1.14	.199	.474	.456	.253	.023	.276	.201	true	8.27	4.65	316833792		4	.637	.076	.665	.255	.025	.001	.00	.00	.019	.106	2
minepump_spec1_product09_true-unreach-call.cil.c	timeout	906	888	5167390720		203	4.88	.012	874	true	10.1	5.43	342548480		1	.467	.00	.007	.037			true	7.82	4.36	334012416		.449	.161	.512	.146	.107	.095	.031	.002	.033	.039	true	7.23	4.09	297619456		2	.107	.395	.730	.177	.011	.001	.00	.00	.004	.027	2
minepump_spec1_product10_true-unreach-call.cil.c	timeout	905	891	3484340224		176	4.62	.012	878	true	10.2	5.49	353697792		1	.569		.005				true	8.00	4.51	338628608		.457	.165	.539	.166	.113	.102	.037	.001	.038	.041	true	7.76	4.32	301113344		2	.098	.046	.399	.168	.006	.003	.00	.00	.004	.024	2
minepump_spec1_product11_true-unreach-call.cil.c	timeout	905	891	3713310720		188	4.70	.009	877	true	12.0	6.37	376782848		1	.420	.001	.004	.030	1.17	.176	true	7.79	4.36	337117184		.437	.176	.497	.139	.108	.102	.051	.00	.051	.049	true	7.97	4.43	302362624		2	.105	.067	.418	.177	.009	.002	.00	.00	.003	.027	2
minepump_spec1_product12_true-unreach-call.cil.c	timeout	904	887	3343417344		165	4.52	.010	874	true	11.3	6.07	399921152		1	.744	.00	.020	.066			true	7.74	4.38	328744960		.557	.160	.509	.123	.107	.082	.036	.002	.038	.033	true	8.16	4.52	307003392		2	.093	.051	.954	.689	.007	.001	.00	.00	.003	.035	2
minepump_spec1_product13_true-unreach-call.cil.c	timeout	906	892	5091307520		205	5.02	.014	877	true	10.7	5.80	349556736		1	.765	.00	.005	.060			true	9.22	5.10	346091520		.594	.443	1.03	.228	.337	.327	.171	.010	.181	.133	true	8.44	4.74	317841408		4	.238	.096	1.17	.279	.017	.001	.00	.00	.017	.542	2
minepump_spec1_product14_true-unreach-call.cil.c	timeout	905	891	3534557184		179	4.74	.010	878	true	11.4	6.11	356323328		1	.643	.00	.005	.054			true	8.85	4.94	352591872		.522	.479	.978	.202	.363	.333	.206	.009	.215	.123	true	8.39	4.69	311517184		5	.281	.076	1.08	.624	.016	.001	.00	.00	.021	.121	3
minepump_spec1_product15_true-unreach-call.cil.c	timeout	905	891	3722657792		183	5.21	.014	878	true	12.2	6.54	377044992		1	.576	.001	.004	.048			true	9.17	5.10	344399872		.541	.521	1.13	.251	.406	.395	.222	.009	.231	.139	true	8.77	4.87	316309504		4	.231	.082	1.13	.253	.013	.003	.00	.00	.018	.125	2
minepump_spec1_product16_true-unreach-call.cil.c	timeout	905	891	3644280832		179	4.99	.012	876	true	11.3	6.09	390365184		1	.564	.00	.014	.027			true	9.41	5.22	352260096		.620	.545	1.09	.206	.467	.453	.263	.025	.288	.179	true	8.75	4.89	319905792		4	.273	.093	1.22	.243	.014	.001	.00	.00	.017	.105	2
minepump_spec1_product17_true-unreach-call.cil.c	timeout	906	892	5103149056		205	4.55	.007	879	true	10.3	5.52	362147840		1	.672	.001	.005	.054			true	9.80	5.55	363286528		.560	.537	1.20	.243	.435	.396	.217	.010	.227	.138	true	8.55	4.80	306495488		5	.262	.111	1.19	.658	.017	.002	.00	.00	.021	.131	3
minepump_spec1_product18_true-unreach-call.cil.c	timeout	905	892	3413180416		174	4.50	.013	877	true	11.0	5.90	354951168		1	.543	.00	.004	.024			true	8.92	5.04	358985728		.604	.461	1.09	.256	.372	.329	.185	.010	.195	.124	true	8.55	4.83	324677632		4	.257	.078	1.23	.724	.014	.009	.00	.00	.023	.100	2
minepump_spec1_product19_true-unreach-call.cil.c	timeout	906	891	3679371264		181	5.00	.012	877	true	11.0	5.93	355487744		1	.873	.00	.006	.087			true	9.38	5.29	355475456		.584	.563	1.22	.282	.480	.459	.226	.020	.246	.165	true	8.57	4.83	323743744		4	.272	.128	1.17	.649	.018	.001	.00	.00	.015	.097	2
minepump_spec1_product20_true-unreach-call.cil.c	timeout	905	890	3725897728		182	5.08	.015	877	true	11.4	6.13	373559296		1	.951	.004	.006	.090			true	9.80	5.51	348467200		.722	.510	1.21	.274	.426	.407	.252	.008	.260	.155	true	8.46	4.74	312504320		4	.256	.079	1.23	.762	.008	.001	.00	.00	.014	.110	2
minepump_spec1_product21_true-unreach-call.cil.c	timeout	906	891	5093601280		201	5.41	.015	875	true	11.9	6.36	364937216		1	.598	.00	.013	.064			true	10.4	5.73	370241536		.628	.706	1.57	.341	.608	.580	.315	.031	.346	.243	true	9.08	5.08	323710976		4	.332	.103	1.35	.775	.014	.002	.00	.00	.024	.146	2
minepump_spec1_product22_true-unreach-call.cil.c	timeout	906	891	3461492736		176	5.10	.010	876	true	11.7	6.21	375422976		1	.947	.00	.007	.072			true	10.4	5.79	380112896		.615	.629	1.50	.329	.490	.452	.248	.020	.268	.178	true	9.06	5.15	324161536		4	.294	.108	1.47	.825	.012	.00	.00	.00	.023	.124	2
minepump_spec1_product23_true-unreach-call.cil.c	timeout	913	896	5174284288						true	12.0	6.42	375341056		1	1.16	.00	.003	.136			true	10.2	5.66	370233344		.677	.717	1.55	.331	.588	.539	.291	.043	.334	.221	true	9.26	5.23	323907584		4	.369	.123	1.37	.344	.022	.002	.00	.00	.018	.153	2
minepump_spec1_product24_true-unreach-call.cil.c	timeout	905	888	3798216704		179	5.25	.012	873	true	14.2	7.46	402096128		1	1.06	.010	.007	.085			true	10.3	5.73	378712064		.613	.756	1.61	.319	.617	.593	.351	.058	.409	.271	true	8.86	5.00	323817472		4	.349	.106	1.30	.306	.015	.002	.00	.00	.019	.134	2
minepump_spec1_product25_true-unreach-call.cil.c	timeout	906	892	5104164864		203	5.00	.015	877	true	10.8	5.80	359333888		1	.608	.00	.006	.026			true	8.75	4.91	359346176		.539	.473	1.10	.207	.385	.370	.212	.011	.223	.129	true	8.48	4.79	312225792		5	.271	.083	1.17	.644	.005	.001	.00	.00	.024	.132	3
minepump_spec1_product26_true-unreach-call.cil.c	timeout	905	888	3489587200		175	4.51	.009	875	true	11.6	6.16	358416384		1	.677	.00	.019	.033			true	8.98	5.03	351297536		.556	.460	1.09	.236	.365	.350	.182	.011	.193	.132	true	8.84	4.94	318922752		4	.283	.105	1.21	.692	.037	.002	.00	.00	.026	.114	2
minepump_spec1_product27_true-unreach-call.cil.c	timeout	906	891	3700584448		183	5.08	.015	877	true	11.7	6.24	368046080		1	.749	.00	.005	.032			true	9.78	5.51	355368960		.593	.549	1.27	.260	.465	.449	.210	.027	.237	.157	true	8.56	4.81	317816832		4	.265	.097	1.24	.276	.009	.002	.00	.00	.014	.117	2
minepump_spec1_product28_true-unreach-call.cil.c	timeout	905	888	3694981120		179	5.10	.014	874	true	12.2	6.53	392376320		1	.799	.00	.019	.106			true	9.49	5.32	353349632		.652	.562	1.22	.303	.476	.459	.270	.010	.280	.164	true	8.48	4.73	325001216		4	.719	.076	.728	.239	.014	.002	.00	.00	.015	.102	2
minepump_spec1_product29_true-unreach-call.cil.c	timeout	906	890	5107724288		200	5.28	.009	875	true	10.7	5.76	372510720		1	.794		.010				true	10.3	5.73	371933184		.759	.632	1.47	.322	.471	.451	.269	.017	.286	.183	true	9.10	5.12	334454784		4	.312	.122	1.34	.317	.019	.001	.00	.00	.026	.131	2
minepump_spec1_product30_true-unreach-call.cil.c	timeout	905	891	3573141504		181	4.99	.014	878	true	11.4	6.12	386207744		1	.677	.00	.005	.019			true	10.3	5.68	371347456		.688	.629	1.50	.276	.518	.482	.282	.015	.297	.185	true	9.17	5.17	330182656		4	.350	.096	1.30	.746	.015	.001	.00	.00	.022	.120	2
minepump_spec1_product31_true-unreach-call.cil.c	timeout	905	887	3792195584		178	5.14	.016	873	true	13.3	7.04	397918208		1	.865	.00	.006	.027			true	10.5	5.80	374108160		.761	.727	1.62	.338	.632	.605	.373	.048	.421	.295	true	8.99	5.03	325353472		4	.335	.095	1.33	.748	.018	.001	.00	.00	.017	.117	2
minepump_spec1_product32_true-unreach-call.cil.c	timeout	906	891	5111054336		183	5.21	.011	877	true	13.7	7.34	415793152		1	1.55	.001	.015	.266			true	10.0	5.55	365989888		.545	.716	1.60	.326	.611	.589	.364	.033	.397	.250	true	8.88	4.96	328716288		4	.749	.125	.982	.349	.015	.001	.00	.00	.015	.128	2
minepump_spec1_product45_true-unreach-call.cil.c	timeout	905	892	3455229952		76	5.35	48.7	815	true	30.9	15.9	674541568		1	1.61	.089	2.60	.412	6.67	1.09	true	11.7	6.46	375975936		.634	.996	2.26	.505	.855	.825	.557	.030	.587	.368	true	9.43	5.29	330203136		4	.365	.125	1.72	.431	.010	.001	.00	.00	.023	.159	2
minepump_spec1_product46_true-unreach-call.cil.c	timeout	905	890	3440361472		74	5.29	60.4	802	true	28.5	14.7	678203392		1	1.06	.135	.006	.524	6.99	.565	true	11.4	6.25	378785792		.634	.952	2.20	.508	.813	.782	.509	.032	.541	.327	true	9.85	5.51	330391552		4	.419	.098	1.57	.843	.012	.001	.00	.00	.024	.164	2
minepump_spec1_product47_true-unreach-call.cil.c	timeout	905	891	3810021376		77	5.51	418	441	true	33.8	17.4	775774208		2	1.71	.357	.021	.501	7.55	1.55	true	11.2	6.29	375525376		.752	.998	2.12	.408	.852	.819	.527	.062	.589	.330	true	9.77	5.43	330960896		4	.453	.124	1.60	.424	.017	.001	.00	.00	.019	.177	2
minepump_spec1_product48_true-unreach-call.cil.c	timeout	907	892	3456421888		71	5.05	250	613	true	35.7	18.3	796925952		2	1.94	.645	.014	.607	7.67	1.74	true	12.6	6.95	386940928		.821	1.46	2.70	.436	1.30	1.28	.825	.079	.904	.483	true	9.65	5.41	343326720		4	.424	.119	1.47	.434	.026	.003	.00	.00	.014	.150	2
minepump_spec1_product57_true-unreach-call.cil.c	timeout	905	891	2951618560		62	4.58	491	378	true	169	85.0	2827866112		12	2.40	7.84	.016	6.38	25.1	36.2	true	12.5	6.87	377032704		.773	1.36	2.66	.471	1.18	1.13	.721	.093	.814	.479	true	10.7	6.09	340971520		7	.736	.106	1.88	.840	.011	.002	.00	.00	.079	.392	2
minepump_spec1_product58_true-unreach-call.cil.c	timeout	904	891	2931511296		60	4.77	477	392	true	188	94.5	3387600896		13	2.74	8.99	.012	7.99	26.3	41.2	true	13.2	7.19	402939904		.433	1.62	3.31	.790	1.44	1.40	.960	.116	1.08	.598	true	9.46	5.31	335990784		4	.477	.476	1.49	.366	.010	.001	.00	.00	.039	.175	2
minepump_spec1_product59_true-unreach-call.cil.c	timeout	906	892	2977214464		61	5.00	598	270	true	177	89.0	2989899776		12	2.93	10.3	.004	7.86	26.5	34.1	true	13.3	7.39	402780160		.367	1.58	3.46	.952	1.42	1.37	.869	.148	1.02	.554	true	9.68	5.42	333959168		4	.435	.543	1.68	.446	.023	.001	.00	.00	.018	.165	2
minepump_spec1_product60_true-unreach-call.cil.c	timeout	905	892	2988572672		59	4.81	540	330	true	235	118	3683729408		14	3.14	15.4	.011	10.1	30.6	51.5	true	13.7	7.54	399925248		.926	1.55	2.96	.534	1.37	1.35	.825	.153	.978	.591	true	10.0	5.60	335417344		4	.388	.138	1.68	.420	.020	.002	.00	.00	.022	.185	2
minepump_spec1_product61_true-unreach-call.cil.c	timeout	905	890	3431387136		66	6.54	47.9	812	true	34.5	17.7	815099904		1	1.20	.576	.006	.474	8.72	.244	true	14.2	7.67	419688448		.311	1.42	3.76	1.09	1.18	1.12	.745	.047	.792	.448	true	10.5	5.97	342216704		4	.460	.140	2.12	.602	.015	.002	.00	.00	.021	.203	2
minepump_spec1_product62_true-unreach-call.cil.c	timeout	905	891	3441168384		66	6.18	58.4	804	true	38.2	19.6	839475200		1	2.37	.127	3.36	.202	8.03	1.10	true	16.0	8.65	428744704		.379	1.98	4.37	1.03	1.39	1.31	.847	.089	.936	.514	true	10.7	5.95	348434432		4	.559	.121	2.04	1.07	.020	.005	.00	.00	.020	.234	2
minepump_spec1_product63_true-unreach-call.cil.c	timeout	907	892	3650912256		67	6.24	380	480	true	37.6	19.2	842309632		2	1.92	.688	.008	.381	8.40	1.33	true	17.7	9.48	434585600		.524	2.28	5.35	.900	2.00	1.92	1.27	.141	1.41	.775	true	10.5	5.91	350941184		4	.929	.158	1.73	.683	.021	.001	.00	.00	.016	.196	2
minepump_spec1_product64_true-unreach-call.cil.c	timeout	905	890	3270782976		60	5.97	202	660	true	39.1	20.0	886022144		2	2.01	.756	.008	.756	8.38	1.59	true	16.5	8.85	451596288		.540	1.84	4.41	1.12	1.59	1.54	1.00	.134	1.14	.710	true	10.8	6.03	345120768		4	.491	.200	2.17	.579	.043	.002	.00	.00	.016	.212	2
minepump_spec2_product01_true-unreach-call.cil.c	timeout	906	891	5106475008		196	4.95	.010	878	true	10.1	5.43	369348608		1	.631	.001	.004	.046			true	7.79	4.34	340844544		.466	.170	.511	.141	.118	.113	.046	.003	.049	.059	true	8.01	4.40	305930240		2	.080	.644	.980	.148	.621	.611	.563	.007	.575	.036	2	.575
minepump_spec2_product02_true-unreach-call.cil.c	timeout	904	889	3491184640		173	4.31	.012	877	true	10.2	5.52	368132096		1	.763	.00	.018	.070			true	7.98	4.47	336191488		.624	.198	.518	.138	.137	.130	.043	.004	.047	.058	true	7.88	4.34	305664000		2	.085	.504	.872	.175	.463	.461	.413	.005	.422	.040	2	.422
minepump_spec2_product03_true-unreach-call.cil.c	timeout	905	891	3712765952		186	4.84	.013	877	true	11.2	6.00	375840768		1	.505	.00	.005	.062			true	8.29	4.59	333688832		.487	.181	.561	.184	.131	.124	.049	.004	.053	.069	true	7.80	4.34	302714880		2	.082	.150	.928	.599	.103	.096	.035	.007	.046	.028	2	.049
minepump_spec2_product04_true-unreach-call.cil.c	timeout	904	890	3354267648		168	4.62	.007	877	true	14.0	7.42	433872896		1	.576	.00	.006	.042			true	7.64	4.29	342581248		.468	.154	.515	.163	.117	.112	.043	.001	.044	.058	true	7.66	4.27	309080064		2	.080	.493	.868	.183	.440	.433	.050	.005	.058	.037	2	.063
minepump_spec2_product05_true-unreach-call.cil.c	timeout	906	889	5158408192		201	5.08	.010	874	true	10.7	5.69	332554240		1	.761	.00	.005	.042			true	10.3	5.76	361181184		.652	.659	1.46	.287	.564	.538	.307	.030	.337	.361	true	9.89	5.53	321171456		7	.285	.933	1.69	.269	.327	.317	.182	.017	.242	.200	3	.204
minepump_spec2_product06_true-unreach-call.cil.c	timeout	905	888	3562553344		175	4.81	.012	874	true	10.8	5.81	347435008		1	.797	.001	.013	.075			true	10.2	5.63	360325120		.576	.778	1.53	.281	.662	.632	.346	.035	.381	.408	true	9.84	5.59	326041600		7	.368	.865	1.79	.298	.788	.358	.222	.018	.282	.249	2	.248
minepump_spec2_product07_true-unreach-call.cil.c	timeout	906	890	3766177792		181	5.01	.006	876	true	11.9	6.38	379076608		1	.968	.00	.009	.070			true	9.58	5.32	361746432		.540	.647	1.39	.291	.563	.530	.244	.048	.292	.324	true	9.39	5.32	327012352		8	.372	.876	1.72	.328	.307	.290	.185	.012	.240	.206	2	.200
minepump_spec2_product08_true-unreach-call.cil.c	timeout	905	887	3720978432		177	5.19	.010	873	true	14.5	7.80	461119488		1	.711	.00	.016	.143			true	9.94	5.55	363147264		.556	.735	1.47	.290	.633	.611	.329	.060	.389	.416	true	9.80	5.55	326893568		10	.404	.849	1.75	.325	.768	.754	.619	.023	.699	.284	3	.651
minepump_spec2_product09_true-unreach-call.cil.c	timeout	905	889	5143724032		202	4.98	.014	872	true	10.7	5.78	363954176		1	.688	.00	.005	.029			true	7.76	4.29	335724544		.415	.179	.481	.142	.144	.132	.041	.004	.045	.064	true	8.00	4.43	308170752		2	.071	.168	.966	.196	.112	.107	.041	.004	.049	.033	2	.053
minepump_spec2_product10_true-unreach-call.cil.c	timeout	905	891	3460313088		174	4.37	.017	878	true	10.8	5.73	351141888		1	.614	.00	.005	.090			true	7.86	4.40	337932288		.434	.181	.524	.134	.138	.129	.056	.003	.059	.076	true	7.86	4.38	311660544		2	.075	.529	.899	.191	.470	.465	.409	.004	.417	.032	2	.420
minepump_spec2_product11_true-unreach-call.cil.c	timeout	906	891	3637329920		183	5.04	.010	878	true	11.5	6.08	368017408		1	.600	.00	.005	.061			true	7.20	3.98	337010688		.445	.169	.481	.149	.137	.127	.061	.003	.064	.080	true	8.06	4.47	306184192		2	.082	.504	.885	.160	.465	.447	.035	.005	.044	.046	2	.043
minepump_spec2_product12_true-unreach-call.cil.c	timeout	904	886	3304529920		162	4.58	.007	873	true	11.1	5.99	394604544		1	.900	.00	.013	.082			true	8.14	4.53	338833408		.486	.201	.528	.149	.150	.147	.043	.002	.045	.063	true	7.80	4.38	305033216		2	.074	.139	.939	.166	.106	.099	.048	.004	.055	.027	2	.056
minepump_spec2_product13_true-unreach-call.cil.c	timeout	906	888	5177974784		208	5.30	.009	873	true	10.3	5.53	363864064		1	.862		.006				true	10.4	5.74	362749952		.692	.747	1.46	.266	.634	.612	.328	.029	.357	.393	true	9.25	5.25	306872320		7	.303	.368	1.59	.265	.291	.276	.174	.016	.222	.176	3	.195
minepump_spec2_product14_true-unreach-call.cil.c	timeout	905	891	3424022528		172	4.61	.013	878	true	10.9	5.84	380821504		1	.633	.00	.006	.038			true	10.2	5.65	359960576		.565	.872	1.57	.266	.734	.718	.362	.046	.408	.463	true	9.64	5.48	331673600		7	.338	.419	1.78	.787	.352	.343	.214	.018	.270	.244	2	.241
minepump_spec2_product15_true-unreach-call.cil.c	timeout	905	891	5106991104		183	5.93	.015	876	true	12.7	6.70	393392128		1	.596	.00	.005	.026			true	9.92	5.49	356708352		.539	.681	1.47	.300	.595	.574	.275	.059	.334	.362	true	9.25	5.27	323792896		8	.692	.402	1.27	.312	.334	.322	.188	.020	.254	.222	2	.217
minepump_spec2_product16_true-unreach-call.cil.c	timeout	905	889	5170900992		182	5.11	.009	876	true	11.8	6.25	410943488		1	.595	.00	.013	.027			true	10.9	6.04	368898048		.677	.779	1.58	.326	.680	.655	.359	.061	.420	.450	true	9.53	5.45	330334208		10	.391	.445	1.75	.718	.368	.361	.209	.021	.291	.279	3	.243
minepump_spec2_product17_true-unreach-call.cil.c	timeout	906	890	5156581376		198	5.06	.015	875	true	10.5	5.61	361078784		1	.724	.00	.005	.104			true	10.4	5.77	372682752		.596	.734	1.53	.301	.600	.575	.301	.032	.333	.385	true	8.78	5.05	327360512		7	.276	.485	1.50	.552	.403	.390	.251	.024	.304	.190	3	.281
minepump_spec2_product18_true-unreach-call.cil.c	timeout	905	890	3405955072		171	4.51	.015	877	true	11.2	6.00	349298688		1	.774	.00	.003	.069			true	10.3	5.75	357732352		.742	.677	1.49	.307	.590	.571	.323	.031	.354	.384	true	10.1	5.78	339927040		7	.434	.534	1.87	.755	.455	.434	.264	.021	.325	.260	2	.291
minepump_spec2_product19_true-unreach-call.cil.c	timeout	905	891	5117419520		183	5.15	.007	877	true	12.2	6.58	416309248		1	.530	.00	.010	.040			true	10.3	5.79	358051840		.622	.778	1.56	.310	.683	.651	.315	.061	.376	.404	true	10.7	6.06	341970944		9	.475	.692	2.35	.340	.591	.578	.378	.030	.454	.343	3	.416
minepump_spec2_product20_true-unreach-call.cil.c	timeout	905	891	3651141632		178	5.15	.011	877	true	12.9	6.87	401764352		1	.917	.00	.010	.092			true	9.00	5.01	359948288		.487	.532	1.11	.235	.449	.440	.244	.038	.282	.320	true	10.1	5.80	338604032		8	.574	.587	1.97	.314	.489	.480	.322	.025	.402	.297	2	.357
minepump_spec2_product21_true-unreach-call.cil.c	timeout	906	889	5159862272		200	5.41	.013	875	true	11.5	6.19	388702208		1	1.19		.005				true	12.0	6.57	393691136		.673	.952	2.30	.488	.810	.783	.453	.049	.502	.528	true	10.3	5.82	342548480		7	.416	.597	2.09	.772	.490	.479	.298	.036	.369	.238	3	.341
minepump_spec2_product22_true-unreach-call.cil.c	timeout	904	890	3471396864		174	4.99	.009	876	true	11.9	6.39	390168576		1	.702	.001	.018	.020			true	12.4	6.77	378912768		.629	1.17	2.53	.539	1.01	.946	.572	.069	.641	.681	true	10.6	6.10	342441984		7	.510	.638	2.29	.839	.532	.508	.317	.023	.374	.327	2	.346
minepump_spec2_product23_true-unreach-call.cil.c	timeout	905	888	5178843136		180	5.04	.012	874	true	13.1	6.96	386994176		1	.982	.00	.023	.138			true	11.4	6.25	376283136		.835	.998	2.20	.446	.896	.869	.448	.095	.543	.581	true	10.8	6.18	350236672		7	.479	1.09	2.33	.436	.998	.963	.328	.031	.397	.364	2	.363
minepump_spec2_product24_true-unreach-call.cil.c	timeout	905	892	5100822528		178	5.33	.012	877	true	13.7	7.25	433700864		1	.839	.001	.010	.049			true	12.1	6.61	378339328		.654	1.22	2.42	.414	1.03	.984	.583	.083	.666	.694	true	11.9	6.74	351408128		8	.591	1.16	2.61	.471	.617	.597	.396	.042	.488	.461	2	.450
minepump_spec2_product25_true-unreach-call.cil.c	timeout	906	892	5111287808		201	5.07	.014	877	true	11.1	5.93	374566912		1	.543	.001	.005	.034			true	9.69	5.36	366075904		.519	.815	1.53	.258	.681	.639	.343	.038	.381	.411	true	9.33	5.34	330788864		7	.281	.976	1.76	.318	.887	.872	.727	.027	.782	.207	3	.765
minepump_spec2_product26_true-unreach-call.cil.c	timeout	904	890	3476918272		174	4.65	.009	876	true	12.1	6.38	360960000		1	.662	.001	.005	.133			true	10.5	5.81	374550528		.622	.705	1.52	.288	.592	.573	.292	.034	.326	.358	true	10.0	5.66	329994240		7	.388	1.01	1.91	.323	.944	.935	.270	.027	.331	.279	2	.304
minepump_spec2_product27_true-unreach-call.cil.c	timeout	905	891	5102567424		185	5.20	.011	877	true	11.2	6.01	386252800		1	.910	.00	.005	.120			true	10.5	5.82	366497792		.685	.890	1.66	.285	.761	.740	.361	.061	.422	.484	true	10.8	6.14	344924160		9	.520	.628	2.06	.725	.541	.525	.355	.029	.432	.304	3	.397
minepump_spec2_product28_true-unreach-call.cil.c	timeout	906	892	5102956544		182	4.81	.010	878	true	13.2	7.04	427876352		1	.595	.00	.005	.050			true	9.39	5.24	351055872		.674	.511	1.20	.312	.420	.406	.223	.024	.247	.266	true	10.3	5.84	337154048		8	.514	.573	1.97	.303	.491	.479	.317	.027	.401	.304	2	.354
minepump_spec2_product29_true-unreach-call.cil.c	timeout	905	888	5171830784		196	5.17	.013	874	true	10.9	5.84	369860608		1	.669		.005				true	12.6	6.84	391368704		.625	1.06	2.41	.505	.918	.900	.536	.075	.611	.659	true	10.4	5.88	340717568		7	.420	.620	2.10	.339	.541	.523	.334	.038	.403	.253	3	.379
minepump_spec2_product30_true-unreach-call.cil.c	timeout	905	890	3416641536		172	4.92	.008	876	true	10.9	5.83	340209664		1	.719		.005				true	12.3	6.81	382623744		.711	1.22	2.48	.503	1.03	1.01	.563	.059	.622	.700	true	10.5	6.02	344412160		7	.500	.993	2.23	.455	.881	.866	.727	.026	.788	.294	2	.759
minepump_spec2_product31_true-unreach-call.cil.c	timeout	906	891	3685392384		177	5.18	.006	874	true	13.1	6.98	422047744		1	.814	.00	.006	.050			true	11.7	6.42	373841920		.550	1.01	2.31	.537	.890	.870	.486	.078	.564	.590	true	11.4	6.49	341286912		7	.544	1.12	2.39	.446	.519	.507	.344	.032	.413	.360	2	.380
minepump_spec2_product32_true-unreach-call.cil.c	timeout	905	891	3714400256		177	5.23	.028	877	true	14.2	7.59	449175552		1	.863	.007	.005	.189			true	11.1	6.21	384741376		.564	1.01	2.28	.549	.819	.794	.439	.076	.515	.557	true	11.7	6.67	346365952		8	.558	.689	2.66	1.02	.595	.579	.394	.039	.479	.470	2	.443
minepump_spec2_product37_true-unreach-call.cil.c	timeout	904	891	3333160960		81	5.00	52.8	811	true	30.5	15.7	673435648		1	1.31	.00	2.62	.170	6.21	2.09	true	12.5	6.80	375992320		.707	1.24	2.53	.524	1.11	1.08	.637	.152	.789	.813	true	10.5	5.94	341729280		7	.396	.610	2.14	.830	.513	.491	.299	.039	.366	.251	3	.349
minepump_spec2_product38_true-unreach-call.cil.c	timeout	904	888	3378577408		79	4.93	56.7	805	true	28.8	14.8	644308992		1	1.40	.00	2.38	.305	6.15	1.01	true	12.7	6.93	370417664		.748	1.32	2.58	.477	1.14	1.11	.576	.112	.688	.745	true	10.7	6.02	339132416		6	.457	.650	2.06	.379	.536	.512	.340	.033	.408	.194	2	.380
minepump_spec2_product39_true-unreach-call.cil.c	timeout	908	890	3669274624		84	5.18	423	437	true	43.6	22.4	905129984		3	2.11	.282	.005	.842	8.90	4.58	true	12.2	6.71	381329408		.811	1.20	2.36	.410	1.03	1.00	.550	.127	.677	.697	true	10.3	5.90	348037120		8	.544	.659	2.18	.395	.563	.550	.361	.036	.438	.284	2	.405
minepump_spec2_product40_true-unreach-call.cil.c	timeout	905	891	3218694144		75	5.18	231	633	true	47.5	24.2	929607680		3	1.99	.749	.005	1.44	11.3	3.45	true	11.9	6.49	381091840		.777	1.18	2.22	.380	1.02	.991	.596	.119	.715	.741	true	11.7	6.71	348930048		9	.646	.790	2.59	.504	.673	.640	.434	.038	.534	.399	3	.483
minepump_spec2_product45_true-unreach-call.cil.c	timeout	905	890	3306201088		72	5.22	52.2	812	true	36.5	18.8	811896832		1	1.72	.00	3.21	1.15	7.17	2.09	true	13.7	7.54	402903040		.806	1.45	3.11	.628	1.29	1.23	.724	.116	.840	.927	true	11.1	6.30	344760320		7	.475	.693	2.47	.466	.617	.604	.415	.055	.498	.338	3	.474
minepump_spec2_product46_true-unreach-call.cil.c	timeout	904	890	3252150272		70	5.03	48.6	815	true	32.3	16.6	730230784		1	1.66	.00	2.84	.458	7.39	1.25	true	12.8	7.14	398368768		.647	1.45	2.89	.469	1.26	1.21	.761	.140	.901	.940	true	11.2	6.33	350736384		6	.556	1.09	2.33	.429	.998	.971	.372	.037	.441	.306	2	.825
minepump_spec2_product47_true-unreach-call.cil.c	timeout	907	893	3630395392		75	4.69	418	445	true	51.3	26.3	927309824		2	1.96	.358	.006	.811	9.13	8.19	true	12.7	6.95	396726272		.705	1.49	2.83	.430	1.28	1.24	.755	.128	.883	.909	true	12.2	7.16	361148416		9	.827	.874	2.88	.887	.765	.743	.527	.050	.653	.447	3	.585
minepump_spec2_product48_true-unreach-call.cil.c	timeout	905	892	3433390080		70	5.36	283	580	true	51.8	26.4	937910272		3	2.24	1.25	.005	1.76	10.9	4.32	true	13.3	7.23	390991872		.767	1.48	2.92	.465	1.28	1.24	.659	.141	.800	.869	true	11.4	6.49	351203328		8	.647	1.18	2.56	.476	1.02	1.00	.397	.038	.493	.366	2	.442
minepump_spec2_product49_true-unreach-call.cil.c	timeout	905	892	2987986944		70	4.60	482	385	true	294	148	4420190208		18	3.04	13.2	.005	15.3	37.9	70.3	true	12.5	6.87	374673408		.694	1.38	2.64	.450	1.23	1.17	.724	.088	.812	.858	true	13.0	7.52	363151360		11	.983	.951	3.14	1.14	.834	.809	.559	.046	.680	.491	2	.614
minepump_spec2_product50_true-unreach-call.cil.c	timeout	906	891	2938494976		68	4.83	486	382	true	166	83.9	3087749120		13	3.04	6.19	.013	6.89	27.1	33.5	true	12.2	6.61	387309568		.679	1.32	2.56	.461	1.18	1.16	.683	.115	.798	.863	true	15.0	9.09	372252672		16	1.46	1.14	4.03	.946	.980	.954	.677	.064	.881	1.26	2	.758
minepump_spec2_product51_true-unreach-call.cil.c	timeout	904	891	2938683392		65	4.69	612	255	true	228	115	3559358464		15	3.00	12.1	.019	9.71	29.8	52.9	true	12.7	6.89	380669952		.702	1.42	2.70	.522	1.24	1.22	.719	.156	.875	.927	true	11.8	6.77	350023680		9	.714	.791	2.71	.454	.703	.686	.470	.034	.571	.405	3	.514
minepump_spec2_product52_true-unreach-call.cil.c	timeout	904	892	2956214272		60	4.52	503	367	true	233	117	3705622528		15	2.87	12.8	.008	11.3	32.1	50.5	true	12.8	7.04	380223488		.645	1.44	2.65	.532	1.29	1.26	.670	.176	.846	.922	true	11.8	6.83	351842304		8	.668	1.19	2.75	.587	1.08	1.06	.494	.040	.590	.358	2	.889
minepump_spec2_product53_true-unreach-call.cil.c	timeout	905	891	3439304704		72	5.83	51.5	810	true	34.8	17.9	833396736		1	1.59	.00	.016	.110	7.94	1.59	true	16.4	8.87	448663552		.443	1.97	4.69	.735	1.71	1.66	.978	.208	1.19	1.25	true	11.8	6.65	347627520		6	.559	1.17	2.69	.619	1.06	1.02	.831	.035	.892	.269	2	.874
minepump_spec2_product54_true-unreach-call.cil.c	timeout	904	891	3442237440		71	5.92	49.4	812	true	34.6	17.8	793952256		1	1.84	.00	2.80	.171	7.88	1.45	true	15.0	8.10	424935424		.437	1.64	4.08	.688	1.47	1.43	.777	.125	.902	.943	true	13.4	7.56	355598336		7	.744	1.33	3.29	.701	1.22	1.20	.945	.049	1.05	.496	2	1.01
minepump_spec2_product55_true-unreach-call.cil.c	timeout	904	890	3304284160		67	5.67	324	538	true	46.0	23.6	888889344		2	2.12	.353	.010	1.24	10.7	2.49	true	15.7	8.52	462737408		.421	2.09	4.47	.685	1.87	1.80	.983	.254	1.24	1.38	true	12.4	6.90	359993344		6	.557	.824	2.78	.615	.614	.581	.385	.047	.463	.298	2	.437
minepump_spec2_product56_true-unreach-call.cil.c	timeout	904	891	3195736064		65	5.71	244	621	true	46.8	23.9	920461312		3	2.14	.561	.004	.858	11.1	2.98	true	15.3	8.28	432824320		.433	1.88	4.19	.948	1.66	1.58	.856	.223	1.08	1.17	true	12.0	6.76	363229184		6	.568	1.14	2.73	.656	1.01	.982	.447	.042	.527	.258	2	.496
minepump_spec2_product57_true-unreach-call.cil.c	timeout	905	891	2955567104		59	5.00	452	418	true	331	166	4577607680		18	2.83	16.5	.006	16.9	38.2	83.6	true	15.9	8.73	407339008		1.12	2.04	3.85	.610	1.85	1.79	1.01	.195	1.21	1.28	true	13.3	7.74	368205824		11	1.14	1.13	3.24	.581	.990	.965	.646	.061	.778	.534	2	.717
minepump_spec2_product58_true-unreach-call.cil.c	timeout	905	892	2950946816		59	4.90	461	409	true	152	76.7	2914271232		12	2.49	6.00	.005	6.66	26.3	28.3	true	14.5	7.92	395030528		.854	1.87	3.55	.652	1.65	1.62	1.03	.126	1.16	1.20	true	11.7	6.70	359030784		7	.695	.796	2.75	.555	.718	.704	.451	.039	.534	.397	2	.499
minepump_spec2_product59_true-unreach-call.cil.c	timeout	906	891	3013025792		59	5.14	570	299	true	164	82.8	3004932096		12	3.28	7.57	.004	8.23	26.6	30.0	true	16.1	8.73	432955392		.929	2.32	4.11	.656	2.09	2.03	1.06	.358	1.42	1.50	true	12.0	6.95	353013760		7	.663	1.24	2.79	.553	1.13	1.12	.498	.044	.597	.417	2	.932
minepump_spec2_product60_true-unreach-call.cil.c	timeout	906	892	3018571776		55	4.68	494	376	true	149	75.3	2732097536		11	2.75	6.53	.006	6.05	28.4	24.0	true	12.8	7.08	379568128		.795	1.47	2.89	.569	1.30	1.26	.742	.125	.867	.916	true	12.0	6.94	344604672		7	.668	1.30	2.79	.493	1.19	1.17	.466	.056	.569	.419	2	.531
minepump_spec2_product61_true-unreach-call.cil.c	timeout	905	890	3275739136		63	5.98	54.3	809	true	42.2	21.6	917012480		1	1.88	.001	3.76	.692	9.62	1.67	true	17.4	9.36	446492672		.672	1.91	5.06	1.03	1.58	1.48	.865	.148	1.01	1.06	true	13.6	7.56	362139648		6	.775	1.28	3.35	.690	.733	.696	.467	.049	.559	.392	2	.525
minepump_spec2_product62_true-unreach-call.cil.c	timeout	905	891	3345309696		64	5.74	46.4	816	true	42.1	21.6	910143488		1	2.08	.00	4.05	.202	9.49	1.97	true	18.4	9.85	453656576		.624	2.94	5.52	.944	2.16	2.06	1.26	.187	1.44	1.51	true	13.9	7.80	368975872		7	.981	1.09	3.22	.799	.904	.880	.620	.060	.729	.472	3	.692
minepump_spec2_product63_true-unreach-call.cil.c	timeout	905	891	3470020608		63	6.51	390	469	true	46.9	23.9	890085376		2	1.72	.322	.005	1.20	11.3	2.21	true	16.9	9.17	432779264		.594	2.01	4.88	.915	1.76	1.72	1.11	.182	1.29	1.36	true	15.5	8.78	379392000		9	1.04	1.62	4.25	.799	1.48	1.44	.718	.069	.864	.727	3	.796
minepump_spec2_product64_true-unreach-call.cil.c	timeout	904	890	3236515840		59	5.81	206	658	true	49.8	25.3	892903424		2	2.17	.197	.005	1.91	11.7	2.61	true	17.7	9.56	440827904		.565	2.53	5.30	1.17	1.99	1.94	1.18	.239	1.42	1.46	true	15.4	8.85	372490240		8	.952	1.32	4.34	1.30	1.13	1.11	.767	.063	.886	.624	2	.845
minepump_spec3_product33_true-unreach-call.cil.c	timeout	907	894	5384511488		114	4.74	82.4	775	true	21.8	11.3	566882304		1	.635	.035	1.85	.059	4.02	.965	true	9.37	5.20	353390592		.556	.594	1.17	.288	.492	.471	.278	.063	.341	.272	true	8.51	4.79	315158528		4	.307	.083	1.09	.586	.009	.003	.00	.00	.021	.116	2
minepump_spec3_product34_true-unreach-call.cil.c	timeout	907	894	5222469632		110	4.66	94.2	764	true	24.4	12.7	672866304		1	1.38	.146	2.29	.336	4.17	.882	true	8.86	4.96	354365440		.484	.458	1.06	.282	.379	.369	.203	.044	.247	.170	true	9.05	5.11	312332288		4	.287	.092	1.33	.789	.019	.002	.00	.00	.029	.124	2
minepump_spec3_product37_true-unreach-call.cil.c	timeout	905	892	3481702400		80	4.79	59.9	807	true	28.5	14.7	624021504		1	1.47	.166	2.24	.103	5.84	.970	true	11.9	6.57	380395520		.592	1.21	2.30	.444	1.11	1.09	.621	.206	.827	.636	true	9.67	5.46	339656704		4	.448	.131	1.57	.429	.017	.001	.00	.00	.044	.156	2
minepump_spec3_product38_true-unreach-call.cil.c	timeout	905	892	3293220864		75	5.02	51.3	815	true	26.5	13.6	619044864		1	1.16	.285	.005	.133	5.15	1.01	true	11.7	6.43	374476800		.551	1.09	2.21	.496	.982	.954	.519	.192	.711	.574	true	9.30	5.21	336809984		4	.342	.126	1.54	.860	.026	.001	.00	.00	.032	.165	2
minepump_spec3_product41_true-unreach-call.cil.c	timeout	906	889	5189541888		98	4.81	75.4	778	true	26.0	13.5	598880256		1	1.15	.246	2.10	.500	5.11	.990	true	10.5	5.81	361381888		.521	.907	1.64	.325	.816	.793	.436	.121	.557	.373	true	8.88	5.00	327487488		4	.332	.091	1.24	.345	.013	.00	.00	.00	.020	.139	2
minepump_spec3_product42_true-unreach-call.cil.c	timeout	906	891	5134413824		94	4.99	70.7	786	true	23.0	12.0	587591680		1	.702	.142	2.02	.064	4.44	1.02	true	9.98	5.55	360525824		.505	.935	1.70	.377	.822	.800	.465	.109	.574	.375	true	8.83	4.96	320503808		4	.324	.099	1.22	.646	.018	.002	.00	.00	.026	.164	2
minepump_spec3_product45_true-unreach-call.cil.c	timeout	905	891	3420004352		71	5.19	54.7	811	true	30.5	15.7	701358080		1	1.16	.065	2.55	.165	6.82	1.59	true	10.2	5.72	363061248		.553	.779	1.74	.414	.670	.648	.417	.079	.496	.285	true	9.78	5.46	329523200		4	.459	.139	1.60	.819	.015	.003	.00	.00	.029	.189	2
minepump_spec3_product46_true-unreach-call.cil.c	timeout	905	890	3255439360		67	5.09	55.6	810	true	32.4	16.8	748572672		1	1.26	.084	2.72	.484	6.78	1.72	true	10.3	5.77	364728320		.643	.846	1.78	.414	.714	.685	.431	.088	.519	.361	true	9.54	5.36	334577664		4	.445	.099	1.62	.408	.017	.001	.00	.00	.028	.194	2
minepump_spec3_product49_true-unreach-call.cil.c	timeout	905	892	3548614656		78	4.94	242	622	true	28.2	14.5	651935744		1	1.17	.131	2.47	.129	5.90	1.50	true	10.2	5.60	369561600		.676	.593	1.37	.359	.482	.466	.262	.045	.307	.241	true	10.8	6.13	354439168		6	.864	.150	1.83	.511	.025	.001	.00	.00	.074	.369	1
minepump_spec3_product50_true-unreach-call.cil.c	timeout	905	892	3554709504		77	5.07	247	617	true	29.7	15.3	717832192		1	1.29	.612	.004	.404	6.16	1.09	true	9.10	5.13	362258432		.509	.467	1.29	.379	.391	.360	.180	.022	.202	.140	true	9.83	5.56	343805952		4	.498	.167	1.60	.362	.017	.001	.00	.00	.043	.208	1
minepump_spec3_product53_true-unreach-call.cil.c	timeout	906	891	3233095680		65	5.73	324	540	true	37.5	19.3	800215040		1	1.97	.037	3.35	.057	8.36	1.42	true	12.0	6.61	374280192		.195	1.18	2.63	.677	.555	.526	.299	.040	.339	.262	true	12.8	7.17	358436864		6	1.01	.212	2.58	.707	.073	.005	.00	.00	.053	.486	1
minepump_spec3_product54_true-unreach-call.cil.c	timeout	906	891	3173109760		63	5.35	327	538	true	37.3	19.1	826155008		1	2.50	.285	3.26	.175	7.77	1.30	true	11.2	6.13	378531840		.609	.781	2.12	.602	.604	.585	.373	.037	.410	.324	true	13.1	7.25	363880448		6	1.19	.166	2.56	.681	.041	.001	.00	.00	.079	.552	1
minepump_spec3_product57_true-unreach-call.cil.c	timeout	906	892	2958458880		56	4.60	563	308	true	29.8	15.3	703479808		1	1.34	.065	2.50	.055	6.47	1.93	true	11.3	6.30	365920256		.577	.784	1.97	.454	.659	.627	.382	.079	.461	.327	true	19.8	13.0	374546432		25	3.62	.191	5.76	.769	.045	.005	.00	.00	.459	3.48	1
minepump_spec3_product58_true-unreach-call.cil.c	timeout	905	891	3007283200		54	4.48	583	288	true	30.2	15.5	715059200		1	1.26	.085	2.59	.097	6.94	1.28	true	10.8	5.99	375500800		.602	.813	1.86	.409	.670	.653	.415	.064	.479	.360	true	10.9	6.32	348749824		7	.811	.169	2.13	.492	.019	.002	.00	.00	.055	.461	2
minepump_spec3_product61_true-unreach-call.cil.c	timeout	904	891	3059204096		51	5.64	508	361	true	35.9	18.4	844152832		1	1.42	.274	3.00	.210	8.49	1.26	true	12.6	6.85	390729728		.203	1.00	3.09	1.06	.829	.806	.498	.099	.597	.433	true	12.7	7.24	366534656		7	1.09	.201	2.79	1.16	.035	.004	.00	.00	.057	.531	2
minepump_spec3_product62_true-unreach-call.cil.c	timeout	905	890	3065163776		52	5.35	502	366	true	36.8	18.9	877318144		1	1.39	.211	.005	.612	8.16	1.70	true	11.5	6.32	380256256		.184	.878	2.88	.985	.682	.649	.407	.076	.483	.324	true	14.1	7.95	371740672		6	1.23	.255	3.16	.805	.040	.002	.00	.00	.076	.537	1
minepump_spec4_product01_true-unreach-call.cil.c	timeout	906	893	5232406528		228	5.27	.012	878	true	9.82	5.34	356442112		1	.507	.00	.005	.058			true	7.96	4.42	332353536		.500	.146	.491	.144	.091	.078	.029	.001	.030	.033	true	8.08	4.47	297955328		2	.092	.055	.411	.165	.007	.003	.00	.00	.002	.027	2
minepump_spec4_product02_true-unreach-call.cil.c	timeout	906	893	5091274752		195	4.93	.010	879	true	10.0	5.39	353120256		1	.743		.005				true	8.06	4.51	335642624		.389	.126	.482	.149	.084	.079	.025	.001	.026	.032	true	7.55	4.21	303431680		2	.101	.064	.419	.150	.007	.001	.00	.00	.005	.033	2
minepump_spec4_product03_true-unreach-call.cil.c	timeout	906	891	5119328256		198	5.09	.010	877	true	10.3	5.52	346304512		1	.546	.00	.013	.030			true	8.05	4.54	335073280		.497	.147	.498	.170	.105	.096	.039	.003	.042	.039	true	7.50	4.18	308068352		2	.097	.056	.437	.159	.015	.001	.00	.00	.003	.030	2
minepump_spec4_product04_true-unreach-call.cil.c	timeout	906	892	5117038592		189	5.03	.009	878	true	9.87	5.32	359936000		1	.862		.012				true	7.64	4.30	333873152		.425	.164	.489	.143	.098	.090	.041	.001	.042	.039	true	7.77	4.33	297320448		2	.090	.064	.386	.177	.008	.001	.00	.00	.003	.029	2
minepump_spec4_product05_true-unreach-call.cil.c	timeout	906	891	5114183680		223	5.34	.011	875	true	10.0	5.42	356909056		1	.540	.00	.005	.029			true	9.34	5.25	341929984		.537	.335	.872	.231	.231	.221	.114	.011	.125	.097	true	8.37	4.67	316198912		4	.240	.075	1.08	.643	.022	.001	.00	.00	.025	.105	2
minepump_spec4_product06_true-unreach-call.cil.c	timeout	906	892	5099470848		200	5.06	.011	878	true	9.57	5.18	362233856		1	.536	.00	.004	.036			true	8.71	4.86	350384128		.462	.334	.863	.216	.249	.240	.126	.010	.136	.104	true	8.53	4.79	314925056		5	.232	.094	1.23	.265	.013	.004	.00	.00	.010	.141	3
minepump_spec4_product07_true-unreach-call.cil.c	timeout	906	892	5119406080		204	5.35	.017	876	true	9.98	5.37	351150080		1	.700	.00	.004	.022			true	8.80	4.87	343789568		.459	.346	.886	.246	.261	.247	.126	.020	.146	.109	true	8.70	4.82	316239872		5	.294	.065	1.16	.253	.009	.003	.00	.00	.011	.126	3
minepump_spec4_product08_true-unreach-call.cil.c	timeout	906	888	5195653120		201	5.56	.013	872	true	10.6	5.71	361705472		1	.491	.005	.006	.051			true	8.24	4.65	350117888		.474	.341	.837	.209	.271	.261	.147	.020	.167	.116	true	8.17	4.52	314380288		4	.258	.097	1.07	.621	.020	.001	.00	.00	.022	.121	2
minepump_spec4_product09_true-unreach-call.cil.c	timeout	906	890	5129732096		222	5.25	.015	875	true	9.71	5.23	341217280		1	.716		.005				true	7.89	4.41	332464128		.481	.159	.522	.178	.106	.099	.040	.001	.041	.046	true	7.56	4.24	304205824		2	.102	.051	.387	.172	.005	.001	.00	.00	.002	.028	2
minepump_spec4_product10_true-unreach-call.cil.c	timeout	906	892	5130715136		197	4.85	.009	878	true	10.3	5.57	340140032		1	.566	.00	.010	.041			true	7.63	4.27	335458304		.333	.175	.476	.133	.109	.102	.035	.002	.037	.040	true	7.58	4.23	299413504		2	.094	.461	.808	.164	.006	.001	.00	.00	.003	.031	2
minepump_spec4_product11_true-unreach-call.cil.c	timeout	906	892	5103501312		199	5.20	.020	877	true	10.0	5.35	347951104		1	.629	.001	.008	.062			true	8.29	4.58	334721024		.523	.178	.500	.146	.124	.116	.055	.00	.055	.052	true	7.62	4.27	305176576		2	.092	.048	.366	.152	.007	.002	.00	.00	.003	.033	2
minepump_spec4_product12_true-unreach-call.cil.c	timeout	905	892	3681026048		185	5.07	.006	877	true	10.2	5.49	343019520		1	.638	.001	.011	.046			true	8.32	4.59	340140032		.490	.157	.546	.170	.114	.096	.043	.003	.046	.043	true	7.85	4.37	301187072		2	.105	.063	.778	.566	.005	.001	.00	.00	.003	.030	2
minepump_spec4_product13_true-unreach-call.cil.c	timeout	906	891	5113839616		223	5.34	.015	875	true	9.39	5.07	343339008		1	.598	.001	.004	.051			true	8.29	4.58	339984384		.570	.286	.729	.198	.222	.214	.116	.008	.124	.096	true	8.48	4.72	312823808		4	.738	.081	.679	.239	.019	.002	.00	.00	.026	.106	2
minepump_spec4_product14_true-unreach-call.cil.c	timeout	906	892	5120053248		198	5.05	.005	877	true	10.2	5.53	340963328		1	.573		.004				true	8.89	4.91	336723968		.585	.353	.810	.213	.279	.269	.150	.011	.161	.113	true	8.71	4.85	308482048		5	.236	.073	1.23	.226	.014	.002	.00	.00	.013	.141	3
minepump_spec4_product15_true-unreach-call.cil.c	timeout	906	888	5193592832		210	5.55	.015	869	true	9.95	5.36	359391232		1	.784		.017				true	8.21	4.56	352137216		.520	.347	.825	.220	.285	.276	.151	.017	.168	.120	true	8.31	4.65	315219968		5	.594	.081	.704	.240	.009	.001	.00	.00	.013	.119	3
minepump_spec4_product16_true-unreach-call.cil.c	timeout	906	892	5130743808		201	5.46	.012	877	true	9.79	5.28	340938752		1	.649		.014				true	8.50	4.72	344580096		.480	.359	.853	.225	.286	.270	.135	.017	.152	.108	true	8.47	4.75	324042752		4	.292	.083	1.10	.244	.022	.002	.00	.00	.023	.118	2
minepump_spec4_product17_true-unreach-call.cil.c	timeout	906	888	5235511296		225	5.40	.013	872	true	9.68	5.21	350441472		1	.368		.008				true	9.36	5.18	345214976		.469	.368	.918	.244	.289	.272	.135	.011	.146	.107	true	8.42	4.69	317566976		5	.288	.093	1.15	.647	.011	.001	.00	.00	.023	.158	3
minepump_spec4_product18_true-unreach-call.cil.c	timeout	906	889	5175848960		191	4.87	.017	875	true	10.1	5.44	361889792		1	.632	.001	.020	.023			true	8.87	4.94	351150080		.559	.341	.836	.224	.262	.248	.123	.008	.131	.091	true	8.41	4.74	318599168		4	.280	.087	1.19	.244	.010	.002	.00	.00	.022	.117	2
minepump_spec4_product19_true-unreach-call.cil.c	timeout	906	892	5098049536		202	5.38	.018	876	true	9.91	5.31	362385408		1	.589		.007				true	8.55	4.77	338046976		.534	.410	.942	.238	.332	.323	.153	.031	.184	.149	true	8.57	4.76	328728576		5	.243	.086	1.15	.260	.009	.001	.00	.00	.010	.130	3
minepump_spec4_product20_true-unreach-call.cil.c	timeout	906	890	5141032960		203	5.54	.014	874	true	10.0	5.40	351240192		1	.738		.005				true	8.44	4.67	350904320		.481	.345	.872	.235	.284	.277	.140	.024	.164	.112	true	8.65	4.88	316383232		4	.310	.067	1.11	.620	.012	.001	.00	.00	.025	.131	2
minepump_spec4_product21_true-unreach-call.cil.c	timeout	907	890	5203595264		226	5.65	.009	873	true	9.93	5.33	364568576		1	.247		.005				true	9.90	5.50	374452224		.290	.470	1.61	.346	.374	.350	.189	.013	.202	.134	true	9.22	5.14	329695232		4	.352	.090	1.42	.378	.025	.001	.00	.00	.026	.154	2
minepump_spec4_product22_true-unreach-call.cil.c	timeout	906	892	5113077760		195	5.29	.014	877	true	10.8	5.77	365150208		1	.912	.00	.011	.112			true	9.94	5.50	358088704		.435	.501	1.36	.392	.371	.358	.197	.012	.209	.129	true	9.03	5.07	323022848		4	.777	.109	.970	.355	.009	.001	.00	.00	.466	.160	2
minepump_spec4_product23_true-unreach-call.cil.c	timeout	906	889	5155328000		203	5.66	.011	874	true	11.0	5.86	351170560		1	.711	.00	.005	.079			true	9.63	5.42	361668608		.551	.486	1.25	.346	.396	.378	.216	.030	.246	.153	true	9.19	5.16	326230016		4	.344	.110	1.43	.324	.025	.001	.00	.00	.028	.168	2
minepump_spec4_product24_true-unreach-call.cil.c	timeout	906	891	5136867328		198	5.64	.006	875	true	11.8	6.33	350609408		1	.698	.00	.005	.022			true	9.54	5.35	356052992		.612	.418	1.24	.365	.339	.322	.191	.030	.221	.143	true	9.18	5.07	324009984		4	.360	.520	1.30	.304	.017	.002	.00	.00	.020	.145	2
minepump_spec4_product25_true-unreach-call.cil.c	timeout	906	892	5161005056		224	5.39	.017	876	true	9.32	5.01	349265920		1	.528		.005				true	8.38	4.68	343691264		.467	.311	.869	.280	.237	.229	.109	.009	.118	.088	true	8.69	4.85	314245120		5	.301	.108	1.19	.255	.012	.003	.00	.00	.022	.124	3
minepump_spec4_product26_true-unreach-call.cil.c	timeout	906	891	5115670528		195	5.14	.011	877	true	9.64	5.20	348868608		1	.483		.005				true	8.73	4.84	349196288		.553	.387	.851	.203	.316	.305	.156	.012	.168	.132	true	8.36	4.67	316182528		4	.282	.080	1.07	.246	.010	.001	.00	.00	.023	.125	2
minepump_spec4_product27_true-unreach-call.cil.c	timeout	906	891	5108039680		206	5.48	.017	876	true	9.98	5.36	359116800		1	.434		.012				true	8.98	5.01	346906624		.573	.386	.882	.197	.301	.290	.143	.026	.169	.114	true	8.91	4.90	316035072		5	.270	.097	1.34	.257	.017	.004	.00	.00	.013	.156	3
minepump_spec4_product28_true-unreach-call.cil.c	timeout	907	892	5118230528		199	5.41	.022	876	true	10.1	5.42	340271104		1	.606	.001	.015	.063			true	8.59	4.77	345137152		.504	.384	.877	.243	.287	.275	.151	.025	.176	.128	true	8.57	4.80	316846080		4	.319	.079	1.12	.246	.017	.00	.00	.00	.024	.110	2
minepump_spec4_product29_true-unreach-call.cil.c	timeout	906	890	5206351872		226	6.11	.014	872	true	10.5	5.69	363950080		1	.399		.013				true	9.22	5.15	361062400		.581	.416	1.13	.281	.341	.334	.173	.011	.184	.114	true	8.88	5.01	323031040		4	.716	.093	.926	.384	.011	.002	.00	.00	.024	.124	2
minepump_spec4_product30_true-unreach-call.cil.c	timeout	906	892	5128073216		197	4.57	.014	877	true	10.7	5.84	371507200		1	.401		.006				true	9.53	5.27	357543936		.640	.436	1.17	.330	.355	.336	.198	.023	.221	.159	true	8.64	4.90	323293184		4	.681	.092	.917	.305	.007	.001	.00	.00	.023	.144	2
minepump_spec4_product31_true-unreach-call.cil.c	timeout	906	889	5172875264		195	5.36	.017	874	true	10.7	5.79	360468480		1	.862	.002	.008	.049			true	9.96	5.55	359563264		.484	.512	1.28	.308	.411	.395	.217	.041	.258	.193	true	9.07	5.06	323465216		4	.759	.088	.959	.311	.018	.003	.00	.00	.034	.158	2
minepump_spec4_product32_true-unreach-call.cil.c	timeout	906	892	5092839424		204	5.58	.015	876	true	11.0	5.87	360112128		1	1.20		.006				true	9.30	5.17	358592512		.646	.500	1.15	.273	.417	.397	.206	.024	.230	.150	true	9.12	5.13	326823936		4	.368	.099	1.43	.309	.011	.001	.00	.00	.022	.164	2
minepump_spec4_product49_true-unreach-call.cil.c	timeout	906	889	5168111616		93	5.43	92.3	763	true	180	90.7	3150860288		15	3.02	3.69	.010	8.47	29.2	38.8	true	9.76	5.35	356974592		.595	.553	1.37	.328	.482	.466	.255	.046	.301	.140	true	9.86	5.67	339316736		5	.596	.149	1.76	.488	.015	.002	.00	.00	.059	.281	1
minepump_spec4_product50_true-unreach-call.cil.c	timeout	906	891	5115121664		91	5.72	88.2	769	true	241	121	4078383104		17	3.23	5.10	.025	11.6	30.8	62.7	true	9.82	5.47	371200000		.548	.559	1.39	.345	.461	.447	.258	.029	.287	.129	true	8.97	5.03	327958528		3	.371	.468	1.44	.428	.014	.002	.00	.00	.027	.131	1
minepump_spec4_product51_true-unreach-call.cil.c	timeout	907	893	3657801728		82	5.34	418	443	true	230	116	3965968384		16	3.04	13.0	.012	10.5	28.0	54.8	true	11.2	6.18	385073152		.608	.880	1.99	.488	.748	.727	.398	.080	.478	.202	true	9.66	5.40	334012416		4	.466	.111	1.56	.808	.012	.002	.00	.00	.034	.158	1
minepump_spec4_product52_true-unreach-call.cil.c	timeout	904	891	3327643648		75	5.06	312	551	true	139	70.1	2245005312		11	3.19	4.19	.011	5.57	24.5	25.5	true	10.8	5.98	384180224		.543	.941	1.99	.459	.799	.688	.418	.080	.498	.214	true	10.1	5.71	348073984		3	.606	.149	1.63	.474	.028	.004	.00	.00	.031	.121	0
minepump_spec4_product53_true-unreach-call.cil.c	timeout	905	892	3732959232		78	5.86	61.0	799	true	148	74.8	2718486528		12	3.07	2.74	.006	6.61	25.6	29.6	true	13.0	7.09	377946112		.789	.986	2.34	.499	.839	.806	.466	.077	.543	.253	true	11.8	6.64	360988672		5	.755	.154	2.34	.671	.040	.003	.00	.00	.059	.349	1
minepump_spec4_product54_true-unreach-call.cil.c	timeout	905	891	3714043904		77	6.12	67.8	790	true	176	88.7	2995793920		13	3.14	3.52	.017	8.21	28.8	37.4	true	12.8	7.01	406687744		.244	1.41	3.30	.996	1.23	1.18	.743	.166	.909	.480	true	9.88	5.54	344739840		3	.419	.124	1.87	.941	.021	.001	.00	.00	.034	.146	1
minepump_spec4_product55_true-unreach-call.cil.c	timeout	906	892	3637100544		74	5.97	385	474	true	141	71.2	2515992576		10	3.30	4.34	.012	5.61	23.3	26.7	true	13.2	7.17	401891328		.621	1.36	3.01	.641	1.20	1.17	.779	.114	.893	.287	true	9.97	5.57	341389312		3	.423	.585	1.77	.505	.032	.001	.00	.00	.041	.150	1
minepump_spec4_product56_true-unreach-call.cil.c	timeout	904	891	3320840192		68	5.53	316	547	true	176	88.7	3227058176		12	2.88	6.52	.006	9.07	27.8	35.0	true	11.9	6.49	382189568		.261	1.11	2.69	.440	.949	.915	.551	.128	.679	.300	true	11.8	6.68	356573184		6	.834	.131	2.38	1.13	.022	.002	.00	.00	.046	.374	1
minepump_spec4_product57_true-unreach-call.cil.c	timeout	905	891	3689918464		78	5.71	61.5	798	true	241	121	3806273536		16	2.64	4.94	.004	12.0	35.3	59.0	true	11.4	6.30	371458048		.609	1.00	2.10	.465	.851	.828	.509	.097	.606	.247	true	9.56	5.39	335065088		3	.443	.153	1.55	.391	.048	.002	.00	.00	.031	.141	1
minepump_spec4_product58_true-unreach-call.cil.c	timeout	906	892	3683807232		77	5.53	64.1	798	true	206	103	3668402176		14	2.99	4.83	.017	10.3	29.7	48.0	true	12.6	6.91	378753024		.719	1.11	2.39	.479	.922	.896	.540	.101	.641	.294	true	9.98	5.56	342339584		3	.476	.149	1.55	.440	.028	.001	.00	.00	.035	.144	1
minepump_spec4_product59_true-unreach-call.cil.c	timeout	907	893	3580981248		74	5.63	415	447	true	199	100	3237326848		13	3.00	7.77	.010	9.04	26.7	46.5	true	11.5	6.41	374251520		.656	1.18	2.17	.413	1.06	.990	.643	.122	.765	.294	true	10.4	5.80	345120768		4	.561	.145	1.75	.378	.023	.003	.00	.00	.037	.239	1
minepump_spec4_product60_true-unreach-call.cil.c	timeout	906	891	3203076096		66	5.23	325	539	true	203	102	3531526144		13	3.01	6.87	.034	9.30	27.4	48.4	true	11.5	6.37	386019328		.223	1.09	2.66	.837	1.00	.981	.615	.117	.732	.312	true	10.2	5.65	340938752		3	.510	.108	1.67	.935	.012	.00	.00	.00	.045	.154	1
minepump_spec4_product61_true-unreach-call.cil.c	timeout	906	891	3650867200		69	6.11	74.1	786	true	149	74.9	2712330240		11	3.39	3.09	.012	8.18	26.7	25.2	true	14.7	7.97	413380608		.272	1.61	3.88	.592	1.45	1.36	.796	.167	.963	.550	true	10.5	5.90	345223168		3	.449	.593	2.09	.598	.014	.001	.00	.00	.030	.164	1
minepump_spec4_product62_true-unreach-call.cil.c	timeout	905	890	3572269056		67	6.46	81.8	778	true	152	76.8	2606301184		11	3.98	2.83	.007	7.44	29.4	24.5	true	14.1	7.70	421801984		.244	1.69	3.99	1.13	1.52	1.46	.848	.244	1.09	.550	true	10.5	5.92	347103232		3	.448	.157	2.10	1.03	.019	.001	.00	.00	.030	.156	1
minepump_spec4_product63_true-unreach-call.cil.c	timeout	913	899	5247086592						true	110	55.7	2333605888		8	3.09	3.62	.006	4.91	22.0	15.0	true	15.7	8.50	431091712		.264	1.97	4.51	1.16	1.73	1.68	.795	.447	1.24	.783	true	10.4	5.84	352833536		3	.483	.167	2.02	.541	.029	.003	.00	.00	.028	.178	1
minepump_spec4_product64_true-unreach-call.cil.c	timeout	904	890	3485556736		63	6.51	293	567	true	157	79.5	2722811904		10	2.96	6.03	.004	7.18	26.3	29.3	true	13.4	7.47	403771392		.282	1.84	3.60	.679	1.40	1.32	.719	.225	.944	.613	true	10.5	5.88	357105664		3	.505	.193	1.91	.788	.015	.001	.00	.00	.029	.189	1
minepump_spec5_product01_true-unreach-call.cil.c	timeout	906	892	5097181184		191	4.76	.012	878	true	10.2	5.46	344145920		1	.476	.001	.005	.092			true	8.05	4.47	338948096		.404	.231	.650	.206	.183	.173	.095	.006	.101	.115	true	8.23	4.61	316084224		1	.047	.748	1.20	.231	.678	.668	.567	.014	.583	.023	0	.589
minepump_spec5_product02_true-unreach-call.cil.c	timeout	905	891	5108150272		179	5.02	.021	877	true	9.98	5.39	363708416		1	.619	.00	.006	.041			true	7.86	4.42	343351296		.430	.254	.674	.230	.208	.194	.101	.009	.110	.121	true	8.25	4.61	313528320		1	.047	.803	1.29	.231	.722	.715	.637	.011	.650	.029	0	.653
minepump_spec5_product03_true-unreach-call.cil.c	timeout	905	889	5141774336		183	4.86	.015	875	true	12.1	6.46	384008192		1	.578	.00	.014	.023			true	8.20	4.57	341000192		.413	.291	.673	.175	.232	.219	.111	.008	.119	.133	true	8.13	4.58	311054336		1	.047	.644	1.18	.276	.580	.569	.090	.004	.095	.027	0	.109
minepump_spec5_product04_true-unreach-call.cil.c	timeout	905	891	3691892736		173	5.04	.014	877	true	11.9	6.28	345800704		1	.893	.00	.004	.048			true	8.34	4.69	340914176		.485	.279	.682	.193	.224	.207	.107	.006	.113	.131	true	7.95	4.47	310976512		1	.039	.255	1.15	.262	.195	.193	.111	.009	.122	.031	0	.126
minepump_spec5_product05_true-unreach-call.cil.c	timeout	906	892	5113929728		196	5.39	.010	877	true	9.69	5.18	355135488		1	.349		.006				true	8.86	4.96	337461248		.513	.402	.878	.213	.308	.300	.191	.012	.203	.217	true	8.65	4.79	315514880		1	.045	.351	1.37	.267	.294	.280	.176	.013	.190	.030	0	.195
minepump_spec5_product06_true-unreach-call.cil.c	timeout	905	891	3699761152		173	4.73	.009	877	true	11.1	5.94	353800192		1	.660	.00	.005	.057			true	8.40	4.69	336453632		.467	.371	.853	.232	.310	.292	.163	.015	.178	.192	true	9.23	5.05	310206464		1	.049	.376	1.48	.257	.313	.299	.190	.017	.208	.029	0	.214
minepump_spec5_product07_true-unreach-call.cil.c	timeout	906	890	5156306944		184	5.17	.009	875	true	12.4	6.60	391757824		1	.593	.00	.005	.036			true	8.44	4.74	342401024		.459	.384	.858	.226	.312	.303	.205	.012	.217	.230	true	8.02	4.52	315379712		1	.051	.366	1.19	.258	.317	.299	.187	.008	.196	.031	0	.204
minepump_spec5_product08_true-unreach-call.cil.c	timeout	906	893	5137575936		177	5.12	.012	878	true	12.0	6.45	365473792		1	.797	.00	.009	.075			true	8.74	4.85	338518016		.525	.400	.863	.245	.312	.303	.178	.013	.191	.216	true	8.63	4.83	314654720		1	.044	.366	1.44	.260	.273	.266	.149	.011	.161	.044	0	.166
minepump_spec5_product09_true-unreach-call.cil.c	timeout	906	891	5108625408		189	4.93	.007	877	true	10.3	5.54	352563200		1	.595	.001	.005	.057			true	7.91	4.46	336580608		.353	.265	.676	.207	.196	.185	.099	.008	.107	.118	true	8.03	4.44	303685632		1	.039	.260	1.15	.231	.198	.193	.097	.008	.106	.038	0	.113
minepump_spec5_product10_true-unreach-call.cil.c	timeout	906	892	5322633216		179	5.16	.011	877	true	10.3	5.57	341204992		1	.766	.00	.010	.084			true	8.24	4.63	334168064		.434	.289	.703	.206	.232	.223	.117	.009	.126	.140	true	7.81	4.38	307326976		1	.048	.629	1.06	.184	.558	.550	.463	.009	.473	.023	0	.480
minepump_spec5_product11_true-unreach-call.cil.c	timeout	906	892	5119651840		183	4.65	.014	878	true	10.5	5.62	351772672		1	.947		.013				true	8.46	4.71	338214912		.543	.258	.721	.219	.201	.188	.096	.007	.103	.119	true	8.35	4.69	305295360		1	.044	.731	1.25	.256	.659	.641	.109	.007	.117	.026	0	.122
minepump_spec5_product12_true-unreach-call.cil.c	timeout	906	892	3667542016		172	5.21	.012	878	true	11.7	6.18	352477184		1	.735	.001	.013	.022			true	7.97	4.49	343535616		.420	.269	.666	.202	.211	.206	.096	.007	.103	.119	true	7.94	4.36	308428800		1	.039	.643	1.13	.242	.557	.552	.473	.010	.485	.040	0	.488
minepump_spec5_product13_true-unreach-call.cil.c	timeout	906	892	5114486784		192	5.13	.013	877	true	10.6	5.71	365129728		1	.477	.00	.003	.056			true	8.49	4.73	344403968		.462	.339	.840	.238	.274	.263	.161	.012	.173	.184	true	8.31	4.64	313372672		1	.046	.353	1.39	.701	.296	.288	.183	.011	.195	.037	0	.201
minepump_spec5_product14_true-unreach-call.cil.c	timeout	906	892	5135319040		177	4.93	.013	878	true	10.8	5.80	361889792		1	.730	.001	.009	.078			true	8.76	4.86	340783104		.494	.338	.828	.245	.284	.278	.165	.015	.180	.193	true	8.51	4.72	315854848		1	.047	.396	1.43	.239	.323	.321	.173	.016	.190	.032	0	.200
minepump_spec5_product15_true-unreach-call.cil.c	timeout	906	892	5141508096		182	5.12	.012	878	true	10.9	5.88	351961088		1	.761	.00	.009	.387			true	8.05	4.49	340967424		.390	.352	.867	.281	.285	.279	.167	.013	.180	.198	true	8.39	4.73	306720768		1	.048	.358	1.32	.258	.288	.278	.169	.012	.182	.031	0	.192
minepump_spec5_product16_true-unreach-call.cil.c	timeout	906	892	5142224896		180	5.42	.010	877	true	11.3	6.00	346800128		1	.649	.001	.005	.081			true	8.51	4.82	350691328		.392	.370	.885	.246	.283	.277	.168	.011	.179	.197	true	8.34	4.71	313262080		1	.046	.731	1.31	.233	.663	.645	.509	.013	.523	.031	0	.533
minepump_spec5_product17_true-unreach-call.cil.c	timeout	906	888	5188898816		195	5.23	.010	873	true	10.8	5.78	373063680		1	.605	.00	.014	.023			true	8.83	4.90	344961024		.484	.401	.919	.245	.335	.328	.199	.017	.216	.232	true	8.72	4.90	314417152		1	.055	.369	1.40	.272	.305	.300	.199	.013	.214	.036	0	.219
minepump_spec5_product18_true-unreach-call.cil.c	timeout	910	894	5173440512		176	4.70	.009	881	true	10.3	5.54	362782720		1	.791		.005				true	8.86	4.96	340332544		.518	.386	.882	.220	.319	.310	.197	.013	.210	.220	true	8.62	4.85	308224000		1	.057	.420	1.52	.804	.325	.317	.199	.009	.210	.041	0	.215
minepump_spec5_product19_true-unreach-call.cil.c	timeout	906	889	5204885504		181	5.50	.019	874	true	11.9	6.34	354787328		1	.587	.001	.011	.030			true	8.74	4.89	354967552		.464	.434	.967	.250	.381	.368	.222	.028	.250	.268	true	8.73	4.87	310599680		1	.052	.929	1.54	.252	.824	.812	.721	.015	.737	.044	0	.739
minepump_spec5_product20_true-unreach-call.cil.c	timeout	906	888	5206736896		185	5.37	.014	873	true	11.2	6.05	374566912		1	.778	.00	.008	.099			true	8.86	4.94	349044736		.552	.513	1.04	.257	.430	.417	.260	.023	.283	.292	true	8.68	4.84	310067200		1	.053	.382	1.37	.264	.311	.299	.173	.011	.186	.032	0	.198
minepump_spec5_product21_true-unreach-call.cil.c	timeout	906	890	5134893056		192	5.31	.010	872	true	11.3	6.01	342376448		1	.895		.011				true	9.50	5.32	348663808		.088	.497	1.69	.358	.388	.375	.244	.023	.267	.283	true	9.66	5.35	332771328		1	.056	.564	1.81	.804	.461	.436	.295	.021	.318	.043	0	.321
minepump_spec5_product22_true-unreach-call.cil.c	timeout	905	887	5208567808		180	5.49	.010	872	true	11.7	6.30	379412480		1	1.05	.00	.019	.100			true	9.08	5.09	349995008		.489	.549	1.23	.325	.444	.430	.260	.017	.277	.288	true	9.29	5.18	326180864		1	.055	.531	1.68	.773	.394	.373	.235	.020	.256	.041	0	.262
minepump_spec5_product23_true-unreach-call.cil.c	timeout	906	892	5132849152		180	5.51	.013	876	true	12.1	6.46	387649536		1	1.04	.001	.006	.040			true	9.05	5.06	349786112		.439	.518	1.15	.256	.437	.426	.283	.019	.302	.317	true	9.55	5.30	329732096		1	.056	.503	1.80	.899	.392	.376	.253	.020	.274	.044	0	.281
minepump_spec5_product24_true-unreach-call.cil.c	timeout	906	892	5136318464		181	5.53	.006	877	true	11.9	6.34	382943232		1	1.06	.00	.014	.151			true	9.13	5.07	349081600		.568	.560	1.18	.295	.469	.450	.279	.018	.297	.316	true	9.55	5.32	334794752		1	.057	.504	1.70	.839	.414	.399	.262	.021	.285	.042	0	.289
minepump_spec5_product25_true-unreach-call.cil.c	timeout	906	892	5117915136		196	5.24	.012	877	true	9.96	5.39	360345600		1	.740	.00	.008	.122			true	9.15	5.07	345149440		.498	.417	.921	.249	.361	.349	.235	.013	.248	.262	true	8.94	4.97	319295488		1	.048	.466	1.53	.326	.360	.349	.225	.015	.242	.037	0	.244
minepump_spec5_product26_true-unreach-call.cil.c	timeout	905	891	3708538880		174	4.84	.012	877	true	11.0	5.92	352837632		1	.750	.00	.015	.085			true	8.42	4.73	345079808		.449	.407	.896	.249	.338	.335	.222	.011	.233	.248	true	8.67	4.83	311070720		1	.049	.414	1.46	.743	.342	.334	.219	.017	.237	.034	0	.240
minepump_spec5_product27_true-unreach-call.cil.c	timeout	905	888	5222174720		189	5.40	.011	873	true	12.0	6.38	384757760		1	.739	.00	.009	.078			true	7.98	4.49	341483520		.384	.387	.860	.237	.322	.314	.191	.012	.203	.219	true	8.51	4.77	314744832		1	.050	.760	1.38	.288	.693	.685	.586	.014	.601	.034	0	.608
minepump_spec5_product28_true-unreach-call.cil.c	timeout	906	888	5221629952		182	5.38	.012	873	true	11.7	6.28	379379712		1	.979	.001	.004	.097			true	8.70	4.86	346832896		.486	.378	.882	.221	.298	.286	.157	.013	.170	.186	true	8.53	4.75	309792768		1	.049	.403	1.38	.264	.332	.322	.227	.014	.242	.036	0	.245
minepump_spec5_product29_true-unreach-call.cil.c	timeout	906	891	5130698752		196	5.37	.016	875	true	11.7	6.24	374779904		1	.840	.001	.009	.027			true	9.65	5.33	348971008		.506	.649	1.37	.339	.557	.548	.360	.020	.380	.400	true	9.55	5.30	323420160		1	.057	.686	1.86	.779	.581	.567	.416	.020	.437	.050	0	.451
minepump_spec5_product30_true-unreach-call.cil.c	timeout	905	888	5197209600		177	5.29	.006	873	true	11.8	6.24	357842944		1	.749	.00	.025	.265			true	9.07	5.04	350539776		.528	.519	1.15	.320	.421	.396	.260	.020	.280	.304	true	9.52	5.26	331419648		1	.054	.948	1.72	.376	.836	.828	.684	.019	.704	.039	0	.708
minepump_spec5_product31_true-unreach-call.cil.c	timeout	905	891	5135753216		183	5.18	.010	876	true	11.5	6.12	375132160		1	.986		.009				true	9.44	5.23	349634560		.429	.655	1.29	.283	.562	.553	.383	.023	.406	.420	true	9.68	5.38	323325952		1	.061	.491	1.75	.831	.398	.381	.251	.021	.274	.042	0	.276
minepump_spec5_product32_true-unreach-call.cil.c	timeout	906	888	5257560064		181	5.15	.017	872	true	12.9	6.84	398938112		1	.986	.001	.005	.049			true	8.88	4.92	354185216		.538	.503	1.14	.295	.417	.410	.261	.019	.280	.302	true	9.27	5.19	322174976		1	.054	.546	1.72	.720	.440	.420	.283	.020	.304	.042	0	.310
minepump_spec5_product33_true-unreach-call.cil.c	timeout	909	894	5215121408		116	4.80	83.3	775	true	23.8	12.4	591372288		1	.827	.060	2.32	.153	4.60	.861	true	8.87	4.93	350531584		.461	.410	1.03	.272	.328	.317	.161	.027	.188	.210	true	9.53	5.40	333987840		6	.872	.476	1.32	.303	.411	.400	.254	.017	.310	.236	1	.279
minepump_spec5_product34_true-unreach-call.cil.c	timeout	907	892	5101244416		105	4.70	65.8	793	true	23.6	12.3	615116800		1	.860	.095	2.00	.043	4.36	.957	true	8.73	4.87	352722944		.519	.463	1.02	.252	.386	.377	.190	.037	.227	.252	true	8.91	5.05	320352256		3	.323	.294	1.38	.695	.234	.221	.136	.012	.184	.111	1	.151
minepump_spec5_product35_true-unreach-call.cil.c	timeout	906	893	5113446400		104	5.02	75.9	783	true	62.8	31.8	1193754624		6	1.83	1.77	9.13	2.27	12.3	8.10	true	9.03	5.03	347824128		.511	.590	1.16	.241	.502	.481	.281	.057	.338	.361	true	9.18	5.14	322179072		3	.298	.814	1.45	.261	.714	.704	.149	.014	.187	.111	1	.168
minepump_spec5_product36_true-unreach-call.cil.c	timeout	905	892	1925718016		60	3.45	703	172	true	55.3	28.1	1033682944		4	1.84	1.78	5.49	1.93	10.7	6.34	true	13.2	7.31	387104768		.866	1.85	2.98	.401	1.72	1.68	.929	.303	1.23	1.31	true	13.2	8.28	362897408		20	1.57	1.19	3.42	.468	1.08	1.07	.854	.034	1.02	1.28	1	.904
minepump_spec5_product37_true-unreach-call.cil.c	timeout	904	892	2905546752		65	4.52	561	309	true	30.0	15.5	661860352		1	1.40	.110	2.68	.339	6.29	1.21	true	12.4	6.87	385724416		.568	1.53	2.81	.503	1.30	1.25	.717	.165	.882	.931	true	14.1	8.48	367190016		14	1.39	.931	3.55	.577	.817	.786	.567	.045	.723	1.01	1	.624
minepump_spec5_product38_true-unreach-call.cil.c	timeout	906	892	2921250816		64	4.65	556	315	true	27.6	14.2	688541696		1	1.09	.100	.006	.079	5.26	2.10	true	13.4	7.23	394772480		.693	1.71	3.02	.515	1.56	1.52	.831	.228	1.06	1.13	true	13.7	8.35	358588416		14	1.55	.907	3.42	.572	.790	.764	.538	.037	.707	.992	1	.583
minepump_spec5_product39_true-unreach-call.cil.c	timeout	904	891	2942156800		62	4.29	601	268	true	68.0	34.5	1331023872		5	2.34	1.51	9.56	1.99	13.9	8.86	true	13.1	7.25	381267968		.672	1.69	2.99	.485	1.53	1.50	.872	.248	1.12	1.19	true	14.2	8.64	358133760		14	1.39	.964	3.75	.958	.831	.806	.572	.048	.740	1.07	1	.630
minepump_spec5_product40_true-unreach-call.cil.c	timeout	905	892	2142195712		57	4.30	668	205	true	421	212	4662988800		20	3.50	38.4	.005	20.5	38.8	101	true	12.5	6.87	389263360		.568	1.63	2.84	.460	1.48	1.44	.868	.228	1.10	1.17	true	12.0	7.02	353730560		10	.926	.859	2.81	.517	.748	.719	.492	.040	.583	.575	1	.539
minepump_spec5_product41_true-unreach-call.cil.c	timeout	905	892	3516014592		84	4.30	439	426	true	26.9	13.9	602103808		1	.961	.043	2.26	.148	5.44	.987	true	10.3	5.72	367943680		.482	1.08	1.91	.314	.967	.949	.582	.118	.700	.728	true	9.47	5.38	326545408		3	.359	.444	1.60	.325	.350	.339	.221	.018	.265	.128	1	.247
minepump_spec5_product42_true-unreach-call.cil.c	timeout	907	888	3601924096		83	4.51	430	431	true	24.2	12.5	614031360		1	.858	.127	2.06	.131	3.21	2.90	true	11.2	6.24	367595520		.617	1.10	2.14	.412	.960	.940	.532	.118	.650	.686	true	10.3	5.99	338231296		6	.590	.573	2.03	.353	.473	.455	.314	.021	.389	.315	1	.343
minepump_spec5_product43_true-unreach-call.cil.c	timeout	907	893	3231801344		76	4.43	489	378	true	66.0	33.5	1175670784		5	2.18	2.17	8.91	2.73	12.9	7.65	true	11.1	6.15	367345664		.595	1.27	2.16	.390	1.16	1.12	.648	.155	.803	.863	true	12.0	7.16	358100992		11	1.42	.775	2.32	.462	.633	.621	.439	.029	.536	.605	2	.474
minepump_spec5_product44_true-unreach-call.cil.c	timeout	905	892	1972707328		55	3.40	692	183	true	44.2	22.5	896372736		3	1.54	1.17	.006	1.44	7.72	5.52	true	13.4	7.56	390955008		.710	2.23	3.43	.482	2.06	2.04	1.20	.369	1.57	1.64	true	17.8	11.8	378540032		21	4.07	1.14	4.24	.585	1.03	1.01	.727	.056	1.01	1.88	0	.794
minepump_spec5_product45_true-unreach-call.cil.c	timeout	905	892	2064257024		52	4.26	675	199	true	33.2	17.1	730206208		1	1.27	.821	2.96	.318	7.18	1.57	true	13.1	7.20	395165696		.632	1.66	3.07	.605	1.49	1.46	.872	.201	1.07	1.14	true	15.8	9.77	363167744		14	1.88	1.66	4.36	.627	1.44	1.43	.682	.054	.865	1.31	1	.748
minepump_spec5_product46_true-unreach-call.cil.c	timeout	905	892	2046054400		51	4.24	670	205	true	27.9	14.4	660959232		1	1.34	.113	2.27	.097	5.94	1.24	true	14.3	7.99	405118976		.887	2.18	3.72	.513	1.99	1.96	1.32	.225	1.55	1.59	true	16.1	9.77	374644736		14	2.09	1.58	4.16	.545	1.41	1.40	.764	.050	.928	1.30	1	1.21
minepump_spec5_product47_true-unreach-call.cil.c	timeout	905	891	2129080320		50	4.62	693	179	true	84.5	42.7	1557684224		6	2.78	2.07	.012	2.77	16.5	11.4	true	16.5	9.01	425435136		1.01	2.59	4.16	.469	2.38	2.33	1.49	.390	1.88	1.93	true	13.5	8.02	367632384		10	1.06	.966	3.52	1.08	.802	.785	.531	.047	.649	.841	1	.583
minepump_spec5_product48_true-unreach-call.cil.c	timeout	906	891	3014717440		54	4.60	616	254	true	226	114	3390763008		15	3.69	19.3	.008	10.8	30.3	40.8	true	12.7	7.09	388050944		.603	1.78	3.08	.507	1.66	1.65	.924	.322	1.25	1.29	true	13.1	7.88	359178240		10	1.12	1.36	3.34	.533	.832	.790	.576	.049	.695	.791	1	.632
minepump_spec5_product49_true-unreach-call.cil.c	timeout	906	893	5126254592		91	5.03	73.3	786	true	27.7	14.3	632975360		1	1.16	.078	2.53	.116	5.62	1.20	true	11.3	6.26	382406656		.571	1.15	2.22	.321	1.02	.982	.578	.087	.665	.710	true	9.93	5.58	329957376		3	.324	.933	1.85	.397	.808	.795	.664	.020	.710	.137	1	.691
minepump_spec5_product50_true-unreach-call.cil.c	timeout	906	892	5121679360		89	5.47	78.4	779	true	29.1	15.0	662024192		1	1.17	.112	2.60	.124	6.33	1.18	true	11.4	6.32	383238144		.607	1.10	2.29	.456	.975	.934	.490	.100	.590	.660	true	11.4	6.50	352714752		5	.617	.716	2.51	.455	.606	.574	.401	.035	.506	.432	1	.445
minepump_spec5_product51_true-unreach-call.cil.c	timeout	908	893	5143244800		90	5.84	99.6	757	true	60.2	30.6	1041088512		3	2.44	1.76	6.12	1.38	12.8	6.38	true	11.4	6.36	374075392		.721	1.10	2.15	.411	.977	.958	.533	.118	.651	.696	true	11.4	6.52	334032896		6	.630	.650	2.50	.911	.547	.530	.353	.034	.441	.422	2	.407
minepump_spec5_product52_true-unreach-call.cil.c	timeout	904	892	2944012288		60	4.50	610	261	true	61.8	31.4	1037090816		3	2.22	1.40	6.05	1.68	12.8	6.78	true	11.3	6.28	372670464		.570	1.09	2.21	.496	.952	.920	.503	.121	.624	.657	true	14.3	8.82	364855296		13	1.49	1.00	3.90	.664	.878	.854	.620	.047	.772	1.14	1	.675
minepump_spec5_product53_true-unreach-call.cil.c	timeout	906	893	5203808256		78	6.03	77.5	782	true	33.0	16.9	804737024		1	1.48	.390	3.04	.237	7.35	1.13	true	14.1	7.59	401190912		.372	1.38	3.48	.696	1.20	1.16	.663	.148	.811	.849	true	10.5	5.97	345522176		3	.398	.575	2.25	.942	.476	.457	.323	.021	.367	.185	1	.351
minepump_spec5_product54_true-unreach-call.cil.c	timeout	905	891	3763580928		75	6.22	64.5	793	true	35.7	18.3	812285952		1	2.03	.795	2.85	.221	7.30	1.09	true	14.7	7.86	401428480		.388	1.59	3.90	1.14	1.34	1.29	.753	.173	.926	.975	true	12.5	7.26	366194688		5	.748	1.22	3.08	.708	1.06	1.05	.440	.043	.534	.377	1	.910
minepump_spec5_product55_true-unreach-call.cil.c	timeout	906	891	5246029824		78	6.49	73.8	783	true	72.3	36.6	1451524096		5	2.60	2.36	.004	1.51	16.6	6.94	true	14.4	7.86	403410944		.663	1.87	3.57	.606	1.69	1.64	.885	.315	1.20	1.26	true	12.6	7.30	370466816		5	.827	.780	3.03	.685	.640	.611	.434	.033	.520	.360	1	.476
minepump_spec5_product56_true-unreach-call.cil.c	timeout	904	890	3074801664		56	5.47	537	330	true	59.0	29.8	1028972544		3	2.43	1.04	5.71	1.32	13.1	5.67	true	14.3	7.82	414220288		.230	1.65	3.74	1.08	1.49	1.45	.897	.203	1.10	1.14	true	14.9	8.64	381685760		8	1.27	1.56	3.98	.831	1.38	1.34	.666	.051	.788	.677	1	.721
minepump_spec5_product57_true-unreach-call.cil.c	timeout	905	891	2997850112		58	4.93	557	311	true	32.8	16.8	808603648		1	1.33	.166	3.12	.479	7.13	1.88	true	12.1	6.66	377188352		.657	1.24	2.42	.475	1.12	1.09	.663	.092	.755	.809	true	11.7	6.76	349650944		5	.794	.724	2.58	.475	.606	.591	.411	.036	.526	.381	1	.454
minepump_spec5_product58_true-unreach-call.cil.c	timeout	904	891	2969849856		58	4.84	594	275	true	31.4	16.2	717971456		1	1.26	.077	.005	.083	7.58	1.33	true	11.2	6.18	376287232		.511	1.11	2.23	.411	.953	.933	.495	.105	.600	.643	true	11.9	6.83	355926016		5	.732	1.41	2.72	.490	1.25	1.23	1.05	.037	1.14	.349	1	1.09
minepump_spec5_product59_true-unreach-call.cil.c	timeout	905	891	3017904128		57	5.15	615	253	true	63.0	32.1	1175068672		4	2.50	2.51	.006	1.38	13.6	5.44	true	11.0	6.14	366407680		.591	1.15	2.17	.339	1.00	.979	.568	.105	.673	.707	true	12.0	6.82	350248960		6	.834	.754	2.64	.948	.645	.632	.434	.037	.529	.370	2	.480
minepump_spec5_product60_true-unreach-call.cil.c	timeout	904	891	2986418176		55	4.73	555	314	true	253	127	4128813056		14	3.00	15.6	.013	10.8	29.2	61.2	true	12.2	6.70	372383744		.726	1.20	2.31	.442	1.06	1.01	.600	.139	.739	.778	true	12.5	7.12	349827072		5	.767	.773	2.82	1.07	.689	.675	.491	.038	.594	.393	1	.535
minepump_spec5_product61_true-unreach-call.cil.c	timeout	905	891	3058290688		55	5.69	495	372	true	42.9	21.9	891396096		1	2.45	.780	4.13	.335	8.09	2.75	true	14.8	8.05	415129600		.308	1.56	3.91	1.23	1.37	1.32	.766	.177	.943	1.00	true	11.8	6.62	362262528		3	.896	.700	2.37	.651	.534	.507	.357	.033	.420	.311	1	.397
minepump_spec5_product62_true-unreach-call.cil.c	timeout	905	891	3078393856		55	5.30	517	350	true	42.5	21.8	998920192		1	1.96	.852	3.90	.187	8.84	2.93	true	14.1	7.56	415444992		.263	1.54	3.63	.766	1.37	1.34	.883	.094	.977	1.01	true	13.8	7.92	367714304		5	.924	.999	3.63	.745	.869	.829	.578	.045	.681	.519	1	.627
minepump_spec5_product63_true-unreach-call.cil.c	timeout	905	891	3053686784		54	5.95	589	275	true	61.5	31.2	1046536192		3	2.74	.979	7.00	1.16	14.7	4.87	true	15.4	8.30	386637824		.291	1.83	4.32	.793	1.64	1.55	.901	.214	1.11	1.17	true	14.1	8.01	369418240		5	.884	.988	3.64	1.25	.810	.783	.574	.049	.683	.495	1	.627
minepump_spec5_product64_true-unreach-call.cil.c	timeout	904	890	3070738432		51	5.65	519	347	true	289	145	4451389440		14	3.42	15.9	.003	16.5	37.7	63.0	true	13.8	7.54	399405056		.731	1.53	3.34	.772	1.31	1.27	.783	.145	.928	.960	true	14.3	8.20	371257344		5	.915	.954	3.75	.766	.815	.764	.522	.048	.628	.546	1	.586
minepump_spec5_productSimulator_true-unreach-call.cil.c	timeout	905	888	2367770624		45	9.91	665	196	true	95.0	48.0	1703079936		4	4.49	1.29	.005	1.17	25.3	6.32	true	22.9	13.0	586473472		.776	3.68	8.53	1.97	3.19	3.11	1.68	.703	2.38	2.48	true	27.8	17.6	631816192		21	4.54	2.20	9.31	1.95	1.87	1.82	1.30	.136	1.60	2.79	2	1.46
test/programs/benchmarks/product-lines/	status	cputime (s)	walltime (s)	memUsage	host	k	BMC formula creation (s)	SMT check (s)	Bounds check (s)	status	cputime (s)	walltime (s)	memUsage	host	k	BMC formula creation (s)	SMT check (s)	Invariant generation (s)	Bounds check (s)	Induction formula creation (s)	Induction check (s)	status	cputime (s)	walltime (s)	memUsage	host	Refinement (s)	Precision adjustment (s)	CPA algorithm (s)	Post operator (s)	Prec operator (s)	Abstraction (s)	Solving (s)	Model enumeration (s)	SMT without itp (s)	Boolean abstraction (s)	status	cputime (s)	walltime (s)	memUsage	host	Attempted forced coverings	Refinement (s)	Precision adjustment (s)	CPA algorithm (s)	Post operator (s)	Prec operator (s)	Abstraction (s)	Solving (s)	Model enumeration (s)	SMT without itp (s)	Forced covering (s)	Successful forced coverings	Boolean abstraction (s)
total tasks	357	236000	231000	1178820411392		39570	1780	32300	166000	357	105000	64200	921585393664		883	610	343	7540	372	2320	3600	357	113000	109000	377078599680		861	44300	45700	666	44200	44200	1420	42200	43600	43500	357	78700	74900	424366759936		2143	6610	485	11000	570	406	391	211	125	518	9430	552	340
correct results	41	1110	681	27773865984		280	157	9.48	7.73	270	19200	9730	339821944832		865	515	342	2390	372	2320	3600	239	4270	2930	102134771712		534	1130	1540	188	1090	1080	424	544	969	760	251	5640	4110	111896027136		1374	823	356	2340	305	309	300	161	92.6	290	1390	390	257
correct true	28	590	318	16492355584		243	94.2	5.71	5.30	257	17000	8640	304165896192		828	440	338	1930	367	2030	3510	239	4270	2930	102134771712		534	1130	1540	188	1090	1080	424	544	969	760	242	4610	3330	94193483776		1326	632	257	1860	203	220	214	116	60.1	211	1190	384	179
correct false	13	522	362	11281510400		37	62.8	3.77	2.43	13	2180	1100	35656048640		37	74.9	4.11	465	4.66	294	85.7	0															9	1030	774	17702543360		48	191	99.8	477	101	88.7	86.3	44.6	32.5	79.0	197	6	77.2
incorrect results	0									0												0															0
incorrect true	0									0												0															0
incorrect false	0									0												0															0
score (357 tasks, max score: 615)	69									527												478															493
Run set	bmc-bitprecise.BMC.ProductLines									k-induction-bitprecise.k-Induction.ProductLines												predicateAnalysis-bitprecise.PredicateAbstraction.ProductLines															impact-bitprecise.Impact.ProductLines