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