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