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