Tool Ceagle Ceagle 1.3 @ 53cfa89
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:52:12 CET ]] [[ 2017-01-14 18:07:02 CET ]] [[ 2017-01-14 19:59:19 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options --compiler clang-3.7 [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.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/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ceagle.2017-01-10_1721.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]]
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
heap-manipulation/bubble_sort_linux_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .14  .14  1.4  8.3 0      0      error (invalid witness file) .49 .32 9.5 43 error (invalid witness file) 6.3 3.3 100 290 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .15  .28  1.9  44   0      36      error (invalid witness file) .51 .34 13   41 error (invalid witness file) 8.0 4.2 97 300 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.4  7.9 0      0      error (invalid witness file) .51 .33 11   42 error (invalid witness file) 7.0 3.6 97 300 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.5  8.2 0      0      error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.6 3.5 120 330 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i aborted 0 wit inspect .13  .13  1.3  7.9 0      0      error (invalid witness file) .48 .32 11   40 error (invalid witness file) 7.7 4.0 82 290 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.2  8.1 0      0      error (invalid witness file) .54 .35 12   40 error (invalid witness file) 6.2 3.3 110 310 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .16  .16  1.6  8.1 0      0      - - error (invalid witness file) .60 .38 10   45 error (invalid witness file) 6.1 3.2 110 310
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .12  .12  1.1  7.9 0      0      - - error (invalid witness file) .50 .35 5.0 40 error (invalid witness file) 7.7 4.0 85 310
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .13  .13  1.3  8.0 0      0      - - error (invalid witness file) .61 .39 8.0 40 error (invalid witness file) 6.6 3.5 95 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.3  7.9 0      0      - - error (invalid witness file) .64 .41 10   44 error (invalid witness file) 6.4 3.4 100 280
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .15  .15  1.3  8.2 0      0      - - error (invalid witness file) .58 .36 12   43 error (invalid witness file) 6.5 3.5 120 310
heap-manipulation/tree_true-unreach-call.i aborted 0 wit inspect .14  .14  1.3  7.7 0      0      - - error (invalid witness file) .56 .36 11   39 error (invalid witness file) 5.9 3.2 120 300
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .12  .12  1.1  7.7 0      0      error (invalid witness file) .50 .33 10   42 error (invalid witness file) 7.5 4.0 80 310 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.3  7.9 0      0      error (invalid witness file) .57 .36 13   42 error (invalid witness file) 7.4 3.8 100 310 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.3  8.1 0      0      error (invalid witness file) .53 .33 13   40 error (invalid witness file) 6.2 3.2 130 300 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .13  .13  1.2  7.9 0      0      error (invalid witness file) .54 .35 14   42 error (invalid witness file) 8.4 4.4 78 310 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.1  7.9 0      .041  error (invalid witness file) .55 .34 13   41 error (invalid witness file) 6.3 3.4 110 310 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .13  .13  1.2  8.0 0      0      error (invalid witness file) .52 .33 9.8 41 error (invalid witness file) 5.7 3.1 110 300 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.1  8.1 0      .070  - - error (invalid witness file) .51 .33 9.7 41 error (invalid witness file) 5.9 3.2 130 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .14  .14  1.0  7.9 0      0      - - error (invalid witness file) .57 .37 11   39 error (invalid witness file) 5.7 3.1 100 300
list-properties/list_search_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .12  .12  1.3  8.0 0      0      - - error (invalid witness file) .59 .39 8.9 40 error (invalid witness file) 6.2 3.3 110 310
list-properties/list_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .12  .12  1.1  7.9 0      0      - - error (invalid witness file) .69 .43 8.5 44 error (invalid witness file) 6.3 3.3 100 300
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .12  .12  1.0  8.1 0      0      - - error (invalid witness file) .63 .40 7.9 39 error (invalid witness file) 5.6 3.0 110 290
list-properties/simple_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .14  .14  1.1  7.9 0      0      - - error (invalid witness file) .66 .41 6.9 41 error (invalid witness file) 7.9 4.1 80 300
list-properties/splice_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .14  .15  1.1  7.9 0      0      - - error (invalid witness file) .52 .34 11   40 error (invalid witness file) 5.8 3.1 120 300
ldv-regression/1_3.c_false-unreach-call.i unknown 0 wit inspect .10  .10  1.2  7.8 0      0      error (invalid witness file) .47 .31 8.8 40 error (invalid witness file) 7.2 3.8 83 310 - -
ldv-regression/alt_test.c_false-unreach-call.i aborted 0 wit inspect .11  .11  1.6  8.1 0      .098  error (invalid witness file) .52 .33 10   42 error (invalid witness file) 6.2 3.3 110 300 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect .045 .046 .47 7.8 .0082 .070  false(unreach-call) 3.7  2.1  85   260 false(unreach-call) 7.2 3.8 140 320 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .080 .081 .96 8.0 0      0      error (invalid witness file) .60 .38 11   42 error (invalid witness file) 6.4 3.4 89 300 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .069 .069 .58 7.8 0      0      false(unreach-call) 3.7  2.1  69   280 true 7.5 4.0 120 310 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect .068 .068 .60 7.8 0      0      false(unreach-call) 3.6  2.0  47   280 true 9.6 5.1 100 310 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect .056 .056 .47 7.8 .0082 0      false(unreach-call) 4.0  2.3  81   270 true 7.6 4.1 140 340 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i unknown 0 wit inspect .10  .10  1.4  7.8 0      0      error (invalid witness file) .52 .34 13   40 error (invalid witness file) 7.4 3.9 100 300 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i aborted 0 wit inspect .11  .11  1.3  8.0 0      0      error (invalid witness file) .48 .31 10   40 error (invalid witness file) 7.0 3.7 82 290 - -
ldv-regression/stateful_check_false-unreach-call.i aborted 0 wit inspect .12  .12  1.4  7.8 0      0      error (invalid witness file) .54 .33 13   40 error (invalid witness file) 8.1 4.2 94 310 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .16  .20  .50 17   .0082 12      false(unreach-call) 3.8  2.1  82   270 true 7.0 3.8 120 320 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .061 .064 .59 7.7 .0082 .86   false(unreach-call) 3.6  2.0  78   270 true 8.8 4.7 130 320 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect .064 .064 .44 7.9 .0082 0      - - true 4.0  2.3  50   260 true 7.7 4.2 140 310
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect .097 .12  .45 14   .0082 6.9    - - true 3.4  1.9  72   260 true 7.6 4.0 160 310
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect .10  .10  .58 7.7 0      0      - - true 4.3  2.4  57   260 true 8.7 4.7 170 330
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect .078 .078 .22 7.9 0      0      - - true 3.4  1.9  62   260 true 8.4 4.4 160 340
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect .062 .065 .55 7.9 .0082 .070  - - true 22    12    230   520 true 31   18   530 710
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect .044 .044 .57 7.6 .0082 0      - - true 3.8  2.1  50   250 true 7.4 3.9 120 310
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect .093 .093 .44 7.8 0      0      - - true 3.9  2.2  47   260 true 9.2 4.9 190 330
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect .11  .24  .82 44   0      36      - - true 3.6  2.0  68   260 true 8.5 4.6 170 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect .056 .057 .44 7.9 .0082 .070  - - true 3.4  1.9  49   260 true 11   6.1 140 350
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect .11  .11  .40 7.8 .0082 0      - - true 4.2  2.4  47   260 true 7.2 3.8 140 310
ldv-regression/nested_structure_noptr_true-unreach-call.i unknown 0 wit inspect .031 .033 .27 7.9 .0041 .066  - - error (invalid witness file) .62 .40 8.1 39 error (invalid witness file) 7.1 3.7 90 300
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect .088 .11  .61 13   .0082 6.6    - - true 4.7  2.6  40   270 true 12   6.6 210 430
ldv-regression/nested_structure_ptr_true-unreach-call.i unknown 0 wit inspect .047 .049 .25 7.8 .0041 .066  - - error (invalid witness file) .59 .37 9.4 40 error (invalid witness file) 7.4 3.8 82 290
ldv-regression/nested_structure_true-unreach-call.i unknown 0 wit inspect .053 .066 .27 8.1 .0041 3.2    - - error (invalid witness file) .52 .35 12   40 error (invalid witness file) 5.2 2.8 110 280
ldv-regression/oomInt.c_true-unreach-call.i unknown 0 wit inspect .074 .074 .19 7.8 .0041 0      - - error (invalid witness file) .50 .32 8.9 41 error (invalid witness file) 5.7 3.1 110 290
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect .056 .056 .45 8.0 .0082 0      - - true 3.5  2.0  57   260 true 7.3 3.9 150 330
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i unknown 0 wit inspect .11  .11  1.1  7.8 0      0      - - error (invalid witness file) .56 .36 8.1 40 error (invalid witness file) 5.5 2.9 120 290
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect .071 .071 .59 8.0 .0082 0      - - true 4.5  2.4  56   260 true 11   6.3 220 370
ldv-regression/rule60_list2.c_true-unreach-call.i aborted 0 wit inspect .12  .12  1.1  7.7 0      .041  - - error (invalid witness file) .58 .37 9.4 40 error (invalid witness file) 5.9 3.1 130 290
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect .027 .027 .18 7.9 0      0      - - true 4.1  2.3  53   260 true 8.8 4.6 160 330
ldv-regression/structure_assignment.c_true-unreach-call.i unknown 0 wit inspect .10  .10  1.3  7.8 0      0      - - error (invalid witness file) .52 .35 6.9 40 error (invalid witness file) 5.6 3.0 89 290
ldv-regression/test_address.c_true-unreach-call.i aborted 0 wit inspect .11  .11  1.3  7.8 0      .020  - - error (invalid witness file) .50 .33 9.7 39 error (invalid witness file) 5.8 3.1 100 300
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect .053 .054 .48 7.9 .0082 0      - - true 4.0  2.2  51   260 true 9.4 5.0 99 320
ldv-regression/test_malloc-1_true-unreach-call.i unknown 0 wit inspect .049 .049 .38 7.9 .0041 0      - - error (invalid witness file) .55 .36 11   40 error (invalid witness file) 6.1 3.2 110 310
ldv-regression/test_malloc-2_true-unreach-call.i unknown 0 wit inspect .045 .045 .30 8.0 .0041 .0082 - - error (invalid witness file) .57 .36 11   39 error (invalid witness file) 5.6 3.0 120 290
ldv-regression/test_overflow.c_true-unreach-call.i aborted 0 wit inspect .11  .11  1.1  8.5 0      .42   - - error (invalid witness file) .56 .36 8.7 40 error (invalid witness file) 6.4 3.3 100 310
ldv-regression/test_union.c_true-unreach-call.i unknown 0 wit inspect .12  .12  1.2  7.6 0      0      - - error (invalid witness file) .54 .33 14   40 error (invalid witness file) 6.6 3.5 130 310
ldv-regression/test_union.c_true-unreach-call_1.i unknown 0 wit inspect .11  .11  1.0  7.7 0      0      - - error (invalid witness file) .71 .45 7.9 43 error (invalid witness file) 6.2 3.2 110 300
ldv-regression/test_union_cast-1_true-unreach-call.i unknown 0 wit inspect .14  .14  1.1  7.7 0      0      - - error (invalid witness file) .55 .35 9.6 40 error (invalid witness file) 5.6 3.0 110 290
ldv-regression/test_union_cast-2_true-unreach-call.i unknown 0 wit inspect .099 .099 1.1  7.9 0      0      - - error (invalid witness file) .53 .35 9.9 40 error (invalid witness file) 6.3 3.3 110 290
ldv-regression/test_union_cast.c_true-unreach-call.i unknown 0 wit inspect .14  .26  1.4  43   0      35      - - error (invalid witness file) .56 .35 12   45 error (invalid witness file) 6.1 3.3 130 290
ldv-regression/test_union_cast.c_true-unreach-call_1.i unknown 0 wit inspect .11  .11  1.2  7.7 0      0      - - error (invalid witness file) .66 .40 7.8 40 error (invalid witness file) 6.5 3.4 80 290
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect .061 .061 .46 7.8 .0082 .0041 - - true 4.4  2.5  42   260 true 8.0 4.3 170 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect .054 .057 .44 7.9 .0082 .070  - - true 3.5  1.9  62   250 true 7.7 4.1 120 310
ldv-regression/test02_false-unreach-call.c unknown 0 wit inspect .13  .13  1.0  7.9 0      0      error (invalid witness file) .49 .31 12   39 error (invalid witness file) 6.9 3.7 74 300 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect .070 .069 .48 7.8 0      0      false(unreach-call) 3.9  2.2  88   290 true 9.3 5.0 96 320 - -
ldv-regression/test08_false-unreach-call.c unknown 0 wit inspect .13  .13  1.7  7.7 0      0      error (invalid witness file) .55 .34 14   40 error (invalid witness file) 6.2 3.3 78 290 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect .063 .063 .50 8.0 .0082 .0041 false(unreach-call) 3.8  2.1  80   280 false(unreach-call) 7.5 3.9 140 320 - -
ldv-regression/test21_false-unreach-call.c segmentation fault 0 wit inspect .054 .056 .14 8.1 0      0      error (invalid witness file) .52 .33 12   39 error (invalid witness file) 6.5 3.4 92 290 - -
ldv-regression/test22_false-unreach-call.c aborted 0 wit inspect .12  .12  .93 7.8 0      0      error (invalid witness file) .51 .33 13   39 error (invalid witness file) 7.0 3.7 93 290 - -
ldv-regression/test23_false-unreach-call.c aborted 0 wit inspect .11  .11  1.2  8.0 0      0      error (invalid witness file) .49 .32 13   39 error (invalid witness file) 7.3 3.8 85 310 - -
ldv-regression/test24_false-unreach-call.c aborted 0 wit inspect .11  .11  1.1  7.8 0      0      error (invalid witness file) .52 .34 11   42 error (invalid witness file) 7.4 3.9 78 300 - -
ldv-regression/test25_false-unreach-call.c aborted 0 wit inspect .12  .12  1.0  7.7 0      0      error (invalid witness file) .61 .39 15   44 error (invalid witness file) 7.2 3.8 64 300 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect .052 .053 .35 7.7 0      0      error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.5 2.9 100 300 - -
ldv-regression/test27_false-unreach-call.c aborted 0 wit inspect .099 .10  1.3  7.5 0      0      error (invalid witness file) .49 .33 13   41 error (invalid witness file) 7.5 3.9 100 290 - -
ldv-regression/test28_false-unreach-call.c unknown 0 wit inspect .12  .12  1.2  7.6 0      0      error (invalid witness file) .49 .32 9.9 39 error (invalid witness file) 6.7 3.6 68 290 - -
ldv-regression/test29_false-unreach-call.c unknown 0 wit inspect .15  .15  1.3  7.9 0      0      error (invalid witness file) .53 .34 11   41 error (invalid witness file) 6.7 3.5 98 300 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect .049 .049 .40 7.8 0      0      false(unreach-call) 3.6  2.0  75   270 true 7.8 4.1 130 320 - -
ldv-regression/test01_true-unreach-call.c unknown 0 wit inspect .11  .11  1.1  7.8 0      0      - - error (invalid witness file) .58 .38 8.9 40 error (invalid witness file) 5.6 3.0 120 300
ldv-regression/test03_true-unreach-call.c unknown 0 wit inspect .12  .12  1.1  7.9 0      0      - - error (invalid witness file) .56 .35 9.9 43 error (invalid witness file) 5.9 3.1 100 300
ldv-regression/test04_true-unreach-call.c unknown 0 wit inspect .10  .10  1.3  7.7 0      0      - - error (invalid witness file) .63 .40 7.5 43 error (invalid witness file) 5.9 3.2 120 300
ldv-regression/test05_true-unreach-call.c true 2 wit inspect .12  .12  .70 7.7 0      0      - - true 3.5  1.9  43   260 true 15   8.8 200 530
ldv-regression/test07_true-unreach-call.c unknown 0 wit inspect .14  .14  1.5  7.6 0      0      - - error (invalid witness file) .64 .42 8.0 41 error (invalid witness file) 5.9 3.1 110 290
ldv-regression/test09_true-unreach-call.c true 2 wit inspect .068 .068 .38 7.9 0      0      - - true 3.9  2.2  60   260 true 11   5.9 180 430
ldv-regression/test10_true-unreach-call.c true 2 wit inspect .052 .053 .48 7.8 0      0      - - true 4.0  2.2  71   260 true 15   8.9 290 470
ldv-regression/test11_true-unreach-call.c segmentation fault 0 wit inspect .035 .035 .14 7.6 0      0      - - error (invalid witness file) .62 .40 10   43 error (invalid witness file) 6.1 3.2 100 300
ldv-regression/test13_true-unreach-call.c true 2 wit inspect .090 .090 .45 7.7 .0082 .0041 - - true 4.1  2.3  50   250 true 7.3 4.0 130 310
ldv-regression/test14_true-unreach-call.c aborted 0 wit inspect .10  .10  1.1  7.7 0      0      - - error (invalid witness file) .55 .35 10   42 error (invalid witness file) 5.3 2.9 100 290
ldv-regression/test15_true-unreach-call.c true 2 wit inspect .045 .045 .28 7.8 0      0      - - true 3.4  1.9  47   250 true 9.7 5.3 180 340
ldv-regression/test16_true-unreach-call.c true 2 wit inspect .056 .056 .54 7.9 .0082 0      - - true 3.4  1.9  66   250 true 9.5 5.2 200 350
ldv-regression/test17_true-unreach-call.c true 2 wit inspect .059 .060 .44 7.8 .0082 .066  - - true 3.9  2.2  58   260 true 7.4 4.0 150 310
ldv-regression/test18_true-unreach-call.c true 2 wit inspect .079 .079 .21 7.8 0      0      - - true 3.3  1.9  72   260 true 9.6 5.2 190 330
ldv-regression/test19_true-unreach-call.c true 2 wit inspect .042 .042 .31 7.8 0      0      - - true 4.4  2.4  46   260 true 11   6.2 250 450
ldv-regression/test20_true-unreach-call.c true 2 wit inspect .057 .058 .44 7.9 .0082 0      - - true 4.2  2.4  50   260 true 7.9 4.3 160 320
ldv-regression/test21_true-unreach-call.c segmentation fault 0 wit inspect .051 .051 .12 7.7 0      0      - - error (invalid witness file) .57 .37 8.5 40 error (invalid witness file) 6.6 3.4 120 310
ldv-regression/test22_true-unreach-call.c aborted 0 wit inspect .094 .094 1.8  7.5 0      0      - - error (invalid witness file) .57 .37 9.6 40 error (invalid witness file) 6.9 3.6 93 290
ldv-regression/test23_true-unreach-call.c aborted 0 wit inspect .10  .10  1.2  7.8 0      0      - - error (invalid witness file) .58 .38 11   40 error (invalid witness file) 5.9 3.1 110 300
ldv-regression/test24_true-unreach-call.c aborted 0 wit inspect .11  .11  1.0  7.7 0      0      - - error (invalid witness file) .57 .37 9.6 40 error (invalid witness file) 6.1 3.2 100 300
ldv-regression/test25_true-unreach-call.c aborted 0 wit inspect .11  .11  1.1  8.0 0      0      - - error (invalid witness file) .65 .40 8.2 40 error (invalid witness file) 5.9 3.2 110 290
ldv-regression/test26_true-unreach-call.c true 2 wit inspect .044 .044 .28 7.8 0      0      - - error (invalid witness file) .58 .38 9.5 41 error (invalid witness file) 6.0 3.2 110 300
ldv-regression/test27_true-unreach-call.c aborted 0 wit inspect .10  .11  1.3  7.8 0      0      - - error (invalid witness file) .52 .34 10   42 error (invalid witness file) 5.9 3.1 120 300
ldv-regression/test28_true-unreach-call.c unknown 0 wit inspect .12  .12  1.3  7.6 0      0      - - error (invalid witness file) .61 .39 8.9 41 error (invalid witness file) 6.8 3.5 150 310
ldv-regression/test29_true-unreach-call.c unknown 0 wit inspect .12  .12  1.5  7.8 0      0      - - error (invalid witness file) .48 .31 8.1 39 error (invalid witness file) 5.7 3.1 120 290
ldv-regression/test30_true-unreach-call.c true 2 wit inspect .047 .047 .26 7.8 0      0      - - true 3.4  2.0  78   260 true 13   7.3 180 480
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .043 .044 .48 9.8 0      .11   error (invalid witness file) .53 .34 10   41 error (invalid witness file) 8.2 4.3 100 310 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .063 .063 .38 9.9 0      .13   error (invalid witness file) .60 .38 13   45 error (invalid witness file) 5.8 3.1 100 290 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .080 .080 .34 9.9 0      0      error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.8 3.6 70 300 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .048 .048 .33 9.6 0      0      - - error (invalid witness file) .58 .37 11   44 error (invalid witness file) 7.6 4.0 110 290
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .049 .049 .39 9.8 0      0      - - error (invalid witness file) .73 .45 8.7 42 error (invalid witness file) 7.4 3.8 110 310
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .084 .085 .33 9.8 0      .11   - - error (invalid witness file) .50 .35 9.5 39 error (invalid witness file) 8.9 4.7 100 310
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .046 .047 .36 9.8 0      .11   - - error (invalid witness file) .65 .42 8.7 40 error (invalid witness file) 6.1 3.2 120 290
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .046 .047 .39 9.7 0      .11   - - error (invalid witness file) .61 .38 8.3 40 error (invalid witness file) 6.5 3.4 120 310
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .055 .055 .29 9.7 0      .045  - - error (invalid witness file) .53 .35 11   40 error (invalid witness file) 6.3 3.3 130 300
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .036 .037 .55 9.6 0      .11   - - error (invalid witness file) .55 .35 10   40 error (invalid witness file) 6.3 3.3 120 300
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .065 .066 .33 9.9 0      .11   - - error (invalid witness file) .62 .39 9.4 44 error (invalid witness file) 6.8 3.6 150 290
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .076 .076 .38 9.7 0      0      - - error (invalid witness file) .60 .38 8.8 43 error (invalid witness file) 6.4 3.4 120 300
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .052 .052 .32 9.6 0      .11   - - error (invalid witness file) .58 .38 9.8 40 error (invalid witness file) 7.0 3.7 91 290
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.3  7.9 0      0      error (invalid witness file) .52 .34 13   41 error (invalid witness file) 5.9 3.1 110 290 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .13  .13  1.2  8.0 0      0      error (invalid witness file) .53 .34 13   43 error (invalid witness file) 7.2 3.8 79 300 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.3  7.9 0      0      error (invalid witness file) .52 .33 12   39 error (invalid witness file) 7.0 3.7 76 300 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .12  .12  1.2  8.0 0      0      error (invalid witness file) .51 .33 9.8 40 error (invalid witness file) 6.2 3.3 81 300 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i aborted 0 wit inspect .11  .11  1.1  8.0 0      0      error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.9 3.7 53 300 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .12  .12  1.2  8.2 0      0      error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.9 3.1 110 300 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.2  7.9 0      0      error (invalid witness file) .51 .32 12   39 error (invalid witness file) 5.4 3.0 110 290 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .12  .12  1.2  7.9 0      0      error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.1 3.2 120 300 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.1  8.1 0      0      error (invalid witness file) .52 .33 13   41 error (invalid witness file) 6.0 3.2 110 300 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i aborted 0 wit inspect .12  .12  1.2  8.0 0      0      error (invalid witness file) .52 .32 14   40 error (invalid witness file) 6.0 3.2 120 300 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .12  .12  1.2  7.9 0      0      error (invalid witness file) .51 .31 11   41 error (invalid witness file) 7.3 3.8 87 300 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.1  7.9 0      0      error (invalid witness file) .49 .31 9.8 39 error (invalid witness file) 6.9 3.6 90 300 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.2  8.0 0      0      error (invalid witness file) .52 .34 14   40 error (invalid witness file) 7.9 4.2 67 300 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.3  7.9 0      0      error (invalid witness file) .52 .32 12   40 error (invalid witness file) 9.8 5.1 88 320 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i aborted 0 wit inspect .11  .11  1.3  8.0 0      0      error (invalid witness file) .61 .40 9.9 40 error (invalid witness file) 6.1 3.2 86 290 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.2  8.2 0      0      error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.8 3.6 77 290 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .12  .12  1.2  8.0 0      0      error (invalid witness file) .59 .37 15   45 error (invalid witness file) 5.8 3.1 98 300 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .11  .11  1.5  7.8 0      0      error (invalid witness file) .53 .33 11   42 error (invalid witness file) 5.6 3.0 89 300 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .14  .14  1.1  8.0 0      0      error (invalid witness file) .51 .33 8.6 41 error (invalid witness file) 7.4 3.9 69 290 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.3  8.2 0      0      - - error (invalid witness file) .61 .39 8.2 41 error (invalid witness file) 7.8 4.1 83 310
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.2  8.0 0      0      - - error (invalid witness file) .64 .41 8.3 39 error (invalid witness file) 6.7 3.5 95 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.1  8.0 0      0      - - error (invalid witness file) .48 .32 10   40 error (invalid witness file) 5.9 3.2 110 290
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.3  7.9 0      0      - - error (invalid witness file) .68 .44 7.6 39 error (invalid witness file) 6.3 3.3 120 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.3  8.1 0      0      - - error (invalid witness file) .63 .40 8.3 39 error (invalid witness file) 6.5 3.5 110 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.2  8.0 0      0      - - error (invalid witness file) .49 .33 6.6 39 error (invalid witness file) 8.6 4.4 76 310
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.2  8.0 0      0      - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.1 3.3 110 300
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .11  .11  1.5  7.9 0      0      - - error (invalid witness file) .59 .37 10   40 error (invalid witness file) 5.7 3.1 100 290
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.4  8.0 0      0      - - error (invalid witness file) .59 .39 8.0 39 error (invalid witness file) 6.1 3.2 120 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .13  .13  1.2  7.9 0      0      - - error (invalid witness file) .52 .32 11   41 error (invalid witness file) 6.8 3.6 73 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.2  8.0 0      0      - - error (invalid witness file) .54 .35 10   44 error (invalid witness file) 5.9 3.1 110 320
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.2  8.3 0      0      - - error (invalid witness file) .61 .38 10   39 error (invalid witness file) 6.1 3.2 130 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.2  8.0 0      0      - - error (invalid witness file) .55 .36 10   40 error (invalid witness file) 5.7 3.0 120 290
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.1  8.0 0      0      - - error (invalid witness file) .61 .39 8.5 40 error (invalid witness file) 6.1 3.3 140 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.2  8.0 0      0      - - error (invalid witness file) .57 .37 9.0 42 error (invalid witness file) 6.0 3.2 75 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.4  8.4 0      .19   - - error (invalid witness file) .67 .41 11   43 error (invalid witness file) 6.0 3.2 120 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.2  7.9 0      0      - - error (invalid witness file) .54 .34 9.5 42 error (invalid witness file) 6.1 3.3 120 310
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.2  8.1 0      0      - - error (invalid witness file) .61 .38 7.7 40 error (invalid witness file) 7.3 3.9 84 300
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i aborted 0 wit inspect .12  .12  1.3  7.9 0      0      - - error (invalid witness file) .68 .43 9.0 43 error (invalid witness file) 6.9 3.7 130 320
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .12  .12  1.2  8.0 0      0      - - error (invalid witness file) .63 .39 9.7 41 error (invalid witness file) 5.9 3.1 100 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i aborted 0 wit inspect .11  .11  1.2  7.8 0      0      - - error (invalid witness file) .63 .41 9.1 39 error (invalid witness file) 6.3 3.3 120 300
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i aborted 0 wit inspect .11  .11  1.2  8.0 0      0      error (invalid witness file) .54 .33 13   40 error (invalid witness file) 6.0 3.2 100 300 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i aborted 0 wit inspect .12  .12  1.2  8.2 0      .074  error (invalid witness file) .49 .32 6.2 39 error (invalid witness file) 7.9 4.1 76 310 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i aborted 0 wit inspect .10  .10  1.1  8.0 0      0      error (invalid witness file) .50 .32 11   40 error (invalid witness file) 6.9 3.7 97 300 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i aborted 0 wit inspect .11  .11  1.3  8.3 0      .12   error (invalid witness file) .51 .32 13   40 error (invalid witness file) 6.6 3.5 110 300 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i aborted 0 wit inspect .11  .11  1.2  7.9 0      0      - - error (invalid witness file) .62 .40 7.5 39 error (invalid witness file) 6.7 3.5 93 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i aborted 0 wit inspect .13  .24  2.2  45   0      36      error (invalid witness file) .54 .34 13   43 error (invalid witness file) 6.0 3.2 110 300 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i aborted 0 wit inspect .11  .11  1.2  8.1 0      0      - - error (invalid witness file) .48 .31 9.6 39 error (invalid witness file) 6.7 3.5 120 300
list-ext2-properties/simple_search_value_false-unreach-call.i aborted 0 wit inspect .11  .11  1.2  8.2 0      0      error (invalid witness file) .53 .33 12   40 error (invalid witness file) 6.3 3.4 85 300 - -
list-ext2-properties/simple_search_value_true-unreach-call.i aborted 0 wit inspect .12  .12  1.1  8.1 0      .070  - - error (invalid witness file) .63 .39 7.5 39 error (invalid witness file) 5.7 3.1 120 290
../../sv-benchmarks/c/ verifier status score witness inspect witness cpu (s) wall (s) energy (J) mem (MB) blkio-w (MB) blkio-r (MB) validator cpachecker violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer violation t<90s status cpu (s) wall (s) energy (J) mem (MB) validator cpachecker correctness t<900s status cpu (s) wall (s) energy (J) mem (MB) validator uautomizer correctness t<900s status cpu (s) wall (s) energy (J) mem (MB)
total 173 69 17    18    160   1600 .20  170 173 63 38 1400 4800   173 460 240 6400 20000   173 170 100 2500 11000   173 790 420 14000 34000  
    correct results 40 69 2.8  3.0  19   370 .17  62 9 35 20 710 2600   9 84 45 1300 3500   28 130 71 1700 7500   28 290 160 5200 11000  
        correct true 29 58 2.0  2.2  13   270 .13  49 0 0 0 0 0   7 0 0 0 0   28 130 71 1700 7500   28 290 160 5200 11000  
        correct false 11 11 .77 .82 5.9 95 .041 12 9 35 20 710 2600   2 84 45 1300 3500   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (173 tasks, max score: 280) 69
Run set sv-comp17.ReachSafety-Heap