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