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 timeout 0 wit inspect 900   380   6300 13000 2.3 0      error (invalid witness file) .53 .34 13   41 error (invalid witness file) 6.1 3.2 93 310 - -
elevator_spec14_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   310   5400 13000 2.3 0      error (invalid witness file) .50 .32 9.9 39 error (invalid witness file) 6.1 3.2 99 300 - -
elevator_spec14_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   420   7100 11000 2.9 0      error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.4 3.4 120 310 - -
elevator_spec14_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   320   6000 13000 2.3 0      error (invalid witness file) .50 .31 8.4 39 error (invalid witness file) 6.3 3.3 130 310 - -
elevator_spec14_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   7000 13000 2.3 0      error (invalid witness file) .51 .33 9.4 40 error (invalid witness file) 6.3 3.3 120 300 - -
elevator_spec1_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   330   6700 13000 2.3 0      error (invalid witness file) .55 .34 10   39 error (invalid witness file) 6.1 3.2 130 300 - -
elevator_spec1_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   8100 13000 2.3 0      error (invalid witness file) .53 .34 9.0 41 error (invalid witness file) 6.0 3.2 88 310 - -
elevator_spec1_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6700 13000 2.3 0      error (invalid witness file) .51 .34 13   42 error (invalid witness file) 6.5 3.5 110 300 - -
elevator_spec1_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   320   5900 14000 2.3 0      error (invalid witness file) .51 .34 9.8 41 error (invalid witness file) 7.3 3.8 120 320 - -
elevator_spec1_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   330   6300 13000 2.3 0      error (invalid witness file) .55 .37 11   41 error (invalid witness file) 6.1 3.3 110 300 - -
elevator_spec1_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   310   6100 14000 2.3 0      error (invalid witness file) .65 .41 9.6 41 error (invalid witness file) 6.5 3.4 110 300 - -
elevator_spec1_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   6700 13000 2.3 0      error (invalid witness file) .61 .37 11   41 error (invalid witness file) 6.7 3.5 120 300 - -
elevator_spec1_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   320   5300 13000 2.3 0      error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.1 3.2 92 300 - -
elevator_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   350   6100 14000 2.3 0      error (invalid witness file) .48 .31 8.2 40 error (invalid witness file) 5.6 3.1 87 290 - -
elevator_spec2_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   360   6100 13000 2.3 0      error (invalid witness file) .49 .31 9.2 39 error (invalid witness file) 6.8 3.5 120 310 - -
elevator_spec2_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   300   5500 13000 2.3 0      error (invalid witness file) .53 .33 11   40 error (invalid witness file) 6.2 3.3 120 300 - -
elevator_spec2_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   330   5800 13000 2.3 0      error (invalid witness file) .49 .32 8.8 41 error (invalid witness file) 5.7 3.1 130 290 - -
elevator_spec2_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   310   5700 14000 2.3 0      error (invalid witness file) .52 .33 3.5 40 error (invalid witness file) 6.2 3.3 130 300 - -
elevator_spec2_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   350   7100 14000 2.3 0      error (invalid witness file) .50 .32 13   39 error (invalid witness file) 6.5 3.5 110 310 - -
elevator_spec2_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   360   6600 12000 2.3 0      error (invalid witness file) .48 .31 8.3 40 error (invalid witness file) 5.8 3.1 110 290 - -
elevator_spec2_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   330   5600 13000 2.3 0      error (invalid witness file) .53 .34 11   42 error (invalid witness file) 7.6 4.0 100 300 - -
elevator_spec2_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   270   5300 13000 2.3 0      error (invalid witness file) .49 .32 9.6 40 error (invalid witness file) 7.4 3.8 140 310 - -
elevator_spec2_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   310   5700 13000 2.3 0      error (invalid witness file) .54 .36 7.5 40 error (invalid witness file) 5.8 3.1 120 290 - -
elevator_spec3_product03_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   290   4900 14000 2.3 0      error (invalid witness file) .51 .32 8.8 40 error (invalid witness file) 6.4 3.4 120 300 - -
elevator_spec3_product11_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   290   5300 13000 2.3 0      error (invalid witness file) .65 .43 7.4 42 error (invalid witness file) 6.6 3.5 130 300 - -
elevator_spec3_product19_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   320   6200 13000 2.3 0      error (invalid witness file) .51 .33 10   41 error (invalid witness file) 6.1 3.3 110 310 - -
elevator_spec3_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   350   5900 13000 2.3 0      error (invalid witness file) .58 .38 10   42 error (invalid witness file) 7.4 3.9 99 300 - -
elevator_spec3_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   300   5500 13000 2.3 0      error (invalid witness file) .64 .42 3.6 40 error (invalid witness file) 6.5 3.4 130 310 - -
elevator_spec3_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   380   6800 13000 2.3 0      error (invalid witness file) .51 .34 11   42 error (invalid witness file) 6.1 3.2 110 300 - -
elevator_spec3_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   300   5900 14000 2.3 0      error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.1 3.2 110 300 - -
elevator_spec3_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   300   6300 13000 2.3 0      error (invalid witness file) .50 .31 7.2 41 error (invalid witness file) 6.2 3.3 120 290 - -
elevator_spec3_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   280   5200 13000 2.3 0      error (invalid witness file) .52 .34 6.7 40 error (invalid witness file) 7.7 4.1 86 300 - -
elevator_spec3_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   350   6100 13000 2.3 0      error (invalid witness file) .63 .40 7.7 40 error (invalid witness file) 6.2 3.3 110 300 - -
elevator_spec3_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   290   5900 13000 2.3 0      error (invalid witness file) .52 .33 8.3 40 error (invalid witness file) 6.2 3.3 110 290 - -
elevator_spec9_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   230   5600 14000 2.3 0      error (invalid witness file) .53 .34 6.1 40 error (invalid witness file) 6.8 3.5 98 300 - -
elevator_spec9_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   230   5400 14000 2.3 0      error (invalid witness file) .48 .31 8.4 40 error (invalid witness file) 6.4 3.4 130 300 - -
elevator_spec9_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   230   4800 14000 2.3 0      error (invalid witness file) .49 .33 7.2 42 error (invalid witness file) 5.9 3.2 110 300 - -
elevator_spec9_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   230   4900 14000 2.3 0      error (invalid witness file) .55 .36 8.0 42 error (invalid witness file) 6.4 3.4 130 300 - -
elevator_spec9_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   240   4800 14000 2.3 0      error (invalid witness file) .50 .34 11   40 error (invalid witness file) 6.1 3.2 84 300 - -
elevator_spec13_product21_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   310   5800 13000 2.3 0      - - error (invalid witness file) .54 .35 10   40 error (invalid witness file) 6.4 3.4 130 300
elevator_spec13_product22_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   270   5300 14000 2.3 0      - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 5.7 3.0 45 290
elevator_spec13_product23_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   270   5400 14000 2.3 0      - - error (invalid witness file) .48 .30 7.5 40 error (invalid witness file) 6.3 3.3 140 300
elevator_spec13_product24_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 900   350   6100 14000 2.3 0      - - error (invalid witness file) .70 .43 5.7 39 error (invalid witness file) 6.4 3.4 130 300
elevator_spec13_product29_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   360   6000 13000 2.3 0      - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 5.6 3.0 110 290
elevator_spec13_product30_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   340   5600 13000 2.3 0      - - error (invalid witness file) .64 .41 7.4 39 error (invalid witness file) 5.8 3.2 120 300
elevator_spec13_product31_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   280   5100 13000 2.3 0      - - error (invalid witness file) .58 .37 11   40 error (invalid witness file) 6.2 3.3 110 300
elevator_spec13_product32_true-unreach-call_false-termination.cil.c timeout 0 wit inspect 910   310   6600 14000 2.3 0      - - error (invalid witness file) .54 .36 11   40 error (invalid witness file) 6.6 3.5 73 310
elevator_spec13_productSimulator_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6300 13000 2.3 0      - - error (invalid witness file) .65 .42 7.7 39 error (invalid witness file) 6.2 3.3 100 300
elevator_spec14_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   7900 13000 2.3 0      - - error (invalid witness file) .63 .40 6.8 40 error (invalid witness file) 6.4 3.4 140 300
elevator_spec14_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   340   6200 13000 2.3 0      - - error (invalid witness file) .65 .42 8.1 41 error (invalid witness file) 5.8 3.1 92 290
elevator_spec14_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   390   8100 13000 2.3 0      - - error (invalid witness file) .64 .41 8.5 40 error (invalid witness file) 7.3 3.9 92 290
elevator_spec14_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   420   7900 13000 2.3 0      - - error (invalid witness file) .63 .41 7.9 39 error (invalid witness file) 6.3 3.3 140 300
elevator_spec14_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   6400 13000 2.3 0      - - error (invalid witness file) .54 .35 12   41 error (invalid witness file) 6.3 3.4 130 300
elevator_spec14_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6900 13000 2.3 0      - - error (invalid witness file) .54 .34 9.8 40 error (invalid witness file) 6.5 3.4 110 300
elevator_spec1_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   350   5500 13000 2.3 0      - - error (invalid witness file) .75 .46 7.8 44 error (invalid witness file) 7.8 4.1 96 300
elevator_spec1_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   6200 12000 2.3 0      - - error (invalid witness file) .51 .34 10   40 error (invalid witness file) 6.4 3.4 130 300
elevator_spec1_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6800 13000 2.3 0      - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.3 3.3 100 310
elevator_spec1_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   7300 11000 2.3 0      - - error (invalid witness file) .57 .37 9.4 40 error (invalid witness file) 6.2 3.3 100 300
elevator_spec1_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   350   7000 13000 2.3 0      - - error (invalid witness file) .62 .40 7.2 40 error (invalid witness file) 6.7 3.5 120 310
elevator_spec1_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6400 11000 2.3 0      - - error (invalid witness file) .62 .38 8.4 40 error (invalid witness file) 5.9 3.2 110 300
elevator_spec1_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   320   6600 13000 2.3 0      - - error (invalid witness file) .52 .31 14   39 error (invalid witness file) 6.3 3.3 87 300
elevator_spec1_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   350   5400 13000 2.3 0      - - error (invalid witness file) .74 .47 8.7 46 error (invalid witness file) 6.7 3.5 130 310
elevator_spec1_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   6100 13000 2.3 0      - - error (invalid witness file) .57 .36 12   43 error (invalid witness file) 6.1 3.3 120 310
elevator_spec1_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   7200 12000 2.3 0      - - error (invalid witness file) .53 .33 13   43 error (invalid witness file) 6.5 3.4 120 300
elevator_spec1_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   320   5800 13000 2.3 0      - - error (invalid witness file) .51 .33 9.2 42 error (invalid witness file) 6.2 3.3 100 310
elevator_spec1_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   360   6800 13000 2.3 0      - - error (invalid witness file) .61 .40 9.4 39 error (invalid witness file) 6.9 3.6 130 310
elevator_spec2_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   240   5100 13000 2.3 0      - - error (invalid witness file) .49 .31 7.7 39 error (invalid witness file) 6.6 3.5 130 300
elevator_spec2_product03_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   380   6400 13000 2.3 0      - - error (invalid witness file) .59 .37 7.9 40 error (invalid witness file) 6.3 3.4 120 310
elevator_spec2_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   240   4600 13000 2.3 0      - - error (invalid witness file) .65 .41 6.6 39 error (invalid witness file) 6.1 3.3 110 300
elevator_spec2_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6100 12000 2.3 0      - - error (invalid witness file) .51 .32 10   40 error (invalid witness file) 6.3 3.3 120 310
elevator_spec2_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   250   4700 13000 2.3 .074  - - error (invalid witness file) .63 .40 11   42 error (invalid witness file) 6.1 3.3 110 310
elevator_spec2_product19_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   370   6100 13000 2.3 0      - - error (invalid witness file) .62 .39 9.6 40 error (invalid witness file) 6.0 3.2 110 290
elevator_spec2_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   230   4700 14000 2.3 0      - - error (invalid witness file) .63 .40 9.1 40 error (invalid witness file) 6.8 3.6 130 300
elevator_spec2_product23_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   310   5700 14000 2.3 0      - - error (invalid witness file) .55 .35 14   41 error (invalid witness file) 6.1 3.3 110 300
elevator_spec2_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   250   4400 13000 2.3 0      - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.6 3.5 120 300
elevator_spec2_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   6600 13000 2.3 0      - - error (invalid witness file) .57 .36 9.3 39 error (invalid witness file) 6.1 3.2 110 300
elevator_spec2_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   230   4200 13000 2.3 0      - - error (invalid witness file) .62 .39 6.5 39 error (invalid witness file) 6.0 3.2 87 310
elevator_spec2_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   290   5200 13000 2.3 0      - - error (invalid witness file) .66 .42 9.0 43 error (invalid witness file) 6.1 3.3 100 310
elevator_spec3_product01_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   280   4900 14000 2.3 0      - - error (invalid witness file) .67 .42 6.6 39 error (invalid witness file) 7.0 3.7 140 320
elevator_spec3_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   250   5000 14000 2.3 0      - - error (invalid witness file) .55 .36 9.4 41 error (invalid witness file) 6.5 3.4 140 310
elevator_spec3_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   280   4900 14000 2.3 0      - - error (invalid witness file) .57 .37 12   45 error (invalid witness file) 6.3 3.3 130 300
elevator_spec3_product18_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   310   6400 13000 2.3 0      - - error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.0 3.1 120 300
elevator_spec3_product21_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   280   5200 13000 2.3 0      - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.2 3.3 120 300
elevator_spec3_product22_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   270   5100 13000 2.3 0      - - error (invalid witness file) .61 .39 9.0 42 error (invalid witness file) 6.9 3.7 100 300
elevator_spec3_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   250   5100 14000 2.3 0      - - error (invalid witness file) .62 .40 8.0 39 error (invalid witness file) 6.6 3.5 130 300
elevator_spec3_product26_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   300   5800 14000 2.3 0      - - error (invalid witness file) .67 .43 7.9 44 error (invalid witness file) 5.6 3.0 93 290
elevator_spec3_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   280   5100 13000 2.3 0      - - error (invalid witness file) .48 .31 9.8 39 error (invalid witness file) 6.4 3.3 120 300
elevator_spec3_product30_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   290   5100 14000 2.3 0      - - error (invalid witness file) .47 .32 6.5 40 error (invalid witness file) 6.4 3.4 130 300
elevator_spec9_product09_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   270   5200 13000 2.3 0      - - error (invalid witness file) .67 .43 9.6 44 error (invalid witness file) 6.6 3.5 120 310
elevator_spec9_product11_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   5800 13000 2.3 0      - - error (invalid witness file) .64 .41 8.0 39 error (invalid witness file) 6.3 3.4 120 290
elevator_spec9_product25_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   240   4500 14000 2.3 0      - - error (invalid witness file) .55 .35 13   41 error (invalid witness file) 6.5 3.4 130 300
elevator_spec9_product27_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   270   5100 14000 2.3 0      - - error (invalid witness file) .50 .32 8.2 40 error (invalid witness file) 6.5 3.4 120 300
elevator_spec9_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   270   5200 14000 2.3 0      - - error (invalid witness file) .59 .38 9.4 41 error (invalid witness file) 6.0 3.2 100 300
elevator_spec9_product31_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   320   5800 13000 2.3 0      - - error (invalid witness file) .51 .34 11   40 error (invalid witness file) 6.7 3.5 120 310
email_spec0_product16_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   7800 13000 2.3 0      error (invalid witness file) .55 .36 11   40 error (invalid witness file) 5.8 3.1 120 290 - -
email_spec0_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6400 13000 2.3 0      error (invalid witness file) .52 .34 10   42 error (invalid witness file) 6.2 3.3 110 300 - -
email_spec0_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   8200 13000 2.3 0      error (invalid witness file) .63 .41 6.5 39 error (invalid witness file) 6.7 3.5 140 300 - -
email_spec0_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   7000 12000 2.3 0      error (invalid witness file) .47 .33 9.6 39 error (invalid witness file) 6.6 3.4 130 300 - -
email_spec0_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   6000 14000 2.3 0      error (invalid witness file) .51 .33 6.7 40 error (invalid witness file) 6.5 3.4 120 310 - -
email_spec0_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   390   7200 13000 2.3 0      error (invalid witness file) .53 .34 7.6 39 error (invalid witness file) 6.3 3.3 120 300 - -
email_spec0_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   370   6500 14000 2.3 0      error (invalid witness file) .63 .39 9.6 40 error (invalid witness file) 6.0 3.2 120 300 - -
email_spec0_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   7900 14000 2.3 0      error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.1 3.3 130 300 - -
email_spec0_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   280   4900 13000 2.3 0      error (invalid witness file) .51 .32 9.8 40 error (invalid witness file) 6.6 3.5 130 320 - -
email_spec11_product15_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6500 13000 2.3 0      error (invalid witness file) .62 .40 7.8 39 error (invalid witness file) 6.0 3.2 82 300 - -
email_spec11_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6100 13000 2.3 0      error (invalid witness file) .52 .34 9.4 41 error (invalid witness file) 5.8 3.1 74 290 - -
email_spec11_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6100 13000 2.3 0      error (invalid witness file) .50 .31 8.5 39 error (invalid witness file) 6.3 3.3 120 290 - -
email_spec11_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   410   5900 13000 2.3 0      error (invalid witness file) .48 .31 8.6 40 error (invalid witness file) 6.4 3.4 130 300 - -
email_spec11_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   430   6800 13000 2.3 0      error (invalid witness file) .48 .32 6.2 41 error (invalid witness file) 5.8 3.1 88 300 - -
email_spec11_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   6500 12000 2.3 0      error (invalid witness file) .69 .43 7.1 40 error (invalid witness file) 6.2 3.2 120 300 - -
email_spec11_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   430   7300 11000 2.3 0      error (invalid witness file) .62 .40 8.3 40 error (invalid witness file) 6.9 3.6 140 320 - -
email_spec11_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6800 12000 2.3 0      error (invalid witness file) .56 .36 6.8 39 error (invalid witness file) 6.7 3.5 110 310 - -
email_spec11_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   300   5200 13000 2.3 0      error (invalid witness file) .60 .38 4.8 41 error (invalid witness file) 6.9 3.6 91 320 - -
email_spec1_product14_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   460   8300 13000 2.3 0      error (invalid witness file) .48 .31 12   40 error (invalid witness file) 5.8 3.1 99 300 - -
email_spec1_product15_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   7000 12000 2.3 0      error (invalid witness file) .51 .34 11   40 error (invalid witness file) 6.3 3.3 120 290 - -
email_spec1_product16_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   7000 14000 2.3 0      error (invalid witness file) .52 .35 8.2 40 error (invalid witness file) 5.7 3.0 110 300 - -
email_spec1_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   480   9200 12000 2.3 0      error (invalid witness file) .70 .45 7.3 40 error (invalid witness file) 6.2 3.3 130 300 - -
email_spec1_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   8000 13000 2.3 0      error (invalid witness file) .49 .32 7.5 40 error (invalid witness file) 5.7 3.1 110 290 - -
email_spec1_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   470   7300 11000 2.3 0      error (invalid witness file) .49 .32 10   40 error (invalid witness file) 6.6 3.4 130 300 - -
email_spec1_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   480   8100 11000 2.3 0      error (invalid witness file) .49 .32 9.2 40 error (invalid witness file) 5.9 3.2 110 300 - -
email_spec1_product29_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   390   6500 13000 2.3 0      error (invalid witness file) .58 .37 8.9 39 error (invalid witness file) 6.0 3.2 100 300 - -
email_spec1_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   7600 13000 2.3 0      error (invalid witness file) .47 .32 3.4 40 error (invalid witness file) 6.5 3.4 120 310 - -
email_spec1_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6400 13000 2.3 0      error (invalid witness file) .48 .32 11   39 error (invalid witness file) 6.5 3.4 120 300 - -
email_spec1_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6900 12000 2.3 0      error (invalid witness file) .52 .34 10   41 error (invalid witness file) 7.2 3.8 97 320 - -
email_spec1_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6000 12000 2.3 0      error (invalid witness file) .61 .38 9.1 40 error (invalid witness file) 6.3 3.4 120 300 - -
email_spec1_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   7000 12000 2.3 0      error (invalid witness file) .52 .34 13   40 error (invalid witness file) 6.1 3.2 97 290 - -
email_spec1_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6700 11000 2.3 0      error (invalid witness file) .51 .34 11   40 error (invalid witness file) 6.3 3.3 97 310 - -
email_spec1_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   380   6200 13000 2.3 0      error (invalid witness file) .51 .33 4.0 41 error (invalid witness file) 7.7 4.0 150 340 - -
email_spec27_product17_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6400 12000 2.3 0      error (invalid witness file) .50 .31 11   39 error (invalid witness file) 6.4 3.4 100 300 - -
email_spec27_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   8300 13000 2.3 0      error (invalid witness file) .56 .37 8.2 39 error (invalid witness file) 5.9 3.2 120 300 - -
email_spec27_product19_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   480   7700 13000 2.3 0      error (invalid witness file) .50 .34 6.6 41 error (invalid witness file) 5.7 3.1 120 290 - -
email_spec27_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   430   7200 13000 2.3 0      error (invalid witness file) .67 .41 5.3 41 error (invalid witness file) 5.7 3.1 110 290 - -
email_spec27_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   480   7300 10000 2.3 0      error (invalid witness file) .62 .39 11   42 error (invalid witness file) 5.6 3.0 100 290 - -
email_spec27_product25_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   460   7300 13000 2.3 0      error (invalid witness file) .55 .35 11   42 error (invalid witness file) 6.0 3.2 86 300 - -
email_spec27_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6300 13000 2.3 0      error (invalid witness file) .54 .35 12   39 error (invalid witness file) 6.2 3.2 110 290 - -
email_spec27_product29_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   6700 13000 2.3 0      error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.5 3.4 130 300 - -
email_spec27_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   8000 13000 2.3 0      error (invalid witness file) .57 .38 7.9 39 error (invalid witness file) 6.5 3.4 130 300 - -
email_spec27_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   8400 12000 2.3 0      error (invalid witness file) .54 .35 11   44 error (invalid witness file) 6.2 3.3 130 300 - -
email_spec27_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   6400 11000 2.3 0      error (invalid witness file) .53 .34 11   40 error (invalid witness file) 6.2 3.3 110 300 - -
email_spec27_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   420   7000 12000 2.3 0      error (invalid witness file) .53 .35 12   41 error (invalid witness file) 7.1 3.7 130 310 - -
email_spec27_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   450   7500 11000 2.3 0      error (invalid witness file) .54 .36 11   39 error (invalid witness file) 6.5 3.4 130 300 - -
email_spec27_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6200 13000 2.3 0      error (invalid witness file) .53 .33 9.4 41 error (invalid witness file) 6.4 3.4 130 300 - -
email_spec27_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   300   6000 13000 2.3 0      error (invalid witness file) .51 .34 9.9 40 error (invalid witness file) 7.0 3.6 110 310 - -
email_spec3_product13_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   380   6400 13000 2.3 0      error (invalid witness file) .53 .35 9.0 39 error (invalid witness file) 6.1 3.2 120 310 - -
email_spec3_product17_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   370   7000 14000 2.3 0      error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.3 3.3 120 300 - -
email_spec3_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   360   6400 13000 2.3 0      error (invalid witness file) .63 .40 6.9 40 error (invalid witness file) 6.8 3.6 110 320 - -
email_spec3_product19_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   6800 13000 2.3 0      error (invalid witness file) .63 .40 9.1 43 error (invalid witness file) 6.0 3.2 120 290 - -
email_spec3_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   360   6700 13000 2.3 0      error (invalid witness file) .63 .39 6.5 41 error (invalid witness file) 6.4 3.4 120 300 - -
email_spec3_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   5800 13000 2.3 0      error (invalid witness file) .56 .37 6.6 39 error (invalid witness file) 6.0 3.2 110 300 - -
email_spec3_product25_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   390   6800 13000 2.3 0      error (invalid witness file) .50 .34 12   39 error (invalid witness file) 5.9 3.2 110 300 - -
email_spec3_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   320   6600 13000 2.3 0      error (invalid witness file) .60 .38 8.1 40 error (invalid witness file) 6.7 3.5 120 310 - -
email_spec3_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   6300 13000 2.3 0      error (invalid witness file) .62 .39 7.7 41 error (invalid witness file) 6.4 3.4 86 300 - -
email_spec3_product29_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   6300 10000 2.3 0      error (invalid witness file) .52 .34 9.4 41 error (invalid witness file) 6.7 3.5 140 300 - -
email_spec3_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   420   6500 13000 2.3 0      error (invalid witness file) .47 .30 7.2 39 error (invalid witness file) 6.4 3.4 120 300 - -
email_spec3_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   430   6300 13000 2.3 0      error (invalid witness file) .48 .30 10   39 error (invalid witness file) 6.5 3.4 120 310 - -
email_spec3_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   460   7300 12000 2.3 0      error (invalid witness file) .68 .44 7.8 43 error (invalid witness file) 6.1 3.3 100 300 - -
email_spec3_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   6800 13000 2.3 0      error (invalid witness file) .47 .30 9.2 39 error (invalid witness file) 6.4 3.4 100 310 - -
email_spec3_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6800 13000 2.3 0      error (invalid witness file) .48 .32 8.8 41 error (invalid witness file) 6.1 3.2 110 300 - -
email_spec3_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   6700 13000 2.3 0      error (invalid witness file) .61 .40 6.0 40 error (invalid witness file) 6.5 3.4 100 310 - -
email_spec3_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   7200 13000 2.5 0      error (invalid witness file) .55 .35 12   43 error (invalid witness file) 6.0 3.2 110 300 - -
email_spec4_product18_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   470   7900 13000 2.3 0      error (invalid witness file) .56 .36 11   44 error (invalid witness file) 6.4 3.4 120 300 - -
email_spec4_product19_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   440   7700 13000 2.3 0      error (invalid witness file) .56 .34 11   43 error (invalid witness file) 6.1 3.2 110 300 - -
email_spec4_product23_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   7900 13000 2.3 0      error (invalid witness file) .62 .40 9.2 40 error (invalid witness file) 6.8 3.6 110 310 - -
email_spec4_product24_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   460   7400 13000 2.3 0      error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.2 3.3 120 300 - -
email_spec4_product25_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   470   7400 12000 2.3 0      error (invalid witness file) .60 .39 12   43 error (invalid witness file) 6.2 3.3 120 300 - -
email_spec4_product27_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   420   8000 14000 2.3 0      error (invalid witness file) .51 .34 9.4 41 error (invalid witness file) 6.6 3.5 120 310 - -
email_spec4_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   7100 13000 2.3 0      error (invalid witness file) .50 .33 9.1 40 error (invalid witness file) 6.3 3.4 140 300 - -
email_spec4_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6900 13000 2.3 0      error (invalid witness file) .53 .33 9.1 41 error (invalid witness file) 5.9 3.2 110 290 - -
email_spec4_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   430   6700 12000 2.3 0      error (invalid witness file) .53 .35 8.2 40 error (invalid witness file) 5.7 3.0 91 300 - -
email_spec4_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   6600 12000 2.3 .066  error (invalid witness file) .54 .34 12   43 error (invalid witness file) 6.5 3.4 130 300 - -
email_spec4_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6600 13000 2.3 0      error (invalid witness file) .53 .34 8.2 39 error (invalid witness file) 6.5 3.4 120 300 - -
email_spec4_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   7400 12000 2.3 0      error (invalid witness file) .49 .33 6.3 40 error (invalid witness file) 6.3 3.3 87 300 - -
email_spec4_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   360   5900 13000 2.3 0      error (invalid witness file) .54 .35 11   39 error (invalid witness file) 6.6 3.5 140 300 - -
email_spec6_product12_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   330   5800 14000 2.3 0      error (invalid witness file) .54 .35 11   41 error (invalid witness file) 5.9 3.2 120 290 - -
email_spec6_product14_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   340   5300 13000 2.3 0      error (invalid witness file) .56 .35 11   42 error (invalid witness file) 6.0 3.2 80 300 - -
email_spec6_product15_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   330   6500 14000 2.3 0      error (invalid witness file) .54 .36 11   40 error (invalid witness file) 6.2 3.3 93 310 - -
email_spec6_product16_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   360   6600 13000 2.3 0      error (invalid witness file) .54 .34 12   39 error (invalid witness file) 6.5 3.4 130 290 - -
email_spec6_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   340   6300 13000 2.3 0      error (invalid witness file) .51 .32 13   41 error (invalid witness file) 6.3 3.4 130 300 - -
email_spec6_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   340   6300 14000 2.3 0      error (invalid witness file) .51 .32 13   40 error (invalid witness file) 5.7 3.1 110 290 - -
email_spec6_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   330   5800 13000 2.3 0      error (invalid witness file) .49 .32 6.0 41 error (invalid witness file) 7.3 3.8 100 300 - -
email_spec6_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   5800 13000 2.3 0      error (invalid witness file) .51 .33 9.8 40 error (invalid witness file) 6.2 3.3 94 300 - -
email_spec6_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   350   6200 14000 2.3 0      error (invalid witness file) .57 .35 12   41 error (invalid witness file) 6.5 3.4 100 310 - -
email_spec6_product29_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6700 14000 2.3 0      error (invalid witness file) .61 .40 8.3 43 error (invalid witness file) 6.4 3.3 120 300 - -
email_spec6_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   340   5400 13000 2.3 0      error (invalid witness file) .65 .43 8.4 44 error (invalid witness file) 7.3 3.9 120 310 - -
email_spec6_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   6800 13000 2.3 0      error (invalid witness file) .52 .34 11   42 error (invalid witness file) 6.4 3.4 130 300 - -
email_spec6_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   360   6100 13000 2.3 0      error (invalid witness file) .49 .32 9.2 40 error (invalid witness file) 6.4 3.4 120 310 - -
email_spec6_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   380   6800 14000 2.3 0      error (invalid witness file) .53 .35 12   39 error (invalid witness file) 5.7 3.1 110 290 - -
email_spec6_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   370   6600 13000 2.3 0      error (invalid witness file) .52 .33 12   42 error (invalid witness file) 6.4 3.4 110 300 - -
email_spec6_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   7200 13000 2.3 0      error (invalid witness file) .52 .32 10   40 error (invalid witness file) 6.1 3.3 87 310 - -
email_spec6_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   350   6400 12000 2.3 0      error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.1 3.2 120 300 - -
email_spec7_product28_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   340   5700 13000 2.3 0      error (invalid witness file) .46 .29 4.6 39 error (invalid witness file) 7.9 4.2 77 290 - -
email_spec7_product29_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   410   7000 12000 2.3 0      error (invalid witness file) .51 .31 7.5 40 error (invalid witness file) 6.1 3.3 120 300 - -
email_spec7_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   380   6300 13000 2.3 0      error (invalid witness file) .49 .32 11   39 error (invalid witness file) 6.2 3.3 110 300 - -
email_spec7_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   6800 13000 2.3 0      error (invalid witness file) .66 .42 8.4 43 error (invalid witness file) 6.3 3.3 120 310 - -
email_spec7_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6300 13000 2.3 0      error (invalid witness file) .56 .36 12   40 error (invalid witness file) 6.2 3.3 120 300 - -
email_spec7_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6400 13000 2.3 0      error (invalid witness file) .52 .36 9.7 40 error (invalid witness file) 6.4 3.4 130 300 - -
email_spec7_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   7200 12000 2.3 0      error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.2 3.3 120 300 - -
email_spec7_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   350   6200 13000 2.3 0      error (invalid witness file) .55 .34 12   41 error (invalid witness file) 6.5 3.4 120 300 - -
email_spec7_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   390   6200 13000 2.3 0      error (invalid witness file) .50 .34 6.5 39 error (invalid witness file) 6.6 3.5 140 300 - -
email_spec8_product15_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   420   7100 13000 2.3 0      error (invalid witness file) .52 .34 6.1 39 error (invalid witness file) 6.5 3.4 140 310 - -
email_spec8_product16_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   7300 11000 2.3 0      error (invalid witness file) .56 .37 12   45 error (invalid witness file) 6.3 3.3 130 300 - -
email_spec8_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   460   7400 11000 2.3 0      error (invalid witness file) .57 .36 7.1 40 error (invalid witness file) 6.3 3.3 120 300 - -
email_spec8_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   6600 12000 2.3 0      error (invalid witness file) .47 .31 11   40 error (invalid witness file) 6.3 3.3 120 300 - -
email_spec8_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   7100 13000 2.3 0      error (invalid witness file) .52 .34 6.6 40 error (invalid witness file) 6.1 3.2 120 300 - -
email_spec8_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   440   7000 11000 2.3 0      error (invalid witness file) .49 .32 8.8 40 error (invalid witness file) 7.4 3.9 110 300 - -
email_spec8_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   420   6400 13000 2.3 0      error (invalid witness file) .47 .30 8.8 39 error (invalid witness file) 6.2 3.3 110 300 - -
email_spec8_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   430   7500 13000 2.3 0      error (invalid witness file) .51 .33 13   39 error (invalid witness file) 6.1 3.2 130 290 - -
email_spec8_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6400 13000 2.3 0      error (invalid witness file) .50 .31 10   40 error (invalid witness file) 6.2 3.3 120 300 - -
email_spec8_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   6800 12000 2.3 0      error (invalid witness file) .51 .33 9.3 41 error (invalid witness file) 7.6 3.9 140 320 - -
email_spec8_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   420   7000 13000 2.3 0      error (invalid witness file) .59 .36 9.1 42 error (invalid witness file) 6.4 3.4 110 300 - -
email_spec8_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   370   6000 13000 2.3 0      error (invalid witness file) .59 .37 9.6 40 error (invalid witness file) 6.4 3.4 110 300 - -
email_spec8_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6400 13000 2.3 0      error (invalid witness file) .54 .35 12   40 error (invalid witness file) 6.1 3.2 120 300 - -
email_spec9_product15_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   470   7500 13000 2.3 0      error (invalid witness file) .50 .31 10   42 error (invalid witness file) 6.3 3.3 120 300 - -
email_spec9_product16_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   450   7000 12000 2.3 0      error (invalid witness file) .52 .33 9.5 39 error (invalid witness file) 6.5 3.4 90 300 - -
email_spec9_product20_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   490   7900 11000 2.3 0      error (invalid witness file) .61 .39 8.3 39 error (invalid witness file) 6.2 3.3 96 300 - -
email_spec9_product21_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   6900 12000 2.3 0      error (invalid witness file) .58 .37 5.5 39 error (invalid witness file) 6.3 3.3 140 300 - -
email_spec9_product22_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   490   7700 11000 2.3 0      error (invalid witness file) .52 .35 10   40 error (invalid witness file) 7.0 3.6 140 320 - -
email_spec9_product26_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   8600 12000 2.3 0      error (invalid witness file) .52 .34 8.5 39 error (invalid witness file) 6.3 3.3 120 300 - -
email_spec9_product30_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   410   6700 11000 2.3 0      error (invalid witness file) .48 .32 7.8 40 error (invalid witness file) 6.6 3.5 130 300 - -
email_spec9_product31_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   6100 13000 2.3 0      error (invalid witness file) .54 .36 12   39 error (invalid witness file) 7.0 3.7 82 300 - -
email_spec9_product32_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   390   6500 12000 2.3 0      error (invalid witness file) .51 .33 9.3 40 error (invalid witness file) 6.0 3.2 110 300 - -
email_spec9_product33_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6000 13000 2.3 0      error (invalid witness file) .50 .32 5.0 41 error (invalid witness file) 5.8 3.1 120 290 - -
email_spec9_product34_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   400   6200 13000 2.3 0      error (invalid witness file) .55 .33 11   40 error (invalid witness file) 6.5 3.4 120 300 - -
email_spec9_product35_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   390   7100 13000 2.3 0      error (invalid witness file) .53 .35 14   40 error (invalid witness file) 6.4 3.4 140 300 - -
email_spec9_productSimulator_false-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   400   6300 13000 2.3 0      error (invalid witness file) .62 .40 4.6 39 error (invalid witness file) 7.3 3.8 140 320 - -
email_spec0_product05_true-unreach-call_true-termination.cil.c true 2 wit inspect 9.1 2.7 68 420 2.7 0      - - true 17    8.8  200   480 true 12   6.6 170 370
email_spec0_product09_true-unreach-call_true-termination.cil.c true 2 wit inspect 10   2.8 78 450 2.8 0      - - true 23    12    270   620 true 13   6.7 170 390
email_spec0_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect 10   2.8 81 440 2.8 0      - - true 18    9.2  260   520 true 14   7.1 280 390
email_spec0_product11_true-unreach-call_true-termination.cil.c true 2 wit inspect 11   3.1 85 500 2.9 0      - - true 18    9.4  330   520 true 15   8.0 270 450
email_spec0_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 12   3.4 100 500 3.0 0      - - true 24    12    290   630 true 20   10   300 610
email_spec0_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 14   3.8 99 560 3.0 0      - - true 23    12    270   630 true 23   12   390 580
email_spec0_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 14   3.6 100 540 3.1 0      - - true 31    16    320   670 true 19   10   310 600
email_spec0_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 16   3.9 120 560 3.1 0      - - true 27    14    510   680 true 22   12   330 620
email_spec0_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect 11   2.9 85 460 2.9 0      - - true 20    10    390   540 true 15   8.0 240 440
email_spec0_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect 22   5.5 170 630 2.9 0      - - true 24    12    230   510 true 33   17   560 700
email_spec0_product38_true-unreach-call_true-termination.cil.c true 2 wit inspect 12   3.3 93 550 3.0 0      - - true 22    11    380   650 true 17   9.0 210 510
email_spec0_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect 23   5.9 180 790 3.0 0      - - true 29    15    340   640 true 32   17   300 720
email_spec11_product03_true-unreach-call_true-termination.cil.c true 2 wit inspect 9.2 2.7 68 420 2.7 0      - - true 18    9.3  190   480 true 12   6.4 210 360
email_spec11_product07_true-unreach-call_true-termination.cil.c true 2 wit inspect 10   2.9 81 420 2.8 0      - - true 21    11    280   500 true 14   7.4 260 400
email_spec11_product08_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   3.5 110 520 2.8 0      - - true 18    9.4  310   510 true 21   11   420 590
email_spec11_product10_true-unreach-call_true-termination.cil.c true 2 wit inspect 9.7 2.7 71 440 2.8 0      - - true 15    7.7  210   470 true 14   7.4 270 400
email_spec11_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 15   4.0 110 620 2.9 0      - - true 20    10    330   530 true 23   12   240 600
email_spec11_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 15   4.0 110 590 3.0 0      - - true 26    14    310   640 true 23   12   240 670
email_spec11_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 14   3.8 99 610 3.0 0      - - true 25    13    340   650 true 21   11   200 590
email_spec11_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 15   3.9 110 640 3.1 0      - - true 28    14    500   640 true 22   11   270 620
email_spec11_product36_true-unreach-call_true-termination.cil.c true 2 wit inspect 11   2.9 80 430 2.9 0      - - true 25    13    200   520 true 14   7.4 210 410
email_spec11_product37_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   3.6 97 580 2.9 0      - - true 22    11    320   530 true 19   9.9 260 570
email_spec11_product39_true-unreach-call_true-termination.cil.c true 2 wit inspect 14   3.8 95 570 2.9 0      - - true 29    15    280   650 true 20   10   290 600
email_spec11_product40_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   3.7 100 540 3.0 0      - - true 26    13    400   640 true 21   11   380 540
email_spec1_product12_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   800   12000 6700 2.3 0      - - error (invalid witness file) .56 .36 9.5 39 error (invalid witness file) 7.5 3.9 92 300
email_spec1_product28_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   680   8500 8200 2.3 0      - - error (invalid witness file) .67 .42 6.6 40 error (invalid witness file) 6.2 3.2 88 310
email_spec27_product13_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   450   6700 13000 2.3 0      - - error (invalid witness file) .59 .38 9.1 40 error (invalid witness file) 6.5 3.4 110 290
email_spec27_product28_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 910   460   7300 12000 2.3 0      - - error (invalid witness file) .67 .45 8.2 40 error (invalid witness file) 6.6 3.5 120 300
email_spec4_product13_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   540   7300 12000 2.3 0      - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 7.0 3.7 130 320
email_spec4_product17_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   690   10000 8200 2.3 .0041 - - error (invalid witness file) .65 .42 8.7 41 error (invalid witness file) 5.8 3.1 86 290
email_spec4_product28_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   610   8400 9700 2.3 0      - - error (invalid witness file) .54 .34 11   39 error (invalid witness file) 6.2 3.3 110 300
email_spec4_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   590   9100 11000 2.3 0      - - error (invalid witness file) .56 .36 10   42 error (invalid witness file) 6.4 3.4 140 300
email_spec7_product13_true-unreach-call_true-termination.cil.c true 2 wit inspect 12   3.3 94 510 2.9 0      - - true 25    13    250   520 true 17   8.7 310 450
email_spec7_product17_true-unreach-call_true-termination.cil.c true 2 wit inspect 11   3.1 81 500 3.0 0      - - true 24    13    300   640 true 18   9.3 200 510
email_spec7_product18_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   3.7 100 540 2.9 0      - - true 19    9.8  300   530 true 26   13   260 590
email_spec7_product19_true-unreach-call_true-termination.cil.c true 2 wit inspect 11   3.1 83 520 3.0 0      - - true 27    14    270   560 true 17   9.1 310 470
email_spec7_product23_true-unreach-call_true-termination.cil.c true 2 wit inspect 14   3.7 100 590 3.0 0      - - true 23    12    470   670 true 20   10   200 560
email_spec7_product24_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   3.6 99 530 3.0 0      - - true 23    12    400   630 true 20   11   300 610
email_spec7_product25_true-unreach-call_true-termination.cil.c true 2 wit inspect 13   3.4 92 510 3.1 0      - - true 25    13    440   670 true 18   9.5 310 520
email_spec7_product27_true-unreach-call_true-termination.cil.c true 2 wit inspect 14   3.8 97 580 3.1 0      - - true 26    13    410   660 true 19   10   260 630
email_spec8_product12_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   810   11000 6800 2.3 0      - - error (invalid witness file) .68 .44 6.3 42 error (invalid witness file) 6.1 3.3 110 300
email_spec8_product14_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   470   8600 11000 2.3 0      - - error (invalid witness file) .64 .41 8.6 39 error (invalid witness file) 6.3 3.4 130 300
email_spec8_product28_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   680   10000 8500 2.3 0      - - error (invalid witness file) .63 .41 9.7 40 error (invalid witness file) 5.4 3.0 96 290
email_spec8_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   390   6300 13000 2.3 0      - - error (invalid witness file) .66 .43 9.0 40 error (invalid witness file) 6.0 3.2 120 290
email_spec9_product12_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   800   12000 7400 2.3 0      - - error (invalid witness file) .50 .33 9.4 40 error (invalid witness file) 5.9 3.1 83 300
email_spec9_product14_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   470   7300 11000 2.3 0      - - error (invalid witness file) .54 .35 11   42 error (invalid witness file) 6.4 3.4 120 320
email_spec9_product28_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   700   10000 8200 2.3 0      - - error (invalid witness file) .66 .41 11   43 error (invalid witness file) 6.3 3.3 85 310
email_spec9_product29_true-unreach-call_true-termination.cil.c timeout 0 wit inspect 900   380   6600 13000 2.3 0      - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 7.5 3.9 110 320
minepump_spec1_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 85 430 2.6 0      true 6.4  3.4  100   330 false(unreach-call) 9.8 5.2 180 340 - -
minepump_spec1_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 90 490 2.6 0      true 5.7  3.1  66   280 false(unreach-call) 8.8 4.8 110 340 - -
minepump_spec1_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 10   2.8 72 440 2.6 0      true 5.8  3.2  76   280 false(unreach-call) 9.6 5.1 130 340 - -
minepump_spec1_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 10   2.8 72 420 2.6 0      true 6.1  3.3  90   310 false(unreach-call) 11   5.8 190 370 - -
minepump_spec1_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 11   3.1 76 480 2.6 0      true 5.9  3.2  83   290 false(unreach-call) 12   6.5 200 370 - -
minepump_spec1_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12   3.3 99 490 2.6 0      true 5.8  3.1  76   280 false(unreach-call) 11   6.1 180 360 - -
minepump_spec1_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 11   3.1 88 450 2.6 0      true 6.2  3.3  90   320 false(unreach-call) 9.8 5.2 170 340 - -
minepump_spec1_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 10   2.9 76 450 2.6 0      true 6.0  3.2  100   290 false(unreach-call) 11   5.8 180 370 - -
minepump_spec1_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 11   3.1 88 470 2.6 0      true 6.9  3.7  89   310 false(unreach-call) 9.9 5.2 140 350 - -
minepump_spec1_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 14   4.0 120 510 2.6 0      true 6.4  3.4  120   310 false(unreach-call) 10   5.4 170 350 - -
minepump_spec1_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 14   3.9 120 560 2.6 0      true 7.3  3.9  88   320 false(unreach-call) 10   5.5 170 350 - -
minepump_spec1_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12   3.2 97 520 2.6 0      true 6.3  3.4  120   310 false(unreach-call) 12   6.5 230 410 - -
minepump_spec1_product49_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 11   3.1 89 480 2.6 0      true 5.9  3.2  65   290 false(unreach-call) 14   7.3 220 360 - -
minepump_spec1_product50_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 11   3.1 80 500 2.6 0      true 6.4  3.4  110   310 false(unreach-call) 10   5.4 180 340 - -
minepump_spec1_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 10   3.0 78 440 2.6 0      true 6.1  3.3  73   340 false(unreach-call) 9.7 5.2 170 340 - -
minepump_spec1_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.9 2.8 78 400 2.6 0      true 6.0  3.3  99   290 false(unreach-call) 10   5.5 180 360 - -
minepump_spec1_product53_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 83 520 2.6 0      true 6.2  3.3  71   320 false(unreach-call) 10   5.3 140 330 - -
minepump_spec1_product54_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 13   3.6 100 490 2.6 0      true 6.0  3.2  48   320 false(unreach-call) 13   6.8 200 370 - -
minepump_spec1_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12   3.1 100 500 2.6 0      true 6.0  3.2  78   290 false(unreach-call) 11   5.8 190 350 - -
minepump_spec1_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.7 2.8 68 410 2.6 0      true 5.9  3.2  78   290 false(unreach-call) 10   5.5 170 340 - -
minepump_spec1_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12   3.2 87 580 2.6 0      true 12    6.1  91   460 false(unreach-call) 16   8.4 210 420 - -
minepump_spec2_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12   3.3 80 500 2.6 0      true 6.4  3.4  110   310 false(unreach-call) 11   5.6 180 360 - -
minepump_spec2_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12   3.3 97 490 2.6 0      true 6.7  3.6  94   300 false(unreach-call) 17   9.1 280 420 - -
minepump_spec2_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 11   3.2 91 540 2.6 0      true 6.4  3.4  98   310 false(unreach-call) 14   7.8 200 400 - -
minepump_spec2_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 12   3.3 89 490 2.6 0      true 8.3  4.4  87   300 false(unreach-call) 11   6.1 190 430 - -
minepump_spec2_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 17   4.6 140 690 2.6 0      true 6.6  3.5  120   290 false(unreach-call) 17   9.1 180 450 - -
minepump_spec2_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 14   4.0 110 570 2.6 0      true 8.1  4.3  82   300 false(unreach-call) 11   5.7 180 350 - -
minepump_spec2_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 14   3.8 120 520 2.6 0      true 6.3  3.4  51   340 false(unreach-call) 14   7.5 130 430 - -
minepump_spec2_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 14   3.8 110 530 2.6 0      true 6.2  3.3  47   330 false(unreach-call) 12   6.5 150 430 - -
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 16   4.1 110 660 2.7 0      true 9.7  5.1  100   470 false(unreach-call) 14   7.1 180 440 - -
minepump_spec3_product01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.6 2.3 53 350 2.6 0      true 6.1  3.3  69   310 false(unreach-call) 9.7 5.2 160 340 - -
minepump_spec3_product02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.9 2.6 62 440 2.6 0      true 5.8  3.1  63   340 false(unreach-call) 9.7 5.2 180 340 - -
minepump_spec3_product03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.4 2.6 69 440 2.6 0      true 7.0  3.8  53   300 false(unreach-call) 11   5.9 140 340 - -
minepump_spec3_product04_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.3 2.7 71 450 2.6 0      true 6.0  3.2  100   300 false(unreach-call) 9.4 4.9 170 340 - -
minepump_spec3_product05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.7 2.6 62 430 2.6 0      true 5.5  3.0  96   290 false(unreach-call) 9.6 5.1 130 350 - -
minepump_spec3_product06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 9.4 2.6 75 430 2.6 0      true 5.9  3.2  83   300