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