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