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