Tool CPAchecker 1.6.1-svn 24048
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 11:18:39 CET [[ 2017-01-14 21:32:33 CET ]] [[ 2017-01-14 22:21:46 CET ]] [[ 2017-01-14 21:35:07 CET ]] [[ 2017-01-14 22:35:09 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options -sv-comp17 -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-seq.2017-01-11_1118.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-seq.2017-01-11_1118.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   870    7500 3500 .14   0      timeout 93   79   1400 1200 timeout 97   84   1400 780 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.6 1.3  29 280 .053  0      false(unreach-call) 5.7 3.1 110 290 true 11   6.0 100 320 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 590   540    7200 2300 1.6    0      unknown 26   14   450 650 false(unreach-call) 15   8.1 320 500 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 360   340    5100 1500 .66   0      unknown 8.9 4.7 180 340 timeout 96   77   1700 1200 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 310   290    3200 1200 .79   0      unknown 13   7.0 250 480 false(unreach-call) 69   60   1400 630 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 310   290    3400 1200 .47   0      unknown 15   7.9 290 480 false(unreach-call) 76   66   1600 670 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870    8100 3300 .14   0      - - timeout 900   890   17000 3100 timeout 960   940   12000 1100
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error 0 wit inspect 4.2 1.5  40 280 0      0      - - error (recursion) 4.7 2.6 72 270 true 840   800   14000 910
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 3.7 1.3  32 280 .053  0      - - false(unreach-call) 6.4 3.5 140 330 true 8.5 4.5 120 320
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   900    11000 1700 .098  0      - - timeout 900   830   16000 6000 timeout 960   890   18000 1500
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   920    12000 1700 .11   0      - - exception 9.8 5.5 120 360 false(unreach-call) 740   640   9500 3400
heap-manipulation/tree_true-unreach-call.i timeout 0 wit inspect 910   870    7500 7400 .098  0      - - out of memory 780   750   13000 7000 timeout 960   930   14000 840
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 99   75    1100 3700 .19   0      unknown 9.0 4.8 160 360 false(unreach-call) 14   7.2 140 370 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 210   200    2600 750 .46   0      unknown 9.5 5.0 160 360 false(unreach-call) 43   28   400 730 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 99   76    1200 4400 .29   0      timeout 92   84   1700 1600 false(unreach-call) 11   6.0 190 360 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 100   82    1200 1400 .18   0      exception 5.9 3.2 100 310 false(unreach-call) 47   31   700 820 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 7.0 2.6  62 410 .19   0      unknown 6.9 3.7 120 300 false(unreach-call) 14   7.5 150 360 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 220   200    2900 890 .61   0      timeout 92   78   2000 3000 false(unreach-call) 14   7.5 130 370 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870    9300 5400 .094  0      - - timeout 900   890   19000 2800 timeout 960   920   19000 2200
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   870    6600 5500 .094  0      - - timeout 900   890   17000 2500 timeout 960   890   17000 2000
list-properties/list_search_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 99   81    1200 1300 .14   0      - - true 28   15   590 690 true 39   26   380 790
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   880    6800 2700 .090  0      - - timeout 900   890   14000 3900 timeout 960   880   27000 1700
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   890    6800 3400 .090  0      - - timeout 900   900   17000 3200 timeout 960   930   18000 2000
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   890    6300 2600 .090  0      - - timeout 900   890   14000 2500 timeout 960   890   13000 3000
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   860    8300 6300 .094  0      - - timeout 900   880   16000 6700 timeout 960   910   21000 1800
ldv-regression/1_3.c_false-unreach-call.i unknown 0 wit inspect 4.3 1.9  35 310 .045  0      false(unreach-call) 4.5 2.5 83 270 false(unreach-call) 10   5.7 120 340 - -
ldv-regression/alt_test.c_false-unreach-call.i unknown 0 wit inspect 7.2 2.3  55 430 .21   0      false(unreach-call) 7.2 3.8 130 300 false(unreach-call) 11   5.9 100 350 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.6 1.1  21 250 .0041 0      false(unreach-call) 3.5 2.0 71 270 false(unreach-call) 7.6 4.0 160 320 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.4 1.2  27 270 .049  0      false(unreach-call) 5.3 2.9 100 280 unknown 18   9.5 240 340 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.8 1.2  23 280 .012  0      false(unreach-call) 3.9 2.2 52 270 false(unreach-call) 10   5.4 110 320 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.9 1.3  25 280 .012  0      false(unreach-call) 4.1 2.3 77 270 false(unreach-call) 9.4 5.0 91 330 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.6 1.1  21 250 .0082 0      false(unreach-call) 4.1 2.3 87 280 false(unreach-call) 10   5.3 93 310 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.9 1.2  25 260 .0082 0      false(unreach-call) 4.1 2.3 81 280 false(unreach-call) 9.8 5.3 110 350 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 3.6 1.4  29 270 .037  0      false(unreach-call) 5.5 3.0 100 290 false(unreach-call) 23   12   190 530 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 1.3  27 260 .029  0      false(unreach-call) 4.8 2.7 110 280 false(unreach-call) 11   5.5 120 330 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 2.5 1.1  22 250 .0041 0      false(unreach-call) 3.6 2.0 48 270 false(unreach-call) 7.0 3.8 120 310 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 2.6 1.1  22 250 .0041 0      false(unreach-call) 3.7 2.1 67 270 false(unreach-call) 8.3 4.5 130 340 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect 2.8 1.2  24 270 .0082 0      - - true 3.9 2.2 56 250 true 8.0 4.3 160 320
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect 2.7 1.2  24 260 .0082 0      - - true 3.5 2.0 75 260 true 7.4 3.9 84 320
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect 2.7 1.2  23 260 .0082 0      - - true 4.1 2.3 51 260 true 7.9 4.3 160 310
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect 2.7 1.2  26 260 .0082 0      - - true 3.5 1.9 69 250 true 7.1 3.8 94 320
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect 2.6 1.1  24 250 0      0      - - true 22   13   260 540 true 32   18   460 740
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect 2.1 .87 19 190 0      0      - - true 3.5 2.0 67 270 true 7.6 4.0 98 310
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect 2.7 1.1  25 260 .0082 0      - - true 4.1 2.3 54 260 true 8.5 4.6 160 310
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect 2.7 1.1  22 260 .0082 0      - - true 4.0 2.3 58 260 true 8.4 4.6 170 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect 3.0 1.2  27 270 .0082 0      - - true 3.6 2.0 67 270 true 9.7 5.2 130 330
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect 2.2 .94 18 240 0      0      - - true 3.5 1.9 66 260 true 7.8 4.1 130 310
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect 2.2 .94 19 240 0      0      - - true 3.7 2.0 70 270 true 7.1 3.8 88 330
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect 2.8 1.2  22 260 .0082 0      - - true 3.7 2.1 68 260 true 13   7.2 140 440
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect 3.0 1.2  25 270 .0082 0      - - true 3.6 2.0 76 260 true 13   7.3 260 480
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect 2.8 1.2  23 260 .0082 0      - - true 3.6 2.0 64 260 true 10   5.4 77 340
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect 2.4 1.0  19 250 0      0      - - true 3.5 2.0 68 260 true 7.9 4.2 120 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect 2.2 .95 20 240 0      0      - - true 3.5 2.0 78 250 true 7.5 4.0 150 320
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect 2.5 1.0  23 240 0      0      - - true 4.5 2.5 69 260 true 8.5 4.6 100 350
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect 3.7 1.4  30 280 .066  0      - - true 5.2 2.9 75 270 true 10   5.7 140 360
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect 2.6 1.1  22 250 0      0      - - true 5.1 2.8 91 270 true 28   16   450 710
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect 2.5 1.0  23 260 0      0      - - true 4.8 2.7 58 260 true 7.4 4.0 120 320
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect 2.7 1.1  26 280 .0082 0      - - true 3.5 1.9 74 260 true 8.6 4.6 73 310
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect 3.7 1.4  35 280 .066  0      - - true 4.6 2.5 90 260 true 7.7 4.1 160 320
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect 2.2 .94 19 240 0      0      - - true 3.6 2.0 64 250 true 8.1 4.3 150 330
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect 3.7 1.4  32 280 .066  0      - - true 5.6 3.1 61 260 true 8.2 4.4 140 320
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect 3.7 1.4  30 280 .066  0      - - true 5.2 2.9 65 260 true 8.3 4.5 160 330
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect 2.8 1.1  24 260 0      0      - - true 5.7 3.1 79 270 true 8.9 4.7 64 320
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect 2.3 .95 20 240 0      0      - - true 3.4 2.0 63 250 true 7.2 3.8 110 310
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect 2.2 .94 18 240 0      0      - - true 4.0 2.2 45 260 true 7.3 3.9 120 320
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect 2.3 .99 20 240 0      0      - - true 3.9 2.2 49 260 unknown 5.4 2.9 74 290
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect 3.0 1.2  23 270 .0082 0      - - true 4.2 2.3 61 260 unknown 6.0 3.2 130 290
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect 2.8 1.2  26 260 .0082 0      - - true 3.8 2.2 51 260 unknown 5.8 3.2 110 290
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect 2.3 .96 20 250 0      0      - - true 3.8 2.2 52 260 unknown 6.3 3.4 140 300
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect 2.8 1.2  22 270 .0082 0      - - true 4.2 2.3 49 260 true 8.2 4.4 180 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect 2.7 1.1  26 270 .0082 0      - - true 4.2 2.3 49 250 true 7.7 4.2 110 320
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect 2.5 1.0  20 250 .0041 0      false(unreach-call) 4.0 2.2 93 280 false(unreach-call) 9.3 4.9 91 320 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect 2.5 1.1  23 250 .0041 0      false(unreach-call) 4.1 2.3 82 280 true 8.1 4.3 130 320 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect 2.6 1.1  25 250 .0041 0      false(unreach-call) 3.7 2.1 78 270 false(unreach-call) 7.8 4.1 120 330 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect 2.5 1.1  21 250 .0041 0      false(unreach-call) 3.8 2.1 79 290 false(unreach-call) 8.3 4.4 150 330 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect 2.5 1.1  20 260 .0082 0      false(unreach-call) 4.0 2.2 65 280 false(unreach-call) 9.0 4.8 180 330 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 1.4  31 300 .020  0      false(unreach-call) 4.5 2.5 76 280 false(unreach-call) 15   8.2 180 410 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 17   13    190 320 .020  0      false(unreach-call) 5.2 2.9 100 300 timeout 98   65   1300 3600 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 5.3 2.9  47 520 .016  0      false(unreach-call) 15   13   440 510 timeout 96   60   1700 6600 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect 9.4 6.7  100 300 .012  0      false(unreach-call) 4.3 2.4 90 290 timeout 98   60   1000 6400 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect 2.4 1.1  23 250 .0041 0      false(unreach-call) 3.6 2.0 72 270 false(unreach-call) 9.4 5.0 95 320 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect 2.6 1.1  23 260 .0041 0      false(unreach-call) 4.0 2.2 77 280 false(unreach-call) 9.3 5.0 130 320 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect 2.9 1.3  28 280 .012  0      false(unreach-call) 3.6 2.0 87 280 false(unreach-call) 9.3 5.0 110 350 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect 2.5 1.1  20 260 .0041 0      false(unreach-call) 3.6 2.0 77 280 false(unreach-call) 9.5 5.1 160 340 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect 2.7 1.1  23 260 .0041 0      false(unreach-call) 4.1 2.3 80 280 false(unreach-call) 8.7 4.6 120 320 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect 2.7 1.1  25 260 .0082 0      - - true 3.4 1.9 65 250 true 8.0 4.2 150 320
ldv-regression/test03_true-unreach-call.c true 2 wit inspect 2.8 1.2  25 260 .0082 0      - - true 4.0 2.3 50 250 true 8.6 4.7 190 320
ldv-regression/test04_true-unreach-call.c true 2 wit inspect 2.7 1.2  26 260 .0082 0      - - true 3.8 2.1 55 260 true 7.8 4.2 66 320
ldv-regression/test05_true-unreach-call.c true 2 wit inspect 3.0 1.3  25 270 .0082 0      - - true 4.0 2.2 77 260 true 13   7.4 170 490
ldv-regression/test07_true-unreach-call.c true 2 wit inspect 2.8 1.2  23 260 .0082 0      - - true 3.5 2.0 65 260 true 11   6.1 230 430
ldv-regression/test09_true-unreach-call.c true 2 wit inspect 3.2 1.3  27 270 .0082 0      - - true 3.8 2.1 64 260 true 13   7.1 140 440
ldv-regression/test10_true-unreach-call.c true 2 wit inspect 3.1 1.3  30 260 .0082 0      - - true 4.3 2.4 55 260 true 15   9.1 180 510
ldv-regression/test11_true-unreach-call.c true 2 wit inspect 3.0 1.2  25 260 .0082 0      - - true 3.8 2.1 75 260 true 9.3 5.0 150 320
ldv-regression/test13_true-unreach-call.c true 2 wit inspect 2.7 1.2  24 260 .0082 0      - - true 4.2 2.4 58 260 true 8.3 4.4 160 320
ldv-regression/test14_true-unreach-call.c true 2 wit inspect 3.1 1.3  25 270 .0082 0      - - true 3.9 2.2 69 260 true 8.4 4.5 110 320
ldv-regression/test15_true-unreach-call.c true 2 wit inspect 2.7 1.1  26 270 .0082 0      - - true 4.2 2.4 49 260 true 10   5.4 200 340
ldv-regression/test16_true-unreach-call.c true 2 wit inspect 2.8 1.2  26 270 .0082 0      - - true 3.4 2.0 65 260 true 10   5.5 210 360
ldv-regression/test17_true-unreach-call.c true 2 wit inspect 2.6 1.2  23 260 .0082 0      - - true 4.2 2.4 48 260 true 7.2 3.8 54 310
ldv-regression/test18_true-unreach-call.c true 2 wit inspect 2.8 1.2  22 260 .0082 0      - - true 3.5 1.9 68 260 true 8.8 4.8 110 320
ldv-regression/test19_true-unreach-call.c true 2 wit inspect 2.8 1.2  22 260 .0082 0      - - true 4.0 2.3 44 260 true 13   7.1 130 470
ldv-regression/test20_true-unreach-call.c true 2 wit inspect 2.6 1.1  21 260 .0082 0      - - true 3.5 2.0 80 250 true 8.1 4.3 160 320
ldv-regression/test21_true-unreach-call.c true 2 wit inspect 3.2 1.3  26 270 .016  0      - - true 4.4 2.5 55 260 true 9.3 5.0 140 330
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 23   11    36 280 .016  0      - - true 7.9 4.6 99 330 true 40   26   680 840
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 18   13    190 400 .029  0      - - true 11   8.4 240 390 timeout 960   840   16000 2200
ldv-regression/test24_true-unreach-call.c true 2 wit inspect 42   39    440 490 .0082 0      - - true 7.6 4.5 91 300 true 13   7.2 200 360
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 210   200    2000 1500 .037  0      - - true 28   22   550 500 true 29   16   450 690
ldv-regression/test26_true-unreach-call.c true 2 wit inspect 2.9 1.2  25 260 .0082 0      - - true 4.2 2.4 49 260 true 9.5 5.2 160 340
ldv-regression/test27_true-unreach-call.c true 2 wit inspect 15   11    190 350 .016  0      - - exception 4.5 2.6 64 280 true 530   510   12000 1200
ldv-regression/test28_true-unreach-call.c true 2 wit inspect 3.0 1.2  27 260 .0082 0      - - true 3.8 2.1 72 260 true 9.8 5.2 150 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect 3.0 1.2  24 270 .0082 0      - - true 3.6 2.0 79 250 true 8.6 4.7 190 320
ldv-regression/test30_true-unreach-call.c true 2 wit inspect 2.9 1.2  25 260 .0082 0      - - true 3.5 2.0 72 260 true 11   6.4 230 460
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 7.8 2.5  74 410 .11   0      false(unreach-call) 15   8.5 260 530 timeout 97   77   1400 1000 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 7.9 2.7  62 410 .11   0      false(unreach-call) 14   7.7 270 530 timeout 97   77   1400 930 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 7.6 2.5  68 400 .11   0      false(unreach-call) 16   9.1 190 530 timeout 97   78   1100 920 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   87    1200 970 0      0      - - true 12   6.1 190 440 true 11   6.1 130 430
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   87    1200 960 0      0      - - true 14   7.2 150 440 true 13   7.0 180 440
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   86    1300 1100 0      0      - - true 10   5.4 200 440 true 10   5.7 120 420
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   87    1100 990 0      0      - - true 11   5.8 250 430 true 13   6.9 250 430
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   87    1400 1100 0      0      - - true 13   6.8 140 420 true 12   6.4 230 420
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   86    1200 1000 0      0      - - true 13   6.7 160 420 true 12   6.4 220 430
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   86    1300 970 0      0      - - true 11   5.8 210 440 true 11   6.0 130 420
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   86    1300 1000 0      0      - - true 11   5.6 190 430 true 12   6.3 150 430
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   86    1300 940 0      0      - - true 12   6.2 190 430 true 12   6.5 240 420
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 94   86    1000 970 0      0      - - true 11   5.9 210 440 true 11   5.8 120 430
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 220   200    2300 970 .38   0      unknown 9.1 4.8 130 330 false(unreach-call) 25   14   160 590 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 220   200    2400 1000 .46   0      unknown 7.1 3.8 120 310 false(unreach-call) 17   9.4 240 540 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.4 1.3  30 270 .045  0      true 4.6 2.5 98 280 false(unreach-call) 12   6.3 110 350 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 220   210    2400 1000 .66   0      timeout 93   79   2200 2500 false(unreach-call) 80   55   1100 1100 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 10   4.9  93 490 .31   0      unknown 6.8 3.7 130 300 false(unreach-call) 13   7.0 150 360 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 260   250    2700 820 1.0    0      unknown 12   6.7 250 430 error 12   6.3 190 300 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 120   86    1200 4200 .88   0      unknown 6.5 3.5 130 310 false(unreach-call) 8.4 4.5 130 350 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 370   340    4100 1000 2.6    .0041 timeout 92   78   2200 2800 false(unreach-call) 14   7.7 190 360 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 220   210    2700 900 1.2    0      unknown 6.6 3.5 95 310 false(unreach-call) 19   11   250 560 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 240   210    2600 1100 1.4    0      timeout 93   80   1600 2000 timeout 97   81   1800 600 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 410   360    4900 4100 1.7    0      unknown 20   11   390 550 false(unreach-call) 80   57   1000 950 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 210   200    2900 990 .43   0      unknown 7.2 3.9 110 310 false(unreach-call) 20   11   180 550 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.3 1.3  29 270 .045  0      true 4.6 2.5 100 280 false(unreach-call) 11   5.8 110 350 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 220   200    2900 900 .66   0      timeout 92   79   1900 2700 false(unreach-call) 67   45   940 1100 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 9.9 4.0  83 490 .31   0      unknown 6.4 3.5 130 300 false(unreach-call) 12   6.4 150 360 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 210   200    2400 880 .39   0      unknown 9.7 5.2 200 370 error 12   6.2 190 300 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 100   77    1200 4100 .29   0      unknown 6.4 3.5 130 300 false(unreach-call) 12   6.6 96 360 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 340   320    4600 1000 2.0    .0041 timeout 92   78   2400 2900 timeout 97   68   1700 1200 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 210   210    2400 910 1.2    0      unknown 6.4 3.4 120 300 false(unreach-call) 12   6.2 170 370 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 290   260    3400 1700 3.9    0      - - out of memory 520   500   12000 7000 timeout 960   900   13000 1100
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   880    7500 2900 .090  0      - - timeout 900   890   12000 3200 timeout 960   880   20000 1200
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 240   220    2400 1400 .29   0      - - unknown 32   21   380 650 timeout 960   870   13000 2400
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   880    6600 3000 .090  0      - - timeout 900   890   18000 3600 timeout 960   860   23000 1900
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 240   220    2500 900 .61   0      - - unknown 15   9.5 300 550 timeout 960   870   15000 2200
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 240   230    2600 780 .68   0      - - unknown 12   6.8 260 420 error 12   6.3 230 310
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   870    8000 7600 .090  0      - - out of memory 500   490   10000 7000 timeout 960   920   18000 1300
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   820    9600 6100 .094  0      - - timeout 900   860   19000 5900 timeout 960   900   16000 2000
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840    12000 5100 .090  0      - - timeout 910   880   24000 5100 timeout 960   870   13000 1700
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   880    6600 3700 .090  0      - - timeout 900   890   17000 3900 timeout 960   930   18000 1200
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 270   240    3000 1400 3.9    0      - - out of memory 570   550   17000 7000 timeout 960   910   16000 1100
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830    12000 5100 .094  0      - - timeout 900   860   14000 6000 timeout 960   910   14000 1100
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   880    6600 2900 .090  0      - - timeout 900   890   19000 3400 timeout 960   880   16000 2300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 230   210    2800 1000 .29   0      - - unknown 22   14   550 610 timeout 960   890   17000 1600
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   880    5800 2800 .090  0      - - timeout 900   890   16000 3500 timeout 960   880   15000 1700
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 210   200    2700 740 .53   0      - - unknown 12   6.5 240 470 timeout 960   900   15000 2400
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 210   210    2500 800 .41   0      - - unknown 12   6.9 230 490 error 11   5.7 100 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   870    7800 8200 .090  0      - - out of memory 700   680   12000 7000 timeout 960   910   13000 2200
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   830    9600 6000 .094  0      - - timeout 900   850   19000 5700 timeout 960   870   16000 1800
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840    9500 5100 .094  0      - - timeout 900   870   19000 5000 timeout 960   870   13000 2000
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   890    7000 3700 .090  0      - - timeout 900   890   13000 3800 timeout 960   900   14000 2400
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   860    13000 2400 .24   0      unknown 6.7 3.6 140 300 false(unreach-call) 14   7.7 220 400 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 930   790    13000 3000 .72   0      timeout 92   80   1600 1700 timeout 96   69   970 1100 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 3.3 1.3  27 270 .045  0      false(unreach-call) 5.4 2.9 110 290 false(unreach-call) 7.7 4.1 140 320 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i unknown 0 wit inspect 860   820    11000 890 3.7    0      unknown 33   19   570 910 false(unreach-call) 54   35   650 840 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i timeout 0 wit inspect 960   920    12000 1400 .094  0      - - timeout 900   870   22000 5600 timeout 960   880   17000 2000
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i unknown 0 wit inspect 42   30    460 1400 .19   0      unknown 20   10   340 440 false(unreach-call) 15   8.3 170 360 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout 0 wit inspect 910   820    10000 5700 .090  0      - - timeout 900   800   18000 6300 timeout 960   890   22000 3700
list-ext2-properties/simple_search_value_false-unreach-call.i timeout 0 wit inspect 910   840    12000 1200 .47   .0041 timeout 92   85   1500 1500 timeout 97   72   1600 1400 - -
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900   530    7200 1400 .11   0      - - timeout 900   890   17000 2600 timeout 960   920   22000 1400
../../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 157 38000   35000   390000 210000 42     .012 173 1400 1000 27000 41000   173 2200 1500 32000 49000   173 24000   23000   450000 150000   173 34000   31000   580000 92000  
    correct results 102 173 1600   1300   19000 37000 1.6   0     31 180 100 3400 9700   24 840 550 11000 28000   70 440   250   7200 21000   66 2300   1800   40000 30000  
        correct true 71 142 1500   1300   18000 29000 .82  0     2 0 0 0 0   2 0 0 0 0   70 440   250   7200 21000   66 2300   1800   40000 30000  
        correct false 31 31 130   60   1200 9000 .81  0     29 180 100 3400 9700   22 840 550 11000 28000   0 0   0   0 0   0 0   0   0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 1 -16 3.7 1.3 32 280 .053 0     0 0 0 0 0   0 0 0 0 0   1 6.4 3.5 140 330   1 8.5 4.5 120 320  
        incorrect true 0
        incorrect false 1 -16 3.7 1.3 32 280 .053 0     0 0 0 0 0   0 0 0 0 0   1 6.4 3.5 140 330   0 8.5 4.5 120 320  
score (173 tasks, max score: 280) 157
Run set sv-comp17.ReachSafety-Heap