Tool CPAchecker 1.4-svn 18373
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-22-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-04 20:04:07 CET [[ 2016-01-15 08:41:31 CET ]] [[ 2016-01-15 22:05:37 CET ]]
Run set sv-comp16.ProductLines
Options -sv-comp16--refsel -disable-java-assertions -heap 12500m -setprop cpa.arg.errorPath.graphml=error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cpa-refsel.2016-01-04_2004.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/product-lines/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
elevator_spec14_product20_false-unreach-call.cil.c false(reach) 12   3.6 540 wit false(reach) 22   12   670 false(reach) 41 26   610
elevator_spec14_product24_false-unreach-call.cil.c false(reach) 13   3.9 570 wit false(reach) 19   9.7 670 false(reach) 39 21   770
elevator_spec14_product28_false-unreach-call.cil.c false(reach) 11   3.3 550 wit false(reach) 22   11   640 false(reach) 35 20   590
elevator_spec14_product32_false-unreach-call.cil.c false(reach) 12   3.5 570 wit false(reach) 24   12   670 false(reach) 41 23   740
elevator_spec14_productSimulator_false-unreach-call.cil.c false(reach) 12   3.7 610 wit false(reach) 25   13   690 false(reach) 50 27   820
elevator_spec1_product18_false-unreach-call.cil.c false(reach) 13   3.9 570 wit false(reach) 23   12   670 false(reach) 49 28   820
elevator_spec1_product20_false-unreach-call.cil.c false(reach) 14   4.1 580 wit false(reach) 24   12   710 false(reach) 50 28   820
elevator_spec1_product22_false-unreach-call.cil.c false(reach) 12   3.6 600 wit false(reach) 23   12   680 false(reach) 52 28   850
elevator_spec1_product24_false-unreach-call.cil.c false(reach) 14   4.0 620 wit false(reach) 21   11   690 false(reach) 50 28   800
elevator_spec1_product26_false-unreach-call.cil.c false(reach) 13   4.0 560 wit false(reach) 23   12   650 false(reach) 53 29   850
elevator_spec1_product28_false-unreach-call.cil.c false(reach) 14   4.0 590 wit false(reach) 21   11   680 false(reach) 54 31   830
elevator_spec1_product30_false-unreach-call.cil.c false(reach) 14   4.2 590 wit false(reach) 18   9.7 660 false(reach) 50 28   810
elevator_spec1_product32_false-unreach-call.cil.c false(reach) 13   3.8 610 wit false(reach) 24   12   710 false(reach) 47 27   800
elevator_spec1_productSimulator_false-unreach-call.cil.c false(reach) 15   4.5 640 wit false(reach) 24   13   780 false(reach) 53 30   880
elevator_spec2_product18_false-unreach-call.cil.c false(reach) 13   3.9 540 wit false(reach) 23   12   650 false(reach) 46 27   790
elevator_spec2_product20_false-unreach-call.cil.c false(reach) 14   4.1 580 wit false(reach) 25   13   680 false(reach) 49 28   800
elevator_spec2_product22_false-unreach-call.cil.c false(reach) 13   4.2 580 wit false(reach) 22   11   650 false(reach) 46 25   750
elevator_spec2_product24_false-unreach-call.cil.c false(reach) 12   3.7 590 wit false(reach) 22   12   690 false(reach) 53 29   790
elevator_spec2_product26_false-unreach-call.cil.c false(reach) 12   3.8 560 wit false(reach) 21   11   660 false(reach) 49 27   790
elevator_spec2_product28_false-unreach-call.cil.c false(reach) 14   4.2 570 wit false(reach) 19   10   650 false(reach) 48 28   780
elevator_spec2_product30_false-unreach-call.cil.c false(reach) 14   4.1 580 wit false(reach) 24   12   680 false(reach) 50 29   860
elevator_spec2_product32_false-unreach-call.cil.c false(reach) 14   4.4 580 wit false(reach) 22   11   660 false(reach) 49 27   800
elevator_spec2_productSimulator_false-unreach-call.cil.c false(reach) 16   4.7 640 wit false(reach) 26   14   740 false(reach) 55 31   780
elevator_spec3_product03_false-unreach-call.cil.c false(reach) 16   4.7 610 wit false(reach) 26   14   750 false(reach) 58 31   1000
elevator_spec3_product11_false-unreach-call.cil.c false(reach) 15   4.5 620 wit false(reach) 28   14   710 false(reach) 62 35   950
elevator_spec3_product19_false-unreach-call.cil.c false(reach) 15   4.6 630 wit false(reach) 27   14   770 false(reach) 59 32   890
elevator_spec3_product20_false-unreach-call.cil.c false(reach) 15   4.5 650 wit false(reach) 23   12   770 false(reach) 50 29   900
elevator_spec3_product23_false-unreach-call.cil.c false(reach) 16   4.8 660 wit false(reach) 24   13   820 false(reach) 59 32   1100
elevator_spec3_product24_false-unreach-call.cil.c false(reach) 15   4.5 670 wit false(reach) 30   15   840 false(reach) 63 36   1000
elevator_spec3_product27_false-unreach-call.cil.c false(reach) 14   4.3 630 wit false(reach) 28   15   750 false(reach) 61 33   1000
elevator_spec3_product28_false-unreach-call.cil.c false(reach) 15   4.6 640 wit false(reach) 22   12   740 false(reach) 66 36   1100
elevator_spec3_product31_false-unreach-call.cil.c false(reach) 16   4.7 650 wit false(reach) 29   15   800 false(reach) 63 37   860
elevator_spec3_product32_false-unreach-call.cil.c false(reach) 16   4.9 640 wit false(reach) 30   15   860 false(reach) 61 34   930
elevator_spec3_productSimulator_false-unreach-call.cil.c false(reach) 25   6.9 930 wit false(reach) 35   18   880 false(reach) 80 46   1200
elevator_spec9_product26_false-unreach-call.cil.c false(reach) 11   3.5 560 wit false(reach) 22   12   680 false(reach) 53 29   800
elevator_spec9_product28_false-unreach-call.cil.c false(reach) 14   4.1 590 wit false(reach) 24   12   680 false(reach) 49 28   800
elevator_spec9_product30_false-unreach-call.cil.c false(reach) 14   4.1 580 wit false(reach) 25   13   690 false(reach) 44 24   790
elevator_spec9_product32_false-unreach-call.cil.c false(reach) 13   3.8 600 wit false(reach) 26   14   690 false(reach) 52 30   900
elevator_spec9_productSimulator_false-unreach-call.cil.c false(reach) 15   4.7 640 wit false(reach) 24   13   790 false(reach) 65 36   1000
elevator_spec13_product21_true-unreach-call.cil.c true 7.2 2.6 280 wit - -
elevator_spec13_product22_true-unreach-call.cil.c true 6.3 2.3 270 wit - -
elevator_spec13_product23_true-unreach-call.cil.c true 7.4 2.7 280 wit - -
elevator_spec13_product24_true-unreach-call.cil.c true 6.5 2.3 290 wit - -
elevator_spec13_product29_true-unreach-call.cil.c true 7.1 2.6 280 wit - -
elevator_spec13_product30_true-unreach-call.cil.c true 6.2 2.3 280 wit - -
elevator_spec13_product31_true-unreach-call.cil.c true 7.4 2.7 280 wit - -
elevator_spec13_product32_true-unreach-call.cil.c true 6.4 2.3 290 wit - -
elevator_spec13_productSimulator_true-unreach-call.cil.c true 9.8 3.3 430 wit - -
elevator_spec14_product03_true-unreach-call.cil.c true 8.8 3.1 300 wit - -
elevator_spec14_product11_true-unreach-call.cil.c true 8.7 3.0 310 wit - -
elevator_spec14_product19_true-unreach-call.cil.c true 8.7 3.1 310 wit - -
elevator_spec14_product23_true-unreach-call.cil.c true 9.1 3.2 330 wit - -
elevator_spec14_product27_true-unreach-call.cil.c true 7.5 2.6 310 wit - -
elevator_spec14_product31_true-unreach-call.cil.c true 9.2 3.2 330 wit - -
elevator_spec1_product01_true-unreach-call.cil.c true 8.3 3.0 300 wit - -
elevator_spec1_product03_true-unreach-call.cil.c true 8.5 3.0 310 wit - -
elevator_spec1_product09_true-unreach-call.cil.c true 7.9 2.9 300 wit - -
elevator_spec1_product11_true-unreach-call.cil.c true 7.0 2.5 310 wit - -
elevator_spec1_product17_true-unreach-call.cil.c true 6.9 2.4 310 wit - -
elevator_spec1_product19_true-unreach-call.cil.c true 7.0 2.5 310 wit - -
elevator_spec1_product21_true-unreach-call.cil.c true 7.0 2.5 310 wit - -
elevator_spec1_product23_true-unreach-call.cil.c true 8.6 3.1 310 wit - -
elevator_spec1_product25_true-unreach-call.cil.c true 6.9 2.5 290 wit - -
elevator_spec1_product27_true-unreach-call.cil.c true 8.5 3.1 310 wit - -
elevator_spec1_product29_true-unreach-call.cil.c true 8.5 3.0 300 wit - -
elevator_spec1_product31_true-unreach-call.cil.c true 8.6 3.1 320 wit - -
elevator_spec2_product01_true-unreach-call.cil.c true 7.5 2.7 280 wit - -
elevator_spec2_product03_true-unreach-call.cil.c true 7.5 2.7 280 wit - -
elevator_spec2_product09_true-unreach-call.cil.c true 7.4 2.7 280 wit - -
elevator_spec2_product11_true-unreach-call.cil.c true 7.7 2.8 280 wit - -
elevator_spec2_product17_true-unreach-call.cil.c true 7.0 2.5 280 wit - -
elevator_spec2_product19_true-unreach-call.cil.c true 7.6 2.8 290 wit - -
elevator_spec2_product21_true-unreach-call.cil.c true 7.4 2.7 280 wit - -
elevator_spec2_product23_true-unreach-call.cil.c true 6.5 2.3 290 wit - -
elevator_spec2_product25_true-unreach-call.cil.c true 7.3 2.7 290 wit - -
elevator_spec2_product27_true-unreach-call.cil.c true 7.7 2.7 290 wit - -
elevator_spec2_product29_true-unreach-call.cil.c true 7.6 2.8 280 wit - -
elevator_spec2_product31_true-unreach-call.cil.c true 7.7 2.8 290 wit - -
elevator_spec3_product01_true-unreach-call.cil.c true 9.0 3.2 320 wit - -
elevator_spec3_product09_true-unreach-call.cil.c true 7.8 2.7 320 wit - -
elevator_spec3_product17_true-unreach-call.cil.c true 8.9 3.2 320 wit - -
elevator_spec3_product18_true-unreach-call.cil.c true 8.9 3.2 320 wit - -
elevator_spec3_product21_true-unreach-call.cil.c true 9.4 3.3 330 wit - -
elevator_spec3_product22_true-unreach-call.cil.c true 7.9 2.8 340 wit - -
elevator_spec3_product25_true-unreach-call.cil.c true 7.5 2.7 320 wit - -
elevator_spec3_product26_true-unreach-call.cil.c true 7.8 2.8 320 wit - -
elevator_spec3_product29_true-unreach-call.cil.c true 9.7 3.3 330 wit - -
elevator_spec3_product30_true-unreach-call.cil.c true 9.5 3.3 330 wit - -
elevator_spec9_product09_true-unreach-call.cil.c true 7.5 2.7 280 wit - -
elevator_spec9_product11_true-unreach-call.cil.c true 7.5 2.7 280 wit - -
elevator_spec9_product25_true-unreach-call.cil.c true 6.4 2.3 280 wit - -
elevator_spec9_product27_true-unreach-call.cil.c true 7.5 2.8 280 wit - -
elevator_spec9_product29_true-unreach-call.cil.c true 6.5 2.4 290 wit - -
elevator_spec9_product31_true-unreach-call.cil.c true 7.5 2.8 280 wit - -
email_spec0_product16_false-unreach-call.cil.c false(reach) 43   18   1300 wit false(reach) 23   12   730 false(reach) 32 17   560
email_spec0_product21_false-unreach-call.cil.c false(reach) 50   21   1800 wit false(reach) 20   10   780 false(reach) 36 20   570
email_spec0_product22_false-unreach-call.cil.c false(reach) 49   20   1800 wit false(reach) 22   11   730 false(reach) 33 19   560
email_spec0_product26_false-unreach-call.cil.c false(reach) 54   22   1800 wit false(reach) 20   11   760 false(reach) 33 18   580
email_spec0_product31_false-unreach-call.cil.c false(reach) 50   21   1800 wit false(reach) 25   13   830 false(reach) 32 18   570
email_spec0_product33_false-unreach-call.cil.c false(reach) 61   21   1400 wit false(reach) 23   12   830 false(reach) 35 18   580
email_spec0_product34_false-unreach-call.cil.c false(reach) 58   25   1800 wit false(reach) 24   13   830 false(reach) 35 19   570
email_spec0_product35_false-unreach-call.cil.c false(reach) 60   26   2000 wit false(reach) 23   12   860 false(reach) 35 19   580
email_spec0_productSimulator_false-unreach-call.cil.c false(reach) 140   58   3800 wit false(reach) 26   13   870 false(reach) 45 25   830
email_spec11_product15_false-unreach-call.cil.c false(reach) 56   20   1300 wit false(reach) 23   12   750 false(reach) 32 19   550
email_spec11_product20_false-unreach-call.cil.c false(reach) 44   18   1800 wit false(reach) 20   11   770 false(reach) 33 18   560
email_spec11_product22_false-unreach-call.cil.c false(reach) 51   21   1800 wit false(reach) 23   12   740 false(reach) 31 17   530
email_spec11_product26_false-unreach-call.cil.c false(reach) 75   25   1800 wit false(reach) 23   12   760 false(reach) 34 18   560
email_spec11_product30_false-unreach-call.cil.c false(reach) 59   23   1800 wit false(reach) 24   12   810 false(reach) 33 18   570
email_spec11_product32_false-unreach-call.cil.c false(reach) 78   27   1800 wit false(reach) 24   12   830 false(reach) 35 19   580
email_spec11_product33_false-unreach-call.cil.c false(reach) 59   24   1800 wit false(reach) 23   12   820 false(reach) 33 19   580
email_spec11_product35_false-unreach-call.cil.c false(reach) 68   27   2000 wit false(reach) 23   12   820 false(reach) 34 18   580
email_spec11_productSimulator_false-unreach-call.cil.c false(reach) 150   62   3800 wit false(reach) 25   13   850 false(reach) 48 27   770
email_spec1_product14_false-unreach-call.cil.c false(reach) 28   8.3 960 wit false(reach) 24   13   850 true 20 11   540
email_spec1_product15_false-unreach-call.cil.c false(reach) 31   9.4 990 wit false(reach) 22   12   800 true 21 13   490
email_spec1_product16_false-unreach-call.cil.c false(reach) 33   9.2 1000 wit false(reach) 26   13   910 true 22 13   540
email_spec1_product20_false-unreach-call.cil.c false(reach) 32   8.6 1000 wit false(reach) 25   13   860 true 23 14   520
email_spec1_product21_false-unreach-call.cil.c false(reach) 30   8.7 970 wit false(reach) 24   13   850 true 20 11   520
email_spec1_product22_false-unreach-call.cil.c false(reach) 31   9.1 1000 wit false(reach) 26   14   840 true 23 12   540
email_spec1_product26_false-unreach-call.cil.c false(reach) 28   8.6 960 wit false(reach) 23   12   820 true 23 13   530
email_spec1_product29_false-unreach-call.cil.c false(reach) 30   9.0 1000 wit false(reach) 25   13   830 true 20 11   540
email_spec1_product30_false-unreach-call.cil.c false(reach) 33   10   1100 wit false(reach) 27   14   860 true 23 13   530
email_spec1_product31_false-unreach-call.cil.c false(reach) 29   9.6 1000 wit false(reach) 23   12   850 true 24 13   550
email_spec1_product32_false-unreach-call.cil.c false(reach) 28   8.7 980 wit false(reach) 22   12   860 true 23 13   530
email_spec1_product33_false-unreach-call.cil.c false(reach) 33   10   1100 wit false(reach) 23   12   840 true 24 13   550
email_spec1_product34_false-unreach-call.cil.c false(reach) 30   9.0 980 wit false(reach) 23   12   860 true 22 12   530
email_spec1_product35_false-unreach-call.cil.c false(reach) 32   9.8 1000 wit false(reach) 26   14   840 true 26 14   540
email_spec1_productSimulator_false-unreach-call.cil.c false(reach) 48   17   1700 wit false(reach) 27   14   840 true 26 16   540
email_spec27_product17_false-unreach-call.cil.c false(reach) 24   6.3 910 wit false(reach) 23   12   860 false(reach) 35 18   590
email_spec27_product18_false-unreach-call.cil.c false(reach) 33   9.7 1000 wit false(reach) 21   11   850 true 22 13   390
email_spec27_product19_false-unreach-call.cil.c false(reach) 29   9.2 990 wit false(reach) 26   13   860 true 23 13   540
email_spec27_product23_false-unreach-call.cil.c false(reach) 22   5.9 900 wit false(reach) 26   14   860 true 22 12   540
email_spec27_product24_false-unreach-call.cil.c false(reach) 28   8.7 1000 wit false(reach) 25   13   830 true 25 17   420
email_spec27_product25_false-unreach-call.cil.c false(reach) 23   5.9 880 wit false(reach) 25   13   850 false(reach) 33 19   580
email_spec27_product27_false-unreach-call.cil.c false(reach) 23   6.4 890 wit false(reach) 26   14   850 false(reach) 37 20   580
email_spec27_product29_false-unreach-call.cil.c false(reach) 24   6.7 910 wit false(reach) 25   13   850 true 24 13   530
email_spec27_product30_false-unreach-call.cil.c false(reach) 36   9.9 1100 wit false(reach) 27   14   860 true 24 13   530
email_spec27_product31_false-unreach-call.cil.c false(reach) 32   9.8 1100 wit false(reach) 29   15   840 true 24 14   540
email_spec27_product32_false-unreach-call.cil.c false(reach) 27   6.9 950 wit false(reach) 27   14   850 true 24 13   540
email_spec27_product33_false-unreach-call.cil.c false(reach) 30   10   1100 wit false(reach) 26   14   880 true 24 18   540
email_spec27_product34_false-unreach-call.cil.c false(reach) 25   6.9 940 wit false(reach) 29   15   910 true 24 14   410
email_spec27_product35_false-unreach-call.cil.c false(reach) 24   6.9 950 wit false(reach) 29   15   840 true 25 14   540
email_spec27_productSimulator_false-unreach-call.cil.c false(reach) 31   9.3 1000 wit false(reach) 29   15   850 true 26 15   530
email_spec3_product13_false-unreach-call.cil.c false(reach) 12   3.5 490 wit false(reach) 19   10   600 false(reach) 26 14   540
email_spec3_product17_false-unreach-call.cil.c false(reach) 12   3.5 500 wit false(reach) 20   10   600 false(reach) 30 16   520
email_spec3_product18_false-unreach-call.cil.c false(reach) 11   3.4 490 wit false(reach) 19   10   590 false(reach) 25 14   400
email_spec3_product19_false-unreach-call.cil.c false(reach) 10   3.1 490 wit false(reach) 18   9.3 600 false(reach) 28 17   530
email_spec3_product23_false-unreach-call.cil.c false(reach) 12   3.5 510 wit false(reach) 19   10   610 false(reach) 27 14   520
email_spec3_product24_false-unreach-call.cil.c false(reach) 10   3.0 480 wit false(reach) 17   8.8 630 false(reach) 31 16   530
email_spec3_product25_false-unreach-call.cil.c false(reach) 12   3.6 490 wit false(reach) 21   11   620 false(reach) 31 18   440
email_spec3_product27_false-unreach-call.cil.c false(reach) 10   3.0 490 wit false(reach) 19   9.9 620 false(reach) 31 16   550
email_spec3_product28_false-unreach-call.cil.c false(reach) 10   3.1 510 wit false(reach) 20   11   620 false(reach) 31 17   530
email_spec3_product29_false-unreach-call.cil.c false(reach) 12   3.7 500 wit false(reach) 20   10   640 false(reach) 31 18   550
email_spec3_product30_false-unreach-call.cil.c false(reach) 12   3.5 520 wit false(reach) 20   11   620 false(reach) 31 16   540
email_spec3_product31_false-unreach-call.cil.c false(reach) 13   3.7 510 wit false(reach) 19   10   620 false(reach) 29 16   540
email_spec3_product32_false-unreach-call.cil.c false(reach) 12   3.5 520 wit false(reach) 20   11   640 false(reach) 33 18   450
email_spec3_product33_false-unreach-call.cil.c false(reach) 12   3.7 510 wit false(reach) 20   11   620 false(reach) 30 17   530
email_spec3_product34_false-unreach-call.cil.c false(reach) 12   3.7 510 wit false(reach) 20   11   630 false(reach) 32 17   560
email_spec3_product35_false-unreach-call.cil.c false(reach) 12   3.7 520 wit false(reach) 21   11   640 false(reach) 32 18   540
email_spec3_productSimulator_false-unreach-call.cil.c false(reach) 13   3.8 540 wit false(reach) 22   12   710 false(reach) 41 22   770
email_spec4_product18_false-unreach-call.cil.c false(reach) 31   9.5 990 wit false(reach) 22   12   760 true 21 13   480
email_spec4_product19_false-unreach-call.cil.c false(reach) 30   9.1 1000 wit false(reach) 24   12   840 true 23 13   530
email_spec4_product23_false-unreach-call.cil.c false(reach) 33   9.5 1100 wit false(reach) 21   11   780 true 18 10   530
email_spec4_product24_false-unreach-call.cil.c false(reach) 30   9.3 970 wit false(reach) 24   13   860 true 22 12   530
email_spec4_product25_false-unreach-call.cil.c false(reach) 30   9.3 1000 wit false(reach) 23   12   850 true 22 12   530
email_spec4_product27_false-unreach-call.cil.c false(reach) 32   9.9 1000 wit false(reach) 21   11   860 true 23 12   520
email_spec4_product30_false-unreach-call.cil.c false(reach) 35   10   1100 wit false(reach) 24   13   820 true 22 12   530
email_spec4_product31_false-unreach-call.cil.c false(reach) 32   9.5 1100 wit false(reach) 23   12   820 true 23 13   520
email_spec4_product32_false-unreach-call.cil.c false(reach) 34   11   1100 wit false(reach) 22   12   840 true 22 12   530
email_spec4_product33_false-unreach-call.cil.c false(reach) 32   10   1100 wit false(reach) 23   12   850 true 21 11   540
email_spec4_product34_false-unreach-call.cil.c false(reach) 33   11   1100 wit false(reach) 25   13   870 true 23 13   520
email_spec4_product35_false-unreach-call.cil.c false(reach) 32   11   1100 wit false(reach) 25   13   890 true 24 14   480
email_spec4_productSimulator_false-unreach-call.cil.c false(reach) 52   20   1800 wit false(reach) 23   12   870 true 26 14   540
email_spec6_product12_false-unreach-call.cil.c false(reach) 29   8.2 980 wit false(reach) 22   12   710 false(reach) 31 17   470
email_spec6_product14_false-unreach-call.cil.c false(reach) 27   8.5 970 wit false(reach) 19   10   720 false(reach) 31 18   530
email_spec6_product15_false-unreach-call.cil.c false(reach) 31   8.4 1000 wit false(reach) 22   12   710 false(reach) 31 18   540
email_spec6_product16_false-unreach-call.cil.c false(reach) 31   8.7 1000 wit false(reach) 21   11   710 false(reach) 34 18   560
email_spec6_product20_false-unreach-call.cil.c false(reach) 31   9.0 1000 wit false(reach) 22   12   740 false(reach) 29 16   560
email_spec6_product21_false-unreach-call.cil.c false(reach) 27   8.2 970 wit false(reach) 21   11   730 false(reach) 33 18   570
email_spec6_product22_false-unreach-call.cil.c false(reach) 29   8.7 970 wit false(reach) 22   12   700 false(reach) 31 18   560
email_spec6_product26_false-unreach-call.cil.c false(reach) 28   9.0 970 wit false(reach) 24   13   770 false(reach) 32 17   550
email_spec6_product28_false-unreach-call.cil.c false(reach) 28   8.7 970 wit false(reach) 20   10   690 false(reach) 32 18   570
email_spec6_product29_false-unreach-call.cil.c false(reach) 29   9.1 990 wit false(reach) 22   11   760 false(reach) 32 18   560
email_spec6_product30_false-unreach-call.cil.c false(reach) 27   8.3 960 wit false(reach) 22   11   730 false(reach) 32 17   550
email_spec6_product31_false-unreach-call.cil.c false(reach) 30   9.3 990 wit false(reach) 22   12   730 false(reach) 33 18   580
email_spec6_product32_false-unreach-call.cil.c false(reach) 30   9.8 970 wit false(reach) 23   12   780 false(reach) 34 19   550
email_spec6_product33_false-unreach-call.cil.c false(reach) 33   9.9 970 wit false(reach) 21   11   740 false(reach) 32 17   550
email_spec6_product34_false-unreach-call.cil.c false(reach) 30   9.6 990 wit false(reach) 19   10   740 false(reach) 36 21   530
email_spec6_product35_false-unreach-call.cil.c false(reach) 34   10   1100 wit false(reach) 19   10   740 false(reach) 34 19   500
email_spec6_productSimulator_false-unreach-call.cil.c false(reach) 47   18   1800 wit false(reach) 25   13   820 false(reach) 47 26   780
email_spec7_product28_false-unreach-call.cil.c false(reach) 28   8.6 970 wit false(reach) 22   12   720 false(reach) 34 19   590
email_spec7_product29_false-unreach-call.cil.c false(reach) 30   9.2 990 wit false(reach) 19   9.9 730 false(reach) 32 17   540
email_spec7_product30_false-unreach-call.cil.c false(reach) 30   9.0 1000 wit false(reach) 23   12   720 false(reach) 31 17   550
email_spec7_product31_false-unreach-call.cil.c false(reach) 29   9.1 990 wit false(reach) 21   11   740 false(reach) 36 20   590
email_spec7_product32_false-unreach-call.cil.c false(reach) 32   9.6 1000 wit false(reach) 20   11   760 false(reach) 30 16   580
email_spec7_product33_false-unreach-call.cil.c false(reach) 27   8.8 970 wit false(reach) 19   10   710 false(reach) 34 19   570
email_spec7_product34_false-unreach-call.cil.c false(reach) 30   9.7 980 wit false(reach) 22   12   720 false(reach) 31 18   590
email_spec7_product35_false-unreach-call.cil.c false(reach) 34   10   1100 wit false(reach) 22   11   740 false(reach) 30 17   570
email_spec7_productSimulator_false-unreach-call.cil.c false(reach) 46   18   1800 wit false(reach) 23   12   840 false(reach) 46 25   770
email_spec8_product15_false-unreach-call.cil.c false(reach) 28   8.9 990 wit false(reach) 24   12   860 true 21 12   500
email_spec8_product16_false-unreach-call.cil.c false(reach) 29   9.1 1000 wit false(reach) 27   14   870 true 20 11   530
email_spec8_product20_false-unreach-call.cil.c false(reach) 30   9.6 1100 wit false(reach) 22   12   830 true 23 14   550
email_spec8_product21_false-unreach-call.cil.c false(reach) 35   9.7 990 wit false(reach) 29   15   870 true 24 14   550
email_spec8_product22_false-unreach-call.cil.c false(reach) 31   9.3 970 wit false(reach) 24   13   830 true 22 12   390
email_spec8_product26_false-unreach-call.cil.c false(reach) 32   10   1100 wit false(reach) 21   11   830 true 23 13   530
email_spec8_product30_false-unreach-call.cil.c false(reach) 38   11   1100 wit false(reach) 23   12   870 true 23 12   530
email_spec8_product31_false-unreach-call.cil.c false(reach) 30   9.5 1100 wit false(reach) 23   12   890 true 23 14   540
email_spec8_product32_false-unreach-call.cil.c false(reach) 30   11   1100 wit false(reach) 23   12   820 true 21 11   530
email_spec8_product33_false-unreach-call.cil.c false(reach) 33   11   1100 wit false(reach) 29   15   860 true 21 12   540
email_spec8_product34_false-unreach-call.cil.c false(reach) 31   11   1100 wit false(reach) 25   13   850 true 24 17   530
email_spec8_product35_false-unreach-call.cil.c false(reach) 33   11   1100 wit false(reach) 26   14   870 true 25 14   530
email_spec8_productSimulator_false-unreach-call.cil.c false(reach) 52   19   1800 wit false(reach) 28   15   890 true 26 16   530
email_spec9_product15_false-unreach-call.cil.c false(reach) 29   9.5 970 wit false(reach) 23   12   830 true 21 12   490
email_spec9_product16_false-unreach-call.cil.c false(reach) 28   7.9 1000 wit false(reach) 26   13   870 true 21 12   520
email_spec9_product20_false-unreach-call.cil.c false(reach) 32   10   1100 wit false(reach) 25   13   820 true 22 13   530
email_spec9_product21_false-unreach-call.cil.c false(reach) 38   10   1000 wit false(reach) 26   14   880 true 19 10   510
email_spec9_product22_false-unreach-call.cil.c false(reach) 29   8.8 1000 wit false(reach) 23   12   850 true 23 13   540
email_spec9_product26_false-unreach-call.cil.c false(reach) 32   10   1100 wit false(reach) 25   13   860 true 23 13   530
email_spec9_product30_false-unreach-call.cil.c false(reach) 35   11   1100 wit false(reach) 24   12   820 true 23 12   530
email_spec9_product31_false-unreach-call.cil.c false(reach) 30   9.8 1100 wit false(reach) 26   13   880 true 24 14   550
email_spec9_product32_false-unreach-call.cil.c false(reach) 33   11   1100 wit false(reach) 23   12   840 true 22 12   540
email_spec9_product33_false-unreach-call.cil.c false(reach) 33   10   1100 wit false(reach) 27   14   890 true 23 12   530
email_spec9_product34_false-unreach-call.cil.c false(reach) 32   11   1100 wit false(reach) 28   14   940 true 25 15   560
email_spec9_product35_false-unreach-call.cil.c false(reach) 34   11   1100 wit false(reach) 29   15   870 true 25 13   550
email_spec9_productSimulator_false-unreach-call.cil.c false(reach) 52   22   1800 wit false(reach) 26   14   840 true 26 14   550
email_spec0_product05_true-unreach-call.cil.c true 8.6 3.0 350 wit - -
email_spec0_product09_true-unreach-call.cil.c true 10   3.3 430 wit - -
email_spec0_product10_true-unreach-call.cil.c true 10   3.6 360 wit - -
email_spec0_product11_true-unreach-call.cil.c true 46   24   1700 wit - -
email_spec0_product19_true-unreach-call.cil.c true 53   32   2000 wit - -
email_spec0_product24_true-unreach-call.cil.c true 59   37   1900 wit - -
email_spec0_product25_true-unreach-call.cil.c true 59   37   3000 wit - -
email_spec0_product27_true-unreach-call.cil.c true 65   42   2900 wit - -
email_spec0_product36_true-unreach-call.cil.c true 11   3.4 450 wit - -
email_spec0_product37_true-unreach-call.cil.c true 47   26   1800 wit - -
email_spec0_product38_true-unreach-call.cil.c true 51   28   1700 wit - -
email_spec0_product40_true-unreach-call.cil.c true 52   32   1800 wit - -
email_spec11_product03_true-unreach-call.cil.c true 8.7 3.1 340 wit - -
email_spec11_product07_true-unreach-call.cil.c true 13   4.0 420 wit - -
email_spec11_product08_true-unreach-call.cil.c true 44   23   1700 wit - -
email_spec11_product10_true-unreach-call.cil.c true 10   3.6 350 wit - -
email_spec11_product18_true-unreach-call.cil.c true 54   31   1900 wit - -
email_spec11_product23_true-unreach-call.cil.c true 58   35   2600 wit - -
email_spec11_product24_true-unreach-call.cil.c true 57   35   2600 wit - -
email_spec11_product27_true-unreach-call.cil.c true 64   42   3000 wit - -
email_spec11_product36_true-unreach-call.cil.c true 11   3.3 430 wit - -
email_spec11_product37_true-unreach-call.cil.c true 49   27   1800 wit - -
email_spec11_product39_true-unreach-call.cil.c true 48   26   1700 wit - -
email_spec11_product40_true-unreach-call.cil.c true 54   32   1900 wit - -
email_spec1_product12_true-unreach-call.cil.c true 47   26   1600 wit - -
email_spec1_product28_true-unreach-call.cil.c true 53   32   1900 wit - -
email_spec27_product13_true-unreach-call.cil.c true 51   28   1800 wit - -
email_spec27_product28_true-unreach-call.cil.c true 51   33   2100 wit - -
email_spec4_product13_true-unreach-call.cil.c true 47   27   1700 wit - -
email_spec4_product17_true-unreach-call.cil.c true 53   33   2100 wit - -
email_spec4_product28_true-unreach-call.cil.c true 56   33   1900 wit - -
email_spec4_product29_true-unreach-call.cil.c true 60   38   2900 wit - -
email_spec7_product13_true-unreach-call.cil.c true 48   27   1700 wit - -
email_spec7_product17_true-unreach-call.cil.c true 52   31   1800 wit - -
email_spec7_product18_true-unreach-call.cil.c true 52   32   1900 wit - -
email_spec7_product19_true-unreach-call.cil.c true 51   32   2100 wit - -
email_spec7_product23_true-unreach-call.cil.c true 60   36   2900 wit - -
email_spec7_product24_true-unreach-call.cil.c true 56   37   2900 wit - -
email_spec7_product25_true-unreach-call.cil.c true 59   37   2900 wit - -
email_spec7_product27_true-unreach-call.cil.c true 62   43   2900 wit - -
email_spec8_product12_true-unreach-call.cil.c true 46   26   1700 wit - -
email_spec8_product14_true-unreach-call.cil.c true 52   31   1900 wit - -
email_spec8_product28_true-unreach-call.cil.c true 51   33   2100 wit - -
email_spec8_product29_true-unreach-call.cil.c true 59   38   2900 wit - -
email_spec9_product12_true-unreach-call.cil.c true 49   27   1800 wit - -
email_spec9_product14_true-unreach-call.cil.c true 50   31   1800 wit - -
email_spec9_product28_true-unreach-call.cil.c true 51   33   2100 wit - -
email_spec9_product29_true-unreach-call.cil.c true 59   38   2900 wit - -
minepump_spec1_product33_false-unreach-call.cil.c false(reach) 6.8 2.6 350 wit false(reach) 9.5 5.2 400 false(reach) 15 8.2 340
minepump_spec1_product34_false-unreach-call.cil.c false(reach) 7.2 2.6 350 wit false(reach) 9.8 5.4 400 false(reach) 14 7.5 360
minepump_spec1_product35_false-unreach-call.cil.c false(reach) 5.7 2.2 350 wit false(reach) 9.4 5.1 390 false(reach) 17 9.5 360
minepump_spec1_product36_false-unreach-call.cil.c false(reach) 5.8 2.1 360 wit false(reach) 8.4 4.6 400 false(reach) 16 9.8 340
minepump_spec1_product37_false-unreach-call.cil.c false(reach) 7.2 2.6 350 wit false(reach) 9.2 5.1 400 false(reach) 15 8.4 350
minepump_spec1_product38_false-unreach-call.cil.c false(reach) 6.8 2.6 350 wit false(reach) 8.5 4.7 410 false(reach) 19 11   370
minepump_spec1_product39_false-unreach-call.cil.c false(reach) 7.2 2.6 360 wit false(reach) 10   5.7 410 false(reach) 16 8.8 350
minepump_spec1_product40_false-unreach-call.cil.c false(reach) 7.2 2.6 360 wit false(reach) 10   5.7 410 false(reach) 17 9.1 360
minepump_spec1_product41_false-unreach-call.cil.c false(reach) 7.0 2.6 390 wit false(reach) 8.9 4.9 430 false(reach) 17 9.6 350
minepump_spec1_product42_false-unreach-call.cil.c false(reach) 8.7 2.9 400 wit false(reach) 11   6.0 430 false(reach) 18 9.9 420
minepump_spec1_product43_false-unreach-call.cil.c false(reach) 8.3 2.9 400 wit false(reach) 11   5.9 430 false(reach) 19 10   390
minepump_spec1_product44_false-unreach-call.cil.c false(reach) 8.8 3.0 400 wit false(reach) 11   6.2 450 false(reach) 20 11   380
minepump_spec1_product49_false-unreach-call.cil.c false(reach) 7.2 2.6 350 wit false(reach) 11   5.8 410 false(reach) 15 8.2 350
minepump_spec1_product50_false-unreach-call.cil.c false(reach) 7.3 2.6 360 wit false(reach) 10   5.7 410 false(reach) 17 9.8 370
minepump_spec1_product51_false-unreach-call.cil.c false(reach) 7.0 2.6 360 wit false(reach) 10   5.7 400 false(reach) 19 11   380
minepump_spec1_product52_false-unreach-call.cil.c false(reach) 7.1 2.6 360 wit false(reach) 10   5.6 410 false(reach) 20 11   380
minepump_spec1_product53_false-unreach-call.cil.c false(reach) 7.4 2.6 360 wit false(reach) 11   5.8 410 false(reach) 19 12   430
minepump_spec1_product54_false-unreach-call.cil.c false(reach) 6.1 2.2 350 wit false(reach) 10   5.6 410 false(reach) 16 9.0 340
minepump_spec1_product55_false-unreach-call.cil.c false(reach) 6.1 2.2 350 wit false(reach) 9.6 5.3 410 false(reach) 15 8.2 370
minepump_spec1_product56_false-unreach-call.cil.c false(reach) 7.3 2.6 350 wit false(reach) 10   5.6 410 false(reach) 20 11   390
minepump_spec1_productSimulator_false-unreach-call.cil.c false(reach) 9.9 3.2 410 wit false(reach) 11   5.8 430 true 17 9.3 370
minepump_spec2_product33_false-unreach-call.cil.c false(reach) 9.9 3.2 420 wit false(reach) 11   6.0 430 false(reach) 22 12   460
minepump_spec2_product34_false-unreach-call.cil.c false(reach) 9.1 3.1 420 wit false(reach) 11   5.9 420 false(reach) 17 10   370
minepump_spec2_product35_false-unreach-call.cil.c false(reach) 9.3 3.1 410 wit false(reach) 11   6.1 420 false(reach) 20 11   390
minepump_spec2_product36_false-unreach-call.cil.c false(reach) 9.4 3.2 420 wit false(reach) 11   6.4 420 false(reach) 20 11   390
minepump_spec2_product41_false-unreach-call.cil.c false(reach) 31   14   840 wit false(reach) 11   6.2 450 false(reach) 27 15   520
minepump_spec2_product42_false-unreach-call.cil.c false(reach) 34   16   830 wit false(reach) 12   6.3 450 false(reach) 20 11   390
minepump_spec2_product43_false-unreach-call.cil.c false(reach) 34   16   830 wit false(reach) 10   5.6 440 false(reach) 22 12   420
minepump_spec2_product44_false-unreach-call.cil.c false(reach) 38   17   840 wit false(reach) 11   6.1 450 false(reach) 21 13   430
minepump_spec2_productSimulator_false-unreach-call.cil.c false(reach) 67   43   1400 wit false(reach) 12   6.4 470 true 15 9.6 360
minepump_spec3_product01_false-unreach-call.cil.c false(reach) 6.7 2.5 340 wit false(reach) 9.6 5.2 400 false(reach) 16 11   360
minepump_spec3_product02_false-unreach-call.cil.c false(reach) 5.5 2.1 340 wit false(reach) 8.5 4.7 380 false(reach) 15 8.0 350
minepump_spec3_product03_false-unreach-call.cil.c false(reach) 5.5 2.1 340 wit false(reach) 8.7 4.8 380 false(reach) 16 11   360
minepump_spec3_product04_false-unreach-call.cil.c false(reach) 6.9 2.5 340 wit false(reach) 9.0 4.9 380 false(reach) 16 8.7 350
minepump_spec3_product05_false-unreach-call.cil.c false(reach) 7.4 2.6 350 wit false(reach) 7.8 4.3 370 false(reach) 17 9.6 350
minepump_spec3_product06_false-unreach-call.cil.c false(reach) 5.7 2.1 350 wit false(reach) 9.6 5.3 390 false(reach) 16 9.1 360
minepump_spec3_product07_false-unreach-call.cil.c false(reach) 6.5 2.4 340 wit false(reach) 8.8 4.8 390 false(reach) 18 9.6 380
minepump_spec3_product08_false-unreach-call.cil.c false(reach) 7.3 2.6 360 wit false(reach) 9.2 5.0 400 false(reach) 15 8.1 340
minepump_spec3_product09_false-unreach-call.cil.c false(reach) 6.9 2.5 340 wit false(reach) 9.2 5.1 380 false(reach) 15 9.4 340
minepump_spec3_product10_false-unreach-call.cil.c false(reach) 6.8 2.5 340 wit false(reach) 9.5 5.3 390 false(reach) 16 8.9 350
minepump_spec3_product11_false-unreach-call.cil.c false(reach) 6.5 2.4 330 wit false(reach) 9.0 5.0 380 false(reach) 16 9.0 360
minepump_spec3_product12_false-unreach-call.cil.c false(reach) 6.7 2.5 350 wit false(reach) 9.4 5.2 390 false(reach) 16 8.4 350
minepump_spec3_product13_false-unreach-call.cil.c false(reach) 6.6 2.5 350 wit false(reach) 8.7 4.8 380 false(reach) 14 8.0 340
minepump_spec3_product14_false-unreach-call.cil.c false(reach) 5.5 2.1 350 wit false(reach) 9.1 5.0 390 false(reach) 15 8.9 330
minepump_spec3_product15_false-unreach-call.cil.c false(reach) 6.4 2.5 340 wit false(reach) 9.6 5.3 400 false(reach) 15 7.9 350
minepump_spec3_product16_false-unreach-call.cil.c false(reach) 6.7 2.5 340 wit false(reach) 8.4 4.7 400 false(reach) 16 9.0 350
minepump_spec3_product17_false-unreach-call.cil.c false(reach) 5.7 2.1 340 wit false(reach) 9.2 5.0 410 false(reach) 15 8.3 340
minepump_spec3_product18_false-unreach-call.cil.c false(reach) 5.5 2.1 340 wit false(reach) 8.1 4.5 410 false(reach) 15 7.9 350
minepump_spec3_product19_false-unreach-call.cil.c false(reach) 6.7 2.5 340 wit false(reach) 9.9 5.4 410 false(reach) 16 10   350
minepump_spec3_product20_false-unreach-call.cil.c false(reach) 7.1 2.5 360 wit false(reach) 9.7 5.4 400 false(reach) 15 10   340
minepump_spec3_product21_false-unreach-call.cil.c false(reach) 7.1 2.5 340 wit false(reach) 9.6 5.3 400 false(reach) 16 8.6 350
minepump_spec3_product22_false-unreach-call.cil.c false(reach) 7.2 2.5 350 wit false(reach) 8.9 4.9 390 false(reach) 15 8.4 340
minepump_spec3_product23_false-unreach-call.cil.c false(reach) 5.8 2.1 350 wit false(reach) 8.1 4.5 410 false(reach) 20 11   410
minepump_spec3_product24_false-unreach-call.cil.c false(reach) 6.0 2.1 360 wit false(reach) 9.8 5.4 390 false(reach) 17 9.3 360
minepump_spec3_product25_false-unreach-call.cil.c false(reach) 6.9 2.5 350 wit false(reach) 9.9 5.3 390 false(reach) 16 9.4 360
minepump_spec3_product26_false-unreach-call.cil.c false(reach) 6.9 2.5 350 wit false(reach) 10   5.5 400 false(reach) 15 7.9 340
minepump_spec3_product27_false-unreach-call.cil.c false(reach) 6.6 2.5 340 wit false(reach) 9.7 5.3 390 false(reach) 17 9.2 350
minepump_spec3_product28_false-unreach-call.cil.c false(reach) 6.7 2.5 350 wit false(reach) 8.8 4.8 400 false(reach) 16 10   350
minepump_spec3_product29_false-unreach-call.cil.c false(reach) 6.0 2.1 350 wit false(reach) 9.8 5.4 400 false(reach) 16 9.2 350
minepump_spec3_product30_false-unreach-call.cil.c false(reach) 6.9 2.5 360 wit false(reach) 11   5.8 410 false(reach) 15 11   370
minepump_spec3_product31_false-unreach-call.cil.c false(reach) 6.6 2.5 350 wit false(reach) 9.7 5.2 400 false(reach) 16 9.1 350
minepump_spec3_product32_false-unreach-call.cil.c false(reach) 6.9 2.5 350 wit false(reach) 10   5.5 410 false(reach) 20 12   420
minepump_spec3_product35_false-unreach-call.cil.c false(reach) 6.8 2.6 350 wit false(reach) 9.6 5.2 380 false(reach) 16 8.9 360
minepump_spec3_product36_false-unreach-call.cil.c false(reach) 7.1 2.6 350 wit false(reach) 9.7 5.4 390 false(reach) 16 8.8 350
minepump_spec3_product39_false-unreach-call.cil.c false(reach) 6.8 2.5 340 wit false(reach) 8.8 4.9 410 false(reach) 18 11   390
minepump_spec3_product40_false-unreach-call.cil.c false(reach) 7.6 2.7 370 wit false(reach) 8.0 4.4 400 false(reach) 14 8.0 360
minepump_spec3_product43_false-unreach-call.cil.c false(reach) 6.3 2.3 340 wit false(reach) 8.5 4.6 400 false(reach) 17 9.4 370
minepump_spec3_product44_false-unreach-call.cil.c false(reach) 7.5 2.6 370 wit false(reach) 9.9 5.4 400 false(reach) 17 9.0 360
minepump_spec3_product47_false-unreach-call.cil.c false(reach) 7.2 2.6 360 wit false(reach) 9.2 5.0 420 false(reach) 19 10   380
minepump_spec3_product48_false-unreach-call.cil.c false(reach) 7.3 2.6 360 wit false(reach) 9.7 5.3 410 false(reach) 19 11   380
minepump_spec3_product51_false-unreach-call.cil.c false(reach) 7.1 2.6 350 wit false(reach) 10   5.6 410 false(reach) 16 10   340
minepump_spec3_product52_false-unreach-call.cil.c false(reach) 6.2 2.2 360 wit false(reach) 8.8 4.8 410 false(reach) 20 11   390
minepump_spec3_product55_false-unreach-call.cil.c false(reach) 7.5 2.7 370 wit false(reach) 10   5.5 400 false(reach) 16 9.2 360
minepump_spec3_product56_false-unreach-call.cil.c false(reach) 7.5 2.6 360 wit false(reach) 8.4 4.7 410 false(reach) 16 9.3 340
minepump_spec3_product59_false-unreach-call.cil.c false(reach) 7.6 2.7 360 wit false(reach) 10   5.7 400 false(reach) 17 9.0 380
minepump_spec3_product60_false-unreach-call.cil.c false(reach) 7.2 2.6 360 wit false(reach) 9.1 4.9 410 false(reach) 18 9.5 370
minepump_spec3_product63_false-unreach-call.cil.c false(reach) 7.5 2.6 360 wit false(reach) 9.1 5.0 400 false(reach) 18 10   360
minepump_spec3_product64_false-unreach-call.cil.c false(reach) 7.3 2.7 350 wit false(reach) 10   5.7 400 false(reach) 20 12   390
minepump_spec3_productSimulator_false-unreach-call.cil.c false(reach) 8.3 2.9 390 wit false(reach) 10   5.7 430 false(reach) 21 12   430
minepump_spec4_product33_false-unreach-call.cil.c false(reach) 18   6.3 630 wit false(reach) 12   6.4 440 false(reach) 19 11   390
minepump_spec4_product34_false-unreach-call.cil.c false(reach) 16   5.9 660 wit false(reach) 9.7 5.3 440 false(reach) 18 10   370
minepump_spec4_product35_false-unreach-call.cil.c false(reach) 20   6.9 660 wit false(reach) 11   6.1 430 false(reach) 22 12   420
minepump_spec4_product36_false-unreach-call.cil.c false(reach) 20   6.9 710 wit false(reach) 9.2 5.1 430 false(reach) 21 11   400
minepump_spec4_product37_false-unreach-call.cil.c false(reach) 15   3.8 560 wit false(reach) 11   5.7 460 false(reach) 20 12   390
minepump_spec4_product38_false-unreach-call.cil.c false(reach) 16   4.0 580 wit false(reach) 12   6.2 450 false(reach) 19 10   370
minepump_spec4_product39_false-unreach-call.cil.c false(reach) 21   8.5 780 wit false(reach) 12   6.4 430 false(reach) 22 12   430
minepump_spec4_product40_false-unreach-call.cil.c false(reach) 21   8.0 810 wit false(reach) 12   6.3 450 false(reach) 21 11   410
minepump_spec4_product41_false-unreach-call.cil.c false(reach) 22   7.4 730 wit false(reach) 12   6.4 430 false(reach) 20 12   380
minepump_spec4_product42_false-unreach-call.cil.c false(reach) 21   7.7 760 wit false(reach) 11   5.9 440 false(reach) 21 12   400
minepump_spec4_product43_false-unreach-call.cil.c false(reach) 12   3.7 450 wit false(reach) 9.7 5.3 430 false(reach) 21 11   400
minepump_spec4_product44_false-unreach-call.cil.c false(reach) 22   8.4 790 wit false(reach) 11   6.2 440 false(reach) 21 12   400
minepump_spec4_product45_false-unreach-call.cil.c false(reach) 17   4.1 590 wit false(reach) 11   6.1 460 false(reach) 19 11   380
minepump_spec4_product46_false-unreach-call.cil.c false(reach) 16   4.0 610 wit false(reach) 12   6.6 460 false(reach) 22 12   510
minepump_spec4_product47_false-unreach-call.cil.c false(reach) 22   8.9 790 wit false(reach) 11   6.2 450 false(reach) 22 12   430
minepump_spec4_product48_false-unreach-call.cil.c false(reach) 24   9.6 810 wit false(reach) 12   6.5 450 false(reach) 20 11   410
minepump_spec4_productSimulator_false-unreach-call.cil.c false(reach) 55   32   1400 wit false(reach) 12   6.8 470 true 15 10   360
minepump_spec1_product01_true-unreach-call.cil.c true 6.9 2.5 270 wit - -
minepump_spec1_product02_true-unreach-call.cil.c true 5.9 2.2 270 wit - -
minepump_spec1_product03_true-unreach-call.cil.c true 9.7 3.4 320 wit - -
minepump_spec1_product04_true-unreach-call.cil.c true 9.3 3.4 330 wit - -
minepump_spec1_product05_true-unreach-call.cil.c true 5.9 2.2 270 wit - -
minepump_spec1_product06_true-unreach-call.cil.c true 7.2 2.7 280 wit - -
minepump_spec1_product07_true-unreach-call.cil.c true 10   3.5 350 wit - -
minepump_spec1_product08_true-unreach-call.cil.c true 10   3.5 360 wit - -
minepump_spec1_product09_true-unreach-call.cil.c true 6.8 2.6 270 wit - -
minepump_spec1_product10_true-unreach-call.cil.c true 5.9 2.2 270 wit - -
minepump_spec1_product11_true-unreach-call.cil.c true 9.3 3.4 320 wit - -
minepump_spec1_product12_true-unreach-call.cil.c true 9.6 3.5 330 wit - -
minepump_spec1_product13_true-unreach-call.cil.c true 7.2 2.7 280 wit - -
minepump_spec1_product14_true-unreach-call.cil.c true 6.3 2.3 280 wit - -
minepump_spec1_product15_true-unreach-call.cil.c true 11   3.6 370 wit - -
minepump_spec1_product16_true-unreach-call.cil.c true 11   3.6 370 wit - -
minepump_spec1_product17_true-unreach-call.cil.c true 7.3 2.6 270 wit - -
minepump_spec1_product18_true-unreach-call.cil.c true 7.4 2.8 270 wit - -
minepump_spec1_product19_true-unreach-call.cil.c true 11   3.6 350 wit - -
minepump_spec1_product20_true-unreach-call.cil.c true 11   3.7 400 wit - -
minepump_spec1_product21_true-unreach-call.cil.c true 7.2 2.7 280 wit - -
minepump_spec1_product22_true-unreach-call.cil.c true 6.6 2.4 280 wit - -
minepump_spec1_product23_true-unreach-call.cil.c true 9.1 3.1 350 wit - -
minepump_spec1_product24_true-unreach-call.cil.c true 11   3.4 370 wit - -
minepump_spec1_product25_true-unreach-call.cil.c true 6.1 2.3 270 wit - -
minepump_spec1_product26_true-unreach-call.cil.c true 7.4 2.7 270 wit - -
minepump_spec1_product27_true-unreach-call.cil.c true 10   3.6 350 wit - -
minepump_spec1_product28_true-unreach-call.cil.c true 11   3.5 360 wit - -
minepump_spec1_product29_true-unreach-call.cil.c true 7.3 2.7 280 wit - -
minepump_spec1_product30_true-unreach-call.cil.c true 7.5 2.7 280 wit - -
minepump_spec1_product31_true-unreach-call.cil.c true 11   3.7 370 wit - -
minepump_spec1_product32_true-unreach-call.cil.c true 10   3.6 350 wit - -
minepump_spec1_product45_true-unreach-call.cil.c true 14   4.0 490 wit - -
minepump_spec1_product46_true-unreach-call.cil.c true 12   3.5 480 wit - -
minepump_spec1_product47_true-unreach-call.cil.c true 15   5.4 460 wit - -
minepump_spec1_product48_true-unreach-call.cil.c true 14   4.0 480 wit - -
minepump_spec1_product57_true-unreach-call.cil.c true 14   4.0 520 wit - -
minepump_spec1_product58_true-unreach-call.cil.c true 13   3.8 440 wit - -
minepump_spec1_product59_true-unreach-call.cil.c true 23   10   720 wit - -
minepump_spec1_product60_true-unreach-call.cil.c true 13   3.5 480 wit - -
minepump_spec1_product61_true-unreach-call.cil.c true 15   3.7 500 wit - -
minepump_spec1_product62_true-unreach-call.cil.c true 14   4.1 460 wit - -
minepump_spec1_product63_true-unreach-call.cil.c true 13   5.2 540 wit - -
minepump_spec1_product64_true-unreach-call.cil.c true 14   3.8 510 wit - -
minepump_spec2_product01_true-unreach-call.cil.c true 6.9 2.6 270 wit - -
minepump_spec2_product02_true-unreach-call.cil.c true 6.3 2.3 280 wit - -
minepump_spec2_product03_true-unreach-call.cil.c true 15   4.9 480 wit - -
minepump_spec2_product04_true-unreach-call.cil.c true 13   4.7 410 wit - -
minepump_spec2_product05_true-unreach-call.cil.c true 6.2 2.3 270 wit - -
minepump_spec2_product06_true-unreach-call.cil.c true 7.2 2.7 280 wit - -
minepump_spec2_product07_true-unreach-call.cil.c true 14   5.0 460 wit - -
minepump_spec2_product08_true-unreach-call.cil.c true 15   4.9 460 wit - -
minepump_spec2_product09_true-unreach-call.cil.c true 5.8 2.2 270 wit - -
minepump_spec2_product10_true-unreach-call.cil.c true 7.0 2.6 270 wit - -
minepump_spec2_product11_true-unreach-call.cil.c true 17   5.0 490 wit - -
minepump_spec2_product12_true-unreach-call.cil.c true 15   4.9 450 wit - -
minepump_spec2_product13_true-unreach-call.cil.c true 7.3 2.7 270 wit - -
minepump_spec2_product14_true-unreach-call.cil.c true 7.6 2.8 280 wit - -
minepump_spec2_product15_true-unreach-call.cil.c true 13   4.5 490 wit - -
minepump_spec2_product16_true-unreach-call.cil.c true 15   5.1 520 wit - -
minepump_spec2_product17_true-unreach-call.cil.c true 6.1 2.3 270 wit - -
minepump_spec2_product18_true-unreach-call.cil.c true 7.5 2.7 280 wit - -
minepump_spec2_product19_true-unreach-call.cil.c true 12   4.3 450 wit - -
minepump_spec2_product20_true-unreach-call.cil.c true 14   5.1 450 wit - -
minepump_spec2_product21_true-unreach-call.cil.c true 7.2 2.5 280 wit - -
minepump_spec2_product22_true-unreach-call.cil.c true 7.4 2.7 280 wit - -
minepump_spec2_product23_true-unreach-call.cil.c true 13   5.0 520 wit - -
minepump_spec2_product24_true-unreach-call.cil.c true 15   5.7 540 wit - -
minepump_spec2_product25_true-unreach-call.cil.c true 6.1 2.3 270 wit - -
minepump_spec2_product26_true-unreach-call.cil.c true 6.3 2.3 280 wit - -
minepump_spec2_product27_true-unreach-call.cil.c true 14   5.0 450 wit - -
minepump_spec2_product28_true-unreach-call.cil.c true 12   4.3 460 wit - -
minepump_spec2_product29_true-unreach-call.cil.c true 7.4 2.7 280 wit - -
minepump_spec2_product30_true-unreach-call.cil.c true 7.5 2.8 290 wit - -
minepump_spec2_product31_true-unreach-call.cil.c true 17   5.7 590 wit - -
minepump_spec2_product32_true-unreach-call.cil.c true 16   5.6 580 wit - -
minepump_spec2_product37_true-unreach-call.cil.c true 17   4.4 520 wit - -
minepump_spec2_product38_true-unreach-call.cil.c true 18   4.5 560 wit - -
minepump_spec2_product39_true-unreach-call.cil.c true 19   7.9 720 wit - -
minepump_spec2_product40_true-unreach-call.cil.c true 16   4.2 510 wit - -
minepump_spec2_product45_true-unreach-call.cil.c true 16   4.4 520 wit - -
minepump_spec2_product46_true-unreach-call.cil.c true 21   4.8 580 wit - -
minepump_spec2_product47_true-unreach-call.cil.c true 21   8.9 730 wit - -
minepump_spec2_product48_true-unreach-call.cil.c true 15   4.1 550 wit - -
minepump_spec2_product49_true-unreach-call.cil.c true 17   4.4 540 wit - -
minepump_spec2_product50_true-unreach-call.cil.c true 18   4.4 530 wit - -
minepump_spec2_product51_true-unreach-call.cil.c true 35   18   800 wit - -
minepump_spec2_product52_true-unreach-call.cil.c true 18   4.6 560 wit - -
minepump_spec2_product53_true-unreach-call.cil.c true 17   4.5 550 wit - -
minepump_spec2_product54_true-unreach-call.cil.c true 18   4.7 570 wit - -
minepump_spec2_product55_true-unreach-call.cil.c true 15   4.1 560 wit - -
minepump_spec2_product56_true-unreach-call.cil.c true 19   4.7 590 wit - -
minepump_spec2_product57_true-unreach-call.cil.c true 15   4.3 520 wit - -
minepump_spec2_product58_true-unreach-call.cil.c true 15   4.3 530 wit - -
minepump_spec2_product59_true-unreach-call.cil.c true 39   19   800 wit - -
minepump_spec2_product60_true-unreach-call.cil.c true 15   4.4 540 wit - -
minepump_spec2_product61_true-unreach-call.cil.c true 18   4.8 560 wit - -
minepump_spec2_product62_true-unreach-call.cil.c true 14   4.1 580 wit - -
minepump_spec2_product63_true-unreach-call.cil.c true 23   11   790 wit - -
minepump_spec2_product64_true-unreach-call.cil.c true 18   4.5 600 wit - -
minepump_spec3_product33_true-unreach-call.cil.c true 14   4.8 430 wit - -
minepump_spec3_product34_true-unreach-call.cil.c true 14   4.9 420 wit - -
minepump_spec3_product37_true-unreach-call.cil.c true 12   3.5 410 wit - -
minepump_spec3_product38_true-unreach-call.cil.c true 11   3.5 410 wit - -
minepump_spec3_product41_true-unreach-call.cil.c true 12   5.1 490 wit - -
minepump_spec3_product42_true-unreach-call.cil.c true 16   5.7 510 wit - -
minepump_spec3_product45_true-unreach-call.cil.c true 13   3.9 450 wit - -
minepump_spec3_product46_true-unreach-call.cil.c true 13   3.6 460 wit - -
minepump_spec3_product49_true-unreach-call.cil.c true 10   3.1 430 wit - -
minepump_spec3_product50_true-unreach-call.cil.c true 11   3.3 430 wit - -
minepump_spec3_product53_true-unreach-call.cil.c true 13   3.7 410 wit - -
minepump_spec3_product54_true-unreach-call.cil.c true 13   3.5 450 wit - -
minepump_spec3_product57_true-unreach-call.cil.c true 13   3.8 420 wit - -
minepump_spec3_product58_true-unreach-call.cil.c true 13   3.9 460 wit - -
minepump_spec3_product61_true-unreach-call.cil.c true 13   4.0 440 wit - -
minepump_spec3_product62_true-unreach-call.cil.c true 12   3.5 460 wit - -
minepump_spec4_product01_true-unreach-call.cil.c true 5.6 2.2 260 wit - -
minepump_spec4_product02_true-unreach-call.cil.c true 6.8 2.5 270 wit - -
minepump_spec4_product03_true-unreach-call.cil.c true 9.5 3.4 330 wit - -
minepump_spec4_product04_true-unreach-call.cil.c true 7.8 2.8 280 wit - -
minepump_spec4_product05_true-unreach-call.cil.c true 6.0 2.2 270 wit - -
minepump_spec4_product06_true-unreach-call.cil.c true 5.9 2.2 270 wit - -
minepump_spec4_product07_true-unreach-call.cil.c true 10   3.5 360 wit - -
minepump_spec4_product08_true-unreach-call.cil.c true 8.4 2.9 360 wit - -
minepump_spec4_product09_true-unreach-call.cil.c true 6.7 2.5 260 wit - -
minepump_spec4_product10_true-unreach-call.cil.c true 5.7 2.1 260 wit - -
minepump_spec4_product11_true-unreach-call.cil.c true 9.4 3.4 320 wit - -
minepump_spec4_product12_true-unreach-call.cil.c true 7.4 2.7 280 wit - -
minepump_spec4_product13_true-unreach-call.cil.c true 5.7 2.2 270 wit - -
minepump_spec4_product14_true-unreach-call.cil.c true 7.1 2.6 270 wit - -
minepump_spec4_product15_true-unreach-call.cil.c true 11   3.6 360 wit - -
minepump_spec4_product16_true-unreach-call.cil.c true 10   3.5 350 wit - -
minepump_spec4_product17_true-unreach-call.cil.c true 7.2 2.6 270 wit - -
minepump_spec4_product18_true-unreach-call.cil.c true 7.0 2.6 280 wit - -
minepump_spec4_product19_true-unreach-call.cil.c true 9.3 3.1 370 wit - -
minepump_spec4_product20_true-unreach-call.cil.c true 11   3.5 370 wit - -
minepump_spec4_product21_true-unreach-call.cil.c true 6.1 2.2 270 wit - -
minepump_spec4_product22_true-unreach-call.cil.c true 6.2 2.3 280 wit - -
minepump_spec4_product23_true-unreach-call.cil.c true 12   3.7 380 wit - -
minepump_spec4_product24_true-unreach-call.cil.c true 12   3.7 390 wit - -
minepump_spec4_product25_true-unreach-call.cil.c true 6.9 2.6 270 wit - -
minepump_spec4_product26_true-unreach-call.cil.c true 7.1 2.6 270 wit - -
minepump_spec4_product27_true-unreach-call.cil.c true 10   3.5 350 wit - -
minepump_spec4_product28_true-unreach-call.cil.c true 10   3.6 350 wit - -
minepump_spec4_product29_true-unreach-call.cil.c true 7.2 2.6 270 wit - -
minepump_spec4_product30_true-unreach-call.cil.c true 7.4 2.7 280 wit - -
minepump_spec4_product31_true-unreach-call.cil.c true 12   3.7 380 wit - -
minepump_spec4_product32_true-unreach-call.cil.c true 9.4 3.1 370 wit - -
minepump_spec4_product49_true-unreach-call.cil.c true 12   3.6 440 wit - -
minepump_spec4_product50_true-unreach-call.cil.c true 12   3.6 460 wit - -
minepump_spec4_product51_true-unreach-call.cil.c true 15   6.3 640 wit - -
minepump_spec4_product52_true-unreach-call.cil.c true 16   6.9 670 wit - -
minepump_spec4_product53_true-unreach-call.cil.c true 13   3.9 470 wit - -
minepump_spec4_product54_true-unreach-call.cil.c true 12   3.3 470 wit - -
minepump_spec4_product55_true-unreach-call.cil.c true 16   6.3 650 wit - -
minepump_spec4_product56_true-unreach-call.cil.c true 13   3.7 440 wit - -
minepump_spec4_product57_true-unreach-call.cil.c true 11   3.3 470 wit - -
minepump_spec4_product58_true-unreach-call.cil.c true 13   3.8 500 wit - -
minepump_spec4_product59_true-unreach-call.cil.c true 17   8.0 720 wit - -
minepump_spec4_product60_true-unreach-call.cil.c true 21   9.4 700 wit - -
minepump_spec4_product61_true-unreach-call.cil.c true 14   4.0 450 wit - -
minepump_spec4_product62_true-unreach-call.cil.c true 11   3.3 410 wit - -
minepump_spec4_product63_true-unreach-call.cil.c true 18   7.2 670 wit - -
minepump_spec4_product64_true-unreach-call.cil.c true 14   4.0 460 wit - -
minepump_spec5_product01_true-unreach-call.cil.c true 7.0 2.5 280 wit - -
minepump_spec5_product02_true-unreach-call.cil.c true 6.4 2.3 280 wit - -
minepump_spec5_product03_true-unreach-call.cil.c true 9.1 3.3 320 wit - -
minepump_spec5_product04_true-unreach-call.cil.c true 9.1 3.2 310 wit - -
minepump_spec5_product05_true-unreach-call.cil.c true 7.4 2.7 290 wit - -
minepump_spec5_product06_true-unreach-call.cil.c true 7.7 2.8 280 wit - -
minepump_spec5_product07_true-unreach-call.cil.c true 9.3 3.3 320 wit - -
minepump_spec5_product08_true-unreach-call.cil.c true 7.7 2.8 330 wit - -
minepump_spec5_product09_true-unreach-call.cil.c true 7.3 2.7 280 wit - -
minepump_spec5_product10_true-unreach-call.cil.c true 7.5 2.7 280 wit - -
minepump_spec5_product11_true-unreach-call.cil.c true 9.1 3.3 320 wit - -
minepump_spec5_product12_true-unreach-call.cil.c true 9.1 3.3 310 wit - -
minepump_spec5_product13_true-unreach-call.cil.c true 7.6 2.8 280 wit - -
minepump_spec5_product14_true-unreach-call.cil.c true 7.5 2.6 290 wit - -
minepump_spec5_product15_true-unreach-call.cil.c true 9.0 3.1 320 wit - -
minepump_spec5_product16_true-unreach-call.cil.c true 9.1 3.3 310 wit - -
minepump_spec5_product17_true-unreach-call.cil.c true 7.4 2.7 290 wit - -
minepump_spec5_product18_true-unreach-call.cil.c true 7.8 2.8 290 wit - -
minepump_spec5_product19_true-unreach-call.cil.c true 9.3 3.3 320 wit - -
minepump_spec5_product20_true-unreach-call.cil.c true 7.9 2.9 330 wit - -
minepump_spec5_product21_true-unreach-call.cil.c true 9.4 3.3 330 wit - -
minepump_spec5_product22_true-unreach-call.cil.c true 7.9 2.8 330 wit - -
minepump_spec5_product23_true-unreach-call.cil.c true 9.4 3.3 330 wit - -
minepump_spec5_product24_true-unreach-call.cil.c true 9.2 3.3 320 wit - -
minepump_spec5_product25_true-unreach-call.cil.c true 6.0 2.1 280 wit - -
minepump_spec5_product26_true-unreach-call.cil.c true 6.4 2.4 290 wit - -
minepump_spec5_product27_true-unreach-call.cil.c true 9.1 3.3 320 wit - -
minepump_spec5_product28_true-unreach-call.cil.c true 7.7 2.7 330 wit - -
minepump_spec5_product29_true-unreach-call.cil.c true 9.5 3.3 320 wit - -
minepump_spec5_product30_true-unreach-call.cil.c true 7.7 2.8 320 wit - -
minepump_spec5_product31_true-unreach-call.cil.c true 8.0 2.9 330 wit - -
minepump_spec5_product32_true-unreach-call.cil.c true 9.4 3.4 320 wit - -
minepump_spec5_product33_true-unreach-call.cil.c true 11   3.5 430 wit - -
minepump_spec5_product34_true-unreach-call.cil.c true 9.8 2.9 390 wit - -
minepump_spec5_product35_true-unreach-call.cil.c true 18   6.7 670 wit - -
minepump_spec5_product36_true-unreach-call.cil.c true 20   9.1 700 wit - -
minepump_spec5_product37_true-unreach-call.cil.c true 13   3.4 460 wit - -
minepump_spec5_product38_true-unreach-call.cil.c true 16   4.1 510 wit - -
minepump_spec5_product39_true-unreach-call.cil.c true 18   8.1 670 wit - -
minepump_spec5_product40_true-unreach-call.cil.c true 18   7.2 700 wit - -
minepump_spec5_product41_true-unreach-call.cil.c true 12   3.5 400 wit - -
minepump_spec5_product42_true-unreach-call.cil.c true 12   3.5 450 wit - -
minepump_spec5_product43_true-unreach-call.cil.c true 18   7.5 680 wit - -
minepump_spec5_product44_true-unreach-call.cil.c true 13   3.8 430 wit - -
minepump_spec5_product45_true-unreach-call.cil.c true 16   4.1 490 wit - -
minepump_spec5_product46_true-unreach-call.cil.c true 15   4.0 460 wit - -
minepump_spec5_product47_true-unreach-call.cil.c true 14   4.0 500 wit - -
minepump_spec5_product48_true-unreach-call.cil.c true 14   4.0 470 wit - -
minepump_spec5_product49_true-unreach-call.cil.c true 14   3.5 460 wit - -
minepump_spec5_product50_true-unreach-call.cil.c true 15   3.8 460 wit - -
minepump_spec5_product51_true-unreach-call.cil.c true 18   7.1 640 wit - -
minepump_spec5_product52_true-unreach-call.cil.c true 21   8.7 690 wit - -
minepump_spec5_product53_true-unreach-call.cil.c true 15   4.3 500 wit - -
minepump_spec5_product54_true-unreach-call.cil.c true 14   4.2 500 wit - -
minepump_spec5_product55_true-unreach-call.cil.c true 15   4.1 510 wit - -
minepump_spec5_product56_true-unreach-call.cil.c true 11   3.5 440 wit - -
minepump_spec5_product57_true-unreach-call.cil.c true 14   3.6 470 wit - -
minepump_spec5_product58_true-unreach-call.cil.c true 17   4.3 510 wit - -
minepump_spec5_product59_true-unreach-call.cil.c true 14   3.8 500 wit - -
minepump_spec5_product60_true-unreach-call.cil.c true 15   4.2 510 wit - -
minepump_spec5_product61_true-unreach-call.cil.c true 15   4.3 490 wit - -
minepump_spec5_product62_true-unreach-call.cil.c true 14   4.2 500 wit - -
minepump_spec5_product63_true-unreach-call.cil.c true 14   3.7 530 wit - -
minepump_spec5_product64_true-unreach-call.cil.c true 14   4.1 470 wit - -
minepump_spec5_productSimulator_true-unreach-call.cil.c true 59   40   810 wit - -
../../sv-benchmarks/c/product-lines/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 597 11000 4500 420000 597 4900   2600   170000   597 7400   4100   140000  
    correct results 597 11000 4500 420000 265 4900   2600   170000   265 7400   4100   140000  
        correct true 332 5400 2400 200000 0 0   0   0   69 0   0   0  
        correct false 265 6000 2100 210000 265 4900   2600   170000   196 7400   4100   140000  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (597 tasks, max score: 929) 929
Run set sv-comp16.ProductLines