Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-12 12:02:41 CET [[ 2017-01-14 22:52:01 CET ]] [[ 2017-01-15 00:27:39 CET ]] [[ 2017-01-14 23:20:04 CET ]] [[ 2017-01-15 00:48:54 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-12_1202.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-12_1202.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 false(unreach-call) 1 wit inspect .18  .18  1.5  26 .84 0   timeout 92    82    1800   700 true 8.8 4.7 180 330 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .42  .42  5.9  52 .84 0   true 5.4  2.9  73   290 true 8.9 4.8 170 330 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .16  .16  1.8  27 .84 0   true 11    5.6  160   440 true 9.9 5.2 170 370 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13  .13  .87 25 .84 0   false(unreach-call) 5.7  3.1  72   300 true 8.3 4.5 150 320 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .15  .15  1.3  25 .84 0   false(unreach-call) 9.2  5.7  140   310 true 9.0 4.8 180 340 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.4  25 .84 0   true 5.8  3.2  78   280 true 7.9 4.2 99 320 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 5.0   5.0   52    150 .84 0   - - error (invalid witness file) .48 .31 6.9 39 error (invalid witness file) 5.6 3.0 110 290
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .15  .15  1.9  25 .84 0   - - error (invalid witness file) .58 .37 9.5 39 error (invalid witness file) 6.3 3.3 130 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .59  .59  7.6  63 .84 0   - - error (invalid witness file) .59 .37 10   40 error (invalid witness file) 6.5 3.4 120 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .21  .21  2.2  29 .84 0   - - error (invalid witness file) .55 .35 9.7 39 error (invalid witness file) 7.0 3.7 130 310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .31  .31  3.8  35 .84 0   - - error (invalid witness file) .47 .30 6.7 40 error (invalid witness file) 6.5 3.4 110 300
heap-manipulation/tree_true-unreach-call.i unknown 0 wit inspect .13  .13  1.7  26 .84 0   - - error (invalid witness file) .48 .31 9.1 40 error (invalid witness file) 6.2 3.2 120 300
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .10  .10  1.1  24 .84 0   false(unreach-call) 5.8  3.2  100   290 true 7.9 4.3 160 320 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.3  25 .84 0   false(unreach-call) 5.1  2.8  72   280 true 7.6 4.1 140 330 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .14  .14  1.1  24 .84 0   false(unreach-call) 5.2  2.8  78   290 false(unreach-call) 8.1 4.4 140 350 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .14  .14  1.5  25 .84 0   true 4.9  2.7  70   280 true 8.2 4.3 150 320 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .10  .10  1.2  24 .84 0   true 4.6  2.5  54   280 true 13   7.1 210 400 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.1  25 .84 0   false(unreach-call) 5.5  2.9  78   300 false(unreach-call) 9.2 4.9 150 350 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .14  .13  1.2  24 .84 0   - - error (invalid witness file) .49 .32 9.2 39 error (invalid witness file) 6.0 3.2 120 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .12  .12  1.4  24 .84 0   - - error (invalid witness file) .47 .31 8.5 40 error (invalid witness file) 6.0 3.2 120 300
list-properties/list_search_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .25  .25  2.6  29 .84 0   - - true 25    14    350   700 true 39   26   390 810
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .16  .16  1.9  27 .84 0   - - error (invalid witness file) .47 .31 7.4 40 error (invalid witness file) 6.2 3.3 120 310
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .092 .090 .98 24 .84 0   - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 5.7 3.1 130 290
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .11  .11  1.2  24 .84 0   - - error (invalid witness file) .57 .36 7.5 41 error (invalid witness file) 6.0 3.2 110 310
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .12  .11  1.3  25 .84 0   - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 5.4 2.9 100 290
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect .11  .11  .64 23 .84 0   false(unreach-call) 3.9  2.2  46   270 false(unreach-call) 7.7 4.1 160 320 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .12  .12  1.0  25 .84 0   false(unreach-call) 5.4  2.9  89   300 true 8.2 4.3 150 350 - -
ldv-regression/callfpointer.c_false-unreach-call.i unknown 0 wit inspect .071 .072 .71 23 .84 0   error (invalid witness file) .47 .31 4.1 39 error (invalid witness file) 5.7 3.1 110 290 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .084 .083 .89 25 .84 0   false(unreach-call) 5.2  2.8  110   290 true 7.2 3.9 140 310 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .11  .11  .74 23 .84 0   false(unreach-call) 3.6  2.0  57   270 true 6.5 3.5 120 310 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect .073 .073 .85 23 .99 0   false(unreach-call) 4.0  2.2  57   280 false(unreach-call) 7.7 4.1 140 330 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect .078 .077 .79 23 .84 0   false(unreach-call) 3.8  2.1  47   270 true 7.3 3.9 140 310 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect .081 .082 .93 24 .84 0   false(unreach-call) 5.3  2.9  49   290 false(unreach-call) 10   5.5 120 360 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .12  .12  1.5  24 .84 0   false(unreach-call) 5.4  3.0  100   290 true 7.2 3.9 87 330 - -
ldv-regression/stateful_check_false-unreach-call.i unknown 0 wit inspect .10  .10  .98 23 .84 0   error (invalid witness file) .50 .32 9.4 39 error (invalid witness file) 6.3 3.3 120 300 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .11  .11  .63 23 .84 0   false(unreach-call) 4.6  2.6  43   280 true 6.4 3.4 91 300 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .087 .088 .73 23 .84 0   false(unreach-call) 3.5  2.0  47   280 true 7.1 3.8 150 310 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect .071 .071 .83 23 .84 0   - - true 3.4  1.9  59   260 true 8.2 4.4 160 320
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect .071 .071 .79 23 .84 0   - - true 3.4  1.9  43   260 true 7.7 4.1 150 320
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect .099 .098 .87 23 .84 0   - - true 3.3  1.9  39   260 true 7.7 4.2 120 320
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect .093 .092 .76 23 .84 0   - - true 4.5  2.5  41   260 true 7.1 3.8 120 300
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect .11  .11  1.4  23 .84 0   - - true 18    10    310   540 true 30   17   340 740
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect .074 .074 .83 23 .99 0   - - true 3.1  1.7  40   260 true 7.0 3.7 140 310
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect .11  .11  .57 23 .84 0   - - true 3.6  2.0  61   260 true 7.9 4.3 170 310
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect .11  .11  .71 23 .84 0   - - true 3.8  2.1  79   260 true 8.5 4.5 170 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect .078 .078 .76 23 .84 0   - - true 3.5  2.0  63   260 true 9.4 5.1 150 330
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect .076 .075 .82 23 .99 0   - - true 3.9  2.2  58   260 true 6.8 3.7 110 310
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect .082 .083 .73 23 .88 0   - - true 3.8  2.1  66   270 true 7.9 4.2 160 320
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect .10  .10  .64 23 .84 0   - - true 3.4  1.9  63   260 true 12   6.7 170 430
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect .096 .095 .77 23 .84 0   - - true 3.5  2.0  57   260 true 12   6.8 200 450
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect .097 .096 .75 23 .84 0   - - true 3.8  2.2  37   260 true 9.4 5.2 160 340
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect .085 .084 .90 23 .84 0   - - true 3.3  1.8  26   260 true 7.5 4.0 140 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect .070 .071 .87 23 .84 0   - - true 3.3  1.9  44   260 true 7.1 3.9 120 320
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect .081 .081 1.0  23 .99 0   - - true 5.1  2.8  62   280 true 9.7 5.2 180 350
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect .12  .12  .87 24 .84 0   - - true 4.8  2.6  90   270 true 11   6.2 190 370
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect .13  .13  1.4  24 .99 0   - - true 4.9  2.7  75   270 true 28   16   410 680
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect .087 .087 .93 24 .84 0   - - true 4.4  2.4  87   260 true 7.1 3.8 110 330
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect .11  .11  .66 23 .84 0   - - true 3.6  2.1  65   250 true 7.2 3.8 130 320
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect .098 .099 .87 24 .84 0   - - true 4.3  2.4  68   260 true 7.7 4.1 150 320
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect .075 .075 .83 23 .84 0   - - true 3.2  1.8  40   260 true 7.5 4.1 150 320
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect .089 .088 .96 24 .84 0   - - true 4.5  2.4  57   260 true 8.4 4.5 160 330
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect .084 .083 1.0  24 .84 0   - - true 4.6  2.5  81   270 true 8.1 4.4 170 320
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect .089 .089 .93 25 .84 0   - - true 4.9  2.6  73   260 true 7.7 4.1 150 330
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect .078 .077 .76 23 .84 0   - - true 3.4  1.9  64   260 true 7.6 4.1 120 320
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect .11  .11  .70 23 .88 0   - - true 3.4  1.9  49   250 true 7.5 4.0 140 320
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect .28  .28  1.0  23 .84 0   - - true 3.3  1.9  38   260 unknown 6.1 3.3 120 310
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect .11  .11  .86 23 .84 0   - - true 3.4  1.9  58   260 unknown 6.4 3.4 130 310
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect .072 .073 .96 23 .84 0   - - true 3.5  2.0  74   260 unknown 8.0 4.2 140 320
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect .088 .088 .72 23 .84 0   - - true 3.7  2.1  46   260 unknown 6.2 3.3 120 300
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect .073 .073 .81 23 .84 0   - - true 3.7  2.1  44   260 true 8.6 4.6 130 330
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect .098 .10  .78 23 .84 0   - - true 3.4  1.9  56   250 true 7.9 4.3 150 320
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .10  .68 23 .84 0   false(unreach-call) 3.6  2.0  62   280 true 7.1 3.7 130 320 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .76 23 .84 0   false(unreach-call) 4.0  2.2  72   290 true 7.5 4.0 130 310 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect .074 .073 .77 23 .84 0   false(unreach-call) 3.9  2.2  67   290 true 7.3 3.9 130 310 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect .28  .28  .64 23 .84 0   false(unreach-call) 3.6  2.0  60   280 true 6.5 3.5 100 310 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .69 23 .84 0   false(unreach-call) 4.0  2.2  51   290 false(unreach-call) 7.7 4.1 130 320 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .084 .084 .85 23 .84 0   false(unreach-call) 4.1  2.3  53   280 false(unreach-call) 12   6.8 190 410 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 7.0   7.0   82    190 .84 0   true 12    7.6  170   340 false(unreach-call) 55   37   660 870 - -
ldv-regression/test24_false-unreach-call.c true -32 wit inspect .086 .085 1.0  23 .84 0   unknown 48    38    710   1200 false(unreach-call) 26   14   380 650 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect .80  .78  10    43 .84 0   true 3.9  2.2  64   280 false(unreach-call) 17   9.7 200 570 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect .080 .080 .78 23 .84 0   false(unreach-call) 3.6  2.0  61   280 true 7.4 3.9 130 320 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect .086 .086 .95 23 .84 0   false(unreach-call) 4.1  2.3  48   280 true 8.7 4.6 160 340 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect .11  .11  .74 23 .84 0   false(unreach-call) 3.8  2.1  60   280 false(unreach-call) 9.6 5.1 150 360 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect .10  .099 .84 23 .99 0   true 3.6  2.0  69   270 false(unreach-call) 8.4 4.6 140 350 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect .077 .077 .80 23 .84 0   false(unreach-call) 3.5  1.9  46   270 true 7.5 4.0 150 320 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect .075 .075 .82 23 .84 0   - - true 3.6  2.0  60   260 true 7.6 4.1 150 320
ldv-regression/test03_true-unreach-call.c true 2 wit inspect .10  .10  .84 23 .84 0   - - true 3.5  1.9  45   260 true 7.9 4.3 160 310
ldv-regression/test04_true-unreach-call.c true 2 wit inspect .088 .088 .80 23 .84 0   - - true 3.5  2.0  38   260 true 8.5 4.6 150 320
ldv-regression/test05_true-unreach-call.c true 2 wit inspect .11  .11  .75 23 .84 0   - - true 3.6  2.0  69   260 true 12   7.3 160 470
ldv-regression/test07_true-unreach-call.c true 2 wit inspect .074 .074 .80 23 .84 0   - - true 3.6  2.0  57   260 true 11   5.9 160 420
ldv-regression/test09_true-unreach-call.c true 2 wit inspect .10  .10  .75 23 .84 0   - - true 3.7  2.1  74   260 true 9.8 5.4 130 420
ldv-regression/test10_true-unreach-call.c true 2 wit inspect .072 .073 .78 23 .84 0   - - true 3.5  2.0  63   260 true 17   9.8 300 480
ldv-regression/test11_true-unreach-call.c true 2 wit inspect .075 .074 .93 23 .84 0   - - true 3.8  2.1  75   260 true 9.7 5.2 190 330
ldv-regression/test13_true-unreach-call.c true 2 wit inspect .11  .11  .59 23 .84 0   - - true 3.6  2.0  61   260 true 7.5 4.0 140 320
ldv-regression/test14_true-unreach-call.c true 2 wit inspect .10  .10  .82 23 .84 0   - - true 3.8  2.1  60   270 true 8.7 4.7 160 320
ldv-regression/test15_true-unreach-call.c true 2 wit inspect .11  .11  .70 23 .84 0   - - true 3.3  1.9  44   260 true 10   5.5 200 340
ldv-regression/test16_true-unreach-call.c true 2 wit inspect .071 .071 .74 23 .84 0   - - true 3.6  2.0  75   260 true 9.8 5.3 130 360
ldv-regression/test17_true-unreach-call.c true 2 wit inspect .078 .077 .76 23 .84 0   - - true 3.7  2.0  73   260 true 7.7 4.1 140 310
ldv-regression/test18_true-unreach-call.c true 2 wit inspect .072 .072 .84 23 .84 0   - - true 3.6  2.0  53   260 true 9.5 5.1 150 330
ldv-regression/test19_true-unreach-call.c true 2 wit inspect .11  .11  .72 23 .84 0   - - true 3.6  2.0  63   260 true 11   6.1 210 460
ldv-regression/test20_true-unreach-call.c true 2 wit inspect .092 .091 .88 23 .84 0   - - true 3.3  1.8  52   260 true 7.4 4.0 150 310
ldv-regression/test21_true-unreach-call.c true 2 wit inspect .11  .11  .72 23 .84 0   - - true 4.3  2.4  63   260 true 9.7 5.3 180 340
ldv-regression/test22_true-unreach-call.c true 2 wit inspect .19  .19  2.0  23 .84 0   - - true 6.2  3.7  110   300 true 37   24   390 830
ldv-regression/test23_true-unreach-call.c true 2 wit inspect .85  .85  10    42 .84 0   - - true 12    8.7  150   400 true 180   150   2000 1000
ldv-regression/test24_true-unreach-call.c true 2 wit inspect .14  .14  1.4  23 .84 0   - - true 5.7  3.4  110   300 true 14   7.6 220 370
ldv-regression/test25_true-unreach-call.c true 2 wit inspect .15  .14  1.1  23 .99 0   - - true 25    19    390   510 true 26   14   310 700
ldv-regression/test26_true-unreach-call.c true 2 wit inspect .094 .096 .70 23 .84 0   - - true 4.0  2.2  62   260 true 9.7 5.3 190 340
ldv-regression/test27_true-unreach-call.c true 2 wit inspect .12  .12  1.6  23 .84 0   - - true 8.0  5.5  140   310 true 85   66   940 940
ldv-regression/test28_true-unreach-call.c true 2 wit inspect .098 .098 .86 23 .84 0   - - true 3.4  1.9  60   260 true 8.7 4.7 170 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect .080 .080 .86 23 .84 0   - - true 3.5  1.9  59   250 true 9.0 4.8 160 320
ldv-regression/test30_true-unreach-call.c true 2 wit inspect .11  .11  .70 23 .99 0   - - true 3.5  2.0  63   260 true 12   6.4 200 480
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .34  .34  4.5  68 .84 0   error (invalid witness file) .63 .42 5.0 43 error (invalid witness file) 6.2 3.3 89 300 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .34  .34  3.8  67 .84 0   error (invalid witness file) .53 .33 11   40 error (invalid witness file) 6.3 3.3 120 300 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .32  .32  3.8  68 .84 0   error (invalid witness file) .54 .35 8.9 42 error (invalid witness file) 6.5 3.4 130 290 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .29  .29  4.1  66 .84 0   - - error (invalid witness file) .50 .32 9.9 40 error (invalid witness file) 5.9 3.2 87 290
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .30  .30  3.3  66 .84 0   - - error (invalid witness file) .50 .33 7.1 41 error (invalid witness file) 6.3 3.4 100 300
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .31  .31  3.5  66 .84 0   - - error (invalid witness file) .50 .33 8.5 40 error (invalid witness file) 6.9 3.6 130 310
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .31  .31  3.3  66 .99 0   - - error (invalid witness file) .55 .35 13   40 error (invalid witness file) 6.3 3.3 120 290
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .33  .33  3.4  66 .84 0   - - error (invalid witness file) .50 .32 6.9 43 error (invalid witness file) 6.3 3.3 130 300
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .29  .29  3.9  66 .84 0   - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.5 3.4 140 300
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .29  .29  3.9  66 .84 0   - - error (invalid witness file) .47 .31 5.7 39 error (invalid witness file) 6.2 3.3 130 300
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .32  .32  3.3  66 .84 0   - - error (invalid witness file) .48 .31 8.1 40 error (invalid witness file) 6.5 3.4 110 310
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .31  .31  3.8  66 .84 0   - - error (invalid witness file) .49 .33 9.7 40 error (invalid witness file) 6.0 3.2 130 300
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .30  .30  4.2  66 .84 0   - - error (invalid witness file) .54 .36 9.7 39 error (invalid witness file) 6.5 3.5 120 310
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.1  25 .84 0   timeout 92    82    1100   600 true 14   8.0 200 520 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .081 .081 1.2  25 .84 0   false(unreach-call) 5.3  2.9  110   280 true 9.6 5.2 160 360 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .14  .14  .97 25 .84 0   false(unreach-call) 5.1  2.8  64   280 true 7.3 4.0 140 330 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect .12  .11  1.4  25 .84 0   error (invalid witness file) .47 .31 8.9 39 error (invalid witness file) 6.8 3.6 100 300 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .11  .10  .94 25 .84 0   false(unreach-call) 4.9  2.7  81   280 true 8.5 4.6 120 360 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect .25  .24  2.4  38 .97 0   false(unreach-call) 7.2  4.0  64   310 error 11   5.8 150 320 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  1.0  25 .84 0   false(unreach-call) 5.3  2.9  90   290 false(unreach-call) 8.8 4.7 140 350 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .11  .11  1.4  25 .84 0   timeout 91    86    1000   470 true 8.7 4.8 150 330 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .11  .11  .92 25 .84 0   false(unreach-call) 5.1  2.7  82   280 true 14   7.6 190 440 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .16  .16  2.1  28 .84 0   timeout 91    81    990   480 true 10   5.4 110 360 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13  .12  1.5  25 .84 0   false(unreach-call) 6.5  3.6  120   300 true 7.9 4.2 120 320 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .087 .087 .89 24 .84 0   false(unreach-call) 5.3  2.9  54   280 true 9.8 5.3 140 350 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13  .12  .86 25 .84 0   false(unreach-call) 5.1  2.8  89   280 true 8.1 4.3 130 320 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect .14  .14  1.2  25 .84 0   error (invalid witness file) .57 .37 14   46 error (invalid witness file) 5.9 3.2 120 300 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .083 .083 .95 24 .84 0   false(unreach-call) 5.0  2.7  89   280 true 8.8 4.7 140 350 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .11  .11  1.7  25 .84 0   false(unreach-call) 5.5  3.0  68   300 error 11   5.7 170 300 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .12  .12  .91 24 .84 0   false(unreach-call) 5.0  2.8  65   290 false(unreach-call) 8.7 4.6 140 340 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .13  .13  1.4  25 .84 0   true 5.7  3.1  96   290 true 9.6 5.1 190 360 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .087 .087 .83 24 .84 0   false(unreach-call) 5.0  2.7  76   290 false(unreach-call) 9.2 4.9 150 350 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .21  .21  3.1  33 .84 0   - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 6.1 3.2 130 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .18  .18  1.6  27 .99 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 7.3 3.8 110 340
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .20  .20  2.4  31 .84 0   - - error (invalid witness file) .50 .34 10   40 error (invalid witness file) 6.4 3.3 120 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .11  .11  1.5  25 .84 0   - - error (invalid witness file) .55 .35 10   44 error (invalid witness file) 5.7 3.0 110 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .38  .38  3.8  40 .84 0   - - error (invalid witness file) .53 .35 11   42 error (invalid witness file) 6.0 3.2 100 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .39  .39  4.0  45 .84 0   - - error (invalid witness file) .48 .31 9.6 39 error (invalid witness file) 5.7 3.1 97 290
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .22  .22  2.0  31 .84 0   - - error (invalid witness file) .47 .31 8.5 40 error (invalid witness file) 6.0 3.1 110 290
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .25  .25  3.5  32 .84 0   - - error (invalid witness file) .51 .33 11   41 error (invalid witness file) 5.8 3.1 120 290
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .13  .13  1.5  25 .84 0   - - error (invalid witness file) .47 .30 5.5 39 error (invalid witness file) 6.3 3.3 120 310
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .18  .17  1.7  29 .84 0   - - error (invalid witness file) .57 .36 7.4 40 error (invalid witness file) 6.0 3.2 120 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .18  .18  2.2  29 .84 0   - - error (invalid witness file) .66 .41 7.2 40 error (invalid witness file) 5.6 3.0 97 290
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .15  .15  1.9  27 .84 0   - - error (invalid witness file) .57 .36 10   43 error (invalid witness file) 6.1 3.3 110 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .15  .14  1.3  25 .84 0   - - error (invalid witness file) .52 .35 12   40 error (invalid witness file) 6.2 3.3 120 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .18  .18  1.8  29 .84 0   - - error (invalid witness file) .64 .42 7.9 40 error (invalid witness file) 6.3 3.4 85 290
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .14  .14  1.2  25 .84 0   - - error (invalid witness file) .54 .37 12   40 error (invalid witness file) 6.0 3.2 110 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .12  .12  1.4  25 .84 0   - - error (invalid witness file) .62 .39 5.3 39 error (invalid witness file) 6.1 3.3 120 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .12  .12  1.5  25 .84 0   - - error (invalid witness file) .50 .33 4.3 41 error (invalid witness file) 5.4 2.9 110 280
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .18  .17  1.6  26 .84 0   - - error (invalid witness file) .60 .37 7.6 40 error (invalid witness file) 6.1 3.2 120 310
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .17  .17  2.0  27 .84 0   - - error (invalid witness file) .49 .32 9.8 40 error (invalid witness file) 6.4 3.4 130 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .12  .12  1.5  25 .84 0   - - error (invalid witness file) .47 .30 6.0 39 error (invalid witness file) 6.5 3.4 130 310
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .13  .13  1.7  25 .99 0   - - error (invalid witness file) .51 .33 3.7 39 error (invalid witness file) 6.1 3.2 110 290
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .11  .11  .91 24 .84 0   false(unreach-call) 5.1  2.8  87   300 true 8.1 4.3 120 330 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 20     20     67    200 .97 0   timeout 98    81    2100   2800 timeout 97   77   1200 1800 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .11  .11  1.0  24 .84 0   false(unreach-call) 5.1  2.8  87   290 false(unreach-call) 8.1 4.3 110 350 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i false(unreach-call) 1 wit inspect .20  .20  2.2  30 .84 0   false(unreach-call) 6.1  3.3  97   290 true 9.2 4.9 180 340 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i unknown 0 wit inspect .28  .28  3.1  35 .84 0   - - error (invalid witness file) .48 .30 8.2 39 error (invalid witness file) 5.9 3.1 120 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect .14  .14  1.5  25 .84 0   true 6.0  3.2  97   290 true 15   8.1 240 420 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i unknown 0 wit inspect .20  .20  1.9  28 .84 0   - - error (invalid witness file) .64 .40 9.5 44 error (invalid witness file) 5.7 3.0 100 310
list-ext2-properties/simple_search_value_false-unreach-call.i false(unreach-call) 1 wit inspect 2.9   2.9   8.2  79 .84 0   false(unreach-call) 10    6.4  120   430 timeout 97   88   980 1000 - -
list-ext2-properties/simple_search_value_true-unreach-call.i out of memory 0 wit inspect 830     830     8500    15000 .84 0   - - error (invalid witness file) .56 .36 9.8 40 error (invalid witness file) 6.0 3.2 110 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 148 890     890     9000   20000 150    0   173 800 610 12000 22000   173 810 510 12000 25000   173 320 190 5100 19000   173 1200 720 19000 38000  
    correct results 119 180 44     44     300   3300 100    0   53 740 570 11000 21000   54 740 470 11000 23000   61 300 180 4700 17000   57 900 570 13000 24000  
        correct true 61 122 6.9   6.9   64   1400 52    0   10 0 0 0 0   39 0 0 0 0   61 300 180 4700 17000   57 900 570 13000 24000  
        correct false 58 58 37     37     230   1900 49    0   43 740 570 11000 21000   15 740 470 11000 23000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 1 -32 .086 .085 1.0 23 .84 0   0 48 38 710 1200   1 26 14 380 650   0 0 0 0 0   0 0 0 0 0  
        incorrect true 1 -32 .086 .085 1.0 23 .84 0   0 48 38 710 1200   0 26 14 380 650   0 0 0 0 0   0 0 0 0 0  
        incorrect false 0
score (173 tasks, max score: 280) 148
Run set sv-comp17.ReachSafety-Heap