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 inspect 6.1 2.0 57 350 .029 0      true 5.6  3.0  93   310 false(unreach-call) 13   7.0 230 400 - -
minepump_spec2_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.1 2.0 59 340 .029 0      true 5.5  3.0  85   290 false(unreach-call) 15   8.1 270 440 - -
minepump_spec2_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.6 2.1 55 380 .029 0      true 6.2  3.4  110   320 false(unreach-call) 14   7.3 230 410 - -
minepump_spec2_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.8 2.1 55 360 .029 0      true 6.1  3.3  96   320 false(unreach-call) 16   8.3 280 420 - -
minepump_spec2_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.5 2.3 55 470 .037 0      true 6.3  3.4  130   320 false(unreach-call) 16   8.5 290 550 - -
minepump_spec2_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.7 2.3 65 460 .037 0      true 6.4  3.4  120   330 false(unreach-call) 20   11   210 560 - -
minepump_spec2_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.2 2.5 72 460 .037 0      true 6.1  3.3  120   290 false(unreach-call) 18   9.5 240 520 - -
minepump_spec2_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.1 2.5 66 460 .037 0      true 5.9  3.2  81   310 false(unreach-call) 19   10   260 560 - -
minepump_spec2_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 14   3.8 110 690 .037 0      true 12    6.2  190   470 true 8.5 4.6 170 310 - -
minepump_spec3_product01_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.8 40 300 .016 0      true 5.1  2.8  81   280 false(unreach-call) 9.0 4.8 150 330 - -
minepump_spec3_product02_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 1.7 41 310 .016 0      true 5.4  2.9  76   320 false(unreach-call) 9.2 4.9 180 320 - -
minepump_spec3_product03_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.7 46 300 .016 0      true 5.1  2.8  94   290 false(unreach-call) 8.9 4.7 200 320 - -
minepump_spec3_product04_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.8 36 300 .016 0      true 6.6  3.6  53   290 false(unreach-call) 9.0 4.8 160 330 - -
minepump_spec3_product05_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.8 1.7 38 300 .016 0      true 6.2  3.4  46   310 false(unreach-call) 8.8 4.7 180 330 - -
minepump_spec3_product06_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.6 1.7 40 300 .016 0      true 6.6  3.5  89   330 false(unreach-call) 8.5 4.6 160 320 - -
minepump_spec3_product07_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.8 39 300 .016 0      true 5.3  2.9  89   280 false(unreach-call) 8.6 4.6 170 330 - -
minepump_spec3_product08_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 1.7 42 290 .016 0      true 5.3  2.9  67   310 false(unreach-call) 9.2 4.9 170 330 - -
minepump_spec3_product09_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 2.0 40 310 .016 8.0    true 5.3  2.9  98   290 false(unreach-call) 9.9 5.2 130 330 - -
minepump_spec3_product10_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.6 1.7 38 290 .016 0      true 4.9  2.6  38   290 false(unreach-call) 8.2 4.4 160 320 - -
minepump_spec3_product11_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.8 1.7 43 310 .016 0      true 5.9  3.2  66   310 false(unreach-call) 8.7 4.6 160 320 - -
minepump_spec3_product12_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 1.7 41 300 .016 0      true 5.9  3.2  55   290 false(unreach-call) 9.1 4.8 180 340 - -
minepump_spec3_product13_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.8 1.7 40 300 .016 0      true 5.7  3.1  97   320 false(unreach-call) 8.9 4.7 130 330 - -
minepump_spec3_product14_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.8 1.7 41 300 .016 0      true 5.6  3.0  55   330 false(unreach-call) 9.0 4.9 150 330 - -
minepump_spec3_product15_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.8 1.7 42 300 .016 0      true 5.8  3.1  130   330 false(unreach-call) 8.6 4.6 170 330 - -
minepump_spec3_product16_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 1.7 43 310 .016 0      true 5.3  2.9  100   310 false(unreach-call) 8.6 4.6 140 330 - -
minepump_spec3_product17_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 1.7 40 290 .016 0      true 5.4  2.9  82   290 false(unreach-call) 11   5.7 110 320 - -
minepump_spec3_product18_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.8 1.8 45 290 .016 .025  true 5.7  3.1  65   330 false(unreach-call) 8.7 4.6 170 310 - -
minepump_spec3_product19_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 1.7 40 290 .016 0      true 5.6  3.0  110   290 false(unreach-call) 11   5.6 130 330 - -
minepump_spec3_product20_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.6 1.7 37 290 .016 0      true 5.6  3.0  110   310 false(unreach-call) 9.1 4.8 180 320 - -
minepump_spec3_product21_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.8 1.7 41 300 .020 0      true 5.4  2.9  97   310 false(unreach-call) 11   6.1 200 370 - -
minepump_spec3_product22_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.8 39 300 .020 0      true 5.3  2.9  89   310 false(unreach-call) 8.7 4.7 160 330 - -
minepump_spec3_product23_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.8 40 300 .020 0      true 5.4  2.9  120   280 false(unreach-call) 9.5 5.0 190 330 - -
minepump_spec3_product24_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.1 1.9 42 310 .020 0      true 5.5  3.0  87   290 false(unreach-call) 11   5.9 210 350 - -
minepump_spec3_product25_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.0 1.8 46 300 .016 .22   true 5.3  2.9  89   310 false(unreach-call) 8.5 4.6 150 330 - -
minepump_spec3_product26_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.8 41 290 .016 0      true 5.1  2.8  88   280 false(unreach-call) 8.8 4.7 170 320 - -
minepump_spec3_product27_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.7 1.7 39 300 .016 0      true 5.9  3.1  140   320 false(unreach-call) 8.9 4.7 180 340 - -
minepump_spec3_product28_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.0 1.8 46 330 .016 0      true 5.6  3.0  74   330 false(unreach-call) 9.1 4.8 180 310 - -
minepump_spec3_product29_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.5 2.0 44 300 .020 0      true 5.6  3.0  100   320 false(unreach-call) 10   5.4 170 350 - -
minepump_spec3_product30_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.6 1.7 39 290 .020 0      true 5.5  3.0  88   290 false(unreach-call) 8.9 4.8 170 330 - -
minepump_spec3_product31_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.0 1.7 48 300 .020 0      true 5.7  3.1  80   310 false(unreach-call) 9.1 4.9 160 330 - -
minepump_spec3_product32_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.7 43 300 .020 0      true 5.4  2.9  70   290 false(unreach-call) 8.8 4.7 170 320 - -
minepump_spec3_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.1 1.8 45 300 .016 0      true 6.3  3.4  97   320 false(unreach-call) 9.7 5.2 210 360 - -
minepump_spec3_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.4 1.8 39 300 .016 0      true 6.2  3.3  86   340 false(unreach-call) 11   5.7 140 370 - -
minepump_spec3_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.1 1.8 43 300 .016 0      true 5.6  3.1  61   310 false(unreach-call) 9.5 5.1 170 320 - -
minepump_spec3_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.3 1.8 41 310 .016 0      true 5.7  3.1  83   310 false(unreach-call) 8.6 4.6 150 320 - -
minepump_spec3_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.2 1.8 46 310 .016 0      true 6.2  3.3  72   280 false(unreach-call) 9.4 5.0 150 350 - -
minepump_spec3_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.6 1.9 45 310 .016 0      true 5.4  2.9  69   290 false(unreach-call) 10   5.3 170 360 - -
minepump_spec3_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 4.9 1.8 43 290 .016 0      true 5.5  3.0  44   310 false(unreach-call) 9.7 5.2 200 320 - -
minepump_spec3_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.6 1.9 43 310 .016 0      true 7.7  4.1  75   330 false(unreach-call) 8.9 4.8 160 330 - -
minepump_spec3_product51_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.7 1.9 47 320 .016 2.3    true 5.6  3.0  100   290 false(unreach-call) 11   5.6 200 360 - -
minepump_spec3_product52_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.3 1.8 46 320 .016 0      true 5.9  3.2  120   290 false(unreach-call) 9.4 5.1 140 330 - -
minepump_spec3_product55_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.6 1.9 43 310 .016 0      true 6.0  3.2  81   330 false(unreach-call) 9.3 4.9 200 330 - -
minepump_spec3_product56_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.4 1.8 40 320 .016 .0082 true 7.4  4.0  72   320 false(unreach-call) 10   5.4 190 360 - -
minepump_spec3_product59_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.7 2.0 44 320 .016 0      true 5.7  3.1  110   290 false(unreach-call) 9.9 5.3 200 350 - -
minepump_spec3_product60_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.4 1.9 43 300 .016 0      true 6.9  3.7  93   330 false(unreach-call) 8.9 4.7 170 330 - -
minepump_spec3_product63_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.4 1.8 42 310 .016 0      true 6.3  3.4  100   300 false(unreach-call) 9.9 5.3 180 340 - -
minepump_spec3_product64_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 5.4 1.9 42 300 .016 .0082 true 6.4  3.4  120   310 false(unreach-call) 9.4 5.1 180 340 - -
minepump_spec3_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.3 2.0 48 350 .025 0      true 11    5.9  140   500 false(unreach-call) 12   6.5 140 360 - -
minepump_spec4_product33_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.1 2.0 47 330 .033 0      true 7.1  3.8  110   350 false(unreach-call) 14   7.7 270 430 - -
minepump_spec4_product34_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.3 2.1 57 340 .033 0      true 5.5  3.0  67   280 false(unreach-call) 14   7.3 170 450 - -
minepump_spec4_product35_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.3 2.1 58 340 .033 0      true 5.9  3.1  90   290 false(unreach-call) 19   10   230 490 - -
minepump_spec4_product36_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.5 2.2 47 350 .033 0      true 5.8  3.1  89   320 false(unreach-call) 16   8.5 310 520 - -
minepump_spec4_product37_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.1 2.5 65 420 .033 .0041 true 5.8  3.2  120   310 false(unreach-call) 14   7.7 210 420 - -
minepump_spec4_product38_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.8 2.3 65 460 .033 0      true 6.1  3.3  75   340 false(unreach-call) 14   7.6 220 400 - -
minepump_spec4_product39_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.7 2.3 68 470 .037 0      true 6.2  3.4  130   310 false(unreach-call) 16   8.5 240 530 - -
minepump_spec4_product40_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.6 2.5 68 460 .033 0      true 5.8  3.2  68   300 false(unreach-call) 17   9.2 240 570 - -
minepump_spec4_product41_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.7 2.2 58 340 .033 0      true 5.7  3.1  86   290 false(unreach-call) 13   7.1 230 450 - -
minepump_spec4_product42_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.6 2.0 52 360 .033 0      true 5.8  3.1  77   320 false(unreach-call) 14   7.4 200 400 - -
minepump_spec4_product43_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.9 2.2 53 370 .033 0      true 6.2  3.3  110   320 false(unreach-call) 16   8.4 260 470 - -
minepump_spec4_product44_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.6 2.1 49 360 .033 0      true 6.0  3.2  70   310 false(unreach-call) 16   8.8 350 560 - -
minepump_spec4_product45_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.7 2.1 58 380 .037 0      true 6.1  3.3  66   310 false(unreach-call) 18   9.8 290 540 - -
minepump_spec4_product46_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 6.6 2.2 60 380 .037 0      true 6.4  3.4  140   320 false(unreach-call) 14   7.6 210 430 - -
minepump_spec4_product47_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 7.2 2.3 52 410 .037 7.9    true 6.0  3.2  110   290 false(unreach-call) 17   9.2 250 570 - -
minepump_spec4_product48_false-unreach-call_false-termination.cil.c false(unreach-call) 1 wit inspect 8.3 2.5 69 460 .037 0      true 6.3  3.4  120   310 false(unreach-call) 18   9.8 260 550 - -
minepump_spec4_productSimulator_false-unreach-call_false-termination.cil.c false(unreach-call) 0 wit inspect 18   4.7 140 690 .049 0      true 12    6.3  140   490 true 9.1 5.0 190 330 - -
minepump_spec1_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 34 290 0     0      - - out of memory 390    370    8700   7000 true 13   6.9 170 370
minepump_spec1_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.9 1.5 33 290 0     0      - - out of memory 360    350    8100   7000 true 12   6.5 250 350
minepump_spec1_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.9 1.5 35 280 0     0      - - out of memory 360    340    6900   7000 true 10   5.6 200 360
minepump_spec1_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 35 280 0     0      - - out of memory 330    310    7500   7000 true 9.1 4.9 140 340
minepump_spec1_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 33 290 0     0      - - out of memory 330    320    7300   7000 true 10   5.6 210 360
minepump_spec1_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.5 34 290 0     0      - - out of memory 310    300    6100   7000 true 11   6.1 200 370
minepump_spec1_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 36 280 0     0      - - out of memory 300    290    7300   7000 true 10   5.5 150 360
minepump_spec1_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.5 33 290 0     0      - - out of memory 330    310    5400   7000 true 9.7 5.3 190 350
minepump_spec1_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.6 35 280 0     0      - - out of memory 420    400    8000   7000 true 13   7.3 180 360
minepump_spec1_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 34 290 0     0      - - out of memory 370    360    7300   7000 true 12   6.3 230 370
minepump_spec1_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.5 36 290 0     0      - - out of memory 340    320    7200   7000 true 12   6.2 180 360
minepump_spec1_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 36 280 0     0      - - out of memory 360    340    6300   7000 true 9.7 5.2 190 350
minepump_spec1_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.5 38 290 0     0      - - out of memory 360    340    5900   7000 true 9.9 5.3 200 360
minepump_spec1_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.5 35 290 0     0      - - out of memory 330    310    6800   7000 true 10   5.6 210 350
minepump_spec1_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 36 290 0     0      - - out of memory 310    300    7000   7000 true 13   6.9 110 360
minepump_spec1_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 34 290 0     0      - - out of memory 310    300    6000   7000 true 9.8 5.2 190 360
minepump_spec1_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 36 290 0     0      - - out of memory 620    600    12000   7000 true 11   6.1 170 360
minepump_spec1_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 31 290 0     8.0    - - out of memory 470    450    8600   7000 true 11   6.1 240 370
minepump_spec1_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 36 290 0     8.0    - - out of memory 370    350    9700   7000 true 12   6.3 160 360
minepump_spec1_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 39 290 0     0      - - out of memory 470    460    8400   7000 true 9.1 4.9 170 340
minepump_spec1_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 36 290 0     0      - - out of memory 390    370    8000   7000 true 10   5.6 200 360
minepump_spec1_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.7 36 300 0     8.2    - - out of memory 510    500    11000   7000 true 12   6.3 200 370
minepump_spec1_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.5 1.6 36 290 0     0      - - out of memory 400    380    7400   7000 true 11   5.8 190 360
minepump_spec1_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 38 290 0     0      - - out of memory 360    340    10000   7000 true 9.5 5.1 200 350
minepump_spec1_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.5 32 290 0     0      - - out of memory 540    520    13000   7000 true 11   6.1 180 360
minepump_spec1_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 40 290 0     2.1    - - out of memory 430    420    10000   7000 true 11   5.7 190 350
minepump_spec1_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 33 290 0     0      - - out of memory 420    400    8700   7000 true 10   5.6 180 360
minepump_spec1_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 37 280 0     0      - - out of memory 410    390    11000   7000 true 12   6.5 120 360
minepump_spec1_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 37 290 0     0      - - out of memory 390    370    7100   7000 true 11   6.0 230 360
minepump_spec1_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 33 280 0     0      - - out of memory 610    590    12000   7000 true 11   6.1 230 360
minepump_spec1_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.8 1.8 38 290 0     0      - - out of memory 360    350    6800   7000 true 11   6.0 210 360
minepump_spec1_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 34 280 0     0      - - out of memory 370    360    9200   7000 true 9.4 5.1 190 360
minepump_spec1_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.2 1.8 42 290 0     0      - - out of memory 350    340    7000   7000 true 22   12   310 550
minepump_spec1_product46_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.5 1.8 51 300 0     0      - - out of memory 300    290    7900   7000 true 30   17   310 690
minepump_spec1_product47_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.7 1.9 45 310 0     0      - - out of memory 390    370    8800   7000 true 19   10   280 550
minepump_spec1_product48_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.9 1.9 50 350 0     0      - - out of memory 410    390    8000   7000 true 24   13   420 660
minepump_spec1_product57_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.5 1.9 50 310 0     0      - - out of memory 620    610    11000   7000 true 25   14   500 640
minepump_spec1_product58_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.9 1.9 43 320 0     0      - - out of memory 590    570    11000   7000 true 33   18   490 660
minepump_spec1_product59_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.8 1.9 49 320 0     0      - - out of memory 580    570    9700   7000 true 24   13   490 630
minepump_spec1_product60_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.4 2.0 52 350 0     0      - - out of memory 660    640    12000   7000 true 26   14   450 630
minepump_spec1_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.7 1.9 46 310 0     0      - - out of memory 360    340    5500   7000 true 27   15   440 680
minepump_spec1_product62_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.3 2.1 52 300 0     0      - - out of memory 370    350    7200   7000 true 26   14   460 560
minepump_spec1_product63_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.0 2.0 55 310 0     0      - - out of memory 420    400    9100   7000 true 27   15   490 660
minepump_spec1_product64_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.2 2.0 58 360 0     0      - - out of memory 450    440    8900   7000 true 27   15   610 680
minepump_spec2_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.0 1.7 43 300 0     0      - - out of memory 830    800    20000   7000 true 14   7.9 230 490
minepump_spec2_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.8 1.7 39 290 0     0      - - timeout 910    880    17000   6900 true 14   7.5 210 500
minepump_spec2_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.2 1.8 47 290 0     0      - - timeout 910    890    16000   6400 true 9.7 5.2 160 360
minepump_spec2_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.2 1.8 44 300 0     0      - - timeout 910    890    14000   5500 true 10   5.4 190 360
minepump_spec2_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.9 1.7 40 290 0     0      - - out of memory 360    340    6500   7000 true 13   6.9 130 360
minepump_spec2_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.1 1.8 46 290 0     0      - - out of memory 360    350    6100   7000 true 10   5.6 210 370
minepump_spec2_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.3 1.8 40 300 0     0      - - out of memory 300    280    7800   7000 true 9.7 5.2 160 360
minepump_spec2_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.8 1.9 49 310 0     0      - - out of memory 360    340    5700   7000 true 10   5.6 170 360
minepump_spec2_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.4 1.9 48 300 0     0      - - timeout 910    880    24000   6700 true 16   8.5 200 490
minepump_spec2_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.1 1.7 40 290 0     0      - - timeout 910    880    19000   7000 true 14   7.8 280 500
minepump_spec2_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.4 1.9 42 290 0     0      - - timeout 910    890    18000   5900 true 11   6.2 140 350
minepump_spec2_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.0 1.7 42 300 0     0      - - timeout 910    890    17000   5300 true 10   5.4 180 350
minepump_spec2_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.0 1.7 44 290 0     0      - - out of memory 360    340    6300   7000 true 11   5.8 180 360
minepump_spec2_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.3 1.8 42 290 0     0      - - out of memory 290    280    8500   7000 true 11   5.9 190 370
minepump_spec2_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.3 1.8 45 300 0     0      - - out of memory 320    310    6800   7000 true 10   5.5 180 350
minepump_spec2_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.5 1.9 43 330 0     0      - - out of memory 330    310    5900   7000 true 9.9 5.3 180 360
minepump_spec2_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.2 1.8 42 300 0     0      - - out of memory 510    490    11000   7000 true 11   5.8 200 360
minepump_spec2_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.1 2.0 51 320 0     0      - - out of memory 490    470    8200   7000 true 10   5.6 200 360
minepump_spec2_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.3 1.8 44 300 0     0      - - out of memory 440    420    9000   7000 true 8.8 4.8 130 350
minepump_spec2_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.2 2.0 51 330 0     0      - - out of memory 520    500    10000   7000 true 10   5.4 150 350
minepump_spec2_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.1 1.8 44 290 0     0      - - out of memory 400    390    9100   7000 true 11   5.9 190 360
minepump_spec2_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.6 1.8 46 300 0     .0041 - - out of memory 450    440    13000   7000 true 13   7.0 180 360
minepump_spec2_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.5 1.8 45 300 0     .045  - - out of memory 390    370    7600   7000 true 10   5.5 180 360
minepump_spec2_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.3 2.0 47 340 0     0      - - out of memory 370    350    6800   7000 true 10   5.5 190 360
minepump_spec2_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.3 1.8 45 290 0     .020  - - out of memory 520    510    8800   7000 true 11   6.1 160 360
minepump_spec2_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.7 1.8 47 300 0     0      - - out of memory 540    520    13000   7000 true 11   5.9 200 370
minepump_spec2_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.4 1.8 45 300 0     0      - - out of memory 460    440    9600   7000 true 11   5.7 210 370
minepump_spec2_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.0 1.9 47 330 0     0      - - out of memory 410    390    12000   7000 true 11   5.6 160 360
minepump_spec2_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.6 1.8 51 300 0     0      - - out of memory 440    420    7700   7000 true 11   6.0 220 360
minepump_spec2_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.5 1.8 47 310 0     0      - - out of memory 370    350    9900   7000 true 16   8.4 180 370
minepump_spec2_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.5 1.9 43 300 0     0      - - out of memory 330    320    8800   7000 true 13   6.7 140 350
minepump_spec2_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.9 2.0 47 350 0     0      - - out of memory 320    310    11000   7000 true 12   6.4 190 350
minepump_spec2_product37_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.3 2.0 58 340 0     0      - - out of memory 390    370    7700   7000 true 21   11   360 590
minepump_spec2_product38_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.5 2.1 56 360 0     0      - - out of memory 360    340    9300   7000 true 21   11   250 570
minepump_spec2_product39_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.9 2.2 56 380 0     0      - - out of memory 480    460    7900   7000 true 22   11   410 560
minepump_spec2_product40_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.8 2.1 51 410 0     0      - - out of memory 460    450    10000   7000 true 22   12   390 550
minepump_spec2_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.7 2.1 59 430 0     0      - - out of memory 350    330    6300   7000 true 23   13   390 600
minepump_spec2_product46_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.6 2.3 61 450 0     0      - - out of memory 370    350    6500   7000 true 27   15   560 650
minepump_spec2_product47_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.9 2.1 63 410 0     0      - - out of memory 340    320    8500   7000 true 25   14   290 600
minepump_spec2_product48_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.8 2.4 62 450 0     0      - - out of memory 410    400    11000   7000 true 25   14   370 610
minepump_spec2_product49_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.2 2.0 51 360 0     0      - - out of memory 590    580    14000   7000 true 26   14   520 600
minepump_spec2_product50_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.8 2.1 54 390 0     0      - - out of memory 710    690    12000   7000 true 24   13   360 730
minepump_spec2_product51_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.9 2.2 56 420 0     0      - - out of memory 630    610    13000   7000 true 26   14   560 680
minepump_spec2_product52_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.1 2.2 55 440 0     0      - - out of memory 680    660    15000   7000 true 26   14   370 680
minepump_spec2_product53_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.3 2.0 49 370 0     0      - - out of memory 370    350    9300   7000 true 23   13   340 630
minepump_spec2_product54_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.8 2.1 50 400 0     0      - - out of memory 360    340    7200   7000 true 26   14   320 640
minepump_spec2_product55_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.7 2.1 55 390 0     0      - - out of memory 420    400    8400   7000 true 23   12   350 570
minepump_spec2_product56_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.1 2.2 59 450 0     0      - - out of memory 560    540    9700   7000 true 25   13   340 590
minepump_spec2_product57_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.0 2.1 56 440 0     0      - - out of memory 550    540    11000   7000 true 33   18   460 750
minepump_spec2_product58_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.1 2.4 61 440 0     0      - - out of memory 590    580    12000   7000 true 26   14   370 670
minepump_spec2_product59_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.5 2.5 57 450 0     8.2    - - out of memory 610    590    10000   7000 true 34   19   640 740
minepump_spec2_product60_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.9 2.7 67 440 0     .0041 - - out of memory 760    740    12000   7000 true 33   18   660 730
minepump_spec2_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.6 2.3 55 440 0     0      - - out of memory 350    340    5500   7000 true 23   13   410 610
minepump_spec2_product62_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.8 2.6 74 450 0     0      - - out of memory 320    300    9700   7000 true 23   13   480 600
minepump_spec2_product63_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.3 2.2 62 450 0     0      - - out of memory 410    390    9400   7000 true 25   14   460 650
minepump_spec2_product64_true-unreach-call_false-termination.cil.c true 2 wit inspect 10   3.1 81 450 0     2.3    - - out of memory 350    320    6000   7000 true 32   17   350 630
minepump_spec3_product33_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.3 2.1 50 320 0     0      - - out of memory 340    320    6900   7000 true 15   8.0 310 470
minepump_spec3_product34_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.7 1.9 53 300 0     8.1    - - out of memory 390    380    6000   7000 true 13   7.2 240 490
minepump_spec3_product37_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.5 2.1 52 330 0     0      - - out of memory 340    320    5700   7000 true 26   15   270 570
minepump_spec3_product38_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.2 2.0 50 310 0     0      - - out of memory 320    300    6400   7000 true 18   9.6 310 530
minepump_spec3_product41_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.3 2.0 60 300 0     0      - - out of memory 330    310    8800   7000 true 15   8.2 280 520
minepump_spec3_product42_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.3 2.0 48 310 0     0      - - out of memory 340    320    7200   7000 true 16   8.9 250 560
minepump_spec3_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.2 2.4 52 360 0     8.0    - - out of memory 310    300    9200   7000 true 22   12   250 540
minepump_spec3_product46_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.9 2.1 56 350 0     0      - - out of memory 340    320    7000   7000 true 23   13   250 580
minepump_spec3_product49_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.4 2.0 59 330 0     0      - - out of memory 380    360    13000   7000 true 24   13   360 600
minepump_spec3_product50_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.0 1.9 49 330 0     .0041 - - out of memory 450    440    8100   7000 true 24   13   420 540
minepump_spec3_product53_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.2 2.2 57 340 0     0      - - out of memory 390    370    14000   7000 true 24   13   470 610
minepump_spec3_product54_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.0 1.9 46 320 0     0      - - out of memory 430    410    13000   7000 true 28   15   430 650
minepump_spec3_product57_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.5 2.4 56 360 0     0      - - out of memory 600    580    10000   7000 true 28   16   620 640
minepump_spec3_product58_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.8 2.2 56 360 0     0      - - out of memory 550    530    9200   7000 true 34   19   510 660
minepump_spec3_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.1 2.2 56 400 0     0      - - out of memory 450    440    11000   7000 true 33   18   460 670
minepump_spec3_product62_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.5 2.3 65 410 0     0      - - out of memory 520    500    9800   7000 true 27   14   460 670
minepump_spec4_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.9 1.6 36 290 0     8.2    - - out of memory 350    330    8000   7000 true 10   5.6 180 360
minepump_spec4_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.9 1.5 33 280 0     0      - - out of memory 350    330    6800   7000 true 11   6.1 170 360
minepump_spec4_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 36 290 0     0      - - out of memory 350    330    6700   7000 true 11   5.9 180 360
minepump_spec4_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 33 280 0     0      - - out of memory 310    300    8400   7000 true 9.4 5.0 170 350
minepump_spec4_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.6 34 290 0     8.1    - - out of memory 310    300    8700   7000 true 13   7.0 240 360
minepump_spec4_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.5 35 290 0     0      - - out of memory 290    280    7800   7000 true 9.4 5.1 180 350
minepump_spec4_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 39 290 0     0      - - out of memory 320    310    4900   7000 true 13   7.5 240 490
minepump_spec4_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 36 290 0     0      - - out of memory 330    310    5500   7000 true 9.4 5.0 170 350
minepump_spec4_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect 3.9 1.5 34 290 0     0      - - out of memory 400    380    6500   7000 true 11   5.7 170 360
minepump_spec4_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 35 290 0     0      - - out of memory 380    370    6300   7000 true 12   6.6 130 360
minepump_spec4_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.5 36 280 0     0      - - out of memory 370    350    6200   7000 true 11   6.1 210 360
minepump_spec4_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.5 37 290 0     0      - - out of memory 320    310    7800   7000 true 9.7 5.2 210 350
minepump_spec4_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 35 290 0     0      - - out of memory 370    350    7100   7000 true 12   6.6 210 420
minepump_spec4_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 37 290 0     0      - - out of memory 320    300    8200   7000 true 9.9 5.4 180 350
minepump_spec4_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 38 290 0     0      - - out of memory 330    310    7100   7000 true 13   7.3 280 480
minepump_spec4_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 42 290 0     0      - - out of memory 290    280    7300   7000 true 10   5.5 180 350
minepump_spec4_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 36 290 0     0      - - out of memory 550    530    13000   7000 true 13   7.3 200 400
minepump_spec4_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 32 280 0     0      - - out of memory 510    490    14000   7000 true 12   6.4 140 450
minepump_spec4_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.6 1.7 38 290 0     0      - - out of memory 500    480    7800   7000 true 15   8.5 180 490
minepump_spec4_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 37 290 0     0      - - out of memory 450    430    7700   7000 true 9.9 5.3 210 360
minepump_spec4_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 36 300 0     0      - - out of memory 420    410    11000   7000 true 14   7.6 180 440
minepump_spec4_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 33 290 0     0      - - out of memory 480    460    9800   7000 true 14   8.0 180 480
minepump_spec4_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.6 1.7 42 290 0     0      - - out of memory 430    410    6400   7000 true 13   7.3 240 520
minepump_spec4_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 39 290 0     2.3    - - out of memory 310    290    11000   7000 true 9.8 5.3 180 360
minepump_spec4_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 37 300 0     8.0    - - out of memory 490    470    14000   7000 true 13   6.8 280 420
minepump_spec4_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.5 37 290 0     0      - - out of memory 540    520    13000   7000 true 13   6.9 240 390
minepump_spec4_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 42 290 0     0      - - out of memory 440    430    8600   7000 true 12   6.7 170 500
minepump_spec4_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 35 290 0     0      - - out of memory 390    380    7200   7000 true 9.1 5.0 170 350
minepump_spec4_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 40 290 0     0      - - out of memory 400    390    10000   7000 true 12   6.4 200 440
minepump_spec4_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 37 290 0     0      - - out of memory 510    490    11000   7000 true 12   6.7 250 470
minepump_spec4_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.5 1.6 35 290 0     0      - - out of memory 380    370    6900   7000 true 15   8.2 230 530
minepump_spec4_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.5 1.7 34 290 0     0      - - out of memory 420    400    6000   7000 true 9.9 5.3 190 350
minepump_spec4_product49_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.9 2.1 51 370 0     0      - - out of memory 370    360    13000   7000 true 24   14   420 640
minepump_spec4_product50_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.0 2.2 55 410 0     0      - - out of memory 480    460    7300   7000 true 30   17   430 660
minepump_spec4_product51_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.8 2.2 54 380 0     0      - - out of memory 490    470    9500   7000 true 34   19   430 730
minepump_spec4_product52_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.0 2.2 53 440 0     0      - - out of memory 540    520    11000   7000 true 26   15   470 620
minepump_spec4_product53_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.7 2.1 54 390 0     0      - - out of memory 390    380    8100   7000 true 21   12   290 630
minepump_spec4_product54_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.6 2.6 60 450 0     0      - - out of memory 430    410    9400   7000 true 26   14   280 680
minepump_spec4_product55_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.1 2.3 59 440 0     0      - - out of memory 500    480    9400   7000 true 35   20   480 720
minepump_spec4_product56_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.5 2.4 60 440 0     0      - - out of memory 470    440    8100   7000 true 29   16   380 740
minepump_spec4_product57_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.4 2.1 50 340 0     0      - - out of memory 360    340    7900   7000 true 32   18   680 720
minepump_spec4_product58_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.6 2.1 56 350 0     0      - - out of memory 430    410    7400   7000 true 34   19   320 750
minepump_spec4_product59_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.5 2.1 55 370 0     0      - - out of memory 510    500    11000   7000 true 34   19   500 710
minepump_spec4_product60_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.0 2.2 56 440 0     0      - - out of memory 470    450    12000   7000 true 31   17   400 690
minepump_spec4_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.6 2.1 49 400 0     0      - - out of memory 410    390    6700   7000 true 26   14   460 640
minepump_spec4_product62_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.1 2.2 58 410 0     0      - - out of memory 280    270    7300   7000 true 24   13   380 620
minepump_spec4_product63_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.6 2.3 59 460 0     0      - - out of memory 390    370    9900   7000 true 39   21   480 750
minepump_spec4_product64_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.1 2.4 62 440 0     0      - - out of memory 430    420    8000   7000 true 34   19   490 710
minepump_spec5_product01_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 33 290 0     0      - - true 10    5.4  93   300 true 11   6.2 180 350
minepump_spec5_product02_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 39 280 0     2.1    - - true 9.5  5.0  120   340 true 12   6.7 190 360
minepump_spec5_product03_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.6 33 290 0     0      - - true 9.9  5.3  130   310 true 10   5.6 160 350
minepump_spec5_product04_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.5 35 290 0     0      - - true 8.2  4.4  150   310 true 11   6.1 140 360
minepump_spec5_product05_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.5 31 290 0     0      - - true 10    5.6  120   330 true 12   6.4 200 360
minepump_spec5_product06_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 41 290 0     0      - - true 9.8  5.2  130   330 true 11   5.8 190 370
minepump_spec5_product07_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 41 290 0     0      - - true 11    5.6  110   340 true 11   5.8 200 350
minepump_spec5_product08_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 40 290 0     0      - - true 10    5.4  180   360 true 9.6 5.2 160 360
minepump_spec5_product09_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 38 290 0     0      - - true 8.1  4.3  150   310 true 11   5.9 220 370
minepump_spec5_product10_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.0 1.5 38 280 0     0      - - true 9.7  5.2  150   350 true 11   6.0 210 360
minepump_spec5_product11_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.5 1.6 38 300 0     0      - - true 12    6.0  100   370 true 10   5.5 230 350
minepump_spec5_product12_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.1 1.6 37 290 0     0      - - true 11    6.0  99   340 true 10   5.6 210 350
minepump_spec5_product13_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.7 39 300 0     8.1    - - true 8.0  4.2  58   330 true 12   6.5 150 360
minepump_spec5_product14_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 36 290 0     0      - - true 10    5.4  120   350 true 11   5.7 200 360
minepump_spec5_product15_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.6 1.6 36 290 0     0      - - true 9.1  4.8  170   340 true 11   5.9 190 370
minepump_spec5_product16_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.5 1.6 44 290 0     0      - - true 11    5.8  120   350 true 9.8 5.3 160 360
minepump_spec5_product17_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 36 290 0     0      - - true 9.1  4.7  170   340 true 11   5.8 170 360
minepump_spec5_product18_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 32 290 0     0      - - true 11    5.9  130   360 true 13   6.7 190 360
minepump_spec5_product19_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.5 1.6 41 290 0     0      - - true 9.8  5.2  170   390 true 11   6.1 210 360
minepump_spec5_product20_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.5 1.7 37 290 0     0      - - true 13    6.7  110   360 true 10   5.4 140 350
minepump_spec5_product21_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 40 290 0     0      - - true 11    5.8  150   410 true 10   5.5 200 360
minepump_spec5_product22_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.6 1.7 39 280 0     0      - - true 9.9  5.2  180   410 true 10   5.6 220 370
minepump_spec5_product23_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.8 1.7 38 290 0     0      - - true 10    5.4  200   390 true 11   6.1 210 370
minepump_spec5_product24_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 38 290 0     0      - - true 12    6.0  160   440 true 11   5.7 200 350
minepump_spec5_product25_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.2 1.5 35 290 0     0      - - true 10    5.4  130   340 true 11   5.8 210 360
minepump_spec5_product26_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 38 290 0     .0041 - - true 12    6.3  130   390 true 10   5.5 160 370
minepump_spec5_product27_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.8 1.7 37 290 0     0      - - true 9.7  5.1  180   370 true 11   5.9 210 370
minepump_spec5_product28_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 36 290 0     0      - - true 11    6.0  120   350 true 13   7.1 120 360
minepump_spec5_product29_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 40 290 0     0      - - true 11    5.9  150   390 true 11   5.8 130 370
minepump_spec5_product30_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.3 1.6 36 290 0     0      - - true 12    6.4  140   390 true 11   5.9 190 360
minepump_spec5_product31_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.7 1.7 46 290 0     0      - - true 12    6.0  130   430 true 11   5.9 200 370
minepump_spec5_product32_true-unreach-call_false-termination.cil.c true 2 wit inspect 4.4 1.6 38 290 0     0      - - true 12    6.2  130   420 true 11   5.7 200 350
minepump_spec5_product33_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.0 1.9 47 310 0     0      - - timeout 900    890    20000   5600 true 23   13   420 580
minepump_spec5_product34_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.8 1.9 51 300 0     0      - - timeout 910    890    19000   6500 true 27   15   280 500
minepump_spec5_product35_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.5 2.1 59 320 0     0      - - timeout 900    890    19000   4900 true 21   11   350 540
minepump_spec5_product36_true-unreach-call_false-termination.cil.c true 2 wit inspect 11   3.1 76 440 0     0      - - timeout 900    890    15000   4900 true 31   17   440 640
minepump_spec5_product37_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.7 2.1 58 390 0     0      - - out of memory 830    810    18000   7000 true 27   15   310 740
minepump_spec5_product38_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.0 2.2 61 380 0     0      - - timeout 900    880    16000   6700 true 34   19   430 660
minepump_spec5_product39_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.8 2.2 56 360 0     0      - - timeout 910    890    16000   6100 true 28   15   370 600
minepump_spec5_product40_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.8 2.3 66 440 0     0      - - timeout 900    890    20000   6100 true 36   19   470 700
minepump_spec5_product41_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.7 1.9 48 300 0     0      - - timeout 910    890    17000   6000 true 24   13   400 580
minepump_spec5_product42_true-unreach-call_false-termination.cil.c true 2 wit inspect 5.7 1.9 45 310 0     0      - - timeout 910    890    17000   6500 true 24   13   420 580
minepump_spec5_product43_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.0 2.0 50 330 0     0      - - timeout 910    890    17000   6400 true 26   14   410 540
minepump_spec5_product44_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.7 2.1 53 380 0     0      - - timeout 910    890    17000   5600 true 31   17   250 710
minepump_spec5_product45_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.7 2.1 55 350 0     0      - - timeout 900    890    24000   6900 true 38   21   590 750
minepump_spec5_product46_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.3 2.1 48 380 0     8.0    - - out of memory 890    870    17000   7000 true 36   20   540 750
minepump_spec5_product47_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.8 2.2 60 390 0     .033  - - timeout 900    890    16000   5700 true 39   22   680 740
minepump_spec5_product48_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.0 2.2 50 410 0     0      - - timeout 900    890    27000   6500 true 43   24   850 760
minepump_spec5_product49_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.0 2.1 58 390 0     0      - - timeout 910    880    17000   6700 true 35   19   550 680
minepump_spec5_product50_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.8 2.1 53 390 0     0      - - out of memory 850    830    20000   7000 true 35   19   630 670
minepump_spec5_product51_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.1 2.2 53 380 0     0      - - timeout 910    880    17000   6700 true 41   23   570 740
minepump_spec5_product52_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.4 2.5 62 440 0     0      - - timeout 900    890    19000   6000 true 44   24   390 730
minepump_spec5_product53_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.5 2.3 66 390 0     .0041 - - out of memory 650    630    14000   7000 true 36   20   500 700
minepump_spec5_product54_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.4 2.3 59 400 0     0      - - out of memory 690    670    15000   7000 true 42   23   480 700
minepump_spec5_product55_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.4 2.3 60 380 0     0      - - timeout 900    890    21000   7000 true 31   17   520 740
minepump_spec5_product56_true-unreach-call_false-termination.cil.c true 2 wit inspect 8.1 2.4 60 440 0     0      - - timeout 900    880    15000   6200 true 35   19   530 740
minepump_spec5_product57_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.5 2.1 59 380 0     0      - - timeout 910    890    18000   6800 true 38   21   700 730
minepump_spec5_product58_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.9 2.1 55 390 0     0      - - timeout 900    890    23000   6800 true 37   21   700 720
minepump_spec5_product59_true-unreach-call_false-termination.cil.c true 2 wit inspect 9.2 2.7 72 460 0     0      - - timeout 910    890    16000   6500 true 43   23   540 740
minepump_spec5_product60_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.7 2.3 64 450 0     0      - - timeout 910    880    17000   6400 true 42   23   620 720
minepump_spec5_product61_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.6 2.1 59 410 0     0      - - out of memory 870    850    16000   7000 true 42   24   420 810
minepump_spec5_product62_true-unreach-call_false-termination.cil.c true 2 wit inspect 6.9 2.1 62 410 0     0      - - out of memory 740    720    13000   7000 true 43   25   620 780
minepump_spec5_product63_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.0 2.2 57 440 0     0      - - timeout 910    880    18000   6400 true 41   23   620 780
minepump_spec5_product64_true-unreach-call_false-termination.cil.c true 2 wit inspect 7.5 2.3 64 440 0     0      - - out of memory 820    800    19000   7000 true 42   24   640 860
minepump_spec5_productSimulator_true-unreach-call_false-termination.cil.c true 2 wit inspect 14   4.0 100 550 0     0      - - out of memory 530    510    13000   7000 true 44   24   630 770
../../sv-benchmarks/c/product-lines/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 597 657 140000 45000 900000 2200000 14   200 597 2700 1500 39000 150000   597 4800 2700 72000 120000   597 100000 99000 2100000 1400000   597 9300 5500 140000 280000  
    correct results 377 657 4300 1400 33000 200000 2.5 160 97 590 320 9100 31000   97 1200 630 20000 38000   83 100000 99000 2100000 1400000   264 8900 5300 130000 260000  
        correct true 280 560 3300 1100 25000 150000 0   110 97 0 0 0 0   0 0 0 0 0   83 100000 99000 2100000 1400000   264 8900 5300 130000 260000  
        correct false 97 97 1000 330 7700 51000 2.5 43 0 590 320 9100 31000   97 1200 630 20000 38000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 90 0 21000 7700 150000 550000 11   16 90 2000 1100 29000 120000   44 3200 1800 43000 59000   0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 90 0 21000 7700 150000 550000 11   16 0 2000 1100 29000 120000   0 3200 1800 43000 59000   0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (597 tasks, max score: 929) 657
Run set sv-comp17.ReachSafety-ProductLines