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