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