Tool SMACK+Corral 1.7.2
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 11:09:55 CET [[ 2017-01-15 01:36:45 CET ]] [[ 2017-01-15 02:12:47 CET ]] [[ 2017-01-15 01:38:53 CET ]] [[ 2017-01-15 02:35:07 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-13_1109.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-13_1109.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 1 2.1 2.1 29 84 1.1  0      8.3 4.7 170 360 8.2 4.5 92 330
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i 1 90   90   1100 170 1.1  0      5.9 3.2 94 320 7.9 4.2 83 320
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i 1 2.1 2.0 27 85 1.1  0      6.0 3.2 100 300 10   5.5 83 350
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i 1 2.0 2.0 28 80 1.0  0      6.4 3.5 120 310 11   6.0 100 340
heap-manipulation/tree_false-unreach-call_false-valid-deref.i 1 1.9 1.9 26 81 .97 0      7.3 4.3 130 320 7.1 3.9 100 310
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 27 82 .98 0      7.4 4.4 140 310 8.8 4.7 140 320
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i 0 880   930   8600 420 1.1  0      .53 .34 11   42 6.6 3.5 99 300
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i 2 880   880   10000 390 .95 0      4.9  2.7  49   270 810   770   26000 820
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i 0 880   930   7800 410 1.1  0      .52 .34 4.2 43 6.2 3.3 100 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i 0 880   930   7500 480 1.1  0      .57 .36 10   41 6.0 3.2 63 290
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i 0 880   930   10000 300 1.0  0      .53 .34 11   39 6.6 3.5 74 310
heap-manipulation/tree_true-unreach-call.i 2 880   880   7700 540 .97 0      730    700    11000   7000 960   930   17000 700
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i 1 1.8 1.8 22 84 .92 0      5.5 3.0 100 290 7.6 4.1 110 320
list-properties/list_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 27 80 .92 0      91   86   1600 460 8.2 4.4 94 310
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i 1 1.8 1.8 23 83 .91 0      5.2 2.8 93 290 9.6 5.0 67 320
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i 1 1.8 1.8 27 84 .90 0      5.5 3.0 96 300 9.5 5.0 85 320
list-properties/simple_false-unreach-call_false-valid-memcleanup.i 1 1.8 1.8 23 90 .89 0      5.5 3.0 110 290 7.9 4.2 74 330
list-properties/splice_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 21 83 .93 0      5.4 3.0 110 290 8.7 4.7 92 330
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i 2 880   880   9000 250 .92 0      900    890    17000   2500 960   910   17000 2300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i 2 880   880   9500 310 .91 0      900    890    15000   1600 960   890   19000 1900
list-properties/list_search_true-unreach-call_false-valid-memtrack.i 2 1.6 1.6 20 76 .93 0      27    15    460   710 44   30   980 860
list-properties/list_true-unreach-call_false-valid-memtrack.i 2 880   880   10000 260 .92 0      900    890    18000   4500 960   880   23000 1600
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i 2 880   880   9800 300 .88 0      900    900    18000   3200 960   920   17000 2000
list-properties/simple_true-unreach-call_false-valid-memtrack.i 2 880   880   12000 300 .89 0      900    890    20000   2500 960   890   19000 2100
list-properties/splice_true-unreach-call_false-valid-memtrack.i 2 880   880   11000 330 .93 0      900    880    14000   6200 960   900   25000 1900
ldv-regression/1_3.c_false-unreach-call.i 1 1.5 1.6 21 74 .83 0      3.9 2.2 65 270 7.2 3.8 110 320
ldv-regression/alt_test.c_false-unreach-call.i 1 1.6 1.6 18 82 .88 0      5.6 3.0 100 300 8.3 4.4 62 360
ldv-regression/callfpointer.c_false-unreach-call.i 1 1.5 1.4 21 74 .82 0      3.5 2.0 62 260 6.6 3.5 58 320
ldv-regression/fo_test.c_false-unreach-call.i 1 1.6 1.6 21 69 .88 0      5.0 2.7 72 280 14   7.4 170 350
ldv-regression/mutex_lock_int.c_false-unreach-call.i 1 1.5 1.5 19 75 .83 0      3.7 2.1 65 280 7.9 4.2 70 340
ldv-regression/mutex_lock_struct.c_false-unreach-call.i 1 1.5 1.5 18 73 .83 0      3.7 2.1 69 270 8.3 4.4 98 320
ldv-regression/recursive_list.c_false-unreach-call.i 1 1.6 1.6 23 78 .84 0      3.8 2.1 63 280 6.7 3.6 53 310
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i 1 1.6 1.6 19 77 .91 0      4.3 2.4 96 280 7.8 4.2 70 320
ldv-regression/rule60_list2.c_false-unreach-call_1.i 1 1.6 1.6 20 83 .89 0      5.4 3.0 79 290 8.5 4.5 170 350
ldv-regression/stateful_check_false-unreach-call.i 1 2.0 2.0 26 75 .91 0      4.8 2.6 98 280 7.2 3.8 130 320
ldv-regression/test_while_int.c_false-unreach-call.i 1 1.7 1.8 19 79 .83 0      3.8 2.1 75 270 9.1 4.9 140 350
ldv-regression/test_while_int.c_false-unreach-call_1.i 1 1.7 1.6 23 77 .83 0      3.5 2.0 49 280 8.2 4.4 74 330
ldv-regression/alias_of_return.c_true-unreach-call.i 2 1.2 1.2 17 73 .83 0      4.2  2.4  49   260 9.2 4.9 130 320
ldv-regression/alias_of_return.c_true-unreach-call_1.i 2 1.2 1.2 16 69 .82 0      3.6  2.0  54   260 7.8 4.1 160 320
ldv-regression/alias_of_return_2.c_true-unreach-call.i 2 1.2 1.2 15 75 .84 0      3.8  2.1  58   250 9.7 5.3 120 330
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i 2 1.2 1.2 15 67 .82 0      3.6  2.0  78   260 7.9 4.2 130 310
ldv-regression/ex3_forlist.c_true-unreach-call.i 2 1.5 1.5 17 79 .88 0      18    10    340   520 38   22   500 750
ldv-regression/just_assert.c_true-unreach-call.i 2 1.1 1.1 14 70 .82 0      3.9  2.2  43   250 8.1 4.2 110 310
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i 2 1.2 1.2 16 67 .83 0      3.4  1.9  65   260 9.8 5.3 110 310
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i 2 1.2 1.2 14 69 .83 0      3.6  2.0  73   260 8.5 4.6 110 320
ldv-regression/nested_structure.c_true-unreach-call.i 2 1.2 1.3 17 72 .84 0      3.6  2.0  71   260 12   6.4 140 340
ldv-regression/nested_structure_noptr.c_true-unreach-call.i 2 1.2 1.3 16 66 .83 0      3.7  2.1  61   260 8.5 4.5 95 310
ldv-regression/nested_structure_noptr_true-unreach-call.i 2 1.2 1.2 16 71 .83 0      3.3  1.9  53   260 9.6 5.1 110 320
ldv-regression/nested_structure_ptr.c_true-unreach-call.i 2 1.2 1.3 14 70 .84 0      4.0  2.2  41   250 13   7.0 270 420
ldv-regression/nested_structure_ptr_true-unreach-call.i 2 1.2 1.3 15 66 .84 0      3.5  2.0  79   260 15   8.2 210 490
ldv-regression/nested_structure_true-unreach-call.i 2 1.2 1.3 16 74 .84 0      3.5  2.0  75   260 10   5.6 180 350
ldv-regression/oomInt.c_true-unreach-call.i 2 1.2 1.1 16 66 .84 0      3.9  2.2  52   250 9.4 5.0 110 320
ldv-regression/oomInt.c_true-unreach-call_1.i 2 1.2 1.2 15 68 .84 0      3.7  2.0  63   260 8.4 4.5 85 320
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i 2 1.3 1.4 14 83 .91 18      4.0  2.2  70   260 8.8 4.7 190 340
ldv-regression/rule60_list.c_true-unreach-call.i 2 1.3 1.3 15 68 .86 0      4.7  2.6  75   270 14   7.7 140 370
ldv-regression/rule60_list2.c_true-unreach-call.i 2 1.3 1.3 14 72 .89 0      4.6  2.5  80   270 28   16   560 710
ldv-regression/sizeofparameters_test.c_true-unreach-call.i 2 1.2 1.2 14 66 .85 0      4.3  2.4  77   260 7.3 3.9 140 330
ldv-regression/structure_assignment.c_true-unreach-call.i 2 1.2 1.2 15 68 .83 0      3.7  2.1  60   260 7.1 3.7 130 310
ldv-regression/test_address.c_true-unreach-call.i 2 1.2 1.2 15 67 .84 0      5.4  3.0  57   260 8.2 4.3 130 330
ldv-regression/test_cut_trace.c_true-unreach-call.i 2 1.2 1.2 14 70 .83 0      4.2  2.4  40   250 7.8 4.2 140 320
ldv-regression/test_malloc-1_true-unreach-call.i 2 1.2 1.2 16 73 .86 0      5.2  2.8  68   270 9.8 5.3 88 330
ldv-regression/test_malloc-2_true-unreach-call.i 2 1.2 1.2 16 71 .86 0      4.4  2.4  90   270 10   5.4 110 330
ldv-regression/test_overflow.c_true-unreach-call.i 2 1.2 1.2 23 69 .87 0      4.8  2.6  86   260 9.0 4.8 100 320
ldv-regression/test_union.c_true-unreach-call.i 2 1.2 1.2 16 65 .83 0      3.3  1.8  62   250 8.2 4.4 120 310
ldv-regression/test_union.c_true-unreach-call_1.i 2 1.2 1.2 14 68 .83 0      3.3  1.9  73   260 7.3 3.9 150 310
ldv-regression/test_union_cast-1_true-unreach-call.i 2 1.2 1.2 14 69 .84 0      3.4  1.9  58   260 7.1 3.8 100 310
ldv-regression/test_union_cast-2_true-unreach-call.i 2 1.2 1.3 14 90 .84 16      4.1  2.3  55   260 6.2 3.3 110 310
ldv-regression/test_union_cast.c_true-unreach-call.i 2 1.1 1.1 13 68 .83 0      3.4  1.9  56   260 7.2 3.8 67 300
ldv-regression/test_union_cast.c_true-unreach-call_1.i 2 1.2 1.2 17 73 .83 0      3.7  2.1  55   260 6.7 3.6 97 300
ldv-regression/volatile_alias.c_true-unreach-call.i 2 1.2 1.2 15 68 .83 0      3.6  2.0  63   260 8.3 4.4 140 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i 2 1.2 1.2 17 64 .82 0      3.4  1.9  59   260 9.4 5.1 110 320
ldv-regression/test02_false-unreach-call.c 1 1.5 1.5 18 70 .82 0      3.6 2.0 73 270 7.9 4.2 89 320
ldv-regression/test06_false-unreach-call.c 1 1.5 1.6 19 73 .84 0      3.6 2.0 53 290 7.1 3.8 80 310
ldv-regression/test08_false-unreach-call.c 1 1.5 1.5 17 82 .85 0      3.8 2.1 72 280 9.5 5.0 69 330
ldv-regression/test12_false-unreach-call.c 1 1.5 1.5 18 76 .82 0      3.6 2.0 72 270 6.5 3.5 61 310
ldv-regression/test21_false-unreach-call.c 1 1.6 1.6 19 77 .86 0      3.9 2.2 71 280 9.9 5.2 89 310
ldv-regression/test22_false-unreach-call.c 1 1.8 1.8 23 80 .87 .0041 5.7 3.2 100 320 7.1 3.9 78 320
ldv-regression/test23_false-unreach-call.c 1 2.1 2.0 25 84 .88 0      6.5 4.2 130 310 7.8 4.1 100 320
ldv-regression/test24_false-unreach-call.c 1 2.2 2.1 26 80 .95 0      13   11   310 460 7.4 4.0 85 330
ldv-regression/test25_false-unreach-call.c 1 1.9 1.9 25 76 .85 0      5.6 3.3 110 280 7.5 4.0 68 330
ldv-regression/test26_false-unreach-call.c 1 1.5 1.5 17 74 .84 0      3.9 2.1 74 280 6.7 3.5 50 320
ldv-regression/test27_false-unreach-call.c 1 1.7 1.8 21 88 .87 0      4.1 2.3 83 280 7.1 3.8 85 320
ldv-regression/test28_false-unreach-call.c 1 1.5 1.5 16 78 .83 0      3.6 2.0 45 270 6.6 3.5 79 320
ldv-regression/test29_false-unreach-call.c 1 1.6 1.6 19 80 .84 0      3.8 2.1 79 270 6.0 3.3 59 310
ldv-regression/test30_false-unreach-call.c 1 1.5 1.4 21 75 .84 .25   3.8 2.2 81 290 7.8 4.2 62 310
ldv-regression/test01_true-unreach-call.c 2 1.1 1.1 14 67 .82 0      4.3  2.4  47   250 8.6 4.6 120 320
ldv-regression/test03_true-unreach-call.c 2 1.2 1.2 16 69 .84 0      3.8  2.1  60   260 10   5.5 140 320
ldv-regression/test04_true-unreach-call.c 2 1.2 1.2 15 69 .83 0      3.5  2.0  65   260 10   5.7 120 320
ldv-regression/test05_true-unreach-call.c 2 1.2 1.3 13 71 .84 0      3.5  2.0  61   260 14   8.1 260 530
ldv-regression/test07_true-unreach-call.c 2 1.2 1.2 13 73 .85 0      3.9  2.3  55   260 14   7.6 140 370
ldv-regression/test09_true-unreach-call.c 2 1.2 1.2 16 67 .85 0      4.5  2.5  51   260 11   6.2 170 430
ldv-regression/test10_true-unreach-call.c 2 1.2 1.2 15 66 .86 0      4.3  2.4  60   260 17   9.9 260 480
ldv-regression/test11_true-unreach-call.c 2 1.3 1.3 16 66 .86 0      4.6  2.5  35   260 12   6.2 120 320
ldv-regression/test13_true-unreach-call.c 2 1.1 1.1 13 71 .82 0      3.5  2.0  71   260 9.3 5.0 110 330
ldv-regression/test14_true-unreach-call.c 2 1.2 1.3 15 69 .86 0      4.6  2.6  48   260 8.3 4.5 130 330
ldv-regression/test15_true-unreach-call.c 2 1.2 1.2 16 67 .83 0      3.4  1.9  58   260 12   6.2 110 330
ldv-regression/test16_true-unreach-call.c 2 1.2 1.2 15 68 .84 0      4.3  2.4  49   260 10   5.5 190 360
ldv-regression/test17_true-unreach-call.c 2 1.2 1.2 16 71 .82 0      3.7  2.1  50   260 9.6 5.0 120 320
ldv-regression/test18_true-unreach-call.c 2 1.2 1.3 17 69 .83 0      3.5  2.0  61   260 9.4 5.1 150 320
ldv-regression/test19_true-unreach-call.c 2 1.2 1.3 16 71 .84 .0082 3.3  1.9  52   260 11   6.3 150 470
ldv-regression/test20_true-unreach-call.c 2 1.1 1.1 14 68 .82 0      3.8  2.2  52   260 8.6 4.6 170 340
ldv-regression/test21_true-unreach-call.c 2 1.2 1.3 14 64 .86 0      4.0  2.3  64   260 9.9 5.4 180 340
ldv-regression/test22_true-unreach-call.c 2 1.6 1.6 21 79 .87 0      6.3  3.7  140   310 46   30   460 840
ldv-regression/test23_true-unreach-call.c 2 1.7 1.8 20 76 .88 0      11    8.0  260   390 170   150   5000 880
ldv-regression/test24_true-unreach-call.c 2 1.5 1.4 17 77 .86 0      7.1  4.1  68   310 14   7.6 310 360
ldv-regression/test25_true-unreach-call.c 2 2.2 2.2 25 79 .91 0      23    18    520   480 30   17   320 720
ldv-regression/test26_true-unreach-call.c 2 1.1 1.1 13 71 .84 0      4.2  2.4  57   260 9.9 5.5 160 350
ldv-regression/test27_true-unreach-call.c 2 1.6 1.6 19 77 .87 0      8.3  5.9  230   310 95   75   2900 900
ldv-regression/test28_true-unreach-call.c 2 1.2 1.2 14 69 .84 0      3.7  2.1  78   260 9.3 5.0 160 320
ldv-regression/test29_true-unreach-call.c 2 1.2 1.2 17 65 .84 0      3.6  2.0  59   260 10   5.5 120 320
ldv-regression/test30_true-unreach-call.c 2 1.2 1.2 14 68 .84 .0041 4.0  2.3  57   260 11   6.2 200 470
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i 1 16   16   200 210 2.5  0      14   7.8 260 530 15   8.0 120 440
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i 1 16   16   220 210 2.4  0      14   7.7 260 520 12   6.3 150 430
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i 1 16   16   200 210 2.4  0      13   7.4 230 520 12   6.5 220 430
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i 2 3.0 3.0 34 110 2.4  0      11    5.6  220   430 16   8.4 180 420
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i 2 3.0 3.1 39 110 2.4  0      11    5.7  210   450 16   8.3 160 430
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i 2 3.0 3.0 45 100 2.4  0      11    6.0  210   430 13   7.2 180 430
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i 2 3.0 3.1 37 100 2.4  0      12    6.3  160   420 14   7.6 190 440
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i 2 3.1 3.1 39 130 2.4  16      14    7.5  140   440 15   8.0 160 420
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i 2 3.1 3.1 41 110 2.4  0      13    7.1  150   430 13   7.0 220 430
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i 2 3.0 3.0 40 110 2.4  .25   11    5.7  180   440 12   6.5 210 430
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i 2 3.0 3.1 41 110 2.4  0      11    5.7  160   430 15   8.2 150 420
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i 2 3.0 3.0 38 110 2.4  0      11    6.0  210   440 13   7.3 160 430
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i 2 3.0 3.1 42 100 2.5  0      12    6.4  160   420 16   8.6 180 440
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i 1 2.1 2.0 24 91 1.0  0      5.2 2.9 93 290 8.0 4.4 130 310
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 27 82 .95 0      5.2 2.8 110 300 8.6 4.6 63 320
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 20 83 .95 0      4.9 2.7 87 290 7.2 3.9 85 320
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i 1 2.2 2.2 31 88 1.0  0      6.1 3.3 98 310 8.4 4.5 140 330
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 1.8 1.9 26 82 .95 0      5.0 2.8 82 290 8.5 4.5 130 340
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i 1 2.1 2.1 25 91 .97 0      5.4 3.0 110 290 14   7.2 150 300
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 21 86 .96 0      5.3 2.9 92 290 8.7 4.6 180 320
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i 1 2.2 2.2 31 110 .99 16      5.6 3.0 110 290 7.6 4.0 79 320
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 23 84 .95 0      5.0 2.7 96 280 11   5.5 77 350
forester-heap/sll-01_false-unreach-call_false-valid-deref.i 1 2.4 2.3 31 96 1.0  0      91   82   1200 610 7.7 4.2 98 320
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i 1 2.0 2.0 25 88 .98 0      11   7.0 240 300 10   5.4 140 320
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 22 80 .94 0      5.2 2.8 88 290 7.7 4.1 77 330
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 27 82 .95 0      5.1 2.8 91 290 8.1 4.3 79 340
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i 1 2.2 2.1 32 86 1.0  0      5.7 3.1 120 300 8.6 4.6 160 320
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i 1 1.8 1.7 28 87 .93 0      5.2 2.8 110 290 7.0 3.9 110 310
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i 1 2.0 2.0 29 88 .95 0      6.3 3.5 110 300 9.9 5.3 100 300
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i 1 1.9 1.9 26 84 .95 0      5.5 3.0 86 300 7.6 4.1 120 310
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i 1 2.4 2.3 29 94 .98 0      5.9 3.2 110 290 7.1 3.8 52 320
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i 1 1.9 2.0 22 95 .95 16      5.0 2.7 110 280 8.0 4.3 120 330
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i 2 880   880   8600 260 1.0  0      34    20    490   800 960   890   16000 1000
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i 2 880   880   9100 260 .95 0      900    890    17000   3400 960   890   22000 1100
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i 2 880   880   11000 190 .96 .086  27    18    370   630 960   860   20000 1700
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i 2 880   880   10000 280 1.0  0      900    890    19000   3500 960   860   14000 1600
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 2 880   880   8900 190 .97 0      19    11    210   550 960   860   26000 1500
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 2 880   880   11000 190 .97 0      13    7.4  130   410 13   6.8 170 310
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i 2 880   880   9700 250 .97 0      460    440    8400   7000 960   900   34000 1700
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 2 880   880   8000 230 .96 0      900    860    21000   5900 960   880   21000 2000
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i 2 880   880   9300 300 .98 .33   900    860    23000   5200 960   880   26000 1700
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i 2 880   880   9600 250 .95 0      900    890    19000   4000 960   920   21000 900
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i 2 880   880   8400 230 1.0  0      27    16    560   660 960   910   26000 1100
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i 2 880   880   11000 170 .98 0      900    870    16000   6100 960   880   16000 1100
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i 2 880   880   8900 260 .93 0      900    890    15000   3100 960   870   21000 1600
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i 2 880   880   11000 200 .96 0      23    14    360   620 960   870   18000 1300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i 2 880   880   12000 280 1.0  0      900    890    19000   3400 960   910   15000 1600
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i 2 880   880   11000 170 .95 0      11    6.3  210   450 960   890   17000 2100
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i 2 880   880   11000 170 .95 0      16    8.9  170   470 13   6.9 130 310
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i 2 880   880   9100 220 .96 0      650    630    12000   7000 960   930   28000 1400
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i 2 880   880   9800 230 .95 0      900    860    16000   5700 960   870   24000 1600
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i 2 880   880   7400 350 .98 0      900    860    14000   4800 960   890   26000 1800
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i 2 880   880   10000 250 .95 0      900    890    13000   3800 960   890   19000 2400
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i 1 1.9 1.9 23 84 .95 0      4.9 2.7 69 280 9.7 5.2 84 320
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i 1 25   25   320 110 .93 0      96   76   1700 2700 7.2 3.8 100 320
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i 1 1.8 1.8 23 85 .91 0      5.1 2.8 100 280 8.0 4.3 100 330
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i 1 2.3 2.3 31 100 1.0  0      91   86   1600 460 8.3 4.4 110 320
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i 2 880   880   8600 290 1.0  0      900    860    16000   5600 960   880   29000 2100
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i 1 1.9 1.9 26 86 .98 0      5.7 3.1 110 290 7.5 4.1 85 320
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i 2 880   880   11000 320 .97 0      900    810    18000   6500 960   870   16000 3000
list-ext2-properties/simple_search_value_false-unreach-call.i 1 37   36   420 130 .91 0      91   88   1200 520 6.6 3.6 56 330
list-ext2-properties/simple_search_value_true-unreach-call.i 2 880   880   11000 290 .91 0      900    890    18000   1500 960   930   19000 2700
../../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 272 32000 32000 350000 21000 180 83 173 810 620 14000 23000   173 560 300 6500 22000   173 20000 20000 390000 130000   173 30000 27000 660000 81000  
    correct results 169 272 29000 29000 320000 20000 170 83 61 810 620 14000 23000   63 560 300 6500 22000   71 20000 20000 390000 130000   68 30000 27000 660000 80000  
        correct true 103 206 28000 28000 310000 14000 110 50 4 0 0 0 0   56 0 0 0 0   71 20000 20000 390000 130000   68 30000 27000 660000 80000  
        correct false 66 66 310 310 3900 6000 65 32 57 810 620 14000 23000   7 560 300 6500 22000   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) 272
Run set sv-comp17.ReachSafety-Heap