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