Tool ULTIMATE Kojak f7c3ed31
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-13 13:05:01 CET [[ 2017-01-15 02:11:27 CET ]] [[ 2017-01-15 04:07:55 CET ]] [[ 2017-01-15 02:33:46 CET ]] [[ 2017-01-15 04:34:07 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-13_1305.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-13_1305.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 timeout 0 wit inspect 900   880   11000 1000 2.3 0      error (invalid witness file) .48 .32 8.3 40 error (invalid witness file) 6.1 3.3 89 310 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   520   11000 1600 2.3 0      error (invalid witness file) .60 .39 8.4 41 error (invalid witness file) 6.2 3.3 130 300 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 12   3.7 100 500 2.5 0      exception 4.1  2.2  40   210 false(unreach-call) 11   5.9 180 370 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   860   10000 1200 2.3 0      error (invalid witness file) .54 .35 11   41 error (invalid witness file) 6.1 3.2 120 300 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 22   11   210 610 2.5 0      exception 3.2  1.8  52   200 false(unreach-call) 11   5.9 150 370 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 22   12   210 690 2.5 0      exception 3.6  2.0  31   170 false(unreach-call) 12   6.1 200 380 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   880   13000 810 2.3 0      - - error (invalid witness file) .67 .43 7.1 39 error (invalid witness file) 6.3 3.3 110 300
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   620   11000 1500 2.3 0      - - error (invalid witness file) .62 .38 11   40 error (invalid witness file) 5.9 3.2 81 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   520   11000 1700 2.3 0      - - error (invalid witness file) .64 .40 7.7 39 error (invalid witness file) 6.2 3.3 90 310
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   410   6100 13000 2.3 0      - - error (invalid witness file) .56 .35 11   42 error (invalid witness file) 6.8 3.6 120 310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   810   11000 1900 2.3 0      - - error (invalid witness file) .64 .41 7.6 40 error (invalid witness file) 6.7 3.5 130 310
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 900   880   11000 890 2.3 0      - - error (invalid witness file) .52 .34 9.7 39 error (invalid witness file) 6.4 3.3 130 310
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.4 2.4 58 330 2.5 0      true 4.6  2.5  59   280 false(unreach-call) 8.1 4.4 170 320 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 18   8.1 180 520 2.5 0      true 5.1  2.8  75   280 false(unreach-call) 8.7 4.6 160 340 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.3 2.3 58 340 2.5 0      true 5.0  2.7  79   280 false(unreach-call) 7.8 4.2 150 330 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   730   9700 2000 2.3 0      error (invalid witness file) .55 .34 11   39 error (invalid witness file) 5.3 2.9 86 290 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.9 2.2 60 330 2.5 0      true 4.9  2.6  64   280 false(unreach-call) 8.5 4.5 150 330 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.8 2.3 65 370 2.5 0      true 4.8  2.6  50   290 false(unreach-call) 9.5 5.0 150 330 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   11000 2300 2.3 0      - - error (invalid witness file) .66 .42 7.9 39 error (invalid witness file) 6.7 3.5 100 310
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   830   10000 1500 2.3 0      - - error (invalid witness file) .61 .39 10   40 error (invalid witness file) 5.9 3.1 98 300
list-properties/list_search_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   690   12000 1500 2.3 0      - - error (invalid witness file) .73 .46 9.2 44 error (invalid witness file) 6.4 3.4 98 290
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   840   14000 1500 2.3 0      - - error (invalid witness file) .66 .42 9.2 40 error (invalid witness file) 5.5 2.9 56 300
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   830   12000 1700 2.3 0      - - error (invalid witness file) .50 .32 9.1 40 error (invalid witness file) 6.6 3.4 140 310
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   830   13000 1500 2.3 0      - - error (invalid witness file) .51 .33 9.2 42 error (invalid witness file) 5.2 2.8 50 300
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   830   11000 1300 2.3 0      - - error (invalid witness file) .61 .39 7.8 39 error (invalid witness file) 6.2 3.3 110 300
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.5 2.0 56 330 2.5 0      true 3.6  2.0  36   270 false(unreach-call) 7.4 3.9 110 320 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.4 2.0 48 340 2.5 0      true 4.9  2.6  83   280 false(unreach-call) 11   6.0 91 350 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect 5.8 1.8 47 340 2.5 0      true 3.9  2.2  46   270 false(unreach-call) 7.0 3.8 140 320 - -
ldv-regression/fo_test.c_false-unreach-call.i unknown 0 wit inspect 11   3.5 91 320 2.6 0      error (invalid witness file) .52 .34 12   39 error (invalid witness file) 6.0 3.2 120 290 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.0 1.9 47 330 2.5 0      true 3.5  2.0  57   270 false(unreach-call) 7.8 4.1 160 320 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.2 1.9 50 340 2.5 0      false(unreach-call) 3.5  2.0  27   270 false(unreach-call) 7.4 3.9 160 320 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.5 2.0 47 320 2.5 0      assertion 2.4  1.3  36   160 false(unreach-call) 7.7 4.1 130 320 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.5 2.1 47 330 2.5 0      true 3.9  2.2  53   270 false(unreach-call) 8.6 4.7 190 350 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i timeout 0 wit inspect 900   580   12000 1500 2.3 0      error (invalid witness file) .50 .34 5.7 39 error (invalid witness file) 5.6 3.0 130 280 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect 10   2.9 70 490 2.5 0      false(unreach-call) 4.6  2.6  64   280 false(unreach-call) 9.3 5.0 140 330 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 6.1 2.0 51 330 2.5 0      false(unreach-call) 3.9  2.2  59   270 false(unreach-call) 7.6 4.1 140 330 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 5.8 1.9 44 320 2.5 0      false(unreach-call) 3.8  2.2  87   280 false(unreach-call) 7.2 3.8 150 300 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect 5.8 1.9 46 320 2.5 0      - - true 3.5  2.0  69   260 true 9.1 5.0 110 310
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect 6.1 1.9 46 330 2.5 0      - - true 3.8  2.2  61   260 true 9.0 4.8 100 310
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect 5.9 2.0 42 320 2.5 .0041 - - true 4.3  2.4  56   260 true 8.3 4.5 160 330
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect 7.1 2.0 57 350 2.5 0      - - true 3.5  1.9  70   260 true 7.2 3.9 160 310
ldv-regression/ex3_forlist.c_true-unreach-call.i timeout 0 wit inspect 900   550   9900 1100 2.3 0      - - error (invalid witness file) .63 .40 7.4 40 error (invalid witness file) 6.1 3.3 120 300
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect 5.2 1.7 42 320 2.5 0      - - true 3.1  1.8  64   250 true 8.1 4.3 150 330
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect 6.3 1.9 49 340 2.5 0      - - true 3.9  2.2  61   260 true 8.4 4.6 170 320
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect 6.1 2.0 48 320 2.5 0      - - true 4.5  2.5  51   260 true 8.4 4.5 160 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect 7.0 2.1 57 330 2.5 0      - - true 3.4  1.9  58   260 true 9.6 5.2 170 330
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect 5.9 1.8 44 330 2.5 0      - - true 3.9  2.2  57   260 true 8.4 4.5 100 300
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect 5.9 1.8 44 320 2.5 0      - - true 3.6  2.1  54   260 true 7.0 3.8 110 310
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect 8.9 2.7 69 450 2.5 0      - - true 4.3  2.4  49   260 true 12   6.8 220 450
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect 6.7 2.1 50 330 2.5 0      - - true 3.4  1.9  63   260 true 13   7.0 270 450
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect 6.8 2.0 54 350 2.5 0      - - true 4.1  2.3  67   260 true 10   5.5 150 340
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect 5.6 1.8 45 320 2.5 0      - - true 3.4  1.9  64   250 true 8.5 4.6 130 330
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect 5.4 1.8 46 320 2.5 0      - - true 3.7  2.1  64   260 true 9.1 4.8 170 330
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i timeout 0 wit inspect 900   570   11000 2100 2.3 0      - - error (invalid witness file) .54 .35 12   39 error (invalid witness file) 6.1 3.2 120 290
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect 7.6 2.4 60 370 2.5 0      - - true 4.7  2.6  99   280 true 11   6.1 180 370
ldv-regression/rule60_list2.c_true-unreach-call.i timeout 0 wit inspect 900   580   13000 1600 2.3 0      - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.0 3.2 110 300
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect 6.1 1.9 44 340 2.5 0      - - true 4.2  2.3  82   260 true 6.9 3.7 98 320
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect 5.7 1.8 44 340 2.5 0      - - true 4.1  2.3  53   260 true 7.4 3.9 150 310
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect 5.9 1.9 45 330 2.5 0      - - true 5.1  2.8  92   270 true 7.8 4.2 93 330
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect 5.9 1.8 44 320 2.5 0      - - true 3.7  2.0  55   260 true 7.8 4.2 150 330
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect 6.7 2.0 53 360 2.5 0      - - true 4.7  2.6  86   270 true 8.1 4.4 180 320
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect 5.7 1.9 46 320 2.5 0      - - true 4.7  2.6  77   270 true 10   5.5 130 320
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect 5.8 1.8 45 320 2.5 0      - - true 6.2  3.4  66   270 true 8.3 4.4 150 320
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect 5.6 1.8 50 320 2.5 0      - - true 3.9  2.2  46   260 true 6.9 3.8 110 310
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect 6.2 1.9 49 350 2.5 0      - - true 3.3  1.9  70   250 true 7.2 3.9 140 320
ldv-regression/test_union_cast-1_true-unreach-call.i unknown 0 wit inspect 5.2 1.5 39 320 2.5 0      - - error (invalid witness file) .54 .34 5.9 39 error (invalid witness file) 6.8 3.6 95 310
ldv-regression/test_union_cast-2_true-unreach-call.i unknown 0 wit inspect 5.2 1.5 39 300 2.5 0      - - error (invalid witness file) .69 .43 11   44 error (invalid witness file) 6.3 3.3 110 300
ldv-regression/test_union_cast.c_true-unreach-call.i unknown 0 wit inspect 4.8 1.5 38 310 2.5 0      - - error (invalid witness file) .48 .31 6.8 41 error (invalid witness file) 5.4 2.9 99 300
ldv-regression/test_union_cast.c_true-unreach-call_1.i unknown 0 wit inspect 4.8 1.5 36 300 2.5 0      - - error (invalid witness file) .65 .40 11   44 error (invalid witness file) 7.0 3.7 140 320
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect 6.1 1.8 42 320 2.5 0      - - true 3.4  1.9  69   270 true 7.7 4.2 150 310
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect 6.2 1.8 47 330 2.5 0      - - true 4.4  2.5  46   260 true 8.2 4.4 160 330
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect 5.6 1.9 49 320 2.5 0      true 3.4  1.9  72   270 false(unreach-call) 7.5 4.0 150 320 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect 7.9 2.4 65 350 2.5 0      false(unreach-call) 4.2  2.3  56   280 false(unreach-call) 8.0 4.3 180 320 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect 6.2 2.0 49 320 2.5 0      false(unreach-call) 3.8  2.1  58   270 false(unreach-call) 7.7 4.1 120 320 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect 6.0 1.8 47 340 2.5 0      true 3.3  1.9  41   270 false(unreach-call) 7.2 3.8 140 320 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect 6.7 1.9 47 330 2.5 0      assertion 2.5  1.4  28   160 false(unreach-call) 7.3 3.9 150 320 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 7.2 2.2 61 320 2.5 0      assertion 2.5  1.4  33   160 false(unreach-call) 13   7.0 210 400 - -
ldv-regression/test23_false-unreach-call.c error 0 wit inspect 81   54   780 11000 2.6 0      error (invalid witness file) .48 .32 3.3 39 error (invalid witness file) 5.7 3.0 82 300 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 24   14   220 500 2.6 0      false(unreach-call) 15    12    170   490 timeout 93   55   770 7000 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect 14   4.1 110 480 2.5 0      true 4.3  2.4  48   270 out of memory 75   46   860 7000 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect 6.1 1.9 47 320 2.5 0      false(unreach-call) 3.7  2.1  47   280 false(unreach-call) 8.3 4.4 150 320 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect 7.4 2.2 62 350 2.5 0      false(unreach-call) 4.6  2.5  53   280 false(unreach-call) 11   5.7 130 320 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect 6.3 2.0 55 330 2.5 0      assertion 2.5  1.4  35   160 false(unreach-call) 8.7 4.6 170 340 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect 6.6 1.9 48 320 2.5 0      assertion 2.6  1.5  29   160 false(unreach-call) 8.7 4.7 150 340 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect 7.1 2.2 55 340 2.5 0      false(unreach-call) 3.8  2.1  55   270 false(unreach-call) 7.8 4.1 110 320 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect 5.8 1.8 51 320 2.5 0      - - true 4.3  2.4  45   260 true 7.8 4.2 170 310
ldv-regression/test03_true-unreach-call.c true 2 wit inspect 6.2 1.9 47 340 2.5 0      - - true 4.3  2.4  50   260 true 8.2 4.5 120 320
ldv-regression/test04_true-unreach-call.c true 2 wit inspect 5.5 1.9 44 320 2.5 0      - - true 4.7  2.6  43   260 true 8.6 4.7 150 310
ldv-regression/test05_true-unreach-call.c true 2 wit inspect 18   11   210 480 2.5 0      - - true 4.1  2.3  43   260 true 13   7.7 200 510
ldv-regression/test07_true-unreach-call.c true 2 wit inspect 7.0 2.3 61 380 2.5 0      - - true 4.3  2.4  53   260 true 11   6.2 180 360
ldv-regression/test09_true-unreach-call.c true 2 wit inspect 7.0 2.3 56 370 2.5 0      - - true 4.6  2.5  47   260 true 11   5.9 150 360
ldv-regression/test10_true-unreach-call.c true 2 wit inspect 9.9 3.8 79 380 2.5 0      - - true 4.2  2.3  58   260 true 17   9.8 220 480
ldv-regression/test11_true-unreach-call.c true 2 wit inspect 6.6 2.1 51 320 2.5 0      - - true 3.7  2.1  73   260 true 9.5 5.1 150 350
ldv-regression/test13_true-unreach-call.c true 2 wit inspect 5.4 1.8 45 320 2.5 0      - - true 5.1  2.9  61   260 true 7.5 4.0 150 310
ldv-regression/test14_true-unreach-call.c true 2 wit inspect 6.7 2.0 57 340 2.5 0      - - true 3.8  2.1  64   260 true 8.8 4.7 110 320
ldv-regression/test15_true-unreach-call.c true 2 wit inspect 6.5 2.0 46 320 2.5 0      - - true 4.0  2.3  65   260 true 9.7 5.3 180 340
ldv-regression/test16_true-unreach-call.c true 2 wit inspect 7.1 2.3 57 340 2.5 0      - - true 3.4  1.9  68   260 true 9.9 5.4 140 360
ldv-regression/test17_true-unreach-call.c true 2 wit inspect 5.7 1.9 47 320 2.5 0      - - true 3.4  1.9  58   260 true 7.8 4.2 110 330
ldv-regression/test18_true-unreach-call.c true 2 wit inspect 6.7 2.1 56 320 2.5 0      - - true 3.6  2.0  57   260 true 9.7 5.2 200 320
ldv-regression/test19_true-unreach-call.c true 2 wit inspect 8.2 2.6 69 430 2.5 0      - - true 3.7  2.1  71   260 true 11   6.3 190 460
ldv-regression/test20_true-unreach-call.c true 2 wit inspect 6.2 1.9 50 330 2.5 0      - - true 3.3  1.9  63   260 true 8.1 4.4 170 330
ldv-regression/test21_true-unreach-call.c true 2 wit inspect 6.1 1.9 47 330 2.5 0      - - true 4.1  2.3  64   260 true 9.3 5.1 190 330
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 19   6.4 150 540 2.6 0      - - exception 4.3  2.4  46   260 true 37   25   580 820
ldv-regression/test23_true-unreach-call.c error 0 wit inspect 84   56   810 11000 2.6 0      - - error (invalid witness file) .56 .37 9.5 40 error (invalid witness file) 6.2 3.3 140 290
ldv-regression/test24_true-unreach-call.c true 2 wit inspect 16   6.3 130 520 2.5 0      - - exception 3.9  2.2  46   260 true 13   7.2 250 390
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 54   27   500 870 2.5 0      - - exception 4.5  2.5  57   270 true 28   15   380 710
ldv-regression/test26_true-unreach-call.c true 2 wit inspect 7.2 2.0 54 340 2.5 0      - - true 3.5  2.0  77   260 true 9.5 5.1 150 340
ldv-regression/test27_true-unreach-call.c true 2 wit inspect 830   800   8700 640 2.5 0      - - true 8.3  5.7  220   320 true 94   75   1000 810
ldv-regression/test28_true-unreach-call.c true 2 wit inspect 6.0 1.8 46 330 2.5 0      - - true 4.7  2.6  47   270 true 8.8 4.8 180 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect 6.2 1.9 47 320 2.5 0      - - true 3.5  2.0  64   260 true 8.9 4.8 170 340
ldv-regression/test30_true-unreach-call.c true 2 wit inspect 7.1 2.2 60 350 2.5 0      - - true 4.7  2.6  51   260 true 11   6.2 210 470
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   11000 12000 2.5 0      error (invalid witness file) .49 .32 6.5 39 error (invalid witness file) 6.2 3.3 87 310 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   880   10000 11000 2.5 0      error (invalid witness file) .54 .35 10   42 error (invalid witness file) 6.2 3.3 130 310 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   11000 11000 2.5 0      error (invalid witness file) .61 .40 8.4 39 error (invalid witness file) 6.0 3.2 110 300 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   880   11000 11000 2.5 0      - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 6.3 3.4 120 310
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   880   10000 11000 2.5 0      - - error (invalid witness file) .49 .31 9.0 40 error (invalid witness file) 6.2 3.3 100 310
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   880   10000 11000 2.5 0      - - error (invalid witness file) .57 .36 9.9 40 error (invalid witness file) 7.0 3.7 110 320
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   870   10000 12000 2.5 0      - - error (invalid witness file) .55 .35 10   44 error (invalid witness file) 6.2 3.3 120 290
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   870   10000 11000 2.5 0      - - error (invalid witness file) .70 .44 8.6 43 error (invalid witness file) 7.2 3.7 110 320
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   870   11000 11000 2.5 0      - - error (invalid witness file) .66 .42 7.8 40 error (invalid witness file) 6.3 3.4 120 300
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   880   11000 11000 2.5 0      - - error (invalid witness file) .51 .33 13   41 error (invalid witness file) 6.5 3.4 110 300
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   880   11000 10000 2.5 0      - - error (invalid witness file) .72 .45 8.9 43 error (invalid witness file) 6.2 3.4 110 300
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   880   9800 11000 2.5 0      - - error (invalid witness file) .54 .34 11   40 error (invalid witness file) 6.9 3.6 130 300
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   840   11000 12000 2.5 0      - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 5.9 3.2 120 300
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 14   5.2 120 500 2.5 0      true 5.9  3.1  110   300 false(unreach-call) 14   7.6 160 370 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.5 2.7 68 470 2.5 0      true 5.7  3.2  41   280 false(unreach-call) 16   8.6 260 400 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 9.5 3.5 71 380 2.5 0      true 5.0  2.8  92   290 false(unreach-call) 9.6 5.1 140 360 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   890   13000 540 2.3 0      error (invalid witness file) .52 .34 5.4 40 error (invalid witness file) 6.2 3.3 100 300 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   860   11000 1000 2.3 .97   error (invalid witness file) .48 .31 6.0 40 error (invalid witness file) 6.4 3.4 110 300 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error 0 wit inspect 8.7 2.6 65 320 2.6 0      error (invalid witness file) .50 .33 9.3 39 error (invalid witness file) 6.3 3.4 130 300 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.0 2.4 61 350 2.5 0      true 4.7  2.5  39   280 false(unreach-call) 9.5 5.0 190 340 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.8 2.7 67 420 2.5 0      true 4.8  2.6  37   290 false(unreach-call) 11   5.8 130 360 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 12   3.4 110 480 2.5 0      true 5.0  2.7  81   280 false(unreach-call) 10   5.4 150 360 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 22   9.8 190 600 2.5 0      true 5.5  3.0  97   290 false(unreach-call) 15   7.7 170 410 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 260   230   3000 820 2.5 0      true 7.3  3.9  51   290 false(unreach-call) 11   6.0 190 380 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.4 2.4 63 380 2.5 0      true 4.8  2.6  39   290 false(unreach-call) 17   9.0 240 420 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 8.5 2.5 65 360 2.5 0      true 6.3  3.4  76   280 false(unreach-call) 9.3 4.9 130 360 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   840   11000 1400 2.3 0      error (invalid witness file) .59 .38 9.3 40 error (invalid witness file) 6.0 3.2 110 300 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 430   400   5200 620 2.5 0      true 5.1  2.8  100   290 false(unreach-call) 10   5.3 190 350 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i error 0 wit inspect 8.4 2.7 64 300 2.6 0      error (invalid witness file) .55 .37 11   40 error (invalid witness file) 6.3 3.3 130 310 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.9 2.3 63 340 2.5 0      true 6.0  3.3  59   280 false(unreach-call) 8.6 4.6 160 320 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   840   11000 1100 2.3 0      error (invalid witness file) .52 .33 4.5 39 error (invalid witness file) 6.1 3.3 120 290 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.9 2.4 72 330 2.5 0      true 5.2  2.8  66   280 false(unreach-call) 9.9 5.2 160 360 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1300 2.3 0      - - error (invalid witness file) .72 .45 9.6 43 error (invalid witness file) 5.9 3.2 120 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   890   12000 590 2.3 0      - - error (invalid witness file) .55 .34 10   40 error (invalid witness file) 6.4 3.4 95 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   11000 630 2.3 0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.8 3.1 82 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   890   12000 590 2.3 0      - - error (invalid witness file) .54 .34 12   43 error (invalid witness file) 5.6 3.0 79 290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   12000 1000 2.3 0      - - error (invalid witness file) .52 .33 11   42 error (invalid witness file) 5.8 3.0 94 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 8.1 2.7 60 310 2.6 0      - - error (invalid witness file) .62 .39 8.6 40 error (invalid witness file) 5.8 3.1 67 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   12000 770 2.3 0      - - error (invalid witness file) .65 .50 10   40 error (invalid witness file) 6.2 3.3 130 300
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   890   12000 530 2.3 0      - - error (invalid witness file) .62 .39 8.5 40 error (invalid witness file) 6.0 3.2 120 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   880   13000 680 2.3 0      - - error (invalid witness file) .69 .42 8.7 41 error (invalid witness file) 6.7 3.5 130 310
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   11000 730 2.3 0      - - error (invalid witness file) .51 .33 10   40 error (invalid witness file) 6.5 3.4 100 320
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   13000 1300 2.3 0      - - error (invalid witness file) .50 .31 12   39 error (invalid witness file) 5.9 3.1 98 310
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   11000 1200 2.3 0      - - error (invalid witness file) .48 .31 10   39 error (invalid witness file) 5.9 3.1 110 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   10000 1200 2.3 0      - - error (invalid witness file) .69 .43 8.3 40 error (invalid witness file) 5.5 3.0 74 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   13000 790 2.3 0      - - error (invalid witness file) .60 .37 12   43 error (invalid witness file) 6.7 3.5 120 310
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   11000 1200 2.3 0      - - error (invalid witness file) .70 .45 9.8 44 error (invalid witness file) 5.5 2.9 69 290
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   860   12000 750 2.3 0      - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.9 3.1 94 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 8.8 2.8 74 320 2.6 0      - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 5.9 3.1 110 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1600 2.3 0      - - error (invalid witness file) .55 .35 9.7 40 error (invalid witness file) 7.2 3.8 60 290
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   840   13000 1400 2.3 0      - - error (invalid witness file) .47 .31 12   41 error (invalid witness file) 7.3 3.8 81 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   12000 730 2.3 0      - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 5.7 3.0 110 290
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   13000 1300 2.3 0      - - error (invalid witness file) .64 .40 10   40 error (invalid witness file) 6.2 3.3 130 300
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 7.7 2.1 59 350 2.5 0      true 4.6  2.5  80   280 false(unreach-call) 8.7 4.7 180 320 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   830   14000 1600 2.3 0      error (invalid witness file) .51 .33 10   40 error (invalid witness file) 5.8 3.1 110 300 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.5 2.1 57 320 2.5 0      true 4.6  2.5  57   280 false(unreach-call) 8.0 4.3 140 330 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i false(unreach-call) 1 wit inspect 21   9.0 200 730 2.5 0      true 5.8  3.1  85   280 false(unreach-call) 12   6.1 200 380 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i timeout 0 wit inspect 900   850   11000 1200 2.3 0      - - error (invalid witness file) .60 .39 10   42 error (invalid witness file) 6.2 3.3 110 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect 8.9 2.7 72 450 2.5 0      true 5.6  3.0  74   290 false(unreach-call) 9.0 4.8 150 320 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout 0 wit inspect 900   830   12000 1900 2.3 0      - - error (invalid witness file) .65 .42 7.6 39 error (invalid witness file) 6.0 3.2 100 300
list-ext2-properties/simple_search_value_false-unreach-call.i timeout 0 wit inspect 900   820   11000 1700 2.3 0      error (invalid witness file) .50 .32 7.9 39 error (invalid witness file) 6.1 3.3 110 300 - -
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900   820   13000 1700 2.3 0      - - error (invalid witness file) .57 .36 11   43 error (invalid witness file) 6.2 3.3 110 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 152 58000 52000 730000 280000 430 .97   173 230 130 3100 13000   173 720 390 11000 35000   173 250 140 3900 16000   173 950 540 16000 36000  
    correct results 100 152 2400 1700 24000 39000 250 .0041 40 220 130 2900 13000   46 610 340 9000 30000   49 210 120 3300 14000   52 610 360 9700 19000  
        correct true 52 104 1200 950 12000 19000 130 .0041 30 0 0 0 0   0 0 0 0 0   49 210 120 3300 14000   52 610 360 9700 19000  
        correct false 48 48 1100 790 12000 20000 120 0      10 220 130 2900 13000   46 610 340 9000 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) 152
Run set sv-comp17.ReachSafety-Heap