utaipan.2017-01-14_0946.results.sv-comp17.ReachSafety-ProductLines.xml.bz2.merged.xml.bz2

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