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