Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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-11 11:31:18 CET [[ 2017-01-14 22:07:55 CET ]] [[ 2017-01-14 22:45:22 CET ]] [[ 2017-01-14 22:11:49 CET ]] [[ 2017-01-14 23:12:14 CET ]]; 2017-01-13 04:52:43 CET [[ 2017-01-15 00:23:14 CET ]] [[ 2017-01-15 00:35:58 CET ]] [[ 2017-01-15 00:29:47 CET ]] [[ 2017-01-15 00:40:29 CET ]]; 2017-01-13 05:40:48 CET; 2017-01-13 08:09:41 CET [[ 2017-01-15 00:46:31 CET ]] [[ 2017-01-15 01:12:25 CET ]] [[ 2017-01-15 00:52:40 CET ]] [[ 2017-01-15 01:18:42 CET ]]; 2017-01-13 09:48:46 CET]
Run set [sv-comp17.ReachSafety-Arrays; sv-comp17.ReachSafety-BitVectors; sv-comp17.ReachSafety-ControlFlow; sv-comp17.ReachSafety-ECA; sv-comp17.ReachSafety-Floats; sv-comp17.ReachSafety-Heap; sv-comp17.ReachSafety-Loops; sv-comp17.ReachSafety-ProductLines; sv-comp17.ReachSafety-Recursive; sv-comp17.ReachSafety-Sequentialized; sv-comp17.MemSafety-Arrays; sv-comp17.MemSafety-Heap; sv-comp17.MemSafety-LinkedLists; sv-comp17.MemSafety-Other; sv-comp17; sv-comp17.Overflows-BitVectors; sv-comp17.Overflows-Other; sv-comp17.Termination-MainControlFlow; sv-comp17.Termination-MainHeap; sv-comp17.Termination-Other; sv-comp17.Systems_BusyBox_MemSafety; sv-comp17.Systems_BusyBox_Overflows; sv-comp17.Systems_DeviceDriversLinux64_ReachSafety]
Options [-s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-11_1131.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]; -s fixed; -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0809.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]]
../../sv-benchmarks/c/ verifier status 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)
array-examples/data_structures_set_multi_proc_false-unreach-call_ground.i unreach-call out of memory 64     64     860     15000   .84 0      error (invalid witness file) .53 .35 9.4 43 error (invalid witness file) 6.0 3.2 130 300 - -
array-examples/sorting_bubblesort_false-unreach-call2_ground.i unreach-call out of memory 150     150     1100     15000   .84 0      error (invalid witness file) .50 .32 9.8 40 error (invalid witness file) 5.6 3.0 100 300 - -
array-examples/sorting_bubblesort_false-unreach-call_ground.i unreach-call out of memory 140     140     1100     15000   .84 0      error (invalid witness file) .65 .42 6.6 40 error (invalid witness file) 5.8 3.1 84 290 - -
array-examples/sorting_selectionsort_false-unreach-call2_ground.i unreach-call out of memory 34     34     320     15000   .84 0      error (invalid witness file) .58 .37 10   41 error (invalid witness file) 5.1 2.8 70 290 - -
array-examples/sorting_selectionsort_false-unreach-call_ground.i unreach-call out of memory 34     34     310     15000   .84 0      error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.0 3.2 100 310 - -
array-examples/standard_allDiff2_false-unreach-call_ground.i unreach-call out of memory 40     40     440     15000   .84 0      error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.2 3.3 98 310 - -
array-examples/standard_copy1_false-unreach-call_ground.i unreach-call false(unreach-call) 310     310     4000     670   1.9  0      unknown 7.8  4.1  130   460 timeout 98   62   1100 7000 - -
array-examples/standard_copy2_false-unreach-call_ground.i unreach-call false(unreach-call) 490     490     5800     820   2.0  0      unknown 9.7  5.1  190   520 timeout 96   58   780 6500 - -
array-examples/standard_copy3_false-unreach-call_ground.i unreach-call false(unreach-call) 660     660     8500     970   2.1  0      unknown 13    6.9  130   520 out of memory 86   52   920 7000 - -
array-examples/standard_copy4_false-unreach-call_ground.i unreach-call false(unreach-call) 810     810     11000     1100   2.2  .094  unknown 12    6.3  140   510 timeout 96   57   880 6600 - -
array-examples/standard_copy5_false-unreach-call_ground.i unreach-call false(unreach-call) 890     890     10000     1200   1.7  0      unknown 7.2  3.8  94   320 timeout 96   57   920 5600 - -
array-examples/standard_copy6_false-unreach-call_ground.i unreach-call false(unreach-call) 890     890     12000     1200   1.7  0      unknown 5.2  2.8  81   300 timeout 97   61   1900 5800 - -
array-examples/standard_copy7_false-unreach-call_ground.i unreach-call false(unreach-call) 900     900     10000     1300   1.7  0      unknown 6.4  3.4  120   310 timeout 97   62   1400 5900 - -
array-examples/standard_copy8_false-unreach-call_ground.i unreach-call false(unreach-call) 890     900     10000     1400   1.7  0      unknown 7.2  3.8  120   330 timeout 97   60   1300 5600 - -
array-examples/standard_copy9_false-unreach-call_ground.i unreach-call false(unreach-call) 890     890     9800     1400   1.7  0      unknown 5.7  3.1  80   300 timeout 96   59   1100 6200 - -
array-examples/standard_copyInitSum2_false-unreach-call_ground.i unreach-call false(unreach-call) 340     340     4200     680   2.0  0      unknown 9.1  4.8  160   500 timeout 97   60   1300 6100 - -
array-examples/standard_init1_false-unreach-call_ground.i unreach-call false(unreach-call) 160     160     1800     530   1.9  0      unknown 9.0  4.7  140   470 timeout 97   59   770 6700 - -
array-examples/standard_init2_false-unreach-call_ground.i unreach-call false(unreach-call) 490     490     6000     790   2.0  .094  unknown 11    5.8  160   500 timeout 97   61   1300 6900 - -
array-examples/standard_init3_false-unreach-call_ground.i unreach-call false(unreach-call) 790     790     11000     1100   2.1  0      unknown 9.3  4.9  160   510 timeout 98   61   1100 7000 - -
array-examples/standard_init4_false-unreach-call_ground.i unreach-call false(unreach-call) 900     900     12000     1200   1.7  0      unknown 6.1  3.3  100   310 timeout 97   61   1400 5600 - -
array-examples/standard_init5_false-unreach-call_ground.i unreach-call false(unreach-call) 890     890     12000     1300   1.7  0      unknown 5.6  3.0  120   300 timeout 97   62   1000 6200 - -
array-examples/standard_init6_false-unreach-call_ground.i unreach-call false(unreach-call) 900     900     10000     1400   1.7  0      unknown 7.0  3.7  65   310 timeout 96   62   900 6100 - -
array-examples/standard_init7_false-unreach-call_ground.i unreach-call false(unreach-call) 890     900     10000     1500   1.7  0      unknown 5.6  3.0  100   310 timeout 97   61   890 6200 - -
array-examples/standard_init8_false-unreach-call_ground.i unreach-call false(unreach-call) 890     890     10000     1600   1.7  0      unknown 5.7  3.1  94   310 timeout 97   62   870 5900 - -
array-examples/standard_init9_false-unreach-call_ground.i unreach-call false(unreach-call) 890     890     12000     1800   1.7  0      unknown 5.7  3.1  110   300 timeout 97   59   820 6200 - -
array-examples/standard_minInArray_false-unreach-call_ground.i unreach-call false(unreach-call) 33     33     380     1300   2.0  0      unknown 12    6.3  190   580 timeout 98   61   1300 6900 - -
array-examples/standard_partition_false-unreach-call_ground.i unreach-call false(unreach-call) 890     890     10000     12000   1.7  0      unknown 7.7  4.1  63   360 timeout 97   73   1800 5000 - -
array-examples/standard_running_false-unreach-call.i unreach-call false(unreach-call) 900     900     13000     1400   1.7  0      unknown 4.2  2.3  71   270 timeout 97   59   930 6400 - -
array-examples/data_structures_set_multi_proc_trivial_true-unreach-call_ground_true-termination.i unreach-call out of memory 61     61     610     15000   1.7  0      - - error 12    6.6  170   430 true 9.1 4.9 150 360
array-examples/data_structures_set_multi_proc_true-unreach-call_ground.i unreach-call out of memory 63     63     760     15000   .84 .14   - - error (invalid witness file) .63 .42 8.1 41 error (invalid witness file) 7.1 3.8 61 300
array-examples/relax_true-unreach-call.i unreach-call true 890     900     10000     3200   1.7  0      - - timeout 900    880    14000   5800 timeout 960   900   18000 1500
array-examples/sanfoundry_02_true-unreach-call_ground.i unreach-call timeout 900     900     10000     440   .87 0      - - error (invalid witness file) .52 .34 4.4 40 error (invalid witness file) 6.6 3.5 77 310
array-examples/sanfoundry_10_true-unreach-call_ground.i unreach-call true 900     900     13000     2600   1.7  0      - - out of memory 710    670    10000   7000 timeout 960   780   12000 3200
array-examples/sanfoundry_24_true-unreach-call.i unreach-call true 40     40     560     1700   3.5  0      - - error 8.0  4.3  94   330 true 11   6.0 130 360
array-examples/sanfoundry_27_true-unreach-call_ground.i unreach-call timeout 900     900     10000     360   .99 0      - - error (invalid witness file) .65 .41 7.9 39 error (invalid witness file) 5.9 3.1 48 300
array-examples/sanfoundry_43_true-unreach-call_ground.i unreach-call true .80  .80  8.4   65   2.2  0      - - true 5.9  3.2  72   290 true 7.8 4.1 87 330
array-examples/sorting_bubblesort_true-unreach-call_ground.i unreach-call out of memory 150     150     1000     15000   .84 0      - - error (invalid witness file) .63 .40 8.5 40 error (invalid witness file) 5.6 3.0 90 290
array-examples/sorting_selectionsort_true-unreach-call_ground.i unreach-call out of memory 34     34     330     15000   .84 0      - - error (invalid witness file) .62 .40 8.8 41 error (invalid witness file) 6.0 3.2 91 310
array-examples/standard_compareModified_true-unreach-call_ground.i unreach-call true 29     29     440     2300   3.0  0      - - error 43    36    730   940 timeout 960   820   17000 4000
array-examples/standard_compare_true-unreach-call_ground.i unreach-call true 13     13     160     1200   2.5  0      - - error 29    23    450   480 timeout 960   800   13000 4200
array-examples/standard_copy1_true-unreach-call_ground.i unreach-call true 3.9   3.9   52     420   2.3  0      - - error 10    6.0  150   390 timeout 960   800   19000 3900
array-examples/standard_copy2_true-unreach-call_ground.i unreach-call true 4.1   4.1   46     450   2.5  .0041 - - error 20    14    290   530 timeout 960   840   17000 4600
array-examples/standard_copy3_true-unreach-call_ground.i unreach-call true 4.2   4.2   48     470   2.7  0      - - error 29    24    360   470 timeout 960   850   13000 4800
array-examples/standard_copy4_true-unreach-call_ground.i unreach-call true 4.3   4.3   54     500   2.9  0      - - error 40    33    550   880 timeout 960   860   12000 4700
array-examples/standard_copy5_true-unreach-call_ground.i unreach-call true 4.5   4.5   52     520   3.1  0      - - error 47    42    530   1100 timeout 960   870   17000 4700
array-examples/standard_copy6_true-unreach-call_ground.i unreach-call true 4.7   4.7   55     550   3.3  0      - - error 81    76    1400   790 timeout 960   860   19000 4700
array-examples/standard_copy7_true-unreach-call_ground.i unreach-call true 4.8   4.8   63     570   3.5  0      - - error 110    100    2400   970 timeout 960   860   15000 4700
array-examples/standard_copy8_true-unreach-call_ground.i unreach-call true 5.0   5.0   58     600   3.7  0      - - error 150    140    1900   1900 timeout 960   870   25000 4700
array-examples/standard_copy9_true-unreach-call_ground.i unreach-call true 5.2   5.2   70     620   3.9  0      - - error 190    180    2900   2500 timeout 960   860   15000 4800
array-examples/standard_copyInitSum2_true-unreach-call_ground.i unreach-call true 4.3   4.3   50     470   2.7  0      - - error 25    19    300   620 timeout 960   860   15000 4600
array-examples/standard_copyInitSum3_true-unreach-call_ground.i unreach-call true 4.4   4.4   48     490   2.9  0      - - error 48    41    510   570 timeout 960   860   17000 4700
array-examples/standard_copyInitSum_true-unreach-call_ground.i unreach-call true 4.3   4.3   55     470   2.7  .0082 - - error 8.3  4.4  84   310 timeout 960   860   17000 4600
array-examples/standard_copyInit_true-unreach-call_ground.i unreach-call true 4.1   4.1   56     450   2.5  0      - - error 24    17    220   430 timeout 960   840   18000 4100
array-examples/standard_find_true-unreach-call_ground.i unreach-call true 15     15     220     900   2.8  0      - - error 22    16    360   530 timeout 960   790   17000 4600
array-examples/standard_init1_true-unreach-call_ground.i unreach-call true 3.9   3.9   47     420   2.3  0      - - error 12    7.3  140   420 timeout 960   790   16000 3900
array-examples/standard_init2_true-unreach-call_ground.i unreach-call true 4.1   4.1   51     440   2.5  0      - - error 21    15    280   430 timeout 960   830   15000 3700
array-examples/standard_init3_true-unreach-call_ground.i unreach-call true 4.1   4.1   50     470   2.7  0      - - error 24    19    270   590 timeout 960   850   15000 4400
array-examples/standard_init4_true-unreach-call_ground.i unreach-call true 4.3   4.3   50     490   2.9  0      - - error 40    33    620   790 timeout 960   850   12000 4600
array-examples/standard_init5_true-unreach-call_ground.i unreach-call true 4.4   4.4   51     510   3.1  0      - - error 59    52    880   1600 timeout 960   860   16000 4800
array-examples/standard_init6_true-unreach-call_ground.i unreach-call true 4.5   4.5   52     540   3.3  0      - - error 83    76    1200   1500 timeout 960   860   15000 4700
array-examples/standard_init7_true-unreach-call_ground.i unreach-call true 4.7   4.7   57     560   3.5  0      - - error 100    94    1300   1700 timeout 960   870   14000 4800
array-examples/standard_init8_true-unreach-call_ground.i unreach-call true 4.7   4.7   70     580   3.7  0      - - error 150    140    2300   860 timeout 960   870   14000 4900
array-examples/standard_init9_true-unreach-call_ground.i unreach-call true 4.9   4.9   54     610   3.9  0      - - error 180    180    3200   2500 timeout 960   870   13000 4800
array-examples/standard_maxInArray_true-unreach-call_ground.i unreach-call timeout 900     900     10000     310   .84 0      - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.0 3.2 110 300
array-examples/standard_minInArray_true-unreach-call_ground.i unreach-call timeout 900     900     11000     350   .84 0      - - error (invalid witness file) .60 .38 8.2 43 error (invalid witness file) 7.3 3.8 56 310
array-examples/standard_palindrome_true-unreach-call_ground.i unreach-call true 4.0   4.0   49     420   2.3  0      - - error 12    7.8  170   390 timeout 960   790   14000 3900
array-examples/standard_partial_init_true-unreach-call_ground.i unreach-call timeout 900     900     6600     2300   .84 0      - - error (invalid witness file) .64 .40 7.4 39 error (invalid witness file) 5.9 3.1 100 300
array-examples/standard_partition_original_true-unreach-call_ground.i unreach-call timeout 900     900     9600     2200   .84 0      - - error (invalid witness file) .63 .41 8.1 41 error (invalid witness file) 6.2 3.2 97 300
array-examples/standard_partition_true-unreach-call_ground.i unreach-call timeout 900     900     9200     1700   .84 0      - - error (invalid witness file) .65 .41 9.2 40 error (invalid witness file) 6.9 3.7 56 300
array-examples/standard_password_true-unreach-call_ground.i unreach-call true 13     13     160     1200   2.8  0      - - error 20    15    360   440 timeout 960   800   12000 4600
array-examples/standard_reverse_true-unreach-call_ground.i unreach-call false(unreach-call) 440     440     5700     680   1.9  0      - - unknown 10    5.5  130   500 out of memory 100   64   940 7000
array-examples/standard_running_true-unreach-call.i unreach-call timeout 900     900     9700     1200   .84 0      - - error (invalid witness file) .48 .31 5.8 40 error (invalid witness file) 5.2 2.8 64 300
array-examples/standard_sentinel_true-unreach-call_true-termination.i unreach-call true 14     14     190     140   2.0  0      - - error 7.8  4.2  71   300 true 14   7.6 130 360
array-examples/standard_seq_init_true-unreach-call_ground.i unreach-call true 3.9   3.9   46     420   2.3  0      - - error 14    8.8  220   390 timeout 960   790   16000 3300
array-examples/standard_strcmp_true-unreach-call_ground.i unreach-call true 5.6   5.6   70     550   2.7  0      - - error 31    26    560   470 timeout 960   810   17000 5000
array-examples/standard_strcpy_original_true-unreach-call.i unreach-call true 890     890     12000     1200   1.7  0      - - error 9.2  4.9  120   300 timeout 960   790   13000 3600
array-examples/standard_strcpy_true-unreach-call_ground.i unreach-call timeout 900     900     13000     1200   .84 0      - - error (invalid witness file) .58 .37 8.9 40 error (invalid witness file) 5.9 3.1 78 290
array-examples/standard_two_index_01_true-unreach-call.i unreach-call true 4.4   4.4   51     480   2.5  0      - - error 16    11    190   400 timeout 960   820   13000 2900
array-examples/standard_two_index_02_true-unreach-call.i unreach-call true 4.4   4.4   61     490   2.5  0      - - error 11    6.9  110   410 timeout 960   820   15000 2700
array-examples/standard_two_index_03_true-unreach-call.i unreach-call true 4.4   4.4   58     490   2.5  0      - - error 15    9.6  190   420 timeout 960   820   14000 2800
array-examples/standard_two_index_04_true-unreach-call.i unreach-call true 4.4   4.4   61     490   2.5  0      - - error 15    9.5  190   410 timeout 960   820   15000 2900
array-examples/standard_two_index_05_true-unreach-call.i unreach-call true 4.5   4.5   54     490   2.5  0      - - error 14    8.9  200   400 timeout 960   820   13000 2800
array-examples/standard_two_index_06_true-unreach-call.i unreach-call true 4.4   4.4   53     490   2.5  0      - - error 10    6.2  130   400 timeout 960   820   14000 3000
array-examples/standard_two_index_07_true-unreach-call.i unreach-call true 4.5   4.5   52     490   2.5  0      - - error 16    10    170   410 timeout 960   830   15000 2900
array-examples/standard_two_index_08_true-unreach-call.i unreach-call true 4.5   4.5   58     490   2.5  0      - - error 15    9.3  180   400 timeout 960   820   12000 2800
array-examples/standard_two_index_09_true-unreach-call.i unreach-call true 4.4   4.4   53     490   2.5  0      - - error 15    9.6  210   400 timeout 960   820   12000 2700
array-examples/standard_vararg_true-unreach-call_ground_true-termination.i unreach-call true 14     14     180     850   2.6  0      - - error 9.2  4.9  87   300 timeout 960   820   15000 2800
array-examples/standard_vector_difference_true-unreach-call_ground.i unreach-call true 3.9   3.9   46     420   2.3  0      - - error 13    8.6  210   400 timeout 960   790   11000 3500
array-industry-pattern/array_assert_loop_dep_false-unreach-call.i unreach-call false(unreach-call) 520     520     7200     830   2.0  0      unknown 7.3  3.8  150   480 timeout 97   67   1400 5000 - -
array-industry-pattern/array_of_struct_loop_dep_false-unreach-call.i unreach-call false(unreach-call) 61     61     450     4900   2.0  0      timeout 96    85    3200   1100 timeout 97   89   2100 4600 - -
array-industry-pattern/array_ptr_single_elem_init_false-unreach-call.i unreach-call true 14     14     160     1100   3.3  0      timeout 92    87    1600   780 timeout 97   62   2200 2100 - -
array-industry-pattern/array_range_init_false-unreach-call.i unreach-call true 670     670     7000     790   2.3  0      error 15    9.6  230   460 timeout 96   87   1000 4600 - -
array-industry-pattern/array_single_elem_init_false-unreach-call.i unreach-call true 14     14     150     1100   3.3  0      timeout 93    87    1900   1700 timeout 97   63   910 2300 - -
array-industry-pattern/check_removal_from_set_after_insertion_false-unreach-call.i unreach-call timeout 900     900     12000     4200   .84 0      error (invalid witness file) .54 .35 11   40 error (invalid witness file) 5.7 3.0 99 300 - -
array-industry-pattern/array_monotonic_true-unreach-call.i unreach-call timeout 900     900     9400     730   .84 0      - - error (invalid witness file) .65 .41 5.9 40 error (invalid witness file) 6.5 3.4 68 310
array-industry-pattern/array_mul_init_true-unreach-call.i unreach-call timeout 900     900     10000     1300   .84 0      - - error (invalid witness file) .58 .36 9.8 40 error (invalid witness file) 5.6 2.9 64 300
array-industry-pattern/array_of_struct_break_true-unreach-call.i unreach-call true 70     70     580     5200   2.7  0      - - timeout 910    890    18000   5300 timeout 960   940   9800 4800
array-industry-pattern/array_of_struct_ptr_cond_init_true-unreach-call.i unreach-call out of memory 320     320     2600     15000   1.7  0      - - timeout 900    890    13000   3300 timeout 960   940   9300 5200
array-industry-pattern/array_of_struct_ptr_flag_init_true-unreach-call.i unreach-call true 130     130     930     12000   3.0  0      - - timeout 910    890    14000   5100 timeout 960   820   19000 4700
array-industry-pattern/array_of_struct_ptr_monotonic_true-unreach-call.i unreach-call out of memory 330     330     2900     15000   1.7  .0082 - - timeout 900    890    28000   3600 timeout 960   940   11000 5300
array-industry-pattern/array_of_struct_ptr_mul_init_true-unreach-call.i unreach-call out of memory 350     350     2300     15000   1.7  0      - - out of memory 390    370    6900   7000 timeout 960   940   15000 4900
array-industry-pattern/array_of_struct_single_elem_init_true-unreach-call.i unreach-call true 70     70     480     4700   3.2  0      - - timeout 910    890    17000   6600 error 15   7.6 130 300
array-industry-pattern/array_ptr_partial_init_true-unreach-call.i unreach-call true 170     170     1000     14000   2.6  0      - - timeout 900    890    13000   4000 timeout 960   940   14000 5200
array-industry-pattern/array_ptr_single_elem_init_true-unreach-call.i unreach-call out of memory 480     480     4300     15000   1.7  0      - - timeout 900    890    17000   3700 timeout 960   940   13000 5200
array-industry-pattern/array_shadowinit_true-unreach-call.i unreach-call true 890     890     12000     1300   1.8  0      - - timeout 910    890    13000   5900 timeout 960   810   14000 2700
reducercommutativity/rangesum05_false-unreach-call.i unreach-call false(unreach-call) .20  .20  2.4   24   1.7  0      false(unreach-call) 6.9  4.3  100   370 true 8.7 4.7 99 350 - -
reducercommutativity/rangesum10_false-unreach-call.i unreach-call false(unreach-call) .24  .23  3.3   23   1.7  0      false(unreach-call) 7.3  4.6  130   400 true 11   6.1 180 380 - -
reducercommutativity/rangesum20_false-unreach-call.i unreach-call false(unreach-call) .43  .43  4.8   24   1.7  0      false(unreach-call) 11    7.3  190   450 true 12   6.2 150 410 - -
reducercommutativity/rangesum40_false-unreach-call.i unreach-call false(unreach-call) 6.1   6.0   78     36   1.7  .094  false(unreach-call) 13    8.8  260   610 true 13   6.8 170 540 - -
reducercommutativity/rangesum60_false-unreach-call.i unreach-call false(unreach-call) .96  .95  13     32   1.7  0      false(unreach-call) 20    13    220   700 true 14   7.5 200 540 - -
reducercommutativity/rangesum_false-unreach-call.i unreach-call false(unreach-call) 890     890     9200     2800   1.7  .0041 timeout 95    87    2100   2300 true 23   12   330 930 - -
reducercommutativity/avg05_true-unreach-call.i unreach-call true 150     150     1800     90   1.7  0      - - timeout 900    900    12000   1800 true 170   140   3800 1200
reducercommutativity/avg10_true-unreach-call.i unreach-call timeout 900     900     11000     270   .84 0      - - error (invalid witness file) .62 .39 8.1 40 error (invalid witness file) 5.7 3.0 77 300
reducercommutativity/avg20_true-unreach-call.i unreach-call timeout 900     900     11000     330   .84 0      - - error (invalid witness file) .52 .33 8.4 42 error (invalid witness file) 5.8 3.1 110 300
reducercommutativity/avg40_true-unreach-call.i unreach-call timeout 900     900     12000     390   .84 0      - - error (invalid witness file) .52 .32 7.8 40 error (invalid witness file) 5.3 2.9 76 290
reducercommutativity/avg60_true-unreach-call.i unreach-call timeout 900     900     11000     470   .84 0      - - error (invalid witness file) .59 .38 9.2 42 error (invalid witness file) 6.1 3.2 99 300
reducercommutativity/avg_true-unreach-call.i unreach-call timeout 900     900     11000     410   .84 0      - - error (invalid witness file) .63 .41 6.3 40 error (invalid witness file) 6.1 3.2 76 300
reducercommutativity/max05_true-unreach-call_true-termination.i unreach-call true 6.5   6.5   12     26   1.7  0      - - true 110    98    1700   830 timeout 960   910   22000 1300
reducercommutativity/max10_true-unreach-call_true-termination.i unreach-call true 44     44     520     58   1.7  0      - - timeout 900    890    13000   1900 timeout 960   880   18000 2500
reducercommutativity/max20_true-unreach-call.i unreach-call true 850     850     12000     130   1.7  0      - - timeout 900    890    16000   1800 timeout 960   800   17000 5300
reducercommutativity/max40_true-unreach-call.i unreach-call timeout 900     900     11000     220   .84 0      - - error (invalid witness file) .65 .41 7.7 40 error (invalid witness file) 5.7 3.1 95 300
reducercommutativity/max60_true-unreach-call.i unreach-call timeout 900     900     12000     280   .84 .0082 - - error (invalid witness file) .58 .37 10   43 error (invalid witness file) 7.3 3.8 69 300
reducercommutativity/max_true-unreach-call.i unreach-call timeout 900     900     12000     450   .84 0      - - error (invalid witness file) .54 .34 8.5 39 error (invalid witness file) 5.6 3.0 110 290
reducercommutativity/sep05_true-unreach-call.i unreach-call true .61  .61  7.4   23   1.7  0      - - true 150    140    2700   1000 true 200   140   1900 2800
reducercommutativity/sep10_true-unreach-call.i unreach-call true .60  .60  8.1   23   1.7  0      - - timeout 900    890    14000   1300 out of memory 840   710   16000 7000
reducercommutativity/sep20_true-unreach-call.i unreach-call true .65  .65  7.0   23   1.7  0      - - timeout 900    890    14000   1300 out of memory 310   210   4900 7000
reducercommutativity/sep40_true-unreach-call.i unreach-call true .69  .69  9.3   29   1.8  0      - - timeout 900    880    14000   2200 out of memory 730   590   12000 7000
reducercommutativity/sep60_true-unreach-call.i unreach-call true .74  .74  8.8   35   1.8  0      - - timeout 900    880    13000   4100 timeout 960   830   17000 5500
reducercommutativity/sep_true-unreach-call.i unreach-call timeout 900     900     10000     450   .84 0      - - error (invalid witness file) .57 .37 10   40 error (invalid witness file) 5.8 3.1 91 300
reducercommutativity/sum05_true-unreach-call_true-termination.i unreach-call true .16  .16  2.0   23   1.7  0      - - timeout 900    890    15000   1000 true 34   21   770 710
reducercommutativity/sum10_true-unreach-call.i unreach-call true .20  .20  1.9   23   1.7  0      - - timeout 900    890    15000   2100 true 84   56   1200 1300
reducercommutativity/sum20_true-unreach-call.i unreach-call true .19  .19  2.8   23   1.7  0      - - timeout 900    890    15000   6700 timeout 960   910   10000 5200
reducercommutativity/sum40_true-unreach-call.i unreach-call true .23  .23  3.0   23   1.7  0      - - out of memory 440    420    7900   7000 timeout 960   810   14000 4700
reducercommutativity/sum60_true-unreach-call.i unreach-call true .28  .28  3.1   24   1.8  0      - - out of memory 510    490    8400   7000 timeout 960   840   15000 6200
reducercommutativity/sum_true-unreach-call.i unreach-call timeout 900     900     12000     530   .84 0      - - error (invalid witness file) .58 .37 11   41 error (invalid witness file) 6.9 3.6 97 300
bitvector/byte_add_false-unreach-call_true-no-overflow.i unreach-call false(unreach-call) 51     51     620     2200   1.7  0      true 19    9.9  280   640 false(unreach-call) 56   31   320 570 - -
bitvector/sum02_false-unreach-call_true-no-overflow.i unreach-call false(unreach-call) 2.2   2.2   24     150   1.9  0      timeout 95    83    2900   980 timeout 97   82   2500 3700 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i unreach-call true 41     42     540     2200   5.1  0      - - true 15    7.8  180   540 true 400   350   5800 1500
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i unreach-call true 42     42     530     2200   5.1  0      - - true 16    8.5  170   540 true 410   350   8400 1500
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unreach-call true 120     120     1200     1200   2.3  0      - - true 14    11    210   330 timeout 960   950   16000 570
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unreach-call true 360     360     3800     1300   2.3  0      - - true 140    130    1400   480 timeout 960   950   13000 620
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unreach-call true 230     230     2500     1400   2.3  0      - - true 140    130    2400   500 timeout 960   950   20000 630
bitvector/gcd_4_true-unreach-call_true-no-overflow.i unreach-call true .16  .16  1.4   23   1.7  0      - - true 7.5  5.2  150   310 timeout 960   940   20000 900
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unreach-call true .16  .16  2.0   23   1.7  0      - - true 8.8  5.5  100   340 true 100   86   1300 710
bitvector/jain_1_true-unreach-call_true-no-overflow.i unreach-call true 5.3   5.3   70     510   2.2  0      - - out of memory 300    290    6300   7000 true 9.6 5.1 92 330
bitvector/jain_2_true-unreach-call_true-no-overflow.i unreach-call true 6.8   6.8   91     730   2.4  0      - - out of memory 240    230    4100   7000 true 9.2 4.9 110 360
bitvector/jain_4_true-unreach-call_true-no-overflow.i unreach-call true 8.6   8.6   110     890   2.6  0      - - out of memory 200    190    4100   7000 true 7.5 4.0 90 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i unreach-call true .25  .25  3.3   40   2.0  0      - - out of memory 370    360    6600   7000 timeout 960   820   13000 2900
bitvector/jain_6_true-unreach-call_true-no-overflow.i unreach-call true 8.8   8.8   96     890   2.6  0      - - out of memory 230    220    3900   7000 true 9.9 5.1 140 340
bitvector/jain_7_true-unreach-call_true-no-overflow.i unreach-call true 8.2   8.2   88     760   2.6  0      - - out of memory 310    300    6300   7000 true 8.5 4.5 180 340
bitvector/modulus_true-unreach-call_true-no-overflow.i unreach-call timeout 900     900     8700     5600   .84 0      - - error (invalid witness file) .65 .41 9.7 42 error (invalid witness file) 6.4 3.4 91 290
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unreach-call true .16  .16  1.8   23   1.7  0      - - true 5.4  2.9  97   300 true 72   55   900 520
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unreach-call true .18  .17  2.0   23   1.7  0      - - true 6.7  3.8  65   290 timeout 960   930   18000 950
bitvector/parity_true-unreach-call_true-no-overflow.i unreach-call true 2.3   2.3   25     160   2.2  0      - - true 29    23    380   370 timeout 960   950   16000 1100
bitvector/sum02_true-unreach-call_true-no-overflow.i unreach-call false(unreach-call) 2.6   2.6   34     150   1.9  .094  - - timeout 910    890    19000   1100 out of memory 320   280   4400 7000
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call out of memory 310     310     3900     15000   1.7  0      false(unreach-call) 9.6  5.2  110   330 true 9.4 5.0 160 330 - -
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call false(unreach-call) 890     890     12000     15000   1.7  0      false(unreach-call) 8.6  4.5  190   350 true 8.1 4.4 98 310 - -
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c unreach-call false(unreach-call) 890     890     8200     15000   1.7  0      false(unreach-call) 7.4  3.9  140   310 true 8.9 4.8 130 330 - -
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call out of memory 330     330     3600     15000   1.7  0      - - true 110    82    1300   2800 true 59   32   770 1900
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call true 900     900     7100     15000   1.7  0      - - true 46    26    480   2400 true 68   37   600 1900
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call true 900     900     7500     15000   1.7  0      - - true 33    19    670   2200 true 43   23   490 1900
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call timeout 900     900     8500     2800   .84 0      - - error (invalid witness file) .59 .37 8.0 40 error (invalid witness file) 6.2 3.3 80 300
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call out of memory 410     410     4400     15000   1.7  0      - - timeout 920    890    15000   6700 true 77   41   560 2400
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call out of memory 420     420     4500     15000   1.7  0      - - timeout 920    890    16000   5800 true 52   28   610 2100
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call out of memory 450     450     4800     15000   1.7  0      - - timeout 920    890    16000   5800 true 51   27   640 2100
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call out of memory 430     430     5100     15000   1.7  0      - - timeout 920    890    12000   6900 true 62   33   670 2000
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c unreach-call out of memory 410     400     4300     15000   1.7  0      - - out of memory 830    810    14000   7000 true 54   29   690 2000
bitvector/soft_float_1_true-unreach-call_true-no-overflow.c.cil.c unreach-call true 900     900     12000     2900   1.7  0      - - timeout 910    850    15000   6000 true 220   200   4700 1000
bitvector/soft_float_2_true-unreach-call_true-no-overflow.c.cil.c unreach-call true 890     900     12000     2900   1.7  0      - - out of memory 790    720    18000   7000 true 76   65   970 980
bitvector/soft_float_3_true-unreach-call_true-no-overflow.c.cil.c unreach-call true 890     900     11000     2900   1.7  0      - - timeout 900    820    16000   7000 timeout 960   920   21000 2100
bitvector/soft_float_4_true-unreach-call_true-no-overflow.c.cil.c unreach-call true 890     890     13000     2900   1.7  0      - - true 340    330    11000   690 error 48   34   500 650
bitvector/soft_float_5_true-unreach-call_true-no-overflow.c.cil.c unreach-call true 900     900     12000     2900   1.7  0      - - out of memory 840    770    16000   7000 true 22   12   300 590
bitvector-regression/implicitfloatconversion_false-unreach-call.c unreach-call false(unreach-call) .13  .13  1.3   23   1.7  0      false(unreach-call) 3.7  2.1  68   270 true 9.9 5.4 120 300 - -
bitvector-regression/implicitunsignedconversion_false-unreach-call.c unreach-call false(unreach-call) .14  .14  1.4   23   1.7  .094  false(unreach-call) 4.3  2.4  39   270 true 6.4 3.4 89 310 - -
bitvector-regression/integerpromotion_false-unreach-call.c unreach-call false(unreach-call) .13  .13  1.4   24   1.7  .65   false(unreach-call) 3.6  2.0  78   270 false(unreach-call) 12   6.2 200 310 - -
bitvector-regression/recHanoi03_false-unreach-call.c unreach-call false(unreach-call) 4.1   4.0   51     300   1.8  0      timeout 97    75    2100   4100 timeout 98   70   1600 6100 - -
bitvector-regression/signextension2_false-unreach-call.c unreach-call false(unreach-call) .13  .13  1.5   23   1.7  0      false(unreach-call) 3.5  2.0  58   270 true 6.6 3.5 140 310 - -
bitvector-regression/signextension_false-unreach-call.c unreach-call false(unreach-call) .15  .15  1.4   23   1.7  .094  false(unreach-call) 3.7  2.0  87   280 true 7.6 4.0 130 310 - -
bitvector-regression/implicitunsignedconversion_true-unreach-call.c unreach-call true .17  .17  1.3   23   1.7  0      - - true 4.1  2.3  45   250 true 7.0 3.7 81 320
bitvector-regression/integerpromotion_true-unreach-call.c unreach-call true .15  .15  1.4   23   1.7  0      - - true 4.2  2.4  54   250 true 12   6.6 170 320
bitvector-regression/signextension2_true-unreach-call.c unreach-call true .15  .15  1.4   23   1.7  0      - - true 3.4  1.9  41   260 true 6.8 3.6 58 310
bitvector-regression/signextension_true-unreach-call.c unreach-call true .16  .16  1.5   23   1.7  0      - - true 3.5  1.9  68   270 true 9.0 4.8 71 310
bitvector-loops/diamond_false-unreach-call2.i unreach-call false(unreach-call) 16     16     190     1000   1.7  0      true 3.9  2.2  96   280 false(unreach-call) 7.9 4.2 91 350 - -
bitvector-loops/overflow_false-unreach-call1.i unreach-call false(unreach-call) .15  .15  1.5   23   1.7  0      timeout 97    86    2800   1900 true 6.8 3.7 130 310 - -
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call.i unreach-call false(unreach-call) 2.1   2.1   24     220   1.7  0      false(unreach-call) 6.0  3.3  98   300 timeout 98   60   860 6300 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call false(unreach-call) 1.0   1.0   11     56   1.7  .094  false(unreach-call) 10    5.4  110   300 true 12   6.3 150 440 - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call false(unreach-call) .44  .44  5.3   38   1.7  .094  false(unreach-call) 7.4  4.0  120   300 true 10   5.4 120 340 - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call false(unreach-call) .69  .69  8.5   48   1.7  0      false(unreach-call) 10    5.4  100   310 true 10   5.5 120 380 - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call false(unreach-call) .32  .32  4.2   27   1.7  .094  false(unreach-call) 8.5  4.6  95   330 true 9.2 4.9 140 330 - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true 1.6   1.6   19     140   2.7  0      - - true 18    9.6  270   670 true 96   53   1200 1100
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true 1.4   1.4   17     140   2.3  0      - - out of memory 460    440    8700   7000 true 73   40   490 1000
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true .57  .57  6.1   57   1.9  0      - - true 16    8.2  160   480 true 91   49   920 900
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true .86  .86  9.3   77   2.0  0      - - true 15    7.7  220   520 true 84   45   970 1000
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true .28  .28  3.0   25   1.8  0      - - true 7.5  3.9  100   280 true 23   12   320 560
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c unreach-call true .36  .36  4.7   36   1.9  0      - - true 11    5.7  110   370 true 21   11   300 580
ssh-simplified/s3_clnt_1_false-unreach-call.cil.c unreach-call out of memory 290     290     3700     15000   1.7  0      false(unreach-call) 6.9  3.7  91   300 true 11   5.9 120 320 - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c unreach-call out of memory 280     280     3100     15000   1.7  0      false(unreach-call) 7.5  4.0  130   310 true 9.2 4.9 180 330 - -
ssh-simplified/s3_clnt_3_false-unreach-call.cil.c unreach-call out of memory 260     260     3800     15000   1.7  0      false(unreach-call) 7.2  3.8  120   300 true 8.7 4.6 150 330 - -
ssh-simplified/s3_clnt_4_false-unreach-call.cil.c unreach-call out of memory 270     270     3000     15000   1.7  0      false(unreach-call) 9.1  4.9  100   300 true 8.1 4.4 140 320 - -
ssh-simplified/s3_srvr_10_false-unreach-call.cil.c unreach-call out of memory 340     340     3500     15000   1.7  0      false(unreach-call) 7.4  4.0  77   290 true 8.8 4.7 110 330 - -
ssh-simplified/s3_srvr_11_false-unreach-call.cil.c unreach-call out of memory 460     460     5100     15000   1.7  0      false(unreach-call) 8.3  4.4  140   310 true 8.6 4.7 130 320 - -
ssh-simplified/s3_srvr_12_false-unreach-call.cil.c unreach-call out of memory 600     600     6000     15000   1.7  .0041 false(unreach-call) 7.8  4.1  140   300 true 9.2 4.9 180 310 - -
ssh-simplified/s3_srvr_13_false-unreach-call.cil.c unreach-call out of memory 470     470     4900     15000   1.7  0      false(unreach-call) 25    15    640   790 true 8.0 4.3 110 310 - -
ssh-simplified/s3_srvr_14_false-unreach-call.cil.c unreach-call out of memory 430     430     4900     15000   1.7  0      false(unreach-call) 7.3  3.9  91   290 true 9.8 5.2 190 330 - -
ssh-simplified/s3_srvr_1_false-unreach-call.cil.c unreach-call out of memory 410     410     5500     15000   1.7  0      false(unreach-call) 9.0  4.9  82   300 true 7.6 4.2 92 320 - -
ssh-simplified/s3_srvr_2_false-unreach-call.cil.c unreach-call out of memory 400     400     4800     15000   1.7  0      false(unreach-call) 6.8  3.6  130   290 true 8.6 4.6 150 320 - -
ssh-simplified/s3_srvr_6_false-unreach-call.cil.c unreach-call out of memory 490     480     4900     15000   1.7  0      false(unreach-call) 6.3  3.4  88   280 false(unreach-call) 9.2 4.9 150 340 - -
ssh-simplified/s3_clnt_1_true-unreach-call.cil.c unreach-call out of memory 300     300     4300     15000   1.7  0      - - true 43    24    510   2500 true 59   32   400 2300
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c unreach-call out of memory 290     290     4200     15000   1.7  0      - - true 50    27    910   2800 true 69   37   440 2500
ssh-simplified/s3_clnt_3_true-unreach-call.cil.c unreach-call out of memory 270     270     3200     15000   1.7  0      - - true 59    33    1100   3200 true 73   40   730 2700
ssh-simplified/s3_clnt_4_true-unreach-call.cil.c unreach-call out of memory 280     280     3400     15000   1.7  0      - - true 49    27    380   2700 true 74   40   940 2500
ssh-simplified/s3_srvr_1_true-unreach-call.cil.c unreach-call out of memory 430     430     6000     15000   1.7  0      - - out of memory 670    640    11000   7000 true 67   36   420 2900
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c unreach-call true 300     300     3300     3800   16    0      - - true 20    11    220   900 true 16   8.3 260 700
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c unreach-call true 53     53     710     1800   8.3  0      - - true 13    6.8  130   600 true 13   6.7 220 510
ssh-simplified/s3_srvr_2_true-unreach-call.cil.c unreach-call out of memory 410     410     4300     15000   1.7  0      - - out of memory 850    820    15000   7000 true 72   39   740 2600
ssh-simplified/s3_srvr_3_true-unreach-call.cil.c unreach-call out of memory 390     390     5300     15000   1.7  0      - - timeout 920    890    12000   6700 true 76   41   900 2400
ssh-simplified/s3_srvr_4_true-unreach-call.cil.c unreach-call out of memory 410     410     4700     15000   1.7  0      - - timeout 920    890    13000   6700 true 64   34   860 2500
ssh-simplified/s3_srvr_6_true-unreach-call.cil.c unreach-call out of memory 490     490     5300     15000   1.7  0      - - timeout 920    880    12000   6800 true 83   45   860 3000
ssh-simplified/s3_srvr_7_true-unreach-call.cil.c unreach-call out of memory 420     420     4900     15000   1.7  0      - - timeout 920    880    14000   6700 true 71   39   730 2500
ssh-simplified/s3_srvr_8_true-unreach-call.cil.c unreach-call out of memory 440     440     4900     15000   1.7  0      - - timeout 920    880    12000   6700 true 64   34   480 2500
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 110     110     1100     15000   1.7  0      false(unreach-call) 5.6  3.1  77   280 true 7.3 3.9 97 310 - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 120     110     1400     15000   1.7  0      false(unreach-call) 5.8  3.2  75   280 true 8.2 4.4 69 320 - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 88     88     950     15000   1.7  0      - - true 12    6.6  140   400 true 23   12   210 830
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 92     91     1000     15000   1.7  0      - - true 11    6.0  190   470 true 32   17   580 1100
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 97     97     1300     15000   1.7  0      - - true 12    6.3  160   480 true 35   19   560 2200
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 100     100     1100     15000   1.7  0      - - true 15    8.1  140   500 true 44   26   430 3600
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 110     110     1300     15000   1.7  0      - - true 14    7.2  140   530 true 96   59   1100 6200
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 110     110     1200     15000   1.7  0      - - true 16    8.6  140   610 out of memory 120   77   1200 7000
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call true 140     140     1600     8700   9.3  0      - - true 14    7.6  100   720 true 13   6.8 150 560
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call true 210     210     2100     12000   11    0      - - true 17    8.8  150   790 true 19   9.8 220 680
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 77     77     920     15000   1.7  0      - - true 12    6.2  110   360 true 15   7.7 110 500
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 80     80     910     15000   1.7  0      - - true 12    6.3  110   370 true 19   9.7 170 610
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c unreach-call out of memory 83     83     870     15000   1.7  0      - - true 10    5.3  140   400 true 24   13   200 670
ntdrivers/cdaudio_false-unreach-call.i.cil.c unreach-call out of memory 380     380     3100     15000   .84 0      error (invalid witness file) .54 .34 11   40 error (invalid witness file) 7.3 3.8 110 310 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c unreach-call false(unreach-call) 120     120     1100     4500   1.7  .094  timeout 97    82    2600   2900 true 17   9.2 180 470 - -
ntdrivers/floppy_false-unreach-call.i.cil.c unreach-call timeout 900     900     11000     260   .84 0      error (invalid witness file) .66 .41 7.0 40 error (invalid witness file) 6.9 3.6 130 310 - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c unreach-call false(unreach-call) 4.7   4.7   59     680   1.7  0      false(unreach-call) 13    7.4  220   490 true 13   6.8 180 440 - -
ntdrivers/parport_false-unreach-call.i.cil.c unreach-call timeout 900     900     7400     10000   .84 0      error (invalid witness file) .53 .34 11   40 error (invalid witness file) 7.0 3.7 110 300 - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c unreach-call out of memory 140     140     1500     15000   .84 0      - - error (invalid witness file) .50 .32 7.5 40 error (invalid witness file) 8.2 4.3 80 310
ntdrivers/diskperf_true-unreach-call.i.cil.c unreach-call true 120     120     950     4500   5.8  0      - - out of memory 880    860    14000   7000 true 120   69   1100 1500
ntdrivers/floppy2_true-unreach-call.i.cil.c unreach-call timeout 900     900     10000     1100   .84 0      - - error (invalid witness file) .60 .39 9.9 42 error (invalid witness file) 7.7 4.1 120 310
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c unreach-call timeout 900     900     14000     260   .84 0      - - error (invalid witness file) .61 .40 8.4 41 error (invalid witness file) 8.1 4.3 100 320
ntdrivers/parport_true-unreach-call.i.cil.c unreach-call timeout 900     900     9200     10000   .84 0      - - error (invalid witness file) .63 .40 7.9 39 error (invalid witness file) 6.1 3.3 74 290
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c unreach-call out of memory 390     390     4500     15000   1.7  0      false(unreach-call) 16    8.4  160   470 true 12   6.6 150 370 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c unreach-call out of memory 450     450     5400     15000   1.8  0      false(unreach-call) 11    6.1  220   470 true 9.9 5.3 150 350 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c unreach-call out of memory 440     440     5000     15000   1.7  0      false(unreach-call) 12    6.3  270   470 true 12   6.1 98 360 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c unreach-call out of memory 440     440     5200     15000   1.8  0      false(unreach-call) 15    7.8  130   470 true 10   5.6 180 360 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c unreach-call out of memory 700     700     6800     15000   1.7  0      timeout 96    72    2300   3200 true 10   5.6 150 350 - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c unreach-call out of memory 430     430     4100     15000   .84 0      error (invalid witness file) .51 .33 9.7 41 error (invalid witness file) 6.1 3.2 65 300 - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c unreach-call out of memory 420     420     5300     15000   .84 0      error (invalid witness file) .51 .32 9.9 40 error (invalid witness file) 6.2 3.3 69 300 - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c unreach-call out of memory 430     430     4800     15000   .84 0      error (invalid witness file) .65 .42 8.0 42 error (invalid witness file) 6.2 3.3 110 290 - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c unreach-call out of memory 540     540     5200     15000   .84 0      error (invalid witness file) .53 .34 11   40 error (invalid witness file) 6.4 3.4 110 300 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c unreach-call out of memory 450     450     4500     15000   .84 0      error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.2 3.2 89 300 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c unreach-call out of memory 470     470     4500     15000   .84 0      error (invalid witness file) .60 .39 8.5 40 error (invalid witness file) 5.8 3.1 92 300 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c unreach-call out of memory 450     450     4500     15000   .84 .41   error (invalid witness file) .62 .40 6.9 44 error (invalid witness file) 6.7 3.5 130 310 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c unreach-call out of memory 460     460     4500     15000   .84 0      error (invalid witness file) .55 .34 9.0 42 error (invalid witness file) 6.0 3.2 86 300 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c unreach-call out of memory 470     470     4700     15000   .84 0      error (invalid witness file) .47 .30 9.0 40 error (invalid witness file) 5.6 3.0 110 290 - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c unreach-call out of memory 490     490     4500     15000   .84 0      error (invalid witness file) .55 .36 10   39 error (invalid witness file) 6.3 3.3 95 300 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c unreach-call out of memory 470     470     4600     15000   .84 0      error (invalid witness file) .64 .41 6.5 40 error (invalid witness file) 6.0 3.2 110 300 - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c unreach-call out of memory 490     490     5100     15000   .84 0      error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.7 3.0 87 300 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c unreach-call out of memory 480     480     4600     15000   .84 0      error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.4 3.3 90 300 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c unreach-call out of memory 520     520     4900     15000   .84 0      error (invalid witness file) .63 .41 7.6 39 error (invalid witness file) 6.2 3.2 79 310 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c unreach-call out of memory 400     400     5100     15000   1.7  0      - - true 240    220    4200   2800 timeout 960   880   17000 3800
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c unreach-call out of memory 450     450     4800     15000   1.8  0      - - true 220    200    3400   2700 timeout 960   890   21000 3700
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c unreach-call out of memory 450     450     4800     15000   1.7  0      - - true 210    190    2700   2700 timeout 960   900   16000 4000
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c unreach-call out of memory 460     460     5300     15000   1.7  0      - - true 240    220    3700   2700 timeout 960   880   14000 3700
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c unreach-call out of memory 780     780     8900     15000   1.7  0      - - timeout 910    890    16000   5900 timeout 960   820   11000 5400
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c unreach-call out of memory 430     430     4900     15000   .84 0      - - error (invalid witness file) .60 .38 7.1 40 error (invalid witness file) 6.2 3.3 56 310
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c unreach-call out of memory 560     560     5100     15000   .84 0      - - error (invalid witness file) .50 .31 11   41 error (invalid witness file) 5.5 3.0 91 290
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c unreach-call out of memory 450     450     5400     15000   .84 0      - - error (invalid witness file) .51 .33 7.2 43 error (invalid witness file) 7.3 3.8 88 290
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c unreach-call out of memory 470     470     5100     15000   .84 0      - - error (invalid witness file) .66 .43 6.2 39 error (invalid witness file) 6.8 3.6 130 310
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c unreach-call out of memory 460     460     4000     15000   .84 0      - - error (invalid witness file) .71 .44 8.1 40 error (invalid witness file) 5.7 3.0 73 300
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c unreach-call out of memory 450     450     3700     15000   .84 0      - - error (invalid witness file) .56 .36 8.7 39 error (invalid witness file) 5.7 3.0 50 300
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c unreach-call out of memory 450     450     4800     15000   .84 0      - - error (invalid witness file) .66 .42 7.2 40 error (invalid witness file) 5.9 3.2 100 300
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c unreach-call out of memory 510     510     4600     15000   .84 0      - - error (invalid witness file) .69 .44 7.9 41 error (invalid witness file) 6.4 3.4 91 300
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c unreach-call out of memory 460     460     4400     15000   .84 0      - - error (invalid witness file) .51 .33 8.2 40 error (invalid witness file) 6.4 3.4 110 310
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c unreach-call out of memory 500     500     5400     15000   .84 0      - - error (invalid witness file) .53 .33 11   40 error (invalid witness file) 7.8 4.1 100 300
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c unreach-call out of memory 490     490     4400     15000   .84 0      - - error (invalid witness file) .71 .44 9.1 44 error (invalid witness file) 5.9 3.2 54 310
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c unreach-call out of memory 550     550     5400     15000   .84 .0082 - - error (invalid witness file) .61 .39 7.7 40 error (invalid witness file) 7.8 4.1 120 340
eca-rers2012/Problem01_label15_false-unreach-call.c unreach-call out of memory 840     840     8300     15000   1.7  0      timeout 97    70    2300   3000 true 12   6.1 200 380 - -
eca-rers2012/Problem01_label20_false-unreach-call.c unreach-call out of memory 820     820     9900     15000   1.7  0      true 37    22    460   1500 true 12   6.2 200 360 - -
eca-rers2012/Problem01_label21_false-unreach-call.c unreach-call out of memory 880     880     8000     15000   1.7  0      true 73    52    1500   4200 true 12   6.2 130 360 - -
eca-rers2012/Problem01_label32_false-unreach-call.c unreach-call out of memory 840     840     8700     15000   1.7  0      true 23    13    480   840 true 11   5.8 170 330 - -
eca-rers2012/Problem01_label33_false-unreach-call.c unreach-call out of memory 820     820     9000     15000   1.7  0      true 43    28    960   2400 true 12   6.2 140 380 - -
eca-rers2012/Problem01_label35_false-unreach-call.c unreach-call out of memory 820     820     12000     15000   1.7  0      true 30    18    560   1400 true 11   5.9 150 350 - -
eca-rers2012/Problem01_label37_false-unreach-call.c unreach-call out of memory 850     850     7100     15000   1.7  0      true 44    27    500   2100 true 12   6.2 180 360 - -
eca-rers2012/Problem01_label38_false-unreach-call.c unreach-call out of memory 820     820     8800     15000   1.7  0      true 31    19    770   1600 true 12   6.1 240 340 - -
eca-rers2012/Problem01_label44_false-unreach-call.c unreach-call out of memory 860     860     8200     15000   1.7  0      true 45    30    820   2400 true 15   8.1 140 360 - -
eca-rers2012/Problem01_label47_false-unreach-call.c unreach-call out of memory 840     830     10000     15000   1.7  .0082 true 44    28    1100   2600 true 12   6.5 180 370 - -
eca-rers2012/Problem01_label50_false-unreach-call.c unreach-call out of memory 830     830     7500     15000   1.7  0      true 38    23    590   1600 true 11   5.7 120 350 - -
eca-rers2012/Problem01_label56_false-unreach-call.c unreach-call out of memory 840     840     8100     15000   1.7  0      true 38    23    440   1400 true 11   5.9 160 350 - -
eca-rers2012/Problem01_label57_false-unreach-call.c unreach-call out of memory 800     800     8600     15000   1.7  0      true 27    14    460   830 true 11   6.1 180 370 - -
eca-rers2012/Problem02_label13_false-unreach-call.c unreach-call out of memory 850     850     9300     15000   1.8  0      true 18    9.2  180   470 true 11   6.1 170 360 - -
eca-rers2012/Problem02_label16_false-unreach-call.c unreach-call out of memory 890     890     8300     15000   1.7  0      true 15    7.7  320   470 true 12   6.2 210 370 - -
eca-rers2012/Problem02_label43_false-unreach-call.c unreach-call false(unreach-call) 890     900     8600     9100   1.7  0      true 21    11    330   780 true 11   5.9 130 350 - -
eca-rers2012/Problem02_label44_false-unreach-call.c unreach-call false(unreach-call) 900     900     9100     9600   1.7  0      true 52    34    760   2900 true 11   6.1 150 350 - -
eca-rers2012/Problem02_label45_false-unreach-call.c unreach-call out of memory 850     850     9200     15000   1.7  0      true 27    15    410   1100 true 12   6.1 190 340 - -
eca-rers2012/Problem02_label50_false-unreach-call.c unreach-call out of memory 840     840     10000     15000   1.7  0      true 21    11    310   570 true 11   6.0 130 370 - -
eca-rers2012/Problem02_label59_false-unreach-call.c unreach-call out of memory 850     850     10000     15000   1.7  0      true 21    11    410   620 true 13   7.0 120 360 - -
eca-rers2012/Problem03_label09_false-unreach-call.c unreach-call timeout 900     900     9400     8500   .84 0      error (invalid witness file) .49 .32 11   40 error (invalid witness file) 7.4 3.8 87 290 - -
eca-rers2012/Problem03_label13_false-unreach-call.c unreach-call timeout 900     900     8400     8400   .84 0      error (invalid witness file) .51 .34 4.4 39 error (invalid witness file) 6.3 3.3 94 300 - -
eca-rers2012/Problem03_label26_false-unreach-call.c unreach-call timeout 900     900     7200     8400   .84 0      error (invalid witness file) .47 .32 7.7 40 error (invalid witness file) 6.3 3.3 71 300 - -
eca-rers2012/Problem03_label27_false-unreach-call.c unreach-call timeout 900     900     6600     8400   .84 0      error (invalid witness file) .59 .37 11   39 error (invalid witness file) 5.8 3.1 81 290 - -
eca-rers2012/Problem03_label28_false-unreach-call.c unreach-call timeout 900     900     7700     8500   .84 0      error (invalid witness file) .61 .39 8.4 43 error (invalid witness file) 6.1 3.2 100 300 - -
eca-rers2012/Problem03_label31_false-unreach-call.c unreach-call timeout 900     900     7800     8400   .84 0      error (invalid witness file) .50 .32 12   39 error (invalid witness file) 8.4 4.3 110 300 - -
eca-rers2012/Problem03_label35_false-unreach-call.c unreach-call timeout 900     900     8700     8400   .84 0      error (invalid witness file) .63 .41 8.0 40 error (invalid witness file) 7.5 3.9 68 300 - -
eca-rers2012/Problem03_label37_false-unreach-call.c unreach-call timeout 900     900     11000     8400   .84 0      error (invalid witness file) .62 .41 7.5 40 error (invalid witness file) 6.5 3.5 100 300 - -
eca-rers2012/Problem03_label39_false-unreach-call.c unreach-call timeout 900     900     8800     8400   .84 0      error (invalid witness file) .52 .35 13   40 error (invalid witness file) 6.1 3.2 97 300 - -
eca-rers2012/Problem03_label43_false-unreach-call.c unreach-call timeout 900     900     6500     8400   .84 0      error (invalid witness file) .53 .33 9.0 39 error (invalid witness file) 6.1 3.3 88 290 - -
eca-rers2012/Problem03_label45_false-unreach-call.c unreach-call timeout 900     900     7300     8400   .84 0      error (invalid witness file) .51 .33 14   39 error (invalid witness file) 6.8 3.6 70 300 - -
eca-rers2012/Problem03_label50_false-unreach-call.c unreach-call timeout 900     900     7200     8400   .84 0      error (invalid witness file) .51 .34 13   42 error (invalid witness file) 8.2 4.3 83 300 - -
eca-rers2012/Problem03_label52_false-unreach-call.c unreach-call timeout 900     900     7200     8400   .84 0      error (invalid witness file) .55 .35 14   41 error (invalid witness file) 6.9 3.6 110 310 - -
eca-rers2012/Problem04_label04_false-unreach-call.c unreach-call out of memory 70     70     900     15000   .84 0      error (invalid witness file) .53 .35 12   40 error (invalid witness file) 7.4 3.9 110 310 - -
eca-rers2012/Problem04_label06_false-unreach-call.c unreach-call out of memory 69     69     880     15000   .84 0      error (invalid witness file) .48 .32 4.8 43 error (invalid witness file) 6.1 3.3 110 300 - -
eca-rers2012/Problem04_label09_false-unreach-call.c unreach-call out of memory 70     70     810     15000   .84 0      error (invalid witness file) .55 .34 14   42 error (invalid witness file) 6.9 3.6 110 310 - -
eca-rers2012/Problem04_label11_false-unreach-call.c unreach-call out of memory 70     69     760     15000   .84 0      error (invalid witness file) .63 .41 7.0 39 error (invalid witness file) 6.2 3.3 67 300 - -
eca-rers2012/Problem04_label12_false-unreach-call.c unreach-call out of memory 70     70     830     15000   .84 0      error (invalid witness file) .65 .41 7.1 40 error (invalid witness file) 6.9 3.7 110 310 - -
eca-rers2012/Problem04_label13_false-unreach-call.c unreach-call out of memory 70     70     750     15000   .84 0      error (invalid witness file) .52 .34 13   40 error (invalid witness file) 8.2 4.3 64 300 - -
eca-rers2012/Problem04_label14_false-unreach-call.c unreach-call out of memory 70     70     800     15000   .84 0      error (invalid witness file) .66 .43 7.6 40 error (invalid witness file) 8.1 4.2 100 300 - -
eca-rers2012/Problem04_label15_false-unreach-call.c unreach-call out of memory 130     120     780     15000   .84 0      error (invalid witness file) .51 .33 11   41 error (invalid witness file) 7.2 3.7 100 320 - -
eca-rers2012/Problem04_label17_false-unreach-call.c unreach-call out of memory 70     69     800     15000   .84 0      error (invalid witness file) .64 .41 8.3 40 error (invalid witness file) 6.7 3.5 110 300 - -
eca-rers2012/Problem04_label18_false-unreach-call.c unreach-call out of memory 70     69     930     15000   .84 .0082 error (invalid witness file) .49 .31 9.0 39 error (invalid witness file) 7.0 3.7 83 320 - -
eca-rers2012/Problem04_label19_false-unreach-call.c unreach-call out of memory 70     70     840     15000   .84 0      error (invalid witness file) .53 .33 9.8 41 error (invalid witness file) 6.3 3.3 92 310 - -
eca-rers2012/Problem04_label26_false-unreach-call.c unreach-call out of memory 70     70     1000     15000   .84 0      error (invalid witness file) .66 .42 7.9 40 error (invalid witness file) 6.5 3.4 79 300 - -
eca-rers2012/Problem04_label27_false-unreach-call.c unreach-call out of memory 70     70     750     15000   .84 0      error (invalid witness file) .53 .34 11   42 error (invalid witness file) 6.1 3.2 76 300 - -
eca-rers2012/Problem04_label31_false-unreach-call.c unreach-call out of memory 70     69     990     15000   .84 0      error (invalid witness file) .54 .34 13   40 error (invalid witness file) 8.1 4.3 100 310 - -
eca-rers2012/Problem04_label32_false-unreach-call.c unreach-call out of memory 70     70     860     15000   .84 0      error (invalid witness file) .60 .38 10   41 error (invalid witness file) 6.6 3.5 82 300 - -
eca-rers2012/Problem04_label35_false-unreach-call.c unreach-call out of memory 70     70     860     15000   .84 0      error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.4 3.4 91 300 - -
eca-rers2012/Problem04_label36_false-unreach-call.c unreach-call out of memory 70     70     820     15000   .84 0      error (invalid witness file) .53 .33 12   42 error (invalid witness file) 6.7 3.5 96 300 - -
eca-rers2012/Problem04_label38_false-unreach-call.c unreach-call out of memory 70     70     760     15000   .84 0      error (invalid witness file) .76 .48 7.9 43 error (invalid witness file) 6.6 3.5 110 300 - -
eca-rers2012/Problem04_label39_false-unreach-call.c unreach-call out of memory 70     69     770     15000   .84 0      error (invalid witness file) .49 .32 10   39 error (invalid witness file) 6.8 3.5 89 300 - -
eca-rers2012/Problem04_label40_false-unreach-call.c unreach-call out of memory 69     69     760     15000   .84 0      error (invalid witness file) .53 .33 8.5 40 error (invalid witness file) 6.7 3.5 110 300 - -
eca-rers2012/Problem04_label45_false-unreach-call.c unreach-call out of memory 71     70     870     15000   .84 0      error (invalid witness file) .53 .36 13   41 error (invalid witness file) 6.9 3.7 120 300 - -
eca-rers2012/Problem04_label52_false-unreach-call.c unreach-call out of memory 70     70     890     15000   .84 0      error (invalid witness file) .60 .39 8.5 40 error (invalid witness file) 7.3 3.8 100 320 - -
eca-rers2012/Problem04_label55_false-unreach-call.c unreach-call out of memory 70     70     770     15000   .84 0      error (invalid witness file) .52 .33 10   40 error (invalid witness file) 6.9 3.7 92 300 - -
eca-rers2012/Problem04_label58_false-unreach-call.c unreach-call out of memory 70     70     930     15000   .84 0      error (invalid witness file) .59 .38 9.9 41 error (invalid witness file) 6.6 3.5 110 310 - -
eca-rers2012/Problem05_label00_false-unreach-call.c unreach-call out of memory 66     66     880     15000   .84 0      error (invalid witness file) .55 .35 11   40 error (invalid witness file) 6.9 3.7 110 300 - -
eca-rers2012/Problem05_label01_false-unreach-call.c unreach-call out of memory 67     67     810     15000   .84 0      error (invalid witness file) .51 .32 11   40 error (invalid witness file) 7.3 3.9 110 320 - -
eca-rers2012/Problem05_label11_false-unreach-call.c unreach-call out of memory 67     66     750     15000   .84 0      error (invalid witness file) .62 .39 8.7 41 error (invalid witness file) 8.3 4.4 100 310 - -
eca-rers2012/Problem05_label13_false-unreach-call.c unreach-call out of memory 66     66     780     15000   .84 0      error (invalid witness file) .66 .42 8.9 39 error (invalid witness file) 7.6 3.9 160 310 - -
eca-rers2012/Problem05_label15_false-unreach-call.c unreach-call out of memory 67     67     940     15000   .84 0      error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.5 3.4 110 300 - -
eca-rers2012/Problem05_label18_false-unreach-call.c unreach-call out of memory 67     67     870     15000   .84 0      error (invalid witness file) .49 .32 9.6 39 error (invalid witness file) 6.5 3.4 88 300 - -
eca-rers2012/Problem05_label24_false-unreach-call.c unreach-call out of memory 66     66     740     15000   .84 0      error (invalid witness file) .51 .33 11   42 error (invalid witness file) 6.7 3.5 110 310 - -
eca-rers2012/Problem05_label26_false-unreach-call.c unreach-call out of memory 67     67     830     15000   .84 0      error (invalid witness file) .60 .38 8.4 39 error (invalid witness file) 6.9 3.7 110 300 - -
eca-rers2012/Problem05_label30_false-unreach-call.c unreach-call out of memory 67     66     750     15000   .84 0      error (invalid witness file) .57 .37 10   39 error (invalid witness file) 7.4 3.8 110 320 - -
eca-rers2012/Problem05_label32_false-unreach-call.c unreach-call out of memory 67     67     770     15000   .84 0      error (invalid witness file) .62 .40 8.9 40 error (invalid witness file) 7.5 3.9 150 310 - -
eca-rers2012/Problem05_label33_false-unreach-call.c unreach-call out of memory 280     280     670     15000   .84 0      error (invalid witness file) .52 .33 14   40 error (invalid witness file) 7.6 4.0 97 310 - -
eca-rers2012/Problem05_label36_false-unreach-call.c unreach-call out of memory 66     66     740     15000   .84 0      error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.6 3.5 77 310 - -
eca-rers2012/Problem05_label37_false-unreach-call.c unreach-call out of memory 67     67     890     15000   .84 0      error (invalid witness file) .63 .40 9.5 40 error (invalid witness file) 6.4 3.4 90 300 - -
eca-rers2012/Problem05_label38_false-unreach-call.c unreach-call out of memory 67     67     700     15000   .84 0      error (invalid witness file) .54 .34 12   40 error (invalid witness file) 7.2 3.8 140 310 - -
eca-rers2012/Problem05_label39_false-unreach-call.c unreach-call out of memory 67     67     750     15000   .84 0      error (invalid witness file) .63 .40 9.1 41 error (invalid witness file) 7.2 3.8 150 300 - -
eca-rers2012/Problem05_label40_false-unreach-call.c unreach-call out of memory 67     67     800     15000   .84 0      error (invalid witness file) .61 .38 8.1 39 error (invalid witness file) 6.7 3.5 110 300 - -
eca-rers2012/Problem05_label41_false-unreach-call.c unreach-call out of memory 67     67     920     15000   .84 0      error (invalid witness file) .48 .32 8.2 41 error (invalid witness file) 7.5 3.9 150 320 - -
eca-rers2012/Problem05_label44_false-unreach-call.c unreach-call out of memory 67     67     700     15000   .84 0      error (invalid witness file) .56 .36 13   42 error (invalid witness file) 7.2 3.7 140 320 - -
eca-rers2012/Problem05_label47_false-unreach-call.c unreach-call out of memory 66     66     740     15000   .84 0      error (invalid witness file) .69 .43 9.3 42 error (invalid witness file) 7.7 4.0 110 320 - -
eca-rers2012/Problem05_label48_false-unreach-call.c unreach-call out of memory 67     67     660     15000   .84 0      error (invalid witness file) .55 .35 12   44 error (invalid witness file) 6.8 3.6 83 310 - -
eca-rers2012/Problem05_label51_false-unreach-call.c unreach-call out of memory 67     66     980     15000   .84 0      error (invalid witness file) .49 .32 8.7 40 error (invalid witness file) 7.5 4.0 120 320 - -
eca-rers2012/Problem05_label55_false-unreach-call.c unreach-call out of memory 67     67     970     15000   .84 0      error (invalid witness file) .68 .43 8.6 41 error (invalid witness file) 6.9 3.6 98 310 - -
eca-rers2012/Problem05_label57_false-unreach-call.c unreach-call out of memory 67     67     740     15000   .84 0      error (invalid witness file) .53 .35 15   41 error (invalid witness file) 7.0 3.7 160 300 - -
eca-rers2012/Problem05_label58_false-unreach-call.c unreach-call out of memory 67     67     810     15000   .84 0      error (invalid witness file) .53 .34 14   42 error (invalid witness file) 9.1 4.7 64 310 - -
eca-rers2012/Problem06_label00_false-unreach-call.c unreach-call out of memory 86     86     1000     15000   .84 0      error (invalid witness file) .52 .32 13   40 error (invalid witness file) 6.5 3.5 120 290 - -
eca-rers2012/Problem06_label01_false-unreach-call.c unreach-call out of memory 88     88     1100     15000   .84 0      error (invalid witness file) .49 .33 14   40 error (invalid witness file) 6.5 3.4 130 300 - -
eca-rers2012/Problem06_label02_false-unreach-call.c unreach-call out of memory 87     86     1300     15000   .84 0      error (invalid witness file) .61 .39 7.3 39 error (invalid witness file) 6.5 3.4 130 300 - -
eca-rers2012/Problem06_label04_false-unreach-call.c unreach-call out of memory 87     86     1100     15000   .84 0      error (invalid witness file) .53 .33 9.9 39 error (invalid witness file) 6.4 3.4 130 290 - -
eca-rers2012/Problem06_label05_false-unreach-call.c unreach-call out of memory 87     86     1100     15000   .84 0      error (invalid witness file) .55 .35 8.5 39 error (invalid witness file) 7.0 3.7 110 310 - -
eca-rers2012/Problem06_label09_false-unreach-call.c unreach-call out of memory 87     86     1000     15000   .84 0      error (invalid witness file) .55 .34 13   40 error (invalid witness file) 6.9 3.6 100 310 - -
eca-rers2012/Problem06_label10_false-unreach-call.c unreach-call out of memory 87     87     880     15000   .84 0      error (invalid witness file) .52 .35 12   40 error (invalid witness file) 6.9 3.6 110 310 - -
eca-rers2012/Problem06_label11_false-unreach-call.c unreach-call out of memory 86     86     1100     15000   .84 0      error (invalid witness file) .55 .35 7.6 40 error (invalid witness file) 7.1 3.7 120 310 - -
eca-rers2012/Problem06_label12_false-unreach-call.c unreach-call out of memory 86     86     1100     15000   .84 0      error (invalid witness file) .62 .41 8.8 39 error (invalid witness file) 6.7 3.6 120 290 - -
eca-rers2012/Problem06_label15_false-unreach-call.c unreach-call out of memory 87     87     1200     15000   .84 0      error (invalid witness file) .53 .34 11   43 error (invalid witness file) 7.0 3.7 76 320 - -
eca-rers2012/Problem06_label20_false-unreach-call.c unreach-call out of memory 87     86     1000     15000   .84 0      error (invalid witness file) .63 .40 9.5 41 error (invalid witness file) 7.2 3.8 120 300 - -
eca-rers2012/Problem06_label21_false-unreach-call.c unreach-call out of memory 87     87     1100     15000   .84 0      error (invalid witness file) .52 .33 12   40 error (invalid witness file) 8.8 4.6 78 300 - -
eca-rers2012/Problem06_label24_false-unreach-call.c unreach-call out of memory 87     87     1100     15000   .84 0      error (invalid witness file) .53 .35 11   39 error (invalid witness file) 6.9 3.6 100 310 - -
eca-rers2012/Problem06_label27_false-unreach-call.c unreach-call out of memory 87     87     930     15000   .84 0      error (invalid witness file) .54 .34 15   40 error (invalid witness file) 6.6 3.6 120 300 - -
eca-rers2012/Problem06_label29_false-unreach-call.c unreach-call out of memory 87     87     980     15000   .84 0      error (invalid witness file) .62 .40 8.6 40 error (invalid witness file) 7.5 3.9 150 300 - -
eca-rers2012/Problem06_label33_false-unreach-call.c unreach-call out of memory 87     87     960     15000   .84 0      error (invalid witness file) .65 .42 7.0 40 error (invalid witness file) 6.9 3.7 140 300 - -
eca-rers2012/Problem06_label36_false-unreach-call.c unreach-call out of memory 86     86     1100     15000   .84 0      error (invalid witness file) .57 .36 8.4 39 error (invalid witness file) 7.0 3.7 160 300 - -
eca-rers2012/Problem06_label37_false-unreach-call.c unreach-call out of memory 87     86     950     15000   .84 0      error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.9 3.6 110 300 - -
eca-rers2012/Problem06_label38_false-unreach-call.c unreach-call out of memory 88     87     1100     15000   .84 0      error (invalid witness file) .65 .41 6.8 40 error (invalid witness file) 8.6 4.5 69 300 - -
eca-rers2012/Problem06_label44_false-unreach-call.c unreach-call out of memory 87     86     1100     15000   .84 0      error (invalid witness file) .59 .37 10   39 error (invalid witness file) 7.3 3.8 120 300 - -
eca-rers2012/Problem06_label47_false-unreach-call.c unreach-call out of memory 86     86     940     15000   .84 0      error (invalid witness file) .60 .39 10   40 error (invalid witness file) 7.4 3.9 83 310 - -
eca-rers2012/Problem06_label48_false-unreach-call.c unreach-call out of memory 87     87     1000     15000   .84 0      error (invalid witness file) .64 .41 8.3 41 error (invalid witness file) 6.9 3.6 110 310 - -
eca-rers2012/Problem06_label56_false-unreach-call.c unreach-call out of memory 87     86     1000     15000   .84 0      error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.6 3.4 110 300 - -
eca-rers2012/Problem06_label58_false-unreach-call.c unreach-call out of memory 87     87     1000     15000   .84 0      error (invalid witness file) .69 .44 8.0 42 error (invalid witness file) 7.3 3.8 130 320 - -
eca-rers2012/Problem06_label59_false-unreach-call.c unreach-call out of memory 87     87     1100     15000   .84 0      error (invalid witness file) .51 .32 12   40 error (invalid witness file) 7.1 3.7 110 300 - -
eca-rers2012/Problem07_label03_false-unreach-call.c unreach-call out of memory 47     47     500     15000   .84 0      error (invalid witness file) .62 .40 8.4 40 error (invalid witness file) 7.1 3.9 120 430 - -
eca-rers2012/Problem07_label05_false-unreach-call.c unreach-call out of memory 47     47     510     15000   .84 0      error (invalid witness file) .51 .33 9.3 41 error (invalid witness file) 8.6 4.6 130 430 - -
eca-rers2012/Problem07_label06_false-unreach-call.c unreach-call out of memory 47     47     450     15000   .84 0      error (invalid witness file) .52 .33 11   39 error (invalid witness file) 7.7 4.1 92 430 - -
eca-rers2012/Problem07_label07_false-unreach-call.c unreach-call out of memory 47     47     510     15000   .84 0      error (invalid witness file) .51 .32 12   40 error (invalid witness file) 8.1 4.3 110 440 - -
eca-rers2012/Problem07_label09_false-unreach-call.c unreach-call out of memory 48     47     530     15000   .84 0      error (invalid witness file) .50 .34 13   39 error (invalid witness file) 7.6 4.1 110 430 - -
eca-rers2012/Problem07_label11_false-unreach-call.c unreach-call out of memory 47     47     520     15000   .84 0      error (invalid witness file) .63 .42 7.2 39 error (invalid witness file) 8.7 4.6 150 440 - -
eca-rers2012/Problem07_label15_false-unreach-call.c unreach-call out of memory 47     47     480     15000   .84 0      error (invalid witness file) .61 .38 9.6 41 error (invalid witness file) 7.3 3.9 90 430 - -
eca-rers2012/Problem07_label18_false-unreach-call.c unreach-call out of memory 48     47     540     15000   .84 0      error (invalid witness file) .51 .34 6.9 39 error (invalid witness file) 7.9 4.2 110 430 - -
eca-rers2012/Problem07_label19_false-unreach-call.c unreach-call out of memory 47     47     490     15000   .84 0      error (invalid witness file) .52 .33 11   40 error (invalid witness file) 7.8 4.2 130 430 - -
eca-rers2012/Problem07_label20_false-unreach-call.c unreach-call out of memory 48     47     490     15000   .84 0      error (invalid witness file) .53 .34 11   40 error (invalid witness file) 7.6 4.1 86 430 - -
eca-rers2012/Problem07_label23_false-unreach-call.c unreach-call out of memory 48     47     550     15000   .84 0      error (invalid witness file) .57 .36 10   43 error (invalid witness file) 7.6 4.1 140 420 - -
eca-rers2012/Problem07_label30_false-unreach-call.c unreach-call out of memory 47     47     510     15000   .84 0      error (invalid witness file) .51 .33 11   41 error (invalid witness file) 7.9 4.2 140 430 - -
eca-rers2012/Problem07_label31_false-unreach-call.c unreach-call out of memory 47     47     610     15000   .84 .25   error (invalid witness file) .51 .33 11   39 error (invalid witness file) 7.9 4.2 140 430 - -
eca-rers2012/Problem07_label35_false-unreach-call.c unreach-call out of memory 47     47     570     15000   .84 0      error (invalid witness file) .64 .39 7.1 40 error (invalid witness file) 7.6 4.1 130 420 - -
eca-rers2012/Problem07_label36_false-unreach-call.c unreach-call out of memory 47     47     650     15000   .84 0      error (invalid witness file) .54 .35 7.7 39 error (invalid witness file) 8.2 4.4 130 440 - -
eca-rers2012/Problem07_label37_false-unreach-call.c unreach-call out of memory 48     47     540     15000   .84 0      error (invalid witness file) .63 .41 8.5 41 error (invalid witness file) 7.8 4.2 120 430 - -
eca-rers2012/Problem07_label39_false-unreach-call.c unreach-call out of memory 48     47     540     15000   .84 0      error (invalid witness file) .55 .35 9.6 39 error (invalid witness file) 7.6 4.1 120 430 - -
eca-rers2012/Problem07_label40_false-unreach-call.c unreach-call out of memory 47     47     430     15000   .84 0      error (invalid witness file) .59 .38 8.3 40 error (invalid witness file) 7.7 4.1 87 440 - -
eca-rers2012/Problem07_label42_false-unreach-call.c unreach-call out of memory 47     47     620     15000   .84 0      error (invalid witness file) .61 .38 9.6 40 error (invalid witness file) 7.6 4.1 140 430 - -
eca-rers2012/Problem07_label44_false-unreach-call.c unreach-call out of memory 47     47     480     15000   .84 0      error (invalid witness file) .53 .33 10   41 error (invalid witness file) 7.5 4.0 110 430 - -
eca-rers2012/Problem07_label46_false-unreach-call.c unreach-call out of memory 47     47     560     15000   .84 0      error (invalid witness file) .58 .37 9.6 40 error (invalid witness file) 8.3 4.4 160 430 - -
eca-rers2012/Problem07_label47_false-unreach-call.c unreach-call out of memory 47     47     490     15000   .84 0      error (invalid witness file) .52 .33 11   41 error (invalid witness file) 7.7 4.1 120 420 - -
eca-rers2012/Problem07_label48_false-unreach-call.c unreach-call out of memory 47     47     620     15000   .84 0      error (invalid witness file) .64 .41 7.9 40 error (invalid witness file) 7.3 3.9 120 420 - -
eca-rers2012/Problem07_label58_false-unreach-call.c unreach-call out of memory 47     47     660     15000   .84 0      error (invalid witness file) .66 .42 7.4 41 error (invalid witness file) 7.8 4.2 110 430 - -
eca-rers2012/Problem08_label01_false-unreach-call.c unreach-call out of memory 53     53     670     15000   .84 0      error (invalid witness file) .57 .36 11   44 error (invalid witness file) 8.6 4.7 130 520 - -
eca-rers2012/Problem08_label02_false-unreach-call.c unreach-call out of memory 54     53     560     15000   .84 0      error (invalid witness file) .68 .46 7.3 41 error (invalid witness file) 8.4 4.6 130 520 - -
eca-rers2012/Problem08_label04_false-unreach-call.c unreach-call out of memory 53     53     560     15000   .84 0      error (invalid witness file) .58 .38 8.1 39 error (invalid witness file) 9.1 5.0 150 530 - -
eca-rers2012/Problem08_label05_false-unreach-call.c unreach-call out of memory 53     53     650     15000   .84 0      error (invalid witness file) .60 .38 11   40 error (invalid witness file) 8.4 4.6 150 530 - -
eca-rers2012/Problem08_label06_false-unreach-call.c unreach-call out of memory 54     54     570     15000   .84 0      error (invalid witness file) .51 .33 7.6 39 error (invalid witness file) 8.4 4.6 130 520 - -
eca-rers2012/Problem08_label07_false-unreach-call.c unreach-call out of memory 54     53     570     15000   .84 0      error (invalid witness file) .57 .36 13   44 error (invalid witness file) 8.0 4.4 130 520 - -
eca-rers2012/Problem08_label10_false-unreach-call.c unreach-call out of memory 54     53     630     15000   .84 0      error (invalid witness file) .48 .31 7.4 40 error (invalid witness file) 8.4 4.6 160 520 - -
eca-rers2012/Problem08_label13_false-unreach-call.c unreach-call out of memory 54     53     560     15000   .84 0      error (invalid witness file) .66 .42 6.3 42 error (invalid witness file) 8.8 4.8 180 520 - -
eca-rers2012/Problem08_label15_false-unreach-call.c unreach-call out of memory 54     53     520     15000   .84 0      error (invalid witness file) .64 .40 9.3 40 error (invalid witness file) 9.2 5.0 120 520 - -
eca-rers2012/Problem08_label24_false-unreach-call.c unreach-call out of memory 54     53     600     15000   .84 0      error (invalid witness file) .66 .41 7.5 40 error (invalid witness file) 8.4 4.6 140 520 - -
eca-rers2012/Problem08_label25_false-unreach-call.c unreach-call out of memory 54     53     550     15000   .84 0      error (invalid witness file) .61 .39 9.6 40 error (invalid witness file) 8.2 4.5 130 520 - -
eca-rers2012/Problem08_label26_false-unreach-call.c unreach-call out of memory 54     54     610     15000   .84 0      error (invalid witness file) .51 .32 12   40 error (invalid witness file) 8.7 4.8 150 520 - -
eca-rers2012/Problem08_label28_false-unreach-call.c unreach-call out of memory 54     53     550     15000   .84 0      error (invalid witness file) .53 .33 14   41 error (invalid witness file) 8.1 4.4 140 520 - -
eca-rers2012/Problem08_label29_false-unreach-call.c unreach-call out of memory 54     53     580     15000   .84 0      error (invalid witness file) .55 .36 10   40 error (invalid witness file) 8.7 4.7 120 520 - -
eca-rers2012/Problem08_label34_false-unreach-call.c unreach-call out of memory 53     53     510     15000   .84 0      error (invalid witness file) .55 .36 13   43 error (invalid witness file) 8.8 4.9 110 530 - -
eca-rers2012/Problem08_label37_false-unreach-call.c unreach-call out of memory 54     53     640     15000   .84 0      error (invalid witness file) .64 .41 9.8 40 error (invalid witness file) 8.3 4.5 150 510 - -
eca-rers2012/Problem08_label43_false-unreach-call.c unreach-call out of memory 53     52     700     15000   .84 0      error (invalid witness file) .64 .39 9.2 39 error (invalid witness file) 8.3 4.5 94 520 - -
eca-rers2012/Problem08_label46_false-unreach-call.c unreach-call out of memory 54     53     610     15000   .84 .0082 error (invalid witness file) .63 .39 8.5 39 error (invalid witness file) 8.7 4.8 150 520 - -
eca-rers2012/Problem08_label48_false-unreach-call.c unreach-call out of memory 53     53     690     15000   .84 0      error (invalid witness file) .58 .38 6.8 40 error (invalid witness file) 8.1 4.5 120 510 - -
eca-rers2012/Problem08_label49_false-unreach-call.c unreach-call out of memory 53     53     540     15000   .84 0      error (invalid witness file) .49 .32 11   40 error (invalid witness file) 8.8 4.8 130 520 - -
eca-rers2012/Problem08_label50_false-unreach-call.c unreach-call out of memory 53     53     560     15000   .84 0      error (invalid witness file) .51 .32 11   39 error (invalid witness file) 8.7 4.8 130 520 - -
eca-rers2012/Problem08_label51_false-unreach-call.c unreach-call out of memory 54     53     590     15000   .84 0      error (invalid witness file) .58 .37 11   43 error (invalid witness file) 8.2 4.5 130 510 - -
eca-rers2012/Problem08_label55_false-unreach-call.c unreach-call out of memory 54     53     540     15000   .84 0      error (invalid witness file) .49 .31 9.4 39 error (invalid witness file) 8.6 4.7 130 530 - -
eca-rers2012/Problem08_label59_false-unreach-call.c unreach-call out of memory 54     54     570     15000   .84 .0041 error (invalid witness file) .49 .32 8.5 39 error (invalid witness file) 7.7 4.3 140 510 - -
eca-rers2012/Problem09_label02_false-unreach-call.c unreach-call out of memory 50     50     540     15000   .84 0      error (invalid witness file) .57 .37 9.1 42 error (invalid witness file) 8.4 4.6 130 530 - -
eca-rers2012/Problem09_label03_false-unreach-call.c unreach-call out of memory 50     50     530     15000   .84 0      error (invalid witness file) .66 .43 8.8 41 error (invalid witness file) 8.3 4.6 140 530 - -
eca-rers2012/Problem09_label06_false-unreach-call.c unreach-call out of memory 50     50     550     15000   .84 0      error (invalid witness file) .59 .38 11   41 error (invalid witness file) 8.0 4.4 130 520 - -
eca-rers2012/Problem09_label08_false-unreach-call.c unreach-call out of memory 50     49     510     15000   .84 0      error (invalid witness file) .50 .32 11   39 error (invalid witness file) 7.7 4.3 88 530 - -
eca-rers2012/Problem09_label10_false-unreach-call.c unreach-call out of memory 50     49     510     15000   .84 0      error (invalid witness file) .51 .33 11   40 error (invalid witness file) 8.5 4.7 130 540 - -
eca-rers2012/Problem09_label11_false-unreach-call.c unreach-call out of memory 50     50     580     15000   .84 0      error (invalid witness file) .56 .36 13   44 error (invalid witness file) 8.9 5.0 160 520 - -
eca-rers2012/Problem09_label15_false-unreach-call.c unreach-call out of memory 50     49     620     15000   .84 0      error (invalid witness file) .65 .41 8.8 39 error (invalid witness file) 8.9 4.9 140 540 - -
eca-rers2012/Problem09_label19_false-unreach-call.c unreach-call out of memory 50     49     460     15000   .84 0      error (invalid witness file) .62 .39 8.1 39 error (invalid witness file) 8.5 4.7 140 540 - -
eca-rers2012/Problem09_label20_false-unreach-call.c unreach-call out of memory 50     50     530     15000   .84 0      error (invalid witness file) .62 .40 6.8 41 error (invalid witness file) 9.4 5.1 120 540 - -
eca-rers2012/Problem09_label32_false-unreach-call.c unreach-call out of memory 50     50     520     15000   .84 0      error (invalid witness file) .56 .35 13   41 error (invalid witness file) 11   5.9 54 520 - -
eca-rers2012/Problem09_label34_false-unreach-call.c unreach-call out of memory 49     49     500     15000   .84 0      error (invalid witness file) .55 .35 14   42 error (invalid witness file) 9.8 5.4 69 520 - -
eca-rers2012/Problem09_label35_false-unreach-call.c unreach-call out of memory 50     50     490     15000   .84 0      error (invalid witness file) .67 .43 7.9 42 error (invalid witness file) 8.6 4.7 140 530 - -
eca-rers2012/Problem09_label36_false-unreach-call.c unreach-call out of memory 50     50     560     15000   .84 0      error (invalid witness file) .56 .37 11   41 error (invalid witness file) 8.1 4.5 160 520 - -
eca-rers2012/Problem09_label38_false-unreach-call.c unreach-call out of memory 50     50     480     15000   .84 0      error (invalid witness file) .54 .35 12   41 error (invalid witness file) 7.9 4.5 130 520 - -
eca-rers2012/Problem09_label41_false-unreach-call.c unreach-call out of memory 50     49     560     15000   .84 0      error (invalid witness file) .61 .38 8.7 39 error (invalid witness file) 7.9 4.4 120 630 - -
eca-rers2012/Problem09_label44_false-unreach-call.c unreach-call out of memory 50     50     470     15000   .84 0      error (invalid witness file) .55 .36 8.2 40 error (invalid witness file) 8.6 4.8 130 520 - -
eca-rers2012/Problem09_label46_false-unreach-call.c unreach-call out of memory 50     50     530     15000   .84 0      error (invalid witness file) .50 .33 14   39 error (invalid witness file) 8.5 4.7 160 520 - -
eca-rers2012/Problem09_label47_false-unreach-call.c unreach-call out of memory 50     50     530     15000   .84 0      error (invalid witness file) .49 .33 13   39 error (invalid witness file) 7.9 4.4 120 530 - -
eca-rers2012/Problem09_label51_false-unreach-call.c unreach-call out of memory 50     50     550     15000   .84 0      error (invalid witness file) .53 .34 11   42 error (invalid witness file) 8.9 4.9 130 530 - -
eca-rers2012/Problem09_label53_false-unreach-call.c unreach-call out of memory 50     49     630     15000   .84 0      error (invalid witness file) .50 .32 9.1 40 error (invalid witness file) 10   5.5 140 530 - -
eca-rers2012/Problem09_label54_false-unreach-call.c unreach-call out of memory 51     50     590     15000   .84 0      error (invalid witness file) .66 .42 8.6 40 error (invalid witness file) 8.4 4.6 130 540 - -
eca-rers2012/Problem09_label56_false-unreach-call.c unreach-call out of memory 51     50     550     15000   .84 0      error (invalid witness file) .51 .34 10   40 error (invalid witness file) 8.2 4.6 110 520 - -
eca-rers2012/Problem09_label57_false-unreach-call.c unreach-call out of memory 50     50     560     15000   .84 0      error (invalid witness file) .73 .45 8.8 42 error (invalid witness file) 8.5 4.7 110 530 - -
eca-rers2012/Problem09_label59_false-unreach-call.c unreach-call out of memory 49     49     610     15000   .84 0      error (invalid witness file) .52 .34 12   41 error (invalid witness file) 8.2 4.5 140 530 - -
eca-rers2012/Problem10_label12_false-unreach-call.c unreach-call out of memory 62     61     690     15000   .84 0      error (invalid witness file) .52 .33 13   41 error (invalid witness file) 7.4 3.9 66 300 - -
eca-rers2012/Problem10_label15_false-unreach-call.c unreach-call out of memory 62     62     680     15000   .84 0      error (invalid witness file) .59 .38 8.4 40 error (invalid witness file) 6.6 3.5 79 310 - -
eca-rers2012/Problem10_label24_false-unreach-call.c unreach-call out of memory 63     62     710     15000   .84 0      error (invalid witness file) .66 .41 7.5 39 error (invalid witness file) 6.3 3.3 110 300 - -
eca-rers2012/Problem10_label26_false-unreach-call.c unreach-call out of memory 62     62     720     15000   .84 0      error (invalid witness file) .54 .34 11   42 error (invalid witness file) 6.2 3.2 98 300 - -
eca-rers2012/Problem10_label28_false-unreach-call.c unreach-call out of memory 63     62     680     15000   .84 0      error (invalid witness file) .47 .30 7.2 40 error (invalid witness file) 6.6 3.4 99 300 - -
eca-rers2012/Problem10_label29_false-unreach-call.c unreach-call out of memory 62     62     720     15000   .98 0      error (invalid witness file) .56 .34 13   40 error (invalid witness file) 5.8 3.2 96 300 - -
eca-rers2012/Problem10_label41_false-unreach-call.c unreach-call out of memory 62     61     740     15000   .84 0      error (invalid witness file) .51 .32 13   41 error (invalid witness file) 6.7 3.5 79 310 - -
eca-rers2012/Problem10_label42_false-unreach-call.c unreach-call out of memory 63     62     660     15000   .84 0      error (invalid witness file) .54 .34 13   42 error (invalid witness file) 5.7 3.0 93 300 - -
eca-rers2012/Problem10_label46_false-unreach-call.c unreach-call out of memory 61     61     680     15000   .84 0      error (invalid witness file) .58 .38 5.7 39 error (invalid witness file) 5.4 2.9 68 280 - -
eca-rers2012/Problem10_label47_false-unreach-call.c unreach-call out of memory 62     62     670     15000   .98 0      error (invalid witness file) .65 .43 7.7 41 error (invalid witness file) 6.3 3.3 80 320 - -
eca-rers2012/Problem10_label48_false-unreach-call.c unreach-call out of memory 62     62     590     15000   .84 0      error (invalid witness file) .51 .32 9.9 39 error (invalid witness file) 6.6 3.5 55 290 - -
eca-rers2012/Problem10_label50_false-unreach-call.c unreach-call out of memory 62     61     580     15000   .84 0      error (invalid witness file) .53 .34 11   39 error (invalid witness file) 5.6 3.0 86 290 - -
eca-rers2012/Problem10_label55_false-unreach-call.c unreach-call out of memory 62     61     640     15000   .84 0      error (invalid witness file) .49 .32 7.0 41 error (invalid witness file) 6.0 3.2 100 310 - -
eca-rers2012/Problem10_label57_false-unreach-call.c unreach-call out of memory 61     61     780     15000   .99 0      error (invalid witness file) .64 .41 6.5 41 error (invalid witness file) 6.2 3.2 110 300 - -
eca-rers2012/Problem10_label58_false-unreach-call.c unreach-call out of memory 62     61     800     15000   .84 0      error (invalid witness file) .54 .36 9.1 40 error (invalid witness file) 8.9 4.6 110 300 - -
eca-rers2012/Problem11_label00_false-unreach-call.c unreach-call out of memory 54     53     710     15000   .84 0      error (invalid witness file) .51 .32 11   39 error (invalid witness file) 5.9 3.2 95 300 - -
eca-rers2012/Problem11_label08_false-unreach-call.c unreach-call out of memory 54     53     610     15000   .84 0      error (invalid witness file) .53 .34 8.5 40 error (invalid witness file) 6.6 3.4 140 300 - -
eca-rers2012/Problem11_label14_false-unreach-call.c unreach-call out of memory 54     53     650     15000   .84 0      error (invalid witness file) .55 .36 12   43 error (invalid witness file) 6.0 3.2 100 300 - -
eca-rers2012/Problem11_label15_false-unreach-call.c unreach-call out of memory 53     53     590     15000   .84 0      error (invalid witness file) .50 .33 11   42 error (invalid witness file) 6.0 3.2 100 290 - -
eca-rers2012/Problem11_label20_false-unreach-call.c unreach-call out of memory 53     53     560     15000   .84 0      error (invalid witness file) .53 .33 11   40 error (invalid witness file) 7.2 3.7 140 310 - -
eca-rers2012/Problem11_label29_false-unreach-call.c unreach-call out of memory 53     53     600     15000   .84 0      error (invalid witness file) .70 .44 8.2 43 error (invalid witness file) 6.4 3.4 90 300 - -
eca-rers2012/Problem11_label31_false-unreach-call.c unreach-call out of memory 54     53     620     15000   .84 0      error (invalid witness file) .53 .34 11   39 error (invalid witness file) 6.3 3.3 82 300 -