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