ukojak.2017-01-13_1305.results.sv-comp17.ReachSafety-ProductLines.xml.bz2.merged.xml.bz2

Tool	ULTIMATE Kojak f7c3ed31
Limits	timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host	apollon*
OS	Linux 4.4.0-59-generic
System	CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution	2017-01-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]]
Run set	sv-comp17.ReachSafety-ProductLines
Options	[[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/product-lines/	verifier status	score	witness	inspect witness	cpu (s)	wall (s)	energy (J)	mem (MB)	blkio-w (MB)	blkio-r (MB)	validator cpachecker violation t<90s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator uautomizer violation t<90s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator cpachecker correctness t<900s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator uautomizer correctness t<900s status	cpu (s)	wall (s)	energy (J)	mem (MB)
elevator_spec14_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	1800	2.3	0	error (invalid witness file)	.54	.36	12	40	error (invalid witness file)	6.6	3.5	130	310	-					-
elevator_spec14_product24_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	630	11000	2000	2.3	0	error (invalid witness file)	.54	.34	11	40	error (invalid witness file)	6.1	3.2	120	300	-					-
elevator_spec14_product28_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	11000	1700	2.3	0	error (invalid witness file)	.55	.36	12	42	error (invalid witness file)	6.4	3.4	110	300	-					-
elevator_spec14_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	640	11000	2400	2.3	0	error (invalid witness file)	.52	.33	11	41	error (invalid witness file)	6.5	3.4	120	300	-					-
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	13000	2000	2.3	0	error (invalid witness file)	.49	.31	8.0	39	error (invalid witness file)	6.5	3.4	120	300	-					-
elevator_spec1_product18_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	3500	2.3	0	error (invalid witness file)	.56	.37	11	42	error (invalid witness file)	6.1	3.2	110	290	-					-
elevator_spec1_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	640	12000	2400	2.3	0	error (invalid witness file)	.50	.33	11	40	error (invalid witness file)	6.4	3.4	120	300	-					-
elevator_spec1_product22_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	12000	2100	2.3	0	error (invalid witness file)	.50	.33	10	40	error (invalid witness file)	6.5	3.4	130	300	-					-
elevator_spec1_product24_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	640	12000	4500	2.3	0	error (invalid witness file)	.56	.37	5.7	40	error (invalid witness file)	6.3	3.3	130	300	-					-
elevator_spec1_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	12000	2400	2.3	0	error (invalid witness file)	.50	.31	8.9	40	error (invalid witness file)	5.4	2.9	49	290	-					-
elevator_spec1_product28_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	640	11000	3400	2.3	0	error (invalid witness file)	.53	.34	9.9	40	error (invalid witness file)	5.9	3.2	89	300	-					-
elevator_spec1_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	11000	2400	2.3	0	error (invalid witness file)	.53	.35	8.2	39	error (invalid witness file)	7.2	3.7	140	320	-					-
elevator_spec1_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	630	12000	3800	2.3	0	error (invalid witness file)	.50	.34	8.9	39	error (invalid witness file)	6.6	3.5	120	310	-					-
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	11000	1900	2.3	0	error (invalid witness file)	.50	.32	11	40	error (invalid witness file)	7.5	3.9	120	330	-					-
elevator_spec2_product18_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	14000	3200	2.3	0	error (invalid witness file)	.49	.33	8.3	39	error (invalid witness file)	6.3	3.3	140	300	-					-
elevator_spec2_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2600	2.3	0	error (invalid witness file)	.54	.34	10	40	error (invalid witness file)	6.9	3.6	110	310	-					-
elevator_spec2_product22_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	3100	2.3	0	error (invalid witness file)	.52	.34	8.2	39	error (invalid witness file)	6.4	3.4	120	300	-					-
elevator_spec2_product24_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	11000	2400	2.3	0	error (invalid witness file)	.52	.33	12	39	error (invalid witness file)	6.2	3.3	110	300	-					-
elevator_spec2_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	3400	2.3	0	error (invalid witness file)	.53	.36	13	40	error (invalid witness file)	6.3	3.3	130	310	-					-
elevator_spec2_product28_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	4300	2.3	0	error (invalid witness file)	.53	.34	10	39	error (invalid witness file)	6.2	3.3	130	290	-					-
elevator_spec2_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	12000	2400	2.3	0	error (invalid witness file)	.52	.33	6.7	40	error (invalid witness file)	6.4	3.4	130	300	-					-
elevator_spec2_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2400	2.3	0	error (invalid witness file)	.55	.34	8.9	42	error (invalid witness file)	6.2	3.3	130	290	-					-
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	610	13000	3700	2.3	0	error (invalid witness file)	.53	.34	10	43	error (invalid witness file)	5.9	3.1	120	300	-					-
elevator_spec3_product03_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	11000	2200	2.3	0	error (invalid witness file)	.48	.31	12	40	error (invalid witness file)	6.8	3.6	130	320	-					-
elevator_spec3_product11_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	10000	2300	2.3	0	error (invalid witness file)	.53	.34	8.9	40	error (invalid witness file)	6.5	3.4	130	300	-					-
elevator_spec3_product19_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	9700	3800	2.3	0	error (invalid witness file)	.50	.35	9.2	39	error (invalid witness file)	6.6	3.5	120	300	-					-
elevator_spec3_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	9900	2200	2.3	0	error (invalid witness file)	.51	.33	11	40	error (invalid witness file)	5.9	3.2	120	290	-					-
elevator_spec3_product23_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	11000	2300	2.3	0	error (invalid witness file)	.50	.33	7.4	39	error (invalid witness file)	6.3	3.3	130	300	-					-
elevator_spec3_product24_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	11000	2100	2.3	0	error (invalid witness file)	.63	.40	5.4	39	error (invalid witness file)	6.5	3.5	100	320	-					-
elevator_spec3_product27_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	13000	2200	2.3	0	error (invalid witness file)	.52	.34	8.3	40	error (invalid witness file)	6.0	3.2	120	300	-					-
elevator_spec3_product28_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	11000	2100	2.3	0	error (invalid witness file)	.53	.34	8.0	43	error (invalid witness file)	7.2	3.7	110	320	-					-
elevator_spec3_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	11000	2300	2.3	0	error (invalid witness file)	.49	.32	6.6	41	error (invalid witness file)	6.5	3.5	110	310	-					-
elevator_spec3_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	11000	2500	2.3	0	error (invalid witness file)	.53	.34	10	41	error (invalid witness file)	6.6	3.5	120	300	-					-
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	11000	2600	2.3	0	error (invalid witness file)	.49	.32	9.0	41	error (invalid witness file)	6.2	3.3	120	300	-					-
elevator_spec9_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	13000	2900	2.3	0	error (invalid witness file)	.54	.35	9.1	43	error (invalid witness file)	6.3	3.3	120	300	-					-
elevator_spec9_product28_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	13000	2700	2.3	0	error (invalid witness file)	.51	.34	13	40	error (invalid witness file)	6.4	3.4	130	300	-					-
elevator_spec9_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	11000	2800	2.3	0	error (invalid witness file)	.52	.35	11	39	error (invalid witness file)	5.8	3.1	110	300	-					-
elevator_spec9_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	13000	3200	2.3	0	error (invalid witness file)	.73	.46	8.0	42	error (invalid witness file)	6.8	3.6	120	310	-					-
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	580	12000	3400	2.3	0	error (invalid witness file)	.52	.33	11	40	error (invalid witness file)	6.0	3.2	100	300	-					-
elevator_spec13_product21_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	540	11000	3400	2.3	0	-					-					error (invalid witness file)	.54	.35	8.6	39	error (invalid witness file)	5.9	3.2	110	300
elevator_spec13_product22_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	580	13000	2300	2.3	0	-					-					error (invalid witness file)	.66	.42	8.2	40	error (invalid witness file)	6.2	3.3	89	300
elevator_spec13_product23_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	730	14000	1900	2.3	0	-					-					error (invalid witness file)	.53	.33	13	40	error (invalid witness file)	6.0	3.2	91	300
elevator_spec13_product24_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	580	11000	2400	2.3	0	-					-					error (invalid witness file)	.56	.36	11	41	error (invalid witness file)	7.5	3.9	120	320
elevator_spec13_product29_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	540	9500	2800	2.3	0	-					-					error (invalid witness file)	.64	.40	7.3	40	error (invalid witness file)	5.8	3.1	120	290
elevator_spec13_product30_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	580	10000	2500	2.3	0	-					-					error (invalid witness file)	.65	.43	6.6	40	error (invalid witness file)	7.3	3.8	130	320
elevator_spec13_product31_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	740	14000	4100	2.3	0	-					-					error (invalid witness file)	.61	.38	8.1	39	error (invalid witness file)	6.3	3.4	120	300
elevator_spec13_product32_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	580	11000	2500	2.3	0	-					-					error (invalid witness file)	.51	.33	13	40	error (invalid witness file)	5.9	3.1	91	290
elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	550	12000	2700	2.3	0	-					-					error (invalid witness file)	.64	.42	8.5	40	error (invalid witness file)	6.3	3.3	87	300
elevator_spec14_product03_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	550	11000	3200	2.3	0	-					-					error (invalid witness file)	.60	.38	11	41	error (invalid witness file)	6.5	3.4	120	300
elevator_spec14_product11_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	540	11000	2700	2.3	0	-					-					error (invalid witness file)	.55	.36	7.5	40	error (invalid witness file)	6.1	3.3	110	300
elevator_spec14_product19_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	550	10000	3100	2.3	0	-					-					error (invalid witness file)	.63	.40	8.1	39	error (invalid witness file)	6.6	3.4	120	300
elevator_spec14_product23_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	570	11000	1600	2.3	0	-					-					error (invalid witness file)	.49	.32	7.4	41	error (invalid witness file)	6.1	3.2	95	300
elevator_spec14_product27_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	550	11000	3000	2.3	0	-					-					error (invalid witness file)	.51	.32	12	39	error (invalid witness file)	6.6	3.5	100	300
elevator_spec14_product31_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	570	12000	1800	2.3	0	-					-					error (invalid witness file)	.51	.33	12	41	error (invalid witness file)	6.4	3.4	120	300
elevator_spec1_product01_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	680	12000	2600	2.3	0	-					-					error (invalid witness file)	.54	.34	10	40	error (invalid witness file)	6.1	3.2	79	300
elevator_spec1_product03_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	620	13000	2200	2.3	0	-					-					error (invalid witness file)	.51	.32	11	39	error (invalid witness file)	5.5	3.0	79	300
elevator_spec1_product09_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	680	12000	2300	2.3	0	-					-					error (invalid witness file)	.50	.32	12	39	error (invalid witness file)	5.9	3.1	83	300
elevator_spec1_product11_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	620	11000	2000	2.3	0	-					-					error (invalid witness file)	.61	.38	9.5	40	error (invalid witness file)	6.1	3.3	100	300
elevator_spec1_product17_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	680	11000	2100	2.3	0	-					-					error (invalid witness file)	.51	.33	9.5	40	error (invalid witness file)	6.1	3.2	90	300
elevator_spec1_product19_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	620	12000	2300	2.3	0	-					-					error (invalid witness file)	.65	.41	7.4	39	error (invalid witness file)	6.6	3.4	120	310
elevator_spec1_product21_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	14000	3500	2.4	0	-					-					error (invalid witness file)	.50	.33	11	40	error (invalid witness file)	5.7	3.1	80	290
elevator_spec1_product23_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	640	11000	3200	2.3	0	-					-					error (invalid witness file)	.50	.32	12	40	error (invalid witness file)	6.5	3.4	110	300
elevator_spec1_product25_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	680	13000	1900	2.3	0	-					-					error (invalid witness file)	.54	.35	13	42	error (invalid witness file)	6.1	3.2	110	300
elevator_spec1_product27_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	610	12000	2200	2.3	0	-					-					error (invalid witness file)	.66	.41	6.6	39	error (invalid witness file)	6.4	3.3	120	300
elevator_spec1_product29_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	2200	2.3	0	-					-					error (invalid witness file)	.64	.41	7.8	40	error (invalid witness file)	7.7	4.1	94	290
elevator_spec1_product31_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	640	12000	2200	2.3	0	-					-					error (invalid witness file)	.54	.34	11	42	error (invalid witness file)	6.1	3.2	97	300
elevator_spec2_product01_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	2000	2.3	0	-					-					error (invalid witness file)	.51	.33	13	39	error (invalid witness file)	6.3	3.4	130	300
elevator_spec2_product03_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	520	12000	3600	2.3	0	-					-					error (invalid witness file)	.47	.31	9.1	40	error (invalid witness file)	6.5	3.4	140	310
elevator_spec2_product09_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	11000	2200	2.3	0	-					-					error (invalid witness file)	.61	.39	12	42	error (invalid witness file)	6.3	3.4	120	300
elevator_spec2_product11_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	560	12000	2900	2.3	0	-					-					error (invalid witness file)	.64	.41	7.8	40	error (invalid witness file)	6.5	3.4	120	300
elevator_spec2_product17_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	2400	2.3	0	-					-					error (invalid witness file)	.59	.37	9.5	40	error (invalid witness file)	6.1	3.2	78	300
elevator_spec2_product19_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	550	11000	2700	2.3	0	-					-					error (invalid witness file)	.63	.40	9.3	39	error (invalid witness file)	5.9	3.2	87	300
elevator_spec2_product21_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	590	12000	2300	2.3	0	-					-					error (invalid witness file)	.54	.34	11	40	error (invalid witness file)	7.7	4.0	96	300
elevator_spec2_product23_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	12000	2100	2.3	0	-					-					error (invalid witness file)	.50	.32	7.4	39	error (invalid witness file)	6.7	3.6	120	300
elevator_spec2_product25_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	12000	1900	2.3	0	-					-					error (invalid witness file)	.53	.34	9.8	40	error (invalid witness file)	6.7	3.5	140	300
elevator_spec2_product27_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	550	12000	2600	2.3	0	-					-					error (invalid witness file)	.64	.40	8.7	39	error (invalid witness file)	6.4	3.4	120	300
elevator_spec2_product29_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	570	12000	3200	2.3	0	-					-					error (invalid witness file)	.63	.40	8.1	41	error (invalid witness file)	6.8	3.6	120	320
elevator_spec2_product31_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	15000	2800	2.3	0	-					-					error (invalid witness file)	.56	.36	14	41	error (invalid witness file)	6.4	3.4	120	300
elevator_spec3_product01_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	10000	2500	2.3	0	-					-					error (invalid witness file)	.52	.33	11	39	error (invalid witness file)	6.3	3.3	86	300
elevator_spec3_product09_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	12000	2500	2.3	0	-					-					error (invalid witness file)	.58	.38	9.8	41	error (invalid witness file)	6.0	3.2	110	300
elevator_spec3_product17_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	12000	2400	2.3	0	-					-					error (invalid witness file)	.66	.41	8.1	40	error (invalid witness file)	6.1	3.3	97	300
elevator_spec3_product18_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	520	9700	3100	2.3	0	-					-					error (invalid witness file)	.67	.43	10	45	error (invalid witness file)	6.5	3.4	120	300
elevator_spec3_product21_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	11000	3000	2.3	0	-					-					error (invalid witness file)	.64	.41	7.3	39	error (invalid witness file)	6.7	3.6	54	300
elevator_spec3_product22_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	9700	2100	2.3	0	-					-					error (invalid witness file)	.54	.35	7.9	43	error (invalid witness file)	5.8	3.1	59	300
elevator_spec3_product25_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	10000	2500	2.3	0	-					-					error (invalid witness file)	.63	.40	7.5	39	error (invalid witness file)	6.3	3.3	120	310
elevator_spec3_product26_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	520	11000	3000	2.3	0	-					-					error (invalid witness file)	.64	.41	7.9	40	error (invalid witness file)	6.4	3.4	120	300
elevator_spec3_product29_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	12000	2900	2.3	0	-					-					error (invalid witness file)	.55	.35	13	44	error (invalid witness file)	6.1	3.2	88	300
elevator_spec3_product30_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	510	12000	2800	2.3	0	-					-					error (invalid witness file)	.52	.34	11	41	error (invalid witness file)	6.6	3.5	110	300
elevator_spec9_product09_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	2600	2.3	0	-					-					error (invalid witness file)	.68	.42	8.8	41	error (invalid witness file)	6.4	3.3	120	310
elevator_spec9_product11_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	550	11000	3000	2.3	0	-					-					error (invalid witness file)	.58	.36	8.0	42	error (invalid witness file)	6.1	3.3	99	310
elevator_spec9_product25_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	660	13000	2400	2.3	0	-					-					error (invalid witness file)	.66	.43	8.4	42	error (invalid witness file)	6.5	3.5	120	310
elevator_spec9_product27_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	560	10000	3400	2.3	0	-					-					error (invalid witness file)	.54	.34	10	39	error (invalid witness file)	6.3	3.4	92	310
elevator_spec9_product29_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	2800	2.3	0	-					-					error (invalid witness file)	.47	.32	7.1	40	error (invalid witness file)	6.4	3.4	120	310
elevator_spec9_product31_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	530	11000	3600	2.3	0	-					-					error (invalid witness file)	.51	.33	8.2	39	error (invalid witness file)	5.7	3.1	94	280
email_spec0_product16_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	2900	2.3	0	error (invalid witness file)	.49	.31	5.9	41	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec0_product21_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	2100	2.3	0	error (invalid witness file)	.50	.32	13	40	error (invalid witness file)	6.4	3.4	130	300	-					-
email_spec0_product22_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	2600	2.3	0	error (invalid witness file)	.49	.33	7.1	40	error (invalid witness file)	6.4	3.4	120	300	-					-
email_spec0_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	12000	3500	2.3	0	error (invalid witness file)	.50	.31	7.6	40	error (invalid witness file)	7.3	3.8	130	310	-					-
email_spec0_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	12000	4500	2.3	0	error (invalid witness file)	.54	.34	10	42	error (invalid witness file)	6.3	3.4	120	300	-					-
email_spec0_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	12000	1900	2.3	0	error (invalid witness file)	.63	.40	7.4	39	error (invalid witness file)	6.3	3.3	120	310	-					-
email_spec0_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	15000	2700	2.3	0	error (invalid witness file)	.48	.31	9.6	39	error (invalid witness file)	6.6	3.5	120	310	-					-
email_spec0_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	3200	2.3	.0041	error (invalid witness file)	.51	.32	11	40	error (invalid witness file)	6.5	3.4	120	300	-					-
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	12000	5800	2.3	0	error (invalid witness file)	.51	.33	11	41	error (invalid witness file)	6.5	3.4	130	300	-					-
email_spec11_product15_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	15000	4600	2.3	0	error (invalid witness file)	.49	.32	11	39	error (invalid witness file)	6.9	3.6	59	300	-					-
email_spec11_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	3300	2.3	0	error (invalid witness file)	.49	.33	9.4	40	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec11_product22_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	2300	2.3	0	error (invalid witness file)	.47	.30	5.4	39	error (invalid witness file)	6.2	3.3	110	300	-					-
email_spec11_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	800	13000	3700	2.3	0	error (invalid witness file)	.50	.32	11	40	error (invalid witness file)	5.7	3.1	92	300	-					-
email_spec11_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	12000	2200	2.3	0	error (invalid witness file)	.58	.37	7.7	39	error (invalid witness file)	6.0	3.2	120	290	-					-
email_spec11_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	15000	1800	2.3	0	error (invalid witness file)	.48	.32	10	39	error (invalid witness file)	6.0	3.2	96	300	-					-
email_spec11_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	12000	3000	2.3	0	error (invalid witness file)	.65	.42	7.3	40	error (invalid witness file)	7.2	3.7	130	320	-					-
email_spec11_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	12000	2500	2.3	0	error (invalid witness file)	.50	.33	10	40	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	12000	5700	2.3	0	error (invalid witness file)	.49	.32	4.0	39	error (invalid witness file)	6.4	3.5	130	300	-					-
email_spec1_product14_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	12000	5600	2.3	0	error (invalid witness file)	.65	.42	7.2	40	error (invalid witness file)	6.2	3.3	110	310	-					-
email_spec1_product15_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	11000	5600	2.3	0	error (invalid witness file)	.50	.34	8.1	40	error (invalid witness file)	6.1	3.2	100	310	-					-
email_spec1_product16_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5600	2.3	0	error (invalid witness file)	.50	.33	9.3	41	error (invalid witness file)	6.3	3.3	90	290	-					-
email_spec1_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5600	2.3	0	error (invalid witness file)	.49	.32	4.3	42	error (invalid witness file)	6.4	3.4	140	290	-					-
email_spec1_product21_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	11000	5600	2.3	0	error (invalid witness file)	.49	.30	9.8	39	error (invalid witness file)	5.9	3.2	110	290	-					-
email_spec1_product22_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5600	2.3	0	error (invalid witness file)	.61	.40	7.0	43	error (invalid witness file)	7.2	3.8	150	320	-					-
email_spec1_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	14000	5600	2.3	0	error (invalid witness file)	.53	.34	11	42	error (invalid witness file)	6.5	3.4	120	300	-					-
email_spec1_product29_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5400	2.3	0	error (invalid witness file)	.52	.34	12	41	error (invalid witness file)	6.3	3.3	110	290	-					-
email_spec1_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5600	2.3	0	error (invalid witness file)	.51	.34	5.9	40	error (invalid witness file)	6.3	3.3	120	290	-					-
email_spec1_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5500	2.3	0	error (invalid witness file)	.46	.30	4.2	40	error (invalid witness file)	5.9	3.2	110	300	-					-
email_spec1_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5400	2.3	0	error (invalid witness file)	.51	.33	9.7	40	error (invalid witness file)	6.1	3.2	100	300	-					-
email_spec1_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5600	2.3	0	error (invalid witness file)	.50	.33	13	39	error (invalid witness file)	6.0	3.2	59	300	-					-
email_spec1_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5600	2.3	0	error (invalid witness file)	.56	.38	9.8	42	error (invalid witness file)	6.2	3.3	110	300	-					-
email_spec1_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5400	2.3	0	error (invalid witness file)	.50	.33	11	43	error (invalid witness file)	5.6	3.0	85	300	-					-
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	15000	4400	2.3	0	error (invalid witness file)	.50	.32	10	39	error (invalid witness file)	6.4	3.4	110	300	-					-
email_spec27_product17_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	720	13000	1800	2.3	0	error (invalid witness file)	.52	.32	11	39	error (invalid witness file)	6.2	3.3	110	300	-					-
email_spec27_product18_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	14000	1600	2.3	0	error (invalid witness file)	.50	.31	7.1	39	error (invalid witness file)	7.5	4.0	70	310	-					-
email_spec27_product19_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	720	14000	2200	2.3	.0041	error (invalid witness file)	.70	.44	6.9	39	error (invalid witness file)	5.9	3.2	110	290	-					-
email_spec27_product23_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	720	12000	1900	2.3	0	error (invalid witness file)	.54	.35	8.9	40	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec27_product24_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	720	13000	1700	2.3	0	error (invalid witness file)	.71	.44	8.4	45	error (invalid witness file)	6.6	3.4	110	300	-					-
email_spec27_product25_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	14000	1900	2.3	0	error (invalid witness file)	.57	.37	11	45	error (invalid witness file)	5.9	3.1	98	310	-					-
email_spec27_product27_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	12000	2800	2.3	0	error (invalid witness file)	.51	.35	8.2	40	error (invalid witness file)	5.7	3.0	110	290	-					-
email_spec27_product29_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	13000	1700	2.3	0	error (invalid witness file)	.51	.34	7.0	40	error (invalid witness file)	6.5	3.4	120	300	-					-
email_spec27_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2300	2.3	0	error (invalid witness file)	.51	.32	11	39	error (invalid witness file)	6.1	3.2	97	310	-					-
email_spec27_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	2700	2.3	0	error (invalid witness file)	.65	.41	9.6	45	error (invalid witness file)	6.3	3.4	120	320	-					-
email_spec27_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	2000	2.3	0	error (invalid witness file)	.50	.32	11	40	error (invalid witness file)	6.2	3.3	110	310	-					-
email_spec27_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	2500	2.3	0	error (invalid witness file)	.57	.37	13	40	error (invalid witness file)	6.1	3.3	110	310	-					-
email_spec27_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	2300	2.3	0	error (invalid witness file)	.47	.32	12	39	error (invalid witness file)	5.9	3.2	130	300	-					-
email_spec27_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	15000	2000	2.3	0	error (invalid witness file)	.59	.37	8.5	40	error (invalid witness file)	6.4	3.3	120	310	-					-
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5400	2.3	0	error (invalid witness file)	.48	.32	9.1	39	error (invalid witness file)	6.5	3.5	140	300	-					-
email_spec3_product13_false-unreach-call_true-termination.cil.c	unknown	0	wit	inspect	60	25	580	920	2.6	0	error (invalid witness file)	.51	.32	11	39	error (invalid witness file)	6.5	3.4	130	300	-					-
email_spec3_product17_false-unreach-call_true-termination.cil.c	unknown	0	wit	inspect	68	28	720	890	2.6	0	error (invalid witness file)	.50	.33	9.9	40	error (invalid witness file)	6.4	3.4	120	310	-					-
email_spec3_product18_false-unreach-call_true-termination.cil.c	unknown	0	wit	inspect	63	27	610	910	2.6	0	error (invalid witness file)	.52	.32	11	40	error (invalid witness file)	6.0	3.2	91	300	-					-
email_spec3_product19_false-unreach-call_true-termination.cil.c	unknown	0	wit	inspect	68	28	590	950	2.6	0	error (invalid witness file)	.49	.32	13	40	error (invalid witness file)	6.4	3.3	120	300	-					-
email_spec3_product23_false-unreach-call_true-termination.cil.c	unknown	0	wit	inspect	67	27	690	910	2.6	0	error (invalid witness file)	.58	.37	12	43	error (invalid witness file)	6.9	3.6	110	310	-					-
email_spec3_product24_false-unreach-call_true-termination.cil.c	unknown	0	wit	inspect	68	28	590	850	2.6	0	error (invalid witness file)	.53	.32	13	40	error (invalid witness file)	6.2	3.3	130	300	-					-
email_spec3_product25_false-unreach-call_true-termination.cil.c	unknown	0	wit	inspect	68	29	630	950	2.6	0	error (invalid witness file)	.50	.34	4.8	40	error (invalid witness file)	6.0	3.2	130	300	-					-
email_spec3_product27_false-unreach-call_true-termination.cil.c	unknown	0	wit	inspect	67	28	660	900	2.6	0	error (invalid witness file)	.57	.37	11	44	error (invalid witness file)	6.4	3.4	130	310	-					-
email_spec3_product28_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	3200	2.3	0	error (invalid witness file)	.56	.36	11	41	error (invalid witness file)	7.7	4.0	100	310	-					-
email_spec3_product29_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	13000	2000	2.3	0	error (invalid witness file)	.52	.32	13	40	error (invalid witness file)	6.3	3.3	130	300	-					-
email_spec3_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	13000	2100	2.3	0	error (invalid witness file)	.51	.32	10	40	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec3_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	16000	1900	2.3	0	error (invalid witness file)	.64	.41	6.7	39	error (invalid witness file)	6.6	3.5	120	310	-					-
email_spec3_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	13000	2700	2.3	0	error (invalid witness file)	.48	.31	10	39	error (invalid witness file)	6.0	3.2	120	310	-					-
email_spec3_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2000	2.3	0	error (invalid witness file)	.48	.31	10	40	error (invalid witness file)	5.9	3.2	110	290	-					-
email_spec3_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	15000	3000	2.3	0	error (invalid witness file)	.51	.32	9.8	39	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec3_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	12000	2200	2.3	0	error (invalid witness file)	.48	.31	11	39	error (invalid witness file)	6.7	3.5	130	310	-					-
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	12000	1700	2.5	0	error (invalid witness file)	.52	.33	12	41	error (invalid witness file)	6.1	3.2	110	300	-					-
email_spec4_product18_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	11000	1600	2.3	0	error (invalid witness file)	.66	.43	8.1	46	error (invalid witness file)	6.0	3.2	120	300	-					-
email_spec4_product19_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	12000	1800	2.3	0	error (invalid witness file)	.51	.34	10	41	error (invalid witness file)	6.5	3.4	110	300	-					-
email_spec4_product23_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	14000	2100	2.3	0	error (invalid witness file)	.54	.35	9.6	40	error (invalid witness file)	6.6	3.5	130	310	-					-
email_spec4_product24_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	13000	2700	2.3	0	error (invalid witness file)	.51	.33	9.6	39	error (invalid witness file)	6.4	3.4	120	300	-					-
email_spec4_product25_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	14000	2100	2.3	0	error (invalid witness file)	.50	.32	8.8	40	error (invalid witness file)	6.7	3.5	120	300	-					-
email_spec4_product27_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	13000	2100	2.3	0	error (invalid witness file)	.48	.31	11	39	error (invalid witness file)	6.8	3.5	71	320	-					-
email_spec4_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2000	2.3	0	error (invalid witness file)	.52	.33	13	40	error (invalid witness file)	6.0	3.2	120	290	-					-
email_spec4_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	13000	2400	2.3	0	error (invalid witness file)	.56	.37	8.1	41	error (invalid witness file)	6.4	3.4	110	310	-					-
email_spec4_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2500	2.3	0	error (invalid witness file)	.50	.31	9.4	40	error (invalid witness file)	5.9	3.2	120	300	-					-
email_spec4_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	12000	2100	2.3	0	error (invalid witness file)	.53	.34	10	40	error (invalid witness file)	6.5	3.5	140	300	-					-
email_spec4_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	13000	1700	2.3	0	error (invalid witness file)	.51	.35	8.9	39	error (invalid witness file)	7.4	3.9	130	300	-					-
email_spec4_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	11000	1800	2.3	0	error (invalid witness file)	.51	.32	12	39	error (invalid witness file)	5.9	3.2	100	300	-					-
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	2300	2.3	0	error (invalid witness file)	.54	.35	12	39	error (invalid witness file)	6.1	3.2	100	310	-					-
email_spec6_product12_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	15000	4800	2.3	0	error (invalid witness file)	.58	.37	11	42	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec6_product14_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	15000	5100	2.3	0	error (invalid witness file)	.56	.37	8.0	43	error (invalid witness file)	6.2	3.3	130	300	-					-
email_spec6_product15_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	12000	4900	2.3	0	error (invalid witness file)	.55	.35	12	42	error (invalid witness file)	6.1	3.3	130	290	-					-
email_spec6_product16_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	12000	4500	2.3	0	error (invalid witness file)	.51	.31	7.6	41	error (invalid witness file)	7.1	3.7	110	320	-					-
email_spec6_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	13000	4400	2.3	0	error (invalid witness file)	.63	.40	9.9	43	error (invalid witness file)	7.6	4.0	85	300	-					-
email_spec6_product21_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5300	2.3	0	error (invalid witness file)	.50	.32	11	40	error (invalid witness file)	6.3	3.3	110	300	-					-
email_spec6_product22_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	12000	4700	2.3	0	error (invalid witness file)	.53	.35	8.8	40	error (invalid witness file)	5.9	3.2	79	290	-					-
email_spec6_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	13000	3600	2.3	0	error (invalid witness file)	.50	.33	9.3	40	error (invalid witness file)	6.3	3.3	130	300	-					-
email_spec6_product28_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	14000	5300	2.3	0	error (invalid witness file)	.50	.32	12	39	error (invalid witness file)	7.0	3.7	140	310	-					-
email_spec6_product29_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	910	760	14000	5200	2.3	0	error (invalid witness file)	.57	.37	10	40	error (invalid witness file)	6.6	3.5	110	310	-					-
email_spec6_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	12000	4800	2.3	0	error (invalid witness file)	.50	.32	12	40	error (invalid witness file)	6.4	3.4	140	310	-					-
email_spec6_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	12000	4900	2.3	0	error (invalid witness file)	.51	.32	13	39	error (invalid witness file)	6.1	3.3	93	310	-					-
email_spec6_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	13000	4800	2.3	0	error (invalid witness file)	.55	.35	5.6	41	error (invalid witness file)	6.3	3.3	120	290	-					-
email_spec6_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	760	13000	4800	2.3	0	error (invalid witness file)	.50	.32	12	40	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec6_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	4700	2.3	0	error (invalid witness file)	.63	.40	7.5	43	error (invalid witness file)	5.7	3.0	90	300	-					-
email_spec6_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	12000	3800	2.3	0	error (invalid witness file)	.54	.35	9.3	41	error (invalid witness file)	7.1	3.7	130	320	-					-
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5300	2.3	0	error (invalid witness file)	.50	.32	12	41	error (invalid witness file)	7.2	3.8	130	310	-					-
email_spec7_product28_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	13000	2100	2.3	0	error (invalid witness file)	.52	.32	8.8	41	error (invalid witness file)	6.3	3.3	130	310	-					-
email_spec7_product29_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	12000	2200	2.3	0	error (invalid witness file)	.51	.31	11	40	error (invalid witness file)	6.6	3.5	130	300	-					-
email_spec7_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	12000	3200	2.3	0	error (invalid witness file)	.50	.33	4.9	39	error (invalid witness file)	6.5	3.4	130	310	-					-
email_spec7_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	15000	1800	2.3	0	error (invalid witness file)	.50	.32	9.1	40	error (invalid witness file)	7.2	3.8	150	320	-					-
email_spec7_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2300	2.3	0	error (invalid witness file)	.50	.32	7.2	39	error (invalid witness file)	6.2	3.3	120	300	-					-
email_spec7_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	13000	3300	2.3	0	error (invalid witness file)	.55	.35	9.9	40	error (invalid witness file)	6.0	3.2	110	300	-					-
email_spec7_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	12000	2100	2.3	0	error (invalid witness file)	.48	.32	11	40	error (invalid witness file)	6.4	3.4	94	300	-					-
email_spec7_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	15000	2100	2.3	0	error (invalid witness file)	.55	.37	11	42	error (invalid witness file)	6.3	3.4	130	300	-					-
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	770	12000	4700	2.3	0	error (invalid witness file)	.52	.34	9.2	43	error (invalid witness file)	6.6	3.5	140	300	-					-
email_spec8_product15_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5500	2.3	0	error (invalid witness file)	.51	.34	4.5	40	error (invalid witness file)	6.1	3.3	130	300	-					-
email_spec8_product16_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	12000	5600	2.3	0	error (invalid witness file)	.54	.35	11	42	error (invalid witness file)	6.8	3.6	140	300	-					-
email_spec8_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5600	2.3	0	error (invalid witness file)	.49	.32	10	39	error (invalid witness file)	6.5	3.5	140	300	-					-
email_spec8_product21_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5600	2.3	0	error (invalid witness file)	.63	.40	8.2	40	error (invalid witness file)	5.5	3.0	110	290	-					-
email_spec8_product22_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	12000	5600	2.3	0	error (invalid witness file)	.51	.34	9.5	40	error (invalid witness file)	6.4	3.4	100	300	-					-
email_spec8_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5600	2.3	0	error (invalid witness file)	.56	.37	10	43	error (invalid witness file)	6.0	3.2	120	290	-					-
email_spec8_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	12000	5600	2.3	0	error (invalid witness file)	.61	.39	4.8	39	error (invalid witness file)	6.5	3.4	120	300	-					-
email_spec8_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5500	2.3	0	error (invalid witness file)	.50	.32	11	41	error (invalid witness file)	5.8	3.1	110	290	-					-
email_spec8_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5600	2.3	0	error (invalid witness file)	.57	.37	13	42	error (invalid witness file)	6.1	3.2	120	290	-					-
email_spec8_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5600	2.3	0	error (invalid witness file)	.52	.33	9.6	39	error (invalid witness file)	6.5	3.4	110	310	-					-
email_spec8_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	14000	5500	2.3	0	error (invalid witness file)	.56	.35	12	43	error (invalid witness file)	6.6	3.5	93	310	-					-
email_spec8_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5500	2.3	0	error (invalid witness file)	.49	.32	8.9	40	error (invalid witness file)	6.0	3.2	91	300	-					-
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	15000	4900	2.3	0	error (invalid witness file)	.54	.34	10	40	error (invalid witness file)	6.4	3.4	130	300	-					-
email_spec9_product15_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5600	2.3	0	error (invalid witness file)	.60	.38	4.9	40	error (invalid witness file)	6.7	3.5	120	300	-					-
email_spec9_product16_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5600	2.3	0	error (invalid witness file)	.60	.39	8.7	39	error (invalid witness file)	6.3	3.3	120	300	-					-
email_spec9_product20_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5600	2.3	0	error (invalid witness file)	.52	.35	9.7	40	error (invalid witness file)	6.2	3.3	100	300	-					-
email_spec9_product21_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5500	2.3	0	error (invalid witness file)	.64	.41	9.1	44	error (invalid witness file)	6.7	3.5	110	320	-					-
email_spec9_product22_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5600	2.3	0	error (invalid witness file)	.53	.35	6.4	42	error (invalid witness file)	6.6	3.5	130	300	-					-
email_spec9_product26_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5500	2.3	0	error (invalid witness file)	.49	.33	7.2	40	error (invalid witness file)	6.5	3.4	140	310	-					-
email_spec9_product30_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5500	2.3	0	error (invalid witness file)	.49	.32	9.5	40	error (invalid witness file)	6.1	3.2	130	300	-					-
email_spec9_product31_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	12000	5500	2.3	0	error (invalid witness file)	.50	.31	11	40	error (invalid witness file)	6.2	3.3	110	300	-					-
email_spec9_product32_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	14000	5600	2.3	0	error (invalid witness file)	.50	.32	11	40	error (invalid witness file)	5.9	3.1	72	300	-					-
email_spec9_product33_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	13000	5500	2.3	0	error (invalid witness file)	.52	.35	7.9	40	error (invalid witness file)	6.2	3.3	110	300	-					-
email_spec9_product34_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5300	2.3	0	error (invalid witness file)	.52	.33	9.5	40	error (invalid witness file)	6.2	3.3	130	300	-					-
email_spec9_product35_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5500	2.3	0	error (invalid witness file)	.58	.37	9.3	40	error (invalid witness file)	6.5	3.4	130	300	-					-
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	4900	2.3	0	error (invalid witness file)	.53	.36	7.1	40	error (invalid witness file)	6.0	3.2	130	290	-					-
email_spec0_product05_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	9.1	2.6	76	440	2.7	0	-					-					true	17	8.8	180	470	true	14	7.4	230	380
email_spec0_product09_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	11	3.2	87	470	2.8	0	-					-					true	21	11	370	540	true	15	8.1	310	390
email_spec0_product10_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	9.5	2.8	82	440	2.7	0	-					-					true	15	7.8	280	500	true	13	7.1	220	380
email_spec0_product11_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	11	3.2	92	490	2.8	0	-					-					true	21	11	320	530	true	15	7.9	250	420
email_spec0_product19_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.6	95	500	2.9	0	-					-					true	22	12	310	580	true	16	8.5	210	540
email_spec0_product24_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	13	3.5	110	510	3.0	0	-					-					true	22	11	390	670	true	22	11	310	610
email_spec0_product25_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	13	3.9	110	520	3.0	0	-					-					true	24	12	400	630	true	17	9.2	140	570
email_spec0_product27_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	14	3.8	100	510	3.1	0	-					-					true	24	13	460	690	true	20	11	340	560
email_spec0_product36_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	11	3.0	87	490	2.8	0	-					-					true	22	11	370	540	true	15	8.0	240	400
email_spec0_product37_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	11	3.2	87	480	2.9	0	-					-					true	19	9.6	330	510	true	31	17	490	690
email_spec0_product38_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.5	92	480	2.9	0	-					-					true	26	13	380	670	true	14	7.7	220	440
email_spec0_product40_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	14	3.7	110	510	3.0	0	-					-					true	27	14	320	670	true	27	15	400	730
email_spec11_product03_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	8.7	2.5	66	410	2.7	0	-					-					true	14	7.0	280	460	true	13	6.9	200	370
email_spec11_product07_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	10	2.9	85	500	2.8	0	-					-					true	22	12	220	500	true	14	7.2	240	390
email_spec11_product08_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.2	92	480	2.8	0	-					-					true	16	8.5	120	500	true	17	9.1	260	530
email_spec11_product10_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	8.9	2.6	70	470	2.7	0	-					-					true	15	7.6	320	480	true	13	7.0	220	380
email_spec11_product18_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	13	3.5	97	490	2.9	0	-					-					true	26	13	280	560	true	22	11	320	570
email_spec11_product23_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	13	3.6	110	540	3.0	0	-					-					true	31	16	290	690	true	21	11	360	610
email_spec11_product24_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.5	92	500	3.0	0	-					-					true	29	15	300	640	true	17	8.8	130	590
email_spec11_product27_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	13	3.8	100	570	3.1	0	-					-					true	26	13	430	680	true	21	11	340	600
email_spec11_product36_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	10	2.9	83	490	2.8	0	-					-					true	20	10	410	530	true	14	7.6	230	410
email_spec11_product37_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	11	3.3	100	480	2.9	0	-					-					true	25	13	270	530	true	18	9.6	250	560
email_spec11_product39_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.3	91	500	2.9	0	-					-					true	25	13	280	640	true	19	9.7	260	590
email_spec11_product40_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.5	93	500	3.0	0	-					-					true	26	13	370	680	true	20	10	250	580
email_spec1_product12_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5600	2.3	0	-					-					error (invalid witness file)	.50	.32	11	42	error (invalid witness file)	6.0	3.2	120	290
email_spec1_product28_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5500	2.3	0	-					-					error (invalid witness file)	.63	.40	7.0	40	error (invalid witness file)	6.6	3.5	97	300
email_spec27_product13_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	710	12000	2700	2.3	0	-					-					error (invalid witness file)	.68	.43	6.5	41	error (invalid witness file)	7.1	3.7	120	320
email_spec27_product28_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	13000	2000	2.3	0	-					-					error (invalid witness file)	.59	.37	10	39	error (invalid witness file)	6.8	3.5	71	310
email_spec4_product13_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	720	11000	2100	2.3	0	-					-					error (invalid witness file)	.55	.34	10	40	error (invalid witness file)	6.2	3.3	130	290
email_spec4_product17_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	730	12000	1900	2.3	0	-					-					error (invalid witness file)	.53	.35	14	41	error (invalid witness file)	6.7	3.6	100	310
email_spec4_product28_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	790	12000	1900	2.3	0	-					-					error (invalid witness file)	.55	.35	11	43	error (invalid witness file)	5.9	3.1	90	300
email_spec4_product29_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2400	2.3	0	-					-					error (invalid witness file)	.60	.38	8.5	43	error (invalid witness file)	6.9	3.6	120	310
email_spec7_product13_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.4	89	490	2.9	0	-					-					true	22	11	310	530	true	14	7.6	190	420
email_spec7_product17_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	13	3.6	100	510	3.0	0	-					-					true	30	15	310	670	true	16	8.3	270	430
email_spec7_product18_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.3	93	480	2.9	0	-					-					true	23	12	320	560	true	17	9.1	230	510
email_spec7_product19_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.4	90	500	2.9	0	-					-					true	27	14	250	620	true	15	8.1	280	420
email_spec7_product23_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.6	96	500	3.0	0	-					-					true	23	12	420	660	true	20	10	300	600
email_spec7_product24_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	12	3.4	100	500	3.0	0	-					-					true	24	13	260	620	true	15	7.9	160	480
email_spec7_product25_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	13	3.7	110	510	3.0	0	-					-					true	23	12	360	670	true	16	8.5	220	450
email_spec7_product27_true-unreach-call_true-termination.cil.c	true	2	wit	inspect	13	3.8	100	520	3.1	0	-					-					true	27	14	390	640	true	18	9.5	340	520
email_spec8_product12_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	11000	5600	2.3	0	-					-					error (invalid witness file)	.54	.35	10	41	error (invalid witness file)	5.7	3.0	100	300
email_spec8_product14_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	750	11000	5600	2.3	0	-					-					error (invalid witness file)	.62	.40	7.9	39	error (invalid witness file)	6.2	3.3	110	300
email_spec8_product28_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	11000	5600	2.3	0	-					-					error (invalid witness file)	.47	.32	14	39	error (invalid witness file)	6.7	3.6	120	300
email_spec8_product29_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5600	2.3	0	-					-					error (invalid witness file)	.56	.36	8.9	43	error (invalid witness file)	6.3	3.3	110	300
email_spec9_product12_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	11000	5600	2.3	0	-					-					error (invalid witness file)	.52	.34	11	43	error (invalid witness file)	5.8	3.1	120	290
email_spec9_product14_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5600	2.3	0	-					-					error (invalid witness file)	.64	.41	7.2	40	error (invalid witness file)	5.8	3.1	100	300
email_spec9_product28_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	13000	5600	2.3	0	-					-					error (invalid witness file)	.52	.33	14	40	error (invalid witness file)	6.3	3.3	84	300
email_spec9_product29_true-unreach-call_true-termination.cil.c	timeout	0	wit	inspect	900	740	12000	5600	2.3	0	-					-					error (invalid witness file)	.56	.35	7.0	40	error (invalid witness file)	7.5	4.0	94	300
minepump_spec1_product33_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.7	2.3	56	340	2.6	0	error (invalid witness file)	4.0	2.2	50	220	false(unreach-call)	9.4	5.0	150	350	-					-
minepump_spec1_product34_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.7	2.3	59	350	2.6	0	error (invalid witness file)	4.1	2.3	53	240	false(unreach-call)	9.5	5.0	140	340	-					-
minepump_spec1_product35_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.6	2.4	58	350	2.6	0	error (invalid witness file)	3.9	2.1	56	250	false(unreach-call)	10	5.3	120	360	-					-
minepump_spec1_product36_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.5	2.3	64	370	2.6	0	error (invalid witness file)	3.7	2.0	73	240	false(unreach-call)	11	5.9	170	380	-					-
minepump_spec1_product37_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.6	2.3	60	340	2.6	0	error (invalid witness file)	4.9	2.7	52	250	false(unreach-call)	11	5.8	170	360	-					-
minepump_spec1_product38_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.3	2.3	56	340	2.6	0	error (invalid witness file)	3.9	2.1	60	240	false(unreach-call)	9.5	5.0	140	340	-					-
minepump_spec1_product39_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.7	2.2	58	360	2.6	0	true	5.5	3.0	60	290	false(unreach-call)	13	7.0	120	370	-					-
minepump_spec1_product40_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.0	2.5	65	380	2.6	0	true	5.7	3.0	79	280	false(unreach-call)	13	7.1	220	380	-					-
minepump_spec1_product41_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	11	3.0	80	510	2.6	0	error (invalid witness file)	4.3	2.4	31	280	false(unreach-call)	9.6	5.1	140	350	-					-
minepump_spec1_product42_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	9.7	2.8	76	490	2.6	0	error (invalid witness file)	3.8	2.1	83	240	false(unreach-call)	13	6.7	99	350	-					-
minepump_spec1_product43_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	12	3.6	100	500	2.6	0	error (invalid witness file)	3.7	2.0	63	250	false(unreach-call)	10	5.4	190	360	-					-
minepump_spec1_product44_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	11	3.5	99	500	2.6	0	error (invalid witness file)	3.6	2.0	57	220	false(unreach-call)	16	8.6	200	420	-					-
minepump_spec1_product49_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.1	2.3	69	360	2.6	0	error (invalid witness file)	3.8	2.1	76	220	false(unreach-call)	9.5	5.0	150	350	-					-
minepump_spec1_product50_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.3	2.3	56	340	2.6	0	error (invalid witness file)	4.8	2.6	56	240	false(unreach-call)	9.7	5.2	140	360	-					-
minepump_spec1_product51_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.8	2.5	63	370	2.6	0	true	5.8	3.1	79	320	false(unreach-call)	9.1	4.9	170	330	-					-
minepump_spec1_product52_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.3	2.5	60	390	2.6	0	true	6.0	3.3	100	320	false(unreach-call)	11	6.0	190	360	-					-
minepump_spec1_product53_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.8	2.5	68	410	2.6	0	error (invalid witness file)	3.6	2.0	74	220	false(unreach-call)	9.9	5.2	180	350	-					-
minepump_spec1_product54_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.9	2.4	61	360	2.6	0	error (invalid witness file)	3.6	2.0	49	240	false(unreach-call)	12	6.4	150	370	-					-
minepump_spec1_product55_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.6	2.6	68	440	2.6	0	true	6.0	3.2	78	330	false(unreach-call)	10	5.5	160	340	-					-
minepump_spec1_product56_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.8	2.7	76	450	2.6	0	true	6.0	3.2	75	290	false(unreach-call)	12	6.5	190	380	-					-
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	16	4.2	120	500	2.6	0	true	11	6.0	96	420	false(unreach-call)	13	6.8	150	400	-					-
minepump_spec2_product33_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	11	3.3	92	510	2.6	0	error (invalid witness file)	4.3	2.4	34	250	false(unreach-call)	18	9.4	300	410	-					-
minepump_spec2_product34_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	11	3.1	89	490	2.6	0	error (invalid witness file)	3.8	2.1	57	230	false(unreach-call)	15	8.2	200	410	-					-
minepump_spec2_product35_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	13	3.7	92	510	2.6	0	error (invalid witness file)	4.6	2.6	43	260	false(unreach-call)	12	6.5	180	400	-					-
minepump_spec2_product36_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	12	3.6	100	520	2.6	0	error (invalid witness file)	3.5	2.0	65	220	false(unreach-call)	11	5.7	190	370	-					-
minepump_spec2_product41_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	13	3.5	93	510	2.6	0	error (invalid witness file)	3.7	2.1	55	230	false(unreach-call)	15	8.1	280	450	-					-
minepump_spec2_product42_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	12	3.5	110	490	2.6	0	error (invalid witness file)	3.8	2.1	79	240	false(unreach-call)	11	5.6	160	360	-					-
minepump_spec2_product43_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	18	6.1	150	550	2.6	0	error (invalid witness file)	4.7	2.6	47	220	false(unreach-call)	16	8.6	230	480	-					-
minepump_spec2_product44_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	19	6.3	160	570	2.6	0	error (invalid witness file)	3.8	2.1	69	220	false(unreach-call)	14	7.4	190	450	-					-
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	73	38	790	1400	2.6	0	true	9.3	4.9	150	460	false(unreach-call)	17	8.9	230	510	-					-
minepump_spec3_product01_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.4	2.2	58	350	2.5	0	error (invalid witness file)	4.3	2.4	33	240	false(unreach-call)	10	5.3	160	360	-					-
minepump_spec3_product02_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	6.4	2.0	55	330	2.5	0	error (invalid witness file)	3.2	1.8	46	220	false(unreach-call)	12	6.2	180	370	-					-
minepump_spec3_product03_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	6.7	2.1	55	330	2.5	0	error (invalid witness file)	3.2	1.7	38	210	false(unreach-call)	10	5.6	210	360	-					-
minepump_spec3_product04_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.0	2.3	69	350	2.5	0	error (invalid witness file)	3.4	1.9	37	260	false(unreach-call)	11	5.7	180	360	-					-
minepump_spec3_product05_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.3	2.2	61	370	2.6	0	error (invalid witness file)	4.2	2.4	44	250	false(unreach-call)	8.9	4.8	130	330	-					-
minepump_spec3_product06_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.1	2.2	51	320	2.6	0	error (invalid witness file)	3.5	1.9	46	270	false(unreach-call)	9.2	4.9	130	340	-					-
minepump_spec3_product07_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.0	2.1	56	320	2.6	0	true	5.7	3.1	56	280	false(unreach-call)	9.6	5.1	150	340	-					-
minepump_spec3_product08_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.1	2.2	53	340	2.6	0	true	5.8	3.1	72	340	false(unreach-call)	11	5.7	220	360	-					-
minepump_spec3_product09_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.2	2.1	54	330	2.5	0	error (invalid witness file)	3.5	1.9	58	240	false(unreach-call)	10	5.3	99	370	-					-
minepump_spec3_product10_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	6.8	2.1	56	330	2.5	0	error (invalid witness file)	3.4	1.9	45	220	false(unreach-call)	10	5.5	240	360	-					-
minepump_spec3_product11_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	6.6	2.1	52	330	2.5	0	error (invalid witness file)	4.4	2.4	48	270	false(unreach-call)	11	6.0	160	360	-					-
minepump_spec3_product12_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.2	2.2	57	340	2.5	0	error (invalid witness file)	3.3	1.8	42	200	false(unreach-call)	10	5.6	200	350	-					-
minepump_spec3_product13_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.1	2.2	53	330	2.6	0	error (invalid witness file)	3.4	1.8	30	220	false(unreach-call)	9.4	5.0	180	340	-					-
minepump_spec3_product14_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.2	2.3	64	330	2.6	0	error (invalid witness file)	3.2	1.8	46	240	false(unreach-call)	9.1	4.8	170	340	-					-
minepump_spec3_product15_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	6.8	2.1	52	320	2.6	0	true	5.7	3.1	79	290	false(unreach-call)	9.5	5.0	180	340	-					-
minepump_spec3_product16_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.7	2.2	61	360	2.6	0	true	5.9	3.2	92	340	false(unreach-call)	10	5.3	140	360	-					-
minepump_spec3_product17_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.5	2.3	64	360	2.5	0	error (invalid witness file)	3.9	2.1	48	250	false(unreach-call)	11	5.9	220	340	-					-
minepump_spec3_product18_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.2	2.4	68	370	2.6	0	error (invalid witness file)	4.4	2.4	47	240	false(unreach-call)	12	6.2	130	340	-					-
minepump_spec3_product19_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.2	2.2	51	330	2.5	0	true	5.4	2.9	89	290	false(unreach-call)	9.7	5.1	180	350	-					-
minepump_spec3_product20_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.2	2.3	62	350	2.6	0	true	6.0	3.2	68	290	false(unreach-call)	9.7	5.1	160	340	-					-
minepump_spec3_product21_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.2	2.2	62	340	2.6	0	error (invalid witness file)	3.6	2.0	82	220	false(unreach-call)	9.7	5.1	160	350	-					-
minepump_spec3_product22_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.4	2.3	50	350	2.6	0	error (invalid witness file)	3.6	2.0	44	270	false(unreach-call)	9.8	5.2	140	360	-					-
minepump_spec3_product23_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.9	2.3	62	350	2.6	0	true	5.6	3.0	100	290	false(unreach-call)	10	5.4	170	340	-					-
minepump_spec3_product24_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.5	2.4	54	330	2.6	0	true	6.6	3.6	77	340	false(unreach-call)	9.6	5.1	170	340	-					-
minepump_spec3_product25_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.0	2.3	61	350	2.5	0	error (invalid witness file)	4.3	2.3	32	240	false(unreach-call)	9.4	4.9	140	340	-					-
minepump_spec3_product26_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.8	2.4	63	370	2.6	0	error (invalid witness file)	3.5	1.9	50	220	false(unreach-call)	9.5	5.1	180	340	-					-
minepump_spec3_product27_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.2	2.2	54	330	2.5	0	true	5.5	2.9	60	310	false(unreach-call)	9.9	5.2	180	340	-					-
minepump_spec3_product28_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.1	2.3	67	360	2.6	0	true	6.4	3.4	100	330	false(unreach-call)	12	6.1	95	330	-					-
minepump_spec3_product29_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.0	2.2	57	320	2.6	0	error (invalid witness file)	4.5	2.4	44	220	false(unreach-call)	11	5.8	140	360	-					-
minepump_spec3_product30_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.4	2.3	60	340	2.6	0	error (invalid witness file)	3.6	1.9	50	220	false(unreach-call)	9.7	5.1	140	330	-					-
minepump_spec3_product31_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.9	2.2	63	350	2.6	0	true	5.7	3.1	88	310	false(unreach-call)	11	5.7	140	380	-					-
minepump_spec3_product32_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.6	2.3	65	340	2.6	0	true	5.2	2.8	70	300	false(unreach-call)	11	5.6	170	360	-					-
minepump_spec3_product35_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.2	2.1	51	340	2.5	0	error (invalid witness file)	3.6	2.0	56	220	false(unreach-call)	11	5.7	190	370	-					-
minepump_spec3_product36_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	6.7	2.1	52	330	2.5	0	error (invalid witness file)	3.4	1.9	44	230	false(unreach-call)	9.9	5.3	170	360	-					-
minepump_spec3_product39_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.3	2.3	55	340	2.6	0	true	6.5	3.5	81	330	false(unreach-call)	10	5.3	190	350	-					-
minepump_spec3_product40_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.8	2.3	60	350	2.6	0	true	6.0	3.3	96	310	false(unreach-call)	9.3	5.0	160	330	-					-
minepump_spec3_product43_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.3	2.2	56	330	2.6	0	error (invalid witness file)	3.6	2.0	51	240	false(unreach-call)	11	5.7	190	360	-					-
minepump_spec3_product44_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	6.7	2.1	53	330	2.6	0	error (invalid witness file)	4.4	2.4	48	220	false(unreach-call)	11	5.8	240	370	-					-
minepump_spec3_product47_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.6	2.2	66	320	2.6	0	true	6.3	3.4	100	330	false(unreach-call)	12	6.0	160	380	-					-
minepump_spec3_product48_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.9	2.3	59	350	2.6	0	true	7.0	3.8	74	330	false(unreach-call)	9.6	5.1	160	340	-					-
minepump_spec3_product51_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.6	2.3	56	340	2.6	0	true	6.0	3.3	110	320	false(unreach-call)	10	5.3	120	330	-					-
minepump_spec3_product52_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.6	2.3	62	350	2.6	0	true	6.6	3.6	110	290	false(unreach-call)	11	5.7	170	380	-					-
minepump_spec3_product55_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.3	2.2	51	340	2.6	0	true	7.0	3.8	79	290	false(unreach-call)	9.6	5.1	130	350	-					-
minepump_spec3_product56_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.1	2.3	64	370	2.6	0	true	7.0	3.7	95	330	false(unreach-call)	10	5.4	150	350	-					-
minepump_spec3_product59_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	8.6	2.4	64	400	2.6	0	true	6.0	3.3	75	330	false(unreach-call)	9.4	5.0	76	370	-					-
minepump_spec3_product60_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.7	2.4	61	350	2.6	0	true	6.4	3.4	100	340	false(unreach-call)	9.6	5.1	180	330	-					-
minepump_spec3_product63_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.7	2.3	55	350	2.6	0	true	6.1	3.3	91	290	false(unreach-call)	11	5.7	180	360	-					-
minepump_spec3_product64_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	7.8	2.4	63	360	2.6	0	true	6.4	3.5	100	330	false(unreach-call)	11	5.8	210	370	-					-
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	9.1	2.6	73	410	2.6	0	true	7.6	4.0	61	340	false(unreach-call)	12	6.4	220	370	-					-
minepump_spec4_product33_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	16	4.6	130	550	2.6	0	error (invalid witness file)	3.5	2.0	46	270	false(unreach-call)	10	5.5	160	350	-					-
minepump_spec4_product34_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	15	4.5	120	560	2.6	0	error (invalid witness file)	3.9	2.1	60	220	false(unreach-call)	9.9	5.2	170	350	-					-
minepump_spec4_product35_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	12	3.8	92	500	2.6	0	error (invalid witness file)	4.2	2.3	55	250	false(unreach-call)	15	8.0	230	450	-					-
minepump_spec4_product36_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	13	3.9	100	500	2.6	0	error (invalid witness file)	4.5	2.4	45	220	false(unreach-call)	14	7.8	250	440	-					-
minepump_spec4_product37_false-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	650	12000	2000	2.3	0	error (invalid witness file)	.50	.32	13	40	error (invalid witness file)	5.8	3.1	120	290	-					-
minepump_spec4_product38_false-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	510	10000	1600	2.3	0	error (invalid witness file)	.50	.33	12	42	error (invalid witness file)	5.9	3.1	110	290	-					-
minepump_spec4_product39_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	20	6.5	170	750	2.6	0	true	6.2	3.4	84	340	false(unreach-call)	14	7.5	160	460	-					-
minepump_spec4_product40_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	43	17	400	990	2.6	0	true	6.1	3.3	100	330	false(unreach-call)	15	8.0	230	470	-					-
minepump_spec4_product41_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	16	4.7	120	500	2.6	0	error (invalid witness file)	4.0	2.2	84	260	false(unreach-call)	11	5.8	180	380	-					-
minepump_spec4_product42_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	16	4.6	110	570	2.6	0	error (invalid witness file)	4.2	2.2	67	260	false(unreach-call)	14	7.5	210	420	-					-
minepump_spec4_product43_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	13	4.0	110	520	2.6	0	error (invalid witness file)	3.8	2.1	75	250	false(unreach-call)	16	8.5	230	460	-					-
minepump_spec4_product44_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	12	3.9	97	500	2.6	0	error (invalid witness file)	4.4	2.4	57	250	false(unreach-call)	16	8.6	210	450	-					-
minepump_spec4_product45_false-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	710	12000	1700	2.3	0	error (invalid witness file)	.50	.32	11	40	error (invalid witness file)	6.0	3.2	130	300	-					-
minepump_spec4_product46_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	22	8.8	210	630	2.6	0	error (invalid witness file)	3.4	1.9	30	220	false(unreach-call)	15	7.7	240	450	-					-
minepump_spec4_product47_false-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	730	11000	1600	2.3	0	error (invalid witness file)	.50	.32	8.0	40	error (invalid witness file)	5.9	3.1	100	300	-					-
minepump_spec4_product48_false-unreach-call_false-termination.cil.c	false(unreach-call)	1	wit	inspect	31	12	250	710	2.6	0	true	6.5	3.5	110	330	false(unreach-call)	16	8.6	150	570	-					-
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	13000	1900	2.3	0	error (invalid witness file)	.57	.37	9.9	41	error (invalid witness file)	6.0	3.2	93	300	-					-
minepump_spec1_product01_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.1	2.2	50	330	2.6	0	-					-					out of memory	400	380	7500	7000	true	11	6.2	170	370
minepump_spec1_product02_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.9	2.2	58	360	2.6	0	-					-					out of memory	400	370	6400	7000	true	12	6.4	210	370
minepump_spec1_product03_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.0	2.2	58	330	2.6	0	-					-					out of memory	360	340	6100	7000	true	11	6.2	220	370
minepump_spec1_product04_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.0	2.2	59	340	2.6	0	-					-					out of memory	390	370	5600	7000	true	9.5	5.1	160	350
minepump_spec1_product05_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.2	2.5	64	420	2.6	0	-					-					out of memory	290	270	8700	7000	true	10	5.4	140	370
minepump_spec1_product06_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.7	2.3	65	400	2.6	0	-					-					out of memory	350	340	7200	7000	true	12	6.3	200	370
minepump_spec1_product07_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.6	100	570	2.6	0	-					-					out of memory	320	310	6700	7000	true	10	5.4	140	360
minepump_spec1_product08_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	15	4.5	110	510	2.6	0	-					-					out of memory	320	300	6300	7000	true	9.7	5.3	150	350
minepump_spec1_product09_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	6.7	2.2	55	330	2.6	0	-					-					out of memory	350	340	7600	7000	true	12	6.4	210	380
minepump_spec1_product10_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.0	2.2	55	340	2.6	0	-					-					out of memory	380	360	6800	7000	true	13	6.8	280	380
minepump_spec1_product11_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.0	2.2	57	330	2.6	0	-					-					out of memory	370	350	5600	7000	true	11	5.8	170	370
minepump_spec1_product12_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.2	2.3	54	330	2.6	0	-					-					out of memory	300	280	8300	7000	true	9.4	5.0	130	350
minepump_spec1_product13_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.4	2.7	63	470	2.6	0	-					-					out of memory	370	350	6600	7000	true	11	5.9	220	360
minepump_spec1_product14_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	530	11000	2000	2.3	0	-					-					error (invalid witness file)	.52	.35	10	41	error (invalid witness file)	6.3	3.4	91	320
minepump_spec1_product15_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	14	4.0	110	560	2.6	0	-					-					out of memory	300	280	7200	7000	true	10	5.5	190	350
minepump_spec1_product16_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	14	4.0	110	490	2.6	0	-					-					out of memory	270	260	8200	7000	true	10	5.6	190	360
minepump_spec1_product17_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.7	2.5	73	420	2.6	0	-					-					out of memory	590	570	12000	7000	true	11	5.8	170	370
minepump_spec1_product18_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.1	2.5	70	400	2.6	0	-					-					out of memory	520	500	8700	7000	true	10	5.5	160	370
minepump_spec1_product19_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	13	3.6	90	500	2.6	0	-					-					out of memory	350	330	8100	7000	true	11	5.7	150	360
minepump_spec1_product20_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.4	99	490	2.6	0	-					-					out of memory	490	470	6800	7000	true	10	5.5	140	360
minepump_spec1_product21_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.3	2.6	67	470	2.6	0	-					-					out of memory	410	390	5900	7000	true	11	5.8	180	360
minepump_spec1_product22_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.6	2.8	71	470	2.6	0	-					-					out of memory	520	500	9300	7000	true	11	5.7	180	360
minepump_spec1_product23_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	14	4.4	110	520	2.6	0	-					-					out of memory	370	350	7100	7000	true	10	5.5	170	350
minepump_spec1_product24_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	15	4.9	130	610	2.6	0	-					-					out of memory	400	380	6600	7000	true	11	5.7	180	360
minepump_spec1_product25_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.0	2.5	64	420	2.6	0	-					-					out of memory	490	470	13000	7000	true	10	5.6	120	370
minepump_spec1_product26_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.8	2.5	71	410	2.6	0	-					-					out of memory	520	510	8600	7000	true	11	6.1	190	360
minepump_spec1_product27_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	13	3.6	110	500	2.6	0	-					-					out of memory	390	370	9700	7000	true	10	5.5	120	360
minepump_spec1_product28_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.4	91	480	2.6	0	-					-					out of memory	480	460	7800	7000	true	9.6	5.3	180	340
minepump_spec1_product29_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.9	2.8	77	470	2.6	0	-					-					out of memory	420	400	9800	7000	true	10	5.5	120	370
minepump_spec1_product30_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.7	2.8	65	470	2.6	0	-					-					out of memory	470	450	8000	7000	true	11	6.0	220	360
minepump_spec1_product31_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	16	4.8	130	610	2.6	0	-					-					out of memory	400	380	7100	7000	true	11	5.6	200	350
minepump_spec1_product32_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	17	4.9	150	510	2.6	0	-					-					out of memory	370	360	10000	7000	true	11	5.7	160	370
minepump_spec1_product45_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.0	2.7	66	480	2.6	0	-					-					out of memory	320	300	7000	7000	true	22	12	380	560
minepump_spec1_product46_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.0	2.9	71	470	2.6	0	-					-					out of memory	340	320	6200	7000	true	21	12	410	560
minepump_spec1_product47_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	13	4.3	110	560	2.6	0	-					-					out of memory	390	370	7300	7000	true	25	13	400	600
minepump_spec1_product48_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	18	5.1	140	660	2.6	0	-					-					out of memory	390	370	7400	7000	true	25	14	300	630
minepump_spec1_product57_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	14	4.4	120	500	2.6	0	-					-					out of memory	630	610	10000	7000	true	31	17	440	700
minepump_spec1_product58_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	19	7.4	170	720	2.6	0	-					-					out of memory	610	590	12000	7000	true	23	13	300	610
minepump_spec1_product59_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	17	6.3	160	540	2.6	0	-					-					out of memory	630	620	13000	7000	true	28	15	380	680
minepump_spec1_product60_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	24	8.0	200	630	2.6	1.6	-					-					out of memory	630	610	14000	7000	true	28	15	300	660
minepump_spec1_product61_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.7	3.1	88	470	2.6	0	-					-					out of memory	400	380	6200	7000	true	31	17	500	640
minepump_spec1_product62_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	14	4.8	130	490	2.6	0	-					-					out of memory	370	360	8200	7000	true	23	12	260	590
minepump_spec1_product63_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	17	5.4	150	620	2.6	0	-					-					out of memory	370	360	7900	7000	true	26	14	230	600
minepump_spec1_product64_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	19	5.9	180	680	2.6	0	-					-					out of memory	400	380	12000	7000	true	30	16	450	660
minepump_spec2_product01_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.4	2.5	70	390	2.6	0	-					-					out of memory	770	750	21000	7000	true	15	8.1	230	490
minepump_spec2_product02_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.0	2.4	68	380	2.6	0	-					-					out of memory	860	840	14000	7000	true	14	7.7	200	500
minepump_spec2_product03_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.1	2.6	66	390	2.6	0	-					-					timeout	910	890	20000	5800	true	9.8	5.3	200	350
minepump_spec2_product04_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.3	2.6	64	420	2.6	0	-					-					timeout	910	890	19000	5800	true	9.8	5.3	140	350
minepump_spec2_product05_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.7	2.8	77	470	2.6	0	-					-					out of memory	310	290	7100	7000	true	11	6.1	200	360
minepump_spec2_product06_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.0	2.4	66	400	2.6	0	-					-					out of memory	330	320	7100	7000	true	11	6.0	190	370
minepump_spec2_product07_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	720	13000	2100	2.3	0	-					-					error (invalid witness file)	.58	.36	10	40	error (invalid witness file)	5.8	3.1	99	300
minepump_spec2_product08_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	21	7.1	190	640	2.6	0	-					-					out of memory	280	260	8600	7000	true	10	5.5	160	350
minepump_spec2_product09_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.9	2.4	66	380	2.6	0	-					-					out of memory	780	760	22000	7000	true	14	7.6	170	500
minepump_spec2_product10_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.8	2.4	67	380	2.6	0	-					-					out of memory	890	870	20000	7000	true	14	7.7	250	500
minepump_spec2_product11_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.9	2.4	60	380	2.6	0	-					-					timeout	910	880	20000	6200	true	11	5.9	210	360
minepump_spec2_product12_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.9	2.5	68	400	2.6	0	-					-					timeout	910	890	13000	5600	true	9.7	5.2	180	360
minepump_spec2_product13_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.9	2.3	61	400	2.6	0	-					-					out of memory	300	280	6500	7000	true	11	5.8	160	370
minepump_spec2_product14_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	520	11000	2200	2.3	0	-					-					error (invalid witness file)	.56	.35	7.2	41	error (invalid witness file)	5.6	3.0	96	290
minepump_spec2_product15_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	750	13000	2000	2.3	0	-					-					error (invalid witness file)	.66	.41	8.7	41	error (invalid witness file)	5.7	3.0	89	290
minepump_spec2_product16_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	22	6.9	180	660	2.6	0	-					-					out of memory	330	310	6900	7000	true	10	5.6	180	360
minepump_spec2_product17_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.3	86	490	2.8	0	-					-					out of memory	510	500	11000	7000	true	11	5.7	170	360
minepump_spec2_product18_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	21	5.9	160	560	2.6	0	-					-					out of memory	600	580	10000	7000	true	11	5.9	220	350
minepump_spec2_product19_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	23	7.2	190	740	2.6	0	-					-					out of memory	450	430	10000	7000	true	10	5.5	200	360
minepump_spec2_product20_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	21	6.7	190	560	2.6	0	-					-					out of memory	450	440	8800	7000	true	10	5.4	160	350
minepump_spec2_product21_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.7	3.0	76	470	2.6	0	-					-					out of memory	380	360	8300	7000	true	11	5.9	140	370
minepump_spec2_product22_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.9	2.8	74	490	2.6	0	-					-					out of memory	490	470	8000	7000	true	12	6.2	220	370
minepump_spec2_product23_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	25	8.0	200	650	2.6	0	-					-					out of memory	370	350	8500	7000	true	11	5.9	210	360
minepump_spec2_product24_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	23	7.7	200	730	2.6	0	-					-					out of memory	310	300	7200	7000	true	11	5.7	220	350
minepump_spec2_product25_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.2	96	480	2.6	0	-					-					out of memory	510	490	12000	7000	true	10	5.7	190	360
minepump_spec2_product26_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	20	5.9	180	570	2.6	0	-					-					out of memory	490	470	13000	7000	true	11	5.7	180	350
minepump_spec2_product27_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	16	4.8	120	500	2.6	0	-					-					out of memory	420	400	11000	7000	true	12	6.3	86	350
minepump_spec2_product28_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	21	6.9	170	740	2.6	0	-					-					out of memory	510	490	9500	7000	true	9.8	5.3	180	340
minepump_spec2_product29_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.7	3.1	78	470	2.6	0	-					-					out of memory	460	440	9000	7000	true	11	5.9	200	370
minepump_spec2_product30_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.5	2.7	71	470	2.6	0	-					-					out of memory	420	410	9000	7000	true	11	6.0	180	370
minepump_spec2_product31_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	570	12000	3300	2.3	0	-					-					error (invalid witness file)	.63	.39	7.2	39	error (invalid witness file)	5.9	3.1	90	300
minepump_spec2_product32_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	26	8.8	250	660	2.6	0	-					-					out of memory	370	350	7800	7000	true	12	6.5	120	350
minepump_spec2_product37_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	590	11000	2500	2.3	0	-					-					error (invalid witness file)	.48	.31	13	40	error (invalid witness file)	6.2	3.3	120	300
minepump_spec2_product38_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	570	11000	2400	2.3	0	-					-					error (invalid witness file)	.56	.35	9.3	39	error (invalid witness file)	6.0	3.2	110	300
minepump_spec2_product39_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	27	8.6	210	660	2.6	0	-					-					out of memory	470	450	8400	7000	true	21	11	360	560
minepump_spec2_product40_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	34	11	330	820	2.6	0	-					-					out of memory	450	430	11000	7000	true	25	13	490	590
minepump_spec2_product45_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.9	110	530	2.6	0	-					-					out of memory	320	310	6200	7000	true	33	19	310	690
minepump_spec2_product46_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.7	97	490	3.0	0	-					-					out of memory	380	370	7100	7000	true	32	18	400	730
minepump_spec2_product47_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	27	8.4	220	760	2.6	0	-					-					out of memory	360	350	5400	7000	true	25	14	390	650
minepump_spec2_product48_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	33	11	290	870	2.6	0	-					-					out of memory	400	390	12000	7000	true	24	13	400	550
minepump_spec2_product49_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	770	12000	1700	2.3	0	-					-					error (invalid witness file)	.66	.40	7.5	40	error (invalid witness file)	6.3	3.4	130	300
minepump_spec2_product50_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	620	11000	2000	2.3	0	-					-					error (invalid witness file)	.52	.33	10	40	error (invalid witness file)	5.9	3.2	120	300
minepump_spec2_product51_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	770	13000	1800	2.3	0	-					-					error (invalid witness file)	.63	.41	7.1	40	error (invalid witness file)	6.1	3.2	120	310
minepump_spec2_product52_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	500	10000	2000	2.3	0	-					-					error (invalid witness file)	.56	.35	11	40	error (invalid witness file)	6.5	3.4	120	320
minepump_spec2_product53_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	13	4.3	100	500	2.6	0	-					-					out of memory	400	380	9800	7000	true	27	15	310	650
minepump_spec2_product54_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	13	4.2	120	550	2.6	0	-					-					out of memory	370	350	9400	7000	true	25	14	390	610
minepump_spec2_product55_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	28	8.8	220	820	2.6	0	-					-					out of memory	450	430	9200	7000	true	20	11	310	560
minepump_spec2_product56_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	32	12	300	900	2.6	0	-					-					out of memory	420	400	10000	7000	true	25	14	380	610
minepump_spec2_product57_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	590	10000	2400	2.3	0	-					-					error (invalid witness file)	.63	.41	8.1	40	error (invalid witness file)	7.2	3.8	130	320
minepump_spec2_product58_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	520	10000	3500	2.3	0	-					-					error (invalid witness file)	.49	.32	9.5	42	error (invalid witness file)	5.3	2.9	93	290
minepump_spec2_product59_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	750	14000	1700	2.3	0	-					-					error (invalid witness file)	.64	.40	7.8	40	error (invalid witness file)	6.4	3.4	78	310
minepump_spec2_product60_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	730	11000	1700	2.3	0	-					-					error (invalid witness file)	.64	.40	7.6	39	error (invalid witness file)	5.5	3.0	79	300
minepump_spec2_product61_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	14	4.2	110	560	2.6	0	-					-					out of memory	380	360	9100	7000	true	39	22	450	600
minepump_spec2_product62_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	13	4.1	110	550	2.6	0	-					-					out of memory	360	340	7300	7000	true	43	24	660	770
minepump_spec2_product63_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	30	9.6	270	760	2.6	0	-					-					out of memory	410	390	9600	7000	true	36	20	350	710
minepump_spec2_product64_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	39	13	350	860	2.6	0	-					-					out of memory	470	450	7500	7000	true	36	20	510	810
minepump_spec3_product33_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.4	2.5	60	410	2.6	0	-					-					out of memory	330	310	5700	7000	true	14	7.5	260	480
minepump_spec3_product34_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.7	2.4	59	390	2.6	0	-					-					out of memory	410	390	8000	7000	true	14	7.4	210	480
minepump_spec3_product37_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.5	95	500	2.6	0	-					-					out of memory	310	290	8300	7000	true	24	13	450	610
minepump_spec3_product38_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.5	91	490	2.6	0	-					-					out of memory	320	300	6200	7000	true	22	12	260	600
minepump_spec3_product41_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.1	83	490	2.6	0	-					-					out of memory	360	340	7000	7000	true	17	9.2	320	530
minepump_spec3_product42_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	600	10000	2600	2.3	0	-					-					error (invalid witness file)	.49	.32	11	40	error (invalid witness file)	5.4	2.9	86	290
minepump_spec3_product45_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.6	95	550	2.6	0	-					-					out of memory	360	350	7900	7000	true	30	17	460	640
minepump_spec3_product46_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	13	3.9	99	500	2.6	0	-					-					out of memory	370	350	6500	7000	true	32	18	540	660
minepump_spec3_product49_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	640	11000	1500	2.3	0	-					-					error (invalid witness file)	.56	.36	9.8	40	error (invalid witness file)	6.4	3.4	110	310
minepump_spec3_product50_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	670	12000	1400	2.3	0	-					-					error (invalid witness file)	.72	.45	9.2	44	error (invalid witness file)	6.0	3.2	120	300
minepump_spec3_product53_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	47	25	560	1000	2.6	0	-					-					out of memory	420	400	7200	7000	true	26	14	300	650
minepump_spec3_product54_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	770	12000	1800	2.3	0	-					-					error (invalid witness file)	.65	.42	8.0	42	error (invalid witness file)	5.8	3.1	110	300
minepump_spec3_product57_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	39	19	350	890	2.6	0	-					-					out of memory	580	560	9200	7000	true	26	15	340	650
minepump_spec3_product58_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	750	13000	1800	2.3	0	-					-					error (invalid witness file)	.49	.31	11	40	error (invalid witness file)	5.7	3.1	120	290
minepump_spec3_product61_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	47	23	500	1100	2.6	0	-					-					out of memory	450	430	10000	7000	true	25	13	310	580
minepump_spec3_product62_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	13000	1600	2.3	0	-					-					error (invalid witness file)	.65	.40	6.6	39	error (invalid witness file)	5.9	3.1	89	300
minepump_spec4_product01_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.2	2.5	64	410	2.6	0	-					-					out of memory	390	370	7700	7000	true	10	5.4	180	350
minepump_spec4_product02_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.7	2.6	66	430	2.6	0	-					-					out of memory	330	310	9800	7000	true	10	5.6	150	350
minepump_spec4_product03_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.4	2.6	62	420	2.6	0	-					-					out of memory	360	340	6700	7000	true	11	6.1	220	370
minepump_spec4_product04_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.6	2.7	75	450	2.6	0	-					-					out of memory	310	290	9000	7000	true	9.8	5.2	170	360
minepump_spec4_product05_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.9	2.3	68	390	2.6	0	-					-					out of memory	290	280	6900	7000	true	12	6.3	220	370
minepump_spec4_product06_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.8	2.4	58	390	2.6	0	-					-					out of memory	300	280	7000	7000	true	12	6.7	140	430
minepump_spec4_product07_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.1	2.8	72	480	2.6	0	-					-					out of memory	350	330	5500	7000	true	13	7.3	250	490
minepump_spec4_product08_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.2	90	480	2.6	0	-					-					out of memory	290	280	7100	7000	true	14	7.6	230	490
minepump_spec4_product09_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.0	2.6	74	440	2.6	0	-					-					out of memory	390	370	6600	7000	true	9.5	5.1	110	350
minepump_spec4_product10_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.4	2.6	66	410	2.6	0	-					-					out of memory	390	370	7200	7000	true	9.9	5.4	150	350
minepump_spec4_product11_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.8	2.6	65	430	2.6	0	-					-					out of memory	300	280	9200	7000	true	12	6.4	220	360
minepump_spec4_product12_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.2	2.7	68	420	2.6	0	-					-					out of memory	340	320	8100	7000	true	9.7	5.2	180	350
minepump_spec4_product13_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.2	2.5	67	400	2.6	0	-					-					out of memory	330	320	8100	7000	true	12	6.3	140	370
minepump_spec4_product14_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.1	2.4	68	410	2.6	0	-					-					out of memory	300	280	8000	7000	true	11	6.2	190	380
minepump_spec4_product15_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.0	88	510	2.6	0	-					-					out of memory	340	320	6000	7000	true	13	7.2	200	490
minepump_spec4_product16_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.3	86	490	2.6	0	-					-					out of memory	320	300	7500	7000	true	13	7.1	250	480
minepump_spec4_product17_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.1	2.7	77	490	2.6	0	-					-					out of memory	620	600	13000	7000	true	11	6.2	180	390
minepump_spec4_product18_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.4	2.8	65	470	2.6	0	-					-					out of memory	540	530	12000	7000	true	11	6.3	250	380
minepump_spec4_product19_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	14	3.8	110	500	2.6	0	-					-					out of memory	450	440	9300	7000	true	13	7.3	260	500
minepump_spec4_product20_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	13	3.7	100	500	2.6	0	-					-					out of memory	400	390	8500	7000	true	13	7.3	240	490
minepump_spec4_product21_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.4	2.8	67	480	2.6	0	-					-					out of memory	390	370	8300	7000	true	15	8.3	170	450
minepump_spec4_product22_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.5	2.9	78	490	2.6	0	-					-					out of memory	490	470	10000	7000	true	11	5.9	160	370
minepump_spec4_product23_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	10	3.2	90	500	2.6	0	-					-					out of memory	370	350	8300	7000	true	13	7.0	210	510
minepump_spec4_product24_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.2	80	490	2.6	0	-					-					out of memory	410	400	6800	7000	true	12	7.0	210	500
minepump_spec4_product25_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.8	2.7	70	470	2.6	0	-					-					out of memory	540	520	11000	7000	true	11	5.9	140	370
minepump_spec4_product26_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.4	2.8	66	480	2.6	0	-					-					out of memory	530	510	14000	7000	true	12	6.5	220	390
minepump_spec4_product27_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.5	98	500	2.6	0	-					-					out of memory	460	440	8900	7000	true	12	6.7	130	510
minepump_spec4_product28_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.6	91	500	2.6	0	-					-					out of memory	380	360	11000	7000	true	12	7.0	210	490
minepump_spec4_product29_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.0	2.7	66	470	2.6	0	-					-					out of memory	420	400	7000	7000	true	12	6.7	220	450
minepump_spec4_product30_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.9	2.9	68	500	2.6	0	-					-					out of memory	520	510	9800	7000	true	13	7.0	260	480
minepump_spec4_product31_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	12	3.4	92	480	2.6	0	-					-					out of memory	440	420	8000	7000	true	13	7.1	160	520
minepump_spec4_product32_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.4	93	490	2.6	0	-					-					out of memory	370	350	8600	7000	true	14	7.6	130	520
minepump_spec4_product49_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	17	5.4	140	530	2.6	0	-					-					out of memory	430	410	8900	7000	true	26	14	260	700
minepump_spec4_product50_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	23	7.9	190	700	2.6	0	-					-					out of memory	480	460	8500	7000	true	26	15	440	660
minepump_spec4_product51_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	21	6.8	180	570	2.6	0	-					-					out of memory	480	470	9200	7000	true	28	16	250	720
minepump_spec4_product52_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	39	16	420	830	2.6	0	-					-					out of memory	530	510	10000	7000	true	32	18	440	700
minepump_spec4_product53_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	650	13000	1700	2.3	0	-					-					error (invalid witness file)	.50	.32	9.7	40	error (invalid witness file)	5.8	3.1	110	290
minepump_spec4_product54_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	18	5.5	150	550	2.6	0	-					-					out of memory	360	350	8500	7000	true	30	17	460	720
minepump_spec4_product55_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	22	7.2	190	730	2.6	0	-					-					out of memory	530	510	9400	7000	true	33	18	520	730
minepump_spec4_product56_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	740	12000	1700	2.3	0	-					-					error (invalid witness file)	.61	.39	9.6	41	error (invalid witness file)	5.9	3.1	100	300
minepump_spec4_product57_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	20	6.6	180	560	2.6	0	-					-					out of memory	300	280	6300	7000	true	24	13	310	660
minepump_spec4_product58_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	21	7.3	180	720	2.6	0	-					-					out of memory	400	380	11000	7000	true	26	14	390	650
minepump_spec4_product59_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	28	9.9	260	820	2.6	0	-					-					out of memory	520	500	9100	7000	true	33	18	320	730
minepump_spec4_product60_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	34	14	340	750	3.0	0	-					-					out of memory	540	520	9100	7000	true	33	18	470	730
minepump_spec4_product61_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	20	6.1	160	560	2.6	0	-					-					out of memory	380	360	7300	7000	true	25	14	410	630
minepump_spec4_product62_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	15	4.3	110	500	2.6	0	-					-					out of memory	310	290	8100	7000	true	23	13	260	630
minepump_spec4_product63_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	490	12000	3900	2.3	0	-					-					error (invalid witness file)	.69	.44	9.1	42	error (invalid witness file)	6.0	3.2	120	300
minepump_spec4_product64_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	540	12000	1700	2.3	0	-					-					error (invalid witness file)	.50	.31	10	40	error (invalid witness file)	5.9	3.2	130	290
minepump_spec5_product01_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.3	2.2	56	330	2.6	0	-					-					true	10	5.3	140	320	true	11	5.9	180	380
minepump_spec5_product02_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.2	2.1	59	350	2.6	0	-					-					true	9.7	5.2	190	370	true	11	6.1	170	360
minepump_spec5_product03_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	6.9	2.0	50	330	2.6	0	-					-					true	9.8	5.2	110	350	true	10	5.4	220	350
minepump_spec5_product04_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	6.8	2.2	53	320	2.6	0	-					-					true	9.2	4.8	170	370	true	9.3	5.1	170	350
minepump_spec5_product05_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	11000	1900	2.3	0	-					-					error (invalid witness file)	.67	.43	7.4	41	error (invalid witness file)	6.0	3.2	91	300
minepump_spec5_product06_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.7	2.4	67	410	2.6	0	-					-					true	11	5.6	180	370	true	11	5.8	180	360
minepump_spec5_product07_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.0	2.6	69	460	2.6	0	-					-					true	12	6.4	120	360	true	10	5.6	180	360
minepump_spec5_product08_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.8	2.6	69	490	2.6	0	-					-					true	11	5.8	230	420	true	11	6.1	210	370
minepump_spec5_product09_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	6.9	2.2	52	320	2.6	0	-					-					true	9.9	5.2	140	320	true	12	6.2	190	370
minepump_spec5_product10_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	6.9	2.2	55	320	2.6	0	-					-					true	11	5.7	110	330	true	11	6.1	210	360
minepump_spec5_product11_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	6.7	2.2	56	320	2.6	0	-					-					true	8.9	4.7	120	360	true	11	6.0	170	360
minepump_spec5_product12_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	6.8	2.1	58	340	2.6	0	-					-					true	9.5	5.1	140	340	true	10	5.5	190	350
minepump_spec5_product13_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	12000	1800	2.3	0	-					-					error (invalid witness file)	.50	.32	12	39	error (invalid witness file)	6.0	3.2	92	300
minepump_spec5_product14_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	7.9	2.4	60	410	2.6	0	-					-					true	11	6.0	160	400	true	10	5.6	140	370
minepump_spec5_product15_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.2	2.8	74	470	2.6	0	-					-					true	13	6.6	130	400	true	11	5.8	130	370
minepump_spec5_product16_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	11	3.1	81	480	2.6	0	-					-					true	12	6.2	160	430	true	10	5.5	120	360
minepump_spec5_product17_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	12000	1900	2.3	0	-					-					error (invalid witness file)	.63	.41	5.9	40	error (invalid witness file)	6.0	3.2	120	290
minepump_spec5_product18_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.3	2.5	59	420	2.6	0	-					-					true	10	5.4	200	410	true	13	6.9	150	370
minepump_spec5_product19_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.6	2.6	73	470	2.6	0	-					-					true	12	6.1	140	380	true	11	5.7	140	360
minepump_spec5_product20_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.3	2.6	66	460	2.6	0	-					-					true	11	5.7	200	410	true	10	5.4	150	350
minepump_spec5_product21_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	13000	1700	2.3	0	-					-					error (invalid witness file)	.57	.37	8.4	40	error (invalid witness file)	7.7	4.0	120	340
minepump_spec5_product22_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.9	2.9	75	480	2.6	0	-					-					true	16	8.4	130	460	true	11	6.0	180	370
minepump_spec5_product23_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.6	3.1	83	470	2.6	0	-					-					true	14	7.3	160	450	true	11	5.8	220	350
minepump_spec5_product24_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	10	3.2	89	490	2.6	0	-					-					true	13	7.0	180	460	true	10	5.5	140	360
minepump_spec5_product25_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	11000	1700	2.3	0	-					-					error (invalid witness file)	.67	.43	8.6	42	error (invalid witness file)	6.0	3.2	84	310
minepump_spec5_product26_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.0	2.4	62	430	2.6	0	-					-					true	9.9	5.2	190	370	true	12	6.2	250	370
minepump_spec5_product27_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.0	2.6	63	460	2.9	.18	-					-					true	13	6.8	130	400	true	11	5.8	200	360
minepump_spec5_product28_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.9	3.0	87	480	2.6	0	-					-					true	12	6.5	180	430	true	11	5.7	170	360
minepump_spec5_product29_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	11000	1900	2.3	0	-					-					error (invalid witness file)	.52	.33	8.0	39	error (invalid witness file)	5.3	2.9	79	290
minepump_spec5_product30_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	8.7	2.7	73	470	2.6	0	-					-					true	12	6.4	200	430	true	12	6.2	210	370
minepump_spec5_product31_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.5	3.1	83	460	2.6	0	-					-					true	14	7.1	150	420	true	11	5.9	190	360
minepump_spec5_product32_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	9.4	2.9	87	460	2.6	0	-					-					true	13	6.8	160	430	true	11	5.7	170	360
minepump_spec5_product33_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	570	12000	3500	2.3	0	-					-					error (invalid witness file)	.59	.39	9.0	40	error (invalid witness file)	5.8	3.1	110	290
minepump_spec5_product34_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	600	10000	1900	2.3	0	-					-					error (invalid witness file)	.59	.38	10	40	error (invalid witness file)	5.9	3.2	83	300
minepump_spec5_product35_true-unreach-call_false-termination.cil.c	true	2	wit	inspect	24	8.0	200	630	2.6	0	-					-					timeout	910	890	17000	5900	true	22	12	190	560
minepump_spec5_product36_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	14000	1900	2.3	0	-					-					error (invalid witness file)	.65	.41	7.7	40	error (invalid witness file)	6.0	3.2	120	300
minepump_spec5_product37_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	11000	2300	2.3	0	-					-					error (invalid witness file)	.50	.32	12	40	error (invalid witness file)	6.2	3.2	120	310
minepump_spec5_product38_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	500	9800	2600	2.3	0	-					-					error (invalid witness file)	.65	.41	9.7	40	error (invalid witness file)	5.8	3.1	110	300
minepump_spec5_product39_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	560	12000	3200	2.3	0	-					-					error (invalid witness file)	.52	.33	12	40	error (invalid witness file)	5.7	3.0	91	300
minepump_spec5_product40_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	12000	2100	2.3	0	-					-					error (invalid witness file)	.49	.31	9.0	39	error (invalid witness file)	6.7	3.6	85	300
minepump_spec5_product41_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	610	13000	2900	2.3	0	-					-					error (invalid witness file)	.57	.37	9.2	40	error (invalid witness file)	6.3	3.3	110	310
minepump_spec5_product42_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	740	12000	1800	2.3	0	-					-					error (invalid witness file)	.51	.33	12	39	error (invalid witness file)	5.7	3.0	120	300
minepump_spec5_product43_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	12000	1700	2.3	0	-					-					error (invalid witness file)	.60	.39	9.5	41	error (invalid witness file)	6.2	3.2	63	310
minepump_spec5_product44_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	13000	2000	2.3	0	-					-					error (invalid witness file)	.56	.35	10	40	error (invalid witness file)	6.9	3.6	110	320
minepump_spec5_product45_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	12000	1800	2.3	0	-					-					error (invalid witness file)	.49	.34	12	43	error (invalid witness file)	6.9	3.6	130	310
minepump_spec5_product46_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	15000	2000	2.3	0	-					-					error (invalid witness file)	.67	.43	9.2	43	error (invalid witness file)	6.1	3.2	120	290
minepump_spec5_product47_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2200	2.3	0	-					-					error (invalid witness file)	.64	.41	8.0	42	error (invalid witness file)	5.6	3.0	63	300
minepump_spec5_product48_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	13000	3200	2.3	0	-					-					error (invalid witness file)	.54	.35	14	43	error (invalid witness file)	5.9	3.1	120	310
minepump_spec5_product49_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	12000	1600	2.3	0	-					-					error (invalid witness file)	.60	.38	9.4	40	error (invalid witness file)	5.6	3.0	73	300
minepump_spec5_product50_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	500	11000	2400	2.3	0	-					-					error (invalid witness file)	.66	.42	7.5	40	error (invalid witness file)	5.9	3.1	120	290
minepump_spec5_product51_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	13000	1800	2.3	0	-					-					error (invalid witness file)	.50	.32	12	39	error (invalid witness file)	6.4	3.4	120	300
minepump_spec5_product52_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	12000	2000	2.3	0	-					-					error (invalid witness file)	.51	.32	13	40	error (invalid witness file)	5.8	3.1	85	300
minepump_spec5_product53_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	11000	1700	2.3	0	-					-					error (invalid witness file)	.65	.42	8.5	40	error (invalid witness file)	6.1	3.2	93	290
minepump_spec5_product54_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	730	12000	2100	2.3	0	-					-					error (invalid witness file)	.65	.42	8.1	42	error (invalid witness file)	6.1	3.2	78	300
minepump_spec5_product55_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	560	11000	3500	2.3	0	-					-					error (invalid witness file)	.49	.32	13	39	error (invalid witness file)	6.3	3.3	100	310
minepump_spec5_product56_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	14000	2000	2.3	0	-					-					error (invalid witness file)	.66	.43	7.4	39	error (invalid witness file)	6.2	3.3	120	300
minepump_spec5_product57_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	11000	2000	2.3	0	-					-					error (invalid witness file)	.48	.32	12	40	error (invalid witness file)	5.8	3.1	94	300
minepump_spec5_product58_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	12000	1700	2.3	0	-					-					error (invalid witness file)	.52	.33	12	41	error (invalid witness file)	5.9	3.2	110	300
minepump_spec5_product59_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	13000	1800	2.3	0	-					-					error (invalid witness file)	.64	.40	8.5	41	error (invalid witness file)	6.2	3.3	95	300
minepump_spec5_product60_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	12000	2000	2.3	0	-					-					error (invalid witness file)	.69	.43	8.1	41	error (invalid witness file)	6.6	3.5	130	300
minepump_spec5_product61_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	680	12000	1800	2.3	0	-					-					error (invalid witness file)	.51	.33	13	39	error (invalid witness file)	5.8	3.1	95	300
minepump_spec5_product62_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	770	15000	2900	2.3	0	-					-					error (invalid witness file)	.60	.38	10	41	error (invalid witness file)	5.3	2.9	80	290
minepump_spec5_product63_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	740	13000	2100	2.3	0	-					-					error (invalid witness file)	.72	.47	7.3	40	error (invalid witness file)	6.2	3.3	120	300
minepump_spec5_product64_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	13000	2000	2.3	0	-					-					error (invalid witness file)	.56	.34	14	43	error (invalid witness file)	5.7	3.0	96	300
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c	timeout	0	wit	inspect	900	780	12000	4800	2.3	0	-					-					error (invalid witness file)	.64	.41	8.5	40	error (invalid witness file)	5.9	3.2	97	300
../../sv-benchmarks/c/product-lines/	verifier status	score	witness	inspect witness	cpu (s)	wall (s)	energy (J)	mem (MB)	blkio-w (MB)	blkio-r (MB)	validator cpachecker violation t<90s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator uautomizer violation t<90s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator cpachecker correctness t<900s status	cpu (s)	wall (s)	energy (J)	mem (MB)	validator uautomizer correctness t<900s status	cpu (s)	wall (s)	energy (J)	mem (MB)
total	597	487			270000	210000	3700000	1100000	1500	1.8	597	530	300	7700	32000	597	2100	1100	36000	86000	597	63000	60000	1300000	1000000	597	4000	2200	62000	130000
correct results	289	487			3600	1200	30000	140000	760	1.8	36	440	240	6100	25000	91	1000	550	16000	34000	58	62000	59000	1300000	1000000	198	3200	1700	48000	92000
correct true	198	396			2600	840	22000	100000	520	1.8	36	0	0	0	0	0	0	0	0	0	58	62000	59000	1300000	1000000	198	3200	1700	48000	92000
correct false	91	91			970	310	7900	38000	230	0	0	440	240	6100	25000	91	1000	550	16000	34000	0	0	0	0	0	0	0	0	0	0
correct-unconfimed results	0
correct-unconfirmed true	0
correct-unconfirmed false	0
incorrect results	0
incorrect true	0
incorrect false	0
score (597 tasks, max score: 929)	487
Run set	sv-comp17.ReachSafety-ProductLines