Tool CBMC 5.6
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-57-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 17:21:21 CET [[ 2017-01-14 18:00:17 CET ]] [[ 2017-01-14 19:57:11 CET ]] [[ 2017-01-14 18:18:10 CET ]] [[ 2017-01-14 20:00:30 CET ]]
Run set sv-comp17.ReachSafety-ProductLines
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cbmc.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cbmc.2017-01-10_1721.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 1 .24 .23 2.3 27 .0041 0      12    6.1  210 470 13   6.9 220 500
elevator_spec14_product24_false-unreach-call_true-termination.cil.c 1 .21 .21 2.4 27 .0041 0      14    7.4  230 550 15   7.8 240 510
elevator_spec14_product28_false-unreach-call_true-termination.cil.c 1 .22 .21 2.3 27 .0041 0      12    6.3  210 480 16   8.4 150 500
elevator_spec14_product32_false-unreach-call_true-termination.cil.c 1 .21 .20 1.9 27 .0041 0      12    6.2  180 490 14   7.6 180 500
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c 1 8.8  8.8  110   440 .0041 0      12    6.2  86 490 13   7.3 180 430
elevator_spec1_product18_false-unreach-call_true-termination.cil.c 1 .59 .57 5.3 27 .20   .17   12    6.5  260 570 11   6.1 220 420
elevator_spec1_product20_false-unreach-call_true-termination.cil.c 1 .59 .58 6.1 27 .22   0      13    6.8  160 510 11   6.2 190 420
elevator_spec1_product22_false-unreach-call_true-termination.cil.c 1 .60 .58 5.6 27 .21   0      13    6.9  170 530 11   6.2 220 420
elevator_spec1_product24_false-unreach-call_true-termination.cil.c 1 .61 .60 5.6 28 .24   0      13    7.0  250 540 14   7.6 150 440
elevator_spec1_product26_false-unreach-call_true-termination.cil.c 1 .52 .51 6.3 27 .20   0      12    6.2  160 520 14   7.8 140 420
elevator_spec1_product28_false-unreach-call_true-termination.cil.c 1 .62 .60 5.0 27 .22   0      13    6.7  250 490 14   7.4 160 430
elevator_spec1_product30_false-unreach-call_true-termination.cil.c 1 .59 .58 5.7 27 .21   0      13    6.8  250 530 12   6.5 200 430
elevator_spec1_product32_false-unreach-call_true-termination.cil.c 1 .56 .55 7.7 28 .24   .0041 13    6.7  270 510 12   6.7 170 440
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c 1 76    76    580   1200 .26   0      14    7.3  290 590 16   8.4 180 470
elevator_spec2_product18_false-unreach-call_true-termination.cil.c 1 .55 .54 5.5 27 .19   0      12    6.5  270 530 11   6.1 170 390
elevator_spec2_product20_false-unreach-call_true-termination.cil.c 1 .54 .53 6.8 27 .21   .0041 13    7.0  260 520 11   6.2 260 410
elevator_spec2_product22_false-unreach-call_true-termination.cil.c 1 .58 .56 5.3 27 .20   0      13    6.9  270 530 11   6.0 190 400
elevator_spec2_product24_false-unreach-call_true-termination.cil.c 1 .57 .56 7.4 28 .23   0      13    6.7  140 540 13   7.2 140 420
elevator_spec2_product26_false-unreach-call_true-termination.cil.c 1 .53 .52 6.5 27 .19   0      13    6.7  230 480 11   6.1 230 410
elevator_spec2_product28_false-unreach-call_true-termination.cil.c 1 .62 .60 5.2 27 .21   0      12    6.6  240 520 15   8.0 160 410
elevator_spec2_product30_false-unreach-call_true-termination.cil.c 1 .58 .57 6.1 27 .20   0      12    6.4  240 500 10   5.7 200 400
elevator_spec2_product32_false-unreach-call_true-termination.cil.c 1 .66 .64 5.4 28 .23   0      13    6.9  270 500 12   6.6 200 430
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c 1 40    40    420   910 .25   0      14    7.2  180 600 12   6.4 250 440
elevator_spec3_product03_false-unreach-call_true-termination.cil.c 1 .28 .27 3.0 28 .0041 0      15    7.6  270 580 15   7.9 230 510
elevator_spec3_product11_false-unreach-call_true-termination.cil.c 1 .31 .30 2.8 28 .0041 0      15    7.7  130 590 16   8.6 210 490
elevator_spec3_product19_false-unreach-call_true-termination.cil.c 1 .28 .27 2.4 28 .0041 0      15    7.8  290 620 17   8.9 170 510
elevator_spec3_product20_false-unreach-call_true-termination.cil.c 1 .31 .30 2.6 28 .0041 0      16    8.2  130 590 15   7.9 150 500
elevator_spec3_product23_false-unreach-call_true-termination.cil.c 1 .27 .27 3.3 29 .0041 0      17    8.7  180 620 17   9.1 210 510
elevator_spec3_product24_false-unreach-call_true-termination.cil.c 1 .27 .27 2.9 29 .0041 0      15    7.9  290 670 17   9.1 170 500
elevator_spec3_product27_false-unreach-call_true-termination.cil.c 1 .28 .27 2.7 28 .0041 0      14    7.4  220 630 17   9.1 170 490
elevator_spec3_product28_false-unreach-call_true-termination.cil.c 1 .27 .26 2.9 29 .0041 0      15    7.9  310 670 14   7.4 260 520
elevator_spec3_product31_false-unreach-call_true-termination.cil.c 1 .28 .28 3.1 29 .0041 0      17    9.1  260 690 17   8.9 240 520
elevator_spec3_product32_false-unreach-call_true-termination.cil.c 1 .30 .29 2.7 29 .0041 0      14    7.5  180 690 14   7.7 300 510
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c 1 37    37    360   920 .0041 0      17    8.9  280 700 65   37   730 1700
elevator_spec9_product26_false-unreach-call_true-termination.cil.c 1 .56 .55 5.0 27 .20   0      12    6.5  200 520 11   5.8 240 400
elevator_spec9_product28_false-unreach-call_true-termination.cil.c 1 .58 .57 5.5 27 .22   0      12    6.4  150 480 13   6.9 140 410
elevator_spec9_product30_false-unreach-call_true-termination.cil.c 1 .60 .58 6.2 27 .22   0      13    6.8  250 530 11   6.0 210 400
elevator_spec9_product32_false-unreach-call_true-termination.cil.c 1 .57 .56 6.4 28 .24   0      13    6.8  170 520 11   6.0 200 410
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c 1 40    40    340   910 .26   0      14    7.5  280 610 14   7.4 150 440
elevator_spec13_product21_true-unreach-call_false-termination.cil.c 0 850    850    9800   13000 41      0      .62 .38 7.4 39 7.5 3.9 89 300
elevator_spec13_product22_true-unreach-call_false-termination.cil.c 0 850    850    11000   13000 42      0      .54 .34 9.2 40 7.6 4.0 130 310
elevator_spec13_product23_true-unreach-call_false-termination.cil.c 0 610    610    7700   15000 24      .012  .60 .39 9.1 40 7.9 4.1 93 300
elevator_spec13_product24_true-unreach-call_false-termination.cil.c 0 610    610    8800   15000 24      0      .52 .33 12   40 6.4 3.5 140 310
elevator_spec13_product29_true-unreach-call_false-termination.cil.c 0 850    850    11000   13000 41      10      .50 .33 13   40 6.7 3.5 89 290
elevator_spec13_product30_true-unreach-call_false-termination.cil.c 0 850    850    12000   13000 41      0      .63 .41 6.2 39 6.2 3.2 110 300
elevator_spec13_product31_true-unreach-call_false-termination.cil.c 0 620    610    8100   15000 24      .0041 .48 .31 9.7 39 7.2 3.8 100 300
elevator_spec13_product32_true-unreach-call_false-termination.cil.c 0 630    630    7800   15000 24      .0041 .69 .43 8.7 42 6.5 3.4 130 300
elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c 0 850    850    7400   450 .012  0      .57 .37 7.8 42 8.9 4.7 91 320
elevator_spec14_product03_true-unreach-call_true-termination.cil.c 1 1.5  1.5  18   31 .82   0      8.8  4.6  130   320 280   190   5300 7000
elevator_spec14_product11_true-unreach-call_true-termination.cil.c 1 1.5  1.5  16   31 .83   0      9.6  5.0  190   350 320   230   5600 7000
elevator_spec14_product19_true-unreach-call_true-termination.cil.c 1 1.6  1.6  16   31 .84   .0041 10    5.3  190   370 380   260   6900 7000
elevator_spec14_product23_true-unreach-call_true-termination.cil.c 1 1.6  1.5  16   31 1.0    0      9.7  5.1  200   410 440   320   5500 7000
elevator_spec14_product27_true-unreach-call_true-termination.cil.c 1 1.6  1.6  15   32 .84   0      11    5.8  120   340 250   170   4800 7000
elevator_spec14_product31_true-unreach-call_true-termination.cil.c 1 1.6  1.5  18   32 1.0    0      8.5  4.4  100   390 210   140   2900 7000
elevator_spec1_product01_true-unreach-call_true-termination.cil.c 1 1.3  1.3  15   32 .63   0      10    5.4  92   330 200   130   2600 7000
elevator_spec1_product03_true-unreach-call_true-termination.cil.c 1 1.4  1.4  19   30 .73   0      8.8  4.6  140   340 210   140   1900 7000
elevator_spec1_product09_true-unreach-call_true-termination.cil.c 1 1.4  1.3  12   29 .64   0      8.3  4.3  110   340 210   140   4400 7000
elevator_spec1_product11_true-unreach-call_true-termination.cil.c 1 1.5  1.4  14   30 .74   0      8.3  4.4  140   290 260   170   4300 7000
elevator_spec1_product17_true-unreach-call_true-termination.cil.c 1 1.4  1.3  14   29 .65   0      9.5  5.0  99   290 250   170   2400 7000
elevator_spec1_product19_true-unreach-call_true-termination.cil.c 1 1.5  1.5  18   30 .75   0      8.4  4.4  130   320 230   150   3200 7000
elevator_spec1_product21_true-unreach-call_true-termination.cil.c 1 1.4  1.4  13   30 .72   0      8.2  4.4  160   330 200   130   3200 7000
elevator_spec1_product23_true-unreach-call_true-termination.cil.c 1 1.6  1.6  16   31 .82   0      10    5.3  140   330 200   130   2600 7000
elevator_spec1_product25_true-unreach-call_true-termination.cil.c 1 1.3  1.3  15   30 .66   0      10    5.3  93   300 200   140   3700 7000
elevator_spec1_product27_true-unreach-call_true-termination.cil.c 1 1.5  1.4  15   30 .76   0      9.1  4.8  120   280 270   180   3500 7000
elevator_spec1_product29_true-unreach-call_true-termination.cil.c 1 1.4  1.4  15   30 .73   0      10    5.4  130   340 150   98   1600 7000
elevator_spec1_product31_true-unreach-call_true-termination.cil.c 1 1.5  1.5  19   32 .84   .16   8.6  4.5  140   300 210   140   4600 7000
elevator_spec2_product01_true-unreach-call_true-termination.cil.c 1 .83 .81 7.3 27 .22   0      7.6  4.0  60   310 180   120   3300 7000
elevator_spec2_product03_true-unreach-call_true-termination.cil.c 1 .86 .84 8.3 28 .25   0      8.2  4.3  150   310 240   150   3200 7000
elevator_spec2_product09_true-unreach-call_true-termination.cil.c 1 .77 .75 8.2 27 .23   0      8.5  4.5  100   350 180   110   2700 7000
elevator_spec2_product11_true-unreach-call_true-termination.cil.c 1 .76 .75 9.1 28 .26   0      9.0  4.7  130   290 210   140   3800 7000
elevator_spec2_product17_true-unreach-call_true-termination.cil.c 1 .74 .73 9.8 27 .23   0      9.4  4.9  110   330 170   110   1300 7000
elevator_spec2_product19_true-unreach-call_true-termination.cil.c 1 .85 .83 8.3 28 .26   0      8.3  4.4  180   340 220   140   2300 7000
elevator_spec2_product21_true-unreach-call_true-termination.cil.c 1 .83 .81 7.7 28 .24   0      10    5.2  140   310 150   94   1700 7000
elevator_spec2_product23_true-unreach-call_true-termination.cil.c 1 .83 .82 11   28 .27   0      10    5.3  140   350 240   160   2600 7000
elevator_spec2_product25_true-unreach-call_true-termination.cil.c 1 .82 .80 7.7 27 .23   0      7.7  4.0  120   300 150   94   1900 7000
elevator_spec2_product27_true-unreach-call_true-termination.cil.c 1 .88 .86 8.3 28 .27   0      9.6  5.0  140   330 200   120   2900 7000
elevator_spec2_product29_true-unreach-call_true-termination.cil.c 1 .81 .80 6.9 28 .24   0      8.2  4.3  90   300 140   88   2400 7000
elevator_spec2_product31_true-unreach-call_true-termination.cil.c 1 .88 .87 7.9 28 .27   0      9.8  5.1  150   330 210   140   2300 7000
elevator_spec3_product01_true-unreach-call_true-termination.cil.c 1 1.6  1.6  18   32 .90   0      11    5.9  110   320 160   99   2500 7000
elevator_spec3_product09_true-unreach-call_true-termination.cil.c 1 1.6  1.6  18   32 .91   0      10    5.3  95   320 180   110   2400 7000
elevator_spec3_product17_true-unreach-call_true-termination.cil.c 1 1.7  1.7  18   32 .91   0      12    6.1  130   360 190   120   2600 7000
elevator_spec3_product18_true-unreach-call_true-termination.cil.c 1 1.7  1.7  22   32 .95   0      9.0  4.8  130   410 170   110   3400 7000
elevator_spec3_product21_true-unreach-call_true-termination.cil.c 1 1.9  1.8  23   34 1.0    0      12    6.0  120   400 200   120   3400 7000
elevator_spec3_product22_true-unreach-call_true-termination.cil.c 1 1.9  1.9  20   34 1.1    0      11    5.8  160   440 180   120   3700 7000
elevator_spec3_product25_true-unreach-call_true-termination.cil.c 1 1.7  1.7  20   32 .92   0      10    5.2  110   360 170   110   3700 7000
elevator_spec3_product26_true-unreach-call_true-termination.cil.c 1 1.6  1.6  20   32 .95   0      9.5  5.1  160   460 190   130   2600 7000
elevator_spec3_product29_true-unreach-call_true-termination.cil.c 1 1.8  1.8  21   33 1.1    .0041 9.6  5.0  190   400 200   130   1900 7000
elevator_spec3_product30_true-unreach-call_true-termination.cil.c 1 1.8  1.8  24   33 1.1    0      12    6.4  130   330 190   120   3000 7000
elevator_spec9_product09_true-unreach-call_true-termination.cil.c 1 .76 .75 7.5 27 .24   0      12    6.0  99   320 160   99   1300 7000
elevator_spec9_product11_true-unreach-call_true-termination.cil.c 1 .80 .79 8.6 28 .27   0      12    6.1  100   330 180   110   2400 7000
elevator_spec9_product25_true-unreach-call_true-termination.cil.c 1 .80 .79 7.4 27 .25   0      8.4  4.4  100   360 200   120   2800 7000
elevator_spec9_product27_true-unreach-call_true-termination.cil.c 1 .83 .82 9.8 28 .28   0      8.0  4.2  140   310 220   130   2700 7000
elevator_spec9_product29_true-unreach-call_true-termination.cil.c 1 .82 .81 8.4 28 .25   0      10    5.4  180   340 150   92   2700 7000
elevator_spec9_product31_true-unreach-call_true-termination.cil.c 1 .79 .78 9.2 28 .29   0      10    5.4  100   300 210   130   4100 7000
email_spec0_product16_false-unreach-call_true-termination.cil.c 1 1.6  1.5  20   41 .20   0      12    6.4  200 480 42   24   840 680
email_spec0_product21_false-unreach-call_true-termination.cil.c 1 2.7  2.7  33   57 .25   0      14    7.2  270 710 12   6.6 210 500
email_spec0_product22_false-unreach-call_true-termination.cil.c 1 1.7  1.6  15   43 .21   0      13    6.9  240 600 47   27   480 700
email_spec0_product26_false-unreach-call_true-termination.cil.c 1 2.8  2.8  40   60 .26   0      13    7.2  290 680 13   7.0 200 500
email_spec0_product31_false-unreach-call_true-termination.cil.c 1 1.8  1.8  23   45 .23   0      12    6.4  130 570 46   27   680 770
email_spec0_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.9  20   48 .21   0      13    6.7  250 570 46   27   980 740
email_spec0_product34_false-unreach-call_true-termination.cil.c 1 3.6  3.6  35   72 .23   0      13    7.0  200 620 51   30   920 770
email_spec0_product35_false-unreach-call_true-termination.cil.c 1 3.8  3.8  43   75 .23   0      14    7.1  290 620 49   28   660 770
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c 1 770    770    6600   1700 .34   0      16    8.3  240 700 13   7.1 260 500
email_spec11_product15_false-unreach-call_true-termination.cil.c 1 1.5  1.5  18   41 .18   0      11    6.0  220 480 41   23   470 650
email_spec11_product20_false-unreach-call_true-termination.cil.c 1 2.3  2.3  29   53 .25   0      14    7.3  280 700 13   7.1 200 490
email_spec11_product22_false-unreach-call_true-termination.cil.c 1 1.6  1.6  20   42 .19   0      11    6.1  180 490 48   27   370 680
email_spec11_product26_false-unreach-call_true-termination.cil.c 1 2.9  2.8  31   60 .20   0      11    5.9  90 490 54   31   670 720
email_spec11_product30_false-unreach-call_true-termination.cil.c 1 1.7  1.7  23   44 .20   0      12    6.5  250 520 41   23   770 660
email_spec11_product32_false-unreach-call_true-termination.cil.c 1 3.2  3.1  34   67 .20   .16   12    6.5  140 540 47   27   580 780
email_spec11_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.9  20   45 .20   0      13    6.7  230 570 43   25   820 700
email_spec11_product35_false-unreach-call_true-termination.cil.c 1 3.8  3.8  52   75 .21   0      12    6.3  100 570 46   27   490 780
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c 0 850    850    5100   2000 .037  0      .48 .31 13 39 7.0 3.7 150 310
email_spec1_product14_false-unreach-call_true-termination.cil.c 1 1.5  1.5  15   41 .23   0      15    7.7  200 610 12   6.3 230 480
email_spec1_product15_false-unreach-call_true-termination.cil.c 1 1.5  1.5  16   40 .22   0      13    6.7  220 610 11   6.1 220 460
email_spec1_product16_false-unreach-call_true-termination.cil.c 1 1.6  1.6  16   40 .27   .11   13    6.8  96 670 12   6.5 260 510
email_spec1_product20_false-unreach-call_true-termination.cil.c 1 2.3  2.3  25   51 .24   0      13    7.1  180 670 12   6.5 240 510
email_spec1_product21_false-unreach-call_true-termination.cil.c 1 2.5  2.5  36   55 .29   0      15    7.8  310 730 12   6.6 220 500
email_spec1_product22_false-unreach-call_true-termination.cil.c 1 1.6  1.6  19   41 .26   0      14    7.3  260 700 15   7.9 140 500
email_spec1_product26_false-unreach-call_true-termination.cil.c 1 2.8  2.8  29   58 .25   0      14    7.4  240 690 12   6.7 230 500
email_spec1_product29_false-unreach-call_true-termination.cil.c 1 1.7  1.7  22   42 .28   0      14    7.4  200 700 12   6.2 180 500
email_spec1_product30_false-unreach-call_true-termination.cil.c 1 1.7  1.7  18   41 .27   0      15    7.7  280 700 14   7.3 180 500
email_spec1_product31_false-unreach-call_true-termination.cil.c 1 1.8  1.8  19   42 .33   0      15    8.0  260 700 13   6.9 180 500
email_spec1_product32_false-unreach-call_true-termination.cil.c 1 3.0  3.1  38   77 .28   13      14    7.3  190 690 12   6.6 220 520
email_spec1_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.9  20   43 .28   0      15    7.8  290 700 12   6.3 160 500
email_spec1_product34_false-unreach-call_true-termination.cil.c 1 3.5  3.5  46   69 .26   .12   13    6.9  130 660 13   7.0 230 510
email_spec1_product35_false-unreach-call_true-termination.cil.c 1 3.8  3.8  54   71 .36   0      16    8.6  320 730 12   6.6 270 490
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c 1 100    100    870   600 .27   0      14    7.3  270 710 13   7.0 240 500
email_spec27_product17_false-unreach-call_true-termination.cil.c 1 1.6  1.6  17   42 .28   0      14    7.6  210 690 62   37   870 810
email_spec27_product18_false-unreach-call_true-termination.cil.c 1 1.5  1.5  17   41 .27   0      14    7.5  220 660 12   6.3 220 500
email_spec27_product19_false-unreach-call_true-termination.cil.c 1 1.6  1.6  17   42 .28   0      15    7.7  270 710 12   6.6 260 480
email_spec27_product23_false-unreach-call_true-termination.cil.c 1 2.6  2.6  28   56 .27   0      13    6.9  270 690 56   33   1100 850
email_spec27_product24_false-unreach-call_true-termination.cil.c 1 1.7  1.7  17   42 .27   0      15    8.0  210 600 12   6.6 260 520
email_spec27_product25_false-unreach-call_true-termination.cil.c 1 2.9  2.9  32   58 .29   0      15    7.8  170 720 74   45   690 870
email_spec27_product27_false-unreach-call_true-termination.cil.c 1 3.1  3.1  34   62 .40   0      17    9.0  340 800 13   6.7 230 520
email_spec27_product29_false-unreach-call_true-termination.cil.c 1 1.8  1.8  22   47 .31   0      15    7.7  200 700 15   7.9 190 520
email_spec27_product30_false-unreach-call_true-termination.cil.c 1 1.8  1.8  19   45 .32   0      14    7.6  110 700 12   6.5 230 510
email_spec27_product31_false-unreach-call_true-termination.cil.c 1 1.8  1.8  19   46 .34   0      17    9.0  120 670 15   8.0 140 520
email_spec27_product32_false-unreach-call_true-termination.cil.c 1 3.3  3.3  48   69 .31   0      15    7.7  200 670 16   8.2 160 500
email_spec27_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.9  27   46 .37   0      21    11    220 750 14   7.2 230 500
email_spec27_product34_false-unreach-call_true-termination.cil.c 1 3.9  3.8  48   74 .34   0      16    8.2  150 730 16   8.4 170 510
email_spec27_product35_false-unreach-call_true-termination.cil.c 1 4.1  4.1  44   77 .36   0      16    8.6  280 730 13   7.2 260 510
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c 1 300    300    2300   870 .33   .10   15    8.0  300 710 14   7.7 210 490
email_spec3_product13_false-unreach-call_true-termination.cil.c 1 .45 .44 3.9 34 .012  0      12    6.1  240 480 37   20   650 560
email_spec3_product17_false-unreach-call_true-termination.cil.c 1 .55 .54 5.2 37 .012  0      11    5.9  220 470 35   20   530 560
email_spec3_product18_false-unreach-call_true-termination.cil.c 1 .48 .47 6.2 34 .012  0      11    5.5  100 440 43   24   500 580
email_spec3_product19_false-unreach-call_true-termination.cil.c 1 .53 .52 5.2 37 .012  0      12    6.1  180 460 35   20   660 550
email_spec3_product23_false-unreach-call_true-termination.cil.c 1 .89 .87 9.3 45 .012  0      11    5.8  230 520 35   19   630 580
email_spec3_product24_false-unreach-call_true-termination.cil.c 1 .56 .55 6.0 36 .012  .16   11    5.6  130 460 43   24   500 570
email_spec3_product25_false-unreach-call_true-termination.cil.c 1 .95 .94 10   50 .012  0      11    5.8  240 440 38   22   890 600
email_spec3_product27_false-unreach-call_true-termination.cil.c 1 1.0  1.0  11   51 .012  0      10    5.4  71 450 48   27   540 590
email_spec3_product28_false-unreach-call_true-termination.cil.c 1 .47 .46 4.3 34 .012  0      12    6.3  250 500 42   24   480 570
email_spec3_product29_false-unreach-call_true-termination.cil.c 1 .62 .60 5.8 39 .012  0      11    5.9  220 470 38   22   730 600
email_spec3_product30_false-unreach-call_true-termination.cil.c 1 .54 .53 5.4 36 .012  0      12    6.1  150 520 36   21   650 590
email_spec3_product31_false-unreach-call_true-termination.cil.c 1 .65 .63 6.2 38 .012  0      11    6.1  240 490 35   20   750 570
email_spec3_product32_false-unreach-call_true-termination.cil.c 1 1.1  1.1  12   57 .012  0      12    6.5  220 510 42   24   700 620
email_spec3_product33_false-unreach-call_true-termination.cil.c 1 .59 .59 6.6 37 .012  .11   11    5.9  110 470 45   25   490 600
email_spec3_product34_false-unreach-call_true-termination.cil.c 1 1.3  1.3  13   64 .012  0      12    6.3  240 480 51   29   580 610
email_spec3_product35_false-unreach-call_true-termination.cil.c 1 1.4  1.4  15   66 .012  0      12    6.2  160 510 55   32   720 630
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c 1 38    38    300   630 .012  .11   11    5.9  88 490 52   29   710 780
email_spec4_product18_false-unreach-call_true-termination.cil.c 1 1.4  1.4  14   40 .22   0      12    6.5  200 570 14   7.7 160 480
email_spec4_product19_false-unreach-call_true-termination.cil.c 1 1.5  1.5  16   41 .26   .12   14    7.2  200 700 14   7.3 200 510
email_spec4_product23_false-unreach-call_true-termination.cil.c 1 2.3  2.3  30   52 .30   0      16    8.2  340 680 12   6.6 230 510
email_spec4_product24_false-unreach-call_true-termination.cil.c 1 1.6  1.6  21   52 .24   11      14    7.4  260 660 15   7.7 170 500
email_spec4_product25_false-unreach-call_true-termination.cil.c 1 2.6  2.6  31   55 .27   0      14    7.2  190 700 15   8.0 200 500
email_spec4_product27_false-unreach-call_true-termination.cil.c 1 2.8  2.8  27   57 .29   0      15    7.9  220 730 12   6.5 240 510
email_spec4_product30_false-unreach-call_true-termination.cil.c 1 1.7  1.7  15   43 .24   0      15    7.7  240 640 11   6.1 220 490
email_spec4_product31_false-unreach-call_true-termination.cil.c 1 1.8  1.8  18   42 .29   0      14    7.5  120 720 15   7.9 170 500
email_spec4_product32_false-unreach-call_true-termination.cil.c 1 3.1  3.1  38   63 .32   0      15    7.8  170 740 12   6.4 230 520
email_spec4_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.9  20   44 .25   .16   15    7.8  260 700 13   6.9 200 490
email_spec4_product34_false-unreach-call_true-termination.cil.c 1 3.6  3.6  41   69 .29   .0041 14    7.6  170 690 15   7.7 170 500
email_spec4_product35_false-unreach-call_true-termination.cil.c 1 3.8  3.8  43   72 .30   0      14    7.5  220 700 12   6.7 230 490
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c 1 100    100    920   610 .29   0      15    7.8  320 660 17   9.2 240 490
email_spec6_product12_false-unreach-call_true-termination.cil.c 1 1.2  1.2  14   40 .19   0      13    6.9  160 540 41   23   760 630
email_spec6_product14_false-unreach-call_true-termination.cil.c 1 1.6  1.6  17   42 .22   0      12    6.3  92 560 60   34   780 770
email_spec6_product15_false-unreach-call_true-termination.cil.c 1 1.5  1.5  16   42 .18   0      12    6.2  190 490 46   27   690 650
email_spec6_product16_false-unreach-call_true-termination.cil.c 1 1.6  1.6  17   42 .21   0      12    6.6  240 520 44   26   830 680
email_spec6_product20_false-unreach-call_true-termination.cil.c 1 2.5  2.5  31   68 .21   13      12    6.4  210 510 51   30   960 720
email_spec6_product21_false-unreach-call_true-termination.cil.c 1 2.8  2.7  31   60 .27   0      15    7.9  250 670 12   6.4 210 510
email_spec6_product22_false-unreach-call_true-termination.cil.c 1 1.7  1.6  18   42 .19   0      12    6.2  230 470 42   24   780 670
email_spec6_product26_false-unreach-call_true-termination.cil.c 1 3.0  3.0  32   63 .21   0      12    6.5  260 550 64   37   660 760
email_spec6_product28_false-unreach-call_true-termination.cil.c 1 1.3  1.3  14   39 .19   .10   13    6.6  270 530 42   24   830 680
email_spec6_product29_false-unreach-call_true-termination.cil.c 1 1.9  1.9  19   47 .20   .54   12    6.3  140 540 53   31   620 720
email_spec6_product30_false-unreach-call_true-termination.cil.c 1 1.7  1.7  18   43 .20   0      12    6.3  250 510 52   30   740 660
email_spec6_product31_false-unreach-call_true-termination.cil.c 1 1.8  1.8  22   45 .20   0      12    6.2  110 550 57   33   680 690
email_spec6_product32_false-unreach-call_true-termination.cil.c 1 3.3  3.3  44   67 .38   0      16    8.7  300 830 12   6.3 230 500
email_spec6_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.9  27   45 .27   0      14    7.2  130 700 12   6.7 190 500
email_spec6_product34_false-unreach-call_true-termination.cil.c 1 3.8  3.8  48   73 .29   0      15    7.9  310 690 13   6.9 290 500
email_spec6_product35_false-unreach-call_true-termination.cil.c 1 4.1  4.1  52   77 .23   0      12    6.4  110 590 56   33   960 800
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c 1 99    99    960   610 .34   0      16    8.2  290 690 14   7.6 230 510
email_spec7_product28_false-unreach-call_true-termination.cil.c 1 1.4  1.3  13   40 .21   0      12    6.1  83 490 41   23   550 700
email_spec7_product29_false-unreach-call_true-termination.cil.c 1 1.7  1.7  21   44 .21   0      12    6.4  160 520 45   25   740 710
email_spec7_product30_false-unreach-call_true-termination.cil.c 1 1.7  1.7  21   42 .18   0      11    6.0  100 450 41   23   850 640
email_spec7_product31_false-unreach-call_true-termination.cil.c 1 1.8  1.8  18   43 .20   0      12    6.2  230 480 51   28   470 650
email_spec7_product32_false-unreach-call_true-termination.cil.c 1 3.0  3.0  36   64 .32   0      15    8.0  310 680 14   7.5 200 500
email_spec7_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.9  18   45 .32   0      14    7.7  200 740 13   6.9 240 500
email_spec7_product34_false-unreach-call_true-termination.cil.c 1 3.5  3.5  41   70 .19   .0041 11    5.9  85 520 43   24   590 600
email_spec7_product35_false-unreach-call_true-termination.cil.c 1 3.7  3.7  46   73 .39   .11   16    8.4  250 790 13   6.7 180 490
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c 1 120    120    1100   700 .33   0      15    8.0  340 720 13   7.0 290 490
email_spec8_product15_false-unreach-call_true-termination.cil.c 1 1.5  1.5  15   40 .23   0      13    6.6  150 610 14   7.5 170 460
email_spec8_product16_false-unreach-call_true-termination.cil.c 1 1.6  1.6  17   42 .27   .28   15    7.7  270 680 11   5.9 190 500
email_spec8_product20_false-unreach-call_true-termination.cil.c 1 2.4  2.4  30   52 .31   0      14    7.6  280 700 11   6.1 200 510
email_spec8_product21_false-unreach-call_true-termination.cil.c 1 2.6  2.6  28   56 .29   0      15    8.0  280 710 13   6.8 220 500
email_spec8_product22_false-unreach-call_true-termination.cil.c 1 1.6  1.6  20   55 .24   13      13    6.9  150 650 14   7.3 180 480
email_spec8_product26_false-unreach-call_true-termination.cil.c 1 2.9  2.8  34   58 .33   .13   15    7.9  310 690 13   6.7 250 500
email_spec8_product30_false-unreach-call_true-termination.cil.c 1 1.7  1.7  17   42 .27   0      14    7.1  220 700 12   6.5 190 500
email_spec8_product31_false-unreach-call_true-termination.cil.c 1 1.8  1.8  20   42 .32   0      16    8.4  300 720 17   8.8 200 500
email_spec8_product32_false-unreach-call_true-termination.cil.c 1 3.1  3.0  34   64 .38   .12   17    9.1  310 800 13   6.9 270 500
email_spec8_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.9  19   43 .33   0      15    8.1  290 700 14   7.5 190 500
email_spec8_product34_false-unreach-call_true-termination.cil.c 1 3.7  3.6  43   70 .41   0      16    8.6  210 800 14   7.5 220 510
email_spec8_product35_false-unreach-call_true-termination.cil.c 1 3.8  3.8  51   72 .35   0      15    8.0  200 720 15   8.0 280 500
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c 1 100    100    1000   610 .32   0      15    7.7  150 690 13   7.2 260 480
email_spec9_product15_false-unreach-call_true-termination.cil.c 1 1.5  1.5  14   40 .23   .19   13    6.7  280 580 12   6.3 220 460
email_spec9_product16_false-unreach-call_true-termination.cil.c 1 1.6  1.6  15   40 .25   0      14    7.3  280 700 13   7.0 180 480
email_spec9_product20_false-unreach-call_true-termination.cil.c 1 2.4  2.4  26   51 .31   0      14    7.4  200 680 13   6.8 210 500
email_spec9_product21_false-unreach-call_true-termination.cil.c 1 2.6  2.6  32   56 .29   0      16    8.3  270 700 14   7.5 200 500
email_spec9_product22_false-unreach-call_true-termination.cil.c 1 1.6  1.6  21   43 .25   0      13    7.1  290 710 15   8.2 140 500
email_spec9_product26_false-unreach-call_true-termination.cil.c 1 2.9  2.8  35   58 .32   0      15    7.9  300 690 13   6.8 290 500
email_spec9_product30_false-unreach-call_true-termination.cil.c 1 1.6  1.6  20   41 .26   0      13    7.1  270 690 14   7.3 220 490
email_spec9_product31_false-unreach-call_true-termination.cil.c 1 1.8  1.8  21   42 .31   0      15    7.9  310 690 16   8.7 180 500
email_spec9_product32_false-unreach-call_true-termination.cil.c 1 3.1  3.1  33   63 .28   0      14    7.4  250 720 12   6.5 220 500
email_spec9_product33_false-unreach-call_true-termination.cil.c 1 1.9  1.8  21   42 .27   0      16    8.5  260 700 16   8.4 170 500
email_spec9_product34_false-unreach-call_true-termination.cil.c 1 3.6  3.6  41   70 .42   0      19    9.8  150 780 15   7.9 200 500
email_spec9_product35_false-unreach-call_true-termination.cil.c 1 3.8  3.7  46   72 .27   0      14    7.3  150 690 17   8.8 200 490
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c 1 100    100    980   620 .33   13      16    8.2  200 720 13   6.9 150 500
email_spec0_product05_true-unreach-call_true-termination.cil.c 2 1.4  1.3  12   29 .19   0      8.4  4.5  78   300 16   8.6 290 440
email_spec0_product09_true-unreach-call_true-termination.cil.c 2 1.8  1.8  21   28 .34   0      8.8  4.7  110   350 18   9.8 270 510
email_spec0_product10_true-unreach-call_true-termination.cil.c 2 1.4  1.4  13   29 .22   .11   7.0  3.7  100   330 15   8.3 210 470
email_spec0_product11_true-unreach-call_true-termination.cil.c 2 1.7  1.7  17   32 .38   0      8.2  4.3  110   300 20   11   300 500
email_spec0_product19_true-unreach-call_true-termination.cil.c 2 1.9  1.9  19   31 .44   0      6.8  3.6  110   280 26   14   590 660
email_spec0_product24_true-unreach-call_true-termination.cil.c 2 2.0  1.9  22   31 .47   0      7.3  3.9  120   290 33   18   360 700
email_spec0_product25_true-unreach-call_true-termination.cil.c 2 3.1  3.1  38   33 .71   0      8.2  4.4  120   290 28   15   360 680
email_spec0_product27_true-unreach-call_true-termination.cil.c 2 3.3  3.3  35   32 .81   0      8.8  4.6  130   320 36   19   380 800
email_spec0_product36_true-unreach-call_true-termination.cil.c 2 2.0  2.0  22   28 .41   0      10    5.4  93   320 22   12   250 500
email_spec0_product37_true-unreach-call_true-termination.cil.c 2 1.8  1.7  18   31 .40   0      8.3  4.4  160   320 38   20   760 790
email_spec0_product38_true-unreach-call_true-termination.cil.c 2 2.3  2.3  24   33 .53   .11   7.1  3.8  150   280 23   12   350 530
email_spec0_product40_true-unreach-call_true-termination.cil.c 2 2.5  2.5  27   31 .59   0      9.5  5.0  100   330 43   23   690 800
email_spec11_product03_true-unreach-call_true-termination.cil.c 2 1.3  1.2  12   27 .18   0      7.3  3.9  110   310 15   8.1 260 450
email_spec11_product07_true-unreach-call_true-termination.cil.c 2 1.7  1.7  19   28 .31   0      9.0  4.7  120   320 17   9.2 250 500
email_spec11_product08_true-unreach-call_true-termination.cil.c 2 1.5  1.5  18   30 .36   0      8.7  4.6  92   290 24   13   360 660
email_spec11_product10_true-unreach-call_true-termination.cil.c 2 1.3  1.3  17   28 .22   0      6.5  3.4  110   290 18   9.6 260 480
email_spec11_product18_true-unreach-call_true-termination.cil.c 2 1.8  1.8  19   31 .42   0      9.2  4.9  100   330 29   15   500 680
email_spec11_product23_true-unreach-call_true-termination.cil.c 2 2.7  2.7  32   32 .63   0      7.8  4.1  110   290 29   15   410 680
email_spec11_product24_true-unreach-call_true-termination.cil.c 2 2.0  2.0  21   31 .47   0      9.4  4.9  130   320 28   15   530 670
email_spec11_product27_true-unreach-call_true-termination.cil.c 2 3.4  3.4  38   34 .78   0      9.5  5.0  99   290 35   18   600 800
email_spec11_product36_true-unreach-call_true-termination.cil.c 2 2.0  2.0  21   28 .41   0      7.9  4.2  160   340 19   10   300 490
email_spec11_product37_true-unreach-call_true-termination.cil.c 2 1.7  1.7  17   30 .40   0      9.7  5.1  83   300 25   13   290 680
email_spec11_product39_true-unreach-call_true-termination.cil.c 2 2.1  2.1  25   32 .50   0      8.6  4.5  150   320 28   15   360 700
email_spec11_product40_true-unreach-call_true-termination.cil.c 2 2.5  2.5  27   31 .60   0      9.9  5.2  110   310 28   15   530 720
email_spec1_product12_true-unreach-call_true-termination.cil.c 2 1.6  1.5  15   31 .34   0      8.0  4.3  95   290 130   77   1600 5800
email_spec1_product28_true-unreach-call_true-termination.cil.c 1 1.7  1.6  19   31 .36   0      9.4  5.0  110   310 180   110   1600 7000
email_spec27_product13_true-unreach-call_true-termination.cil.c 1 1.7  1.7  19   39 .35   0      8.2  4.3  160   320 230   150   4800 7000
email_spec27_product28_true-unreach-call_true-termination.cil.c 1 1.7  1.7  18   38 .37   0      7.1  3.7  130   290 230   150   3100 7000
email_spec4_product13_true-unreach-call_true-termination.cil.c 1 1.7  1.7  19   38 .35   0      7.0  3.7  140   310 210   140   3200 7000
email_spec4_product17_true-unreach-call_true-termination.cil.c 1 2.0  2.0  21   41 .43   0      10    5.2  95   320 320   230   6300 7000
email_spec4_product28_true-unreach-call_true-termination.cil.c 1 1.7  1.7  23   38 .37   .17   8.7  4.6  87   290 150   96   1700 7000
email_spec4_product29_true-unreach-call_true-termination.cil.c 1 2.3  2.3  26   45 .49   .11   7.7  4.1  150   280 220   140   3300 7000
email_spec7_product13_true-unreach-call_true-termination.cil.c 2 1.6  1.6  16   32 .34   0      9.0  4.7  99   290 20   11   250 520
email_spec7_product17_true-unreach-call_true-termination.cil.c 2 1.8  1.8  21   32 .42   0      8.6  4.5  100   280 21   11   310 510
email_spec7_product18_true-unreach-call_true-termination.cil.c 2 1.8  1.8  17   31 .41   0      9.0  4.8  110   320 25   13   390 700
email_spec7_product19_true-unreach-call_true-termination.cil.c 2 1.8  1.8  19   32 .44   .11   7.7  4.0  110   310 22   12   500 510
email_spec7_product23_true-unreach-call_true-termination.cil.c 2 2.7  2.7  29   33 .62   0      7.2  3.8  110   290 28   15   450 700
email_spec7_product24_true-unreach-call_true-termination.cil.c 2 2.0  2.0  23   33 .47   .0041 8.4  4.4  150   330 25   14   380 660
email_spec7_product25_true-unreach-call_true-termination.cil.c 2 3.1  3.1  32   31 .71   0      7.3  3.9  110   290 26   14   420 550
email_spec7_product27_true-unreach-call_true-termination.cil.c 2 3.3  3.3  38   33 .77   0      8.6  4.5  150   320 33   17   340 680
email_spec8_product12_true-unreach-call_true-termination.cil.c 2 1.5  1.5  18   31 .35   0      9.6  5.1  100   300 110   65   2200 5900
email_spec8_product14_true-unreach-call_true-termination.cil.c 1 2.0  2.0  30   41 .43   0      7.1  3.8  130   290 170   100   3800 7000
email_spec8_product28_true-unreach-call_true-termination.cil.c 1 1.7  1.7  17   31 .37   0      8.4  4.4  130   310 140   82   1800 7000
email_spec8_product29_true-unreach-call_true-termination.cil.c 1 2.5  2.4  24   43 .50   0      9.1  4.8  130   340 140   86   2800 7000
email_spec9_product12_true-unreach-call_true-termination.cil.c 2 1.6  1.5  20   31 .35   0      8.0  4.3  130   300 120   68   920 5800
email_spec9_product14_true-unreach-call_true-termination.cil.c 1 2.1  2.1  22   42 .43   0      7.5  4.0  140   290 270   180   3200 7000
email_spec9_product28_true-unreach-call_true-termination.cil.c 1 1.6  1.6  24   32 .37   0      7.3  3.9  130   290 150   91   1500 7000
email_spec9_product29_true-unreach-call_true-termination.cil.c 1 2.4  2.4  25   42 .49   0      9.2  4.9  120   320 170   110   2300 7000
minepump_spec1_product33_false-unreach-call_false-termination.cil.c 1 .18 .17 1.3 20 .0041 0      6.0  3.3  110 310 8.3 4.4 140 320
minepump_spec1_product34_false-unreach-call_false-termination.cil.c 1 .18 .17 1.4 20 .0041 0      6.4  3.5  130 330 8.9 4.8 160 320
minepump_spec1_product35_false-unreach-call_false-termination.cil.c 1 .16 .15 1.3 23 .0041 0      6.6  3.5  130 350 8.6 4.6 130 330
minepump_spec1_product36_false-unreach-call_false-termination.cil.c 1 .16 .15 1.5 23 .0041 0      6.0  3.2  120 310 8.2 4.3 160 330
minepump_spec1_product37_false-unreach-call_false-termination.cil.c 1 .16 .15 1.5 22 .0041 0      5.9  3.2  41 320 7.7 4.2 170 330
minepump_spec1_product38_false-unreach-call_false-termination.cil.c 1 .17 .16 1.8 22 .0041 0      6.4  3.5  130 350 9.0 4.7 140 330
minepump_spec1_product39_false-unreach-call_false-termination.cil.c 1 .19 .18 1.6 22 .0041 0      5.9  3.2  110 310 8.0 4.3 140 320
minepump_spec1_product40_false-unreach-call_false-termination.cil.c 1 .17 .17 1.7 22 .0041 0      6.0  3.2  53 340 8.4 4.5 170 320
minepump_spec1_product41_false-unreach-call_false-termination.cil.c 1 .15 .15 1.9 21 .0041 0      6.1  3.3  68 310 9.3 5.0 120 320
minepump_spec1_product42_false-unreach-call_false-termination.cil.c 1 .16 .15 1.5 21 .0041 0      6.1  3.3  100 300 8.6 4.6 130 320
minepump_spec1_product43_false-unreach-call_false-termination.cil.c 1 .16 .15 1.2 22 .0041 0      6.1  3.3  110 320 10   5.5 110 330
minepump_spec1_product44_false-unreach-call_false-termination.cil.c 1 .16 .15 1.3 21 .0041 0      6.4  3.5  78 330 8.3 4.4 170 320
minepump_spec1_product49_false-unreach-call_false-termination.cil.c 1 .17 .16 1.8 22 .0041 0      5.9  3.2  69 330 8.0 4.3 130 320
minepump_spec1_product50_false-unreach-call_false-termination.cil.c 1 .20 .19 1.4 22 .0041 0      6.4  3.5  110 330 9.3 5.0 130 330
minepump_spec1_product51_false-unreach-call_false-termination.cil.c 1 .17 .17 1.7 22 .0041 0      5.6  3.0  110 290 7.6 4.1 150 320
minepump_spec1_product52_false-unreach-call_false-termination.cil.c 1 .17 .16 1.4 24 .0041 0      6.3  3.4  120 300 9.2 4.9 180 330
minepump_spec1_product53_false-unreach-call_false-termination.cil.c 1 .21 .20 2.3 24 .0041 0      6.2  3.4  110 340 9.1 4.8 170 320
minepump_spec1_product54_false-unreach-call_false-termination.cil.c 1 .21 .20 2.2 24 .0041 0      6.0  3.2  99 300 8.6 4.6 170 320
minepump_spec1_product55_false-unreach-call_false-termination.cil.c 1 .22 .21 2.0 25 .0041 0      6.1  3.3  110 340 9.7 5.2 140 330
minepump_spec1_product56_false-unreach-call_false-termination.cil.c 1 .23 .22 1.8 25 .0041 0      5.9  3.2  120 300 8.3 4.4 170 330
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c 1 .41 .40 4.4 39 .0041 0      6.4  3.4  99 300 8.4 4.6 170 320
minepump_spec2_product33_false-unreach-call_false-termination.cil.c 1 .17 .16 1.4 21 .0041 .16   6.4  3.5  70 350 7.5 4.0 130 320
minepump_spec2_product34_false-unreach-call_false-termination.cil.c 1 .16 .15 1.4 21 .0041 0      6.5  3.5  120 330 10   5.3 120 320
minepump_spec2_product35_false-unreach-call_false-termination.cil.c 1 .18 .18 1.3 21 .0041 0      6.1  3.3  52 330 8.9 4.8 110 330
minepump_spec2_product36_false-unreach-call_false-termination.cil.c 1 .14 .13 1.8 21 .0041 0      6.0  3.2  77 290 8.4 4.5 130 330
minepump_spec2_product41_false-unreach-call_false-termination.cil.c 1 .42 .41 3.8 23 .066  .16   6.9  3.7  120 370 7.7 4.1 160 320
minepump_spec2_product42_false-unreach-call_false-termination.cil.c 1 .40 .39 4.6 24 .082  0      7.8  4.2  130 300 9.7 5.1 98 320
minepump_spec2_product43_false-unreach-call_false-termination.cil.c 1