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