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-57-generic; 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-10 22:04:57 CET [[ 2017-01-14 18:01:27 CET ]] [[ 2017-01-14 20:11:29 CET ]] [[ 2017-01-14 18:28:10 CET ]] [[ 2017-01-14 20:42:56 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-10_2204.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-10_2204.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 segmentation fault 0 wit inspect 110   50    900 2100 .070  .033  error (invalid witness file) .62 .39 6.2 41 error (invalid witness file) 6.1 3.2 110 310 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 960   880    10000 1900 7.8    .79   unknown 77    60    2100   2000 timeout 96   79   1200 1800 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 960   890    10000 2600 1.2    .025  unknown 22    12    250   650 false(unreach-call) 14   8.0 190 500 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 32   19    300 720 2.9    0      unknown 8.0  4.3  130   340 timeout 96   77   1200 1100 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 41   24    370 1300 .49   8.8    unknown 13    7.0  230   480 false(unreach-call) 69   60   1200 640 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 44   27    430 1200 .49   0      unknown 14    7.6  260   490 false(unreach-call) 73   64   950 660 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   440    4200 3200 .070  0      - - timeout 900    890    17000   3300 timeout 960   940   19000 1100
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error 0 wit inspect 4.4 1.4  37 320 0      9.0    - - error (recursion) 4.8  2.6  98   300 true 820   780   17000 820
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   880    12000 1800 7.8    0      - - unknown 90    70    1700   2000 timeout 960   920   16000 4700
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   490    9700 2300 .098  0      - - timeout 910    840    16000   6000 timeout 960   900   17000 2300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   500    9800 2000 .053  0      - - exception 7.9  4.3  150   330 false(unreach-call) 760   660   15000 3400
heap-manipulation/tree_true-unreach-call.i segmentation fault 0 wit inspect 66   27    650 1200 .049  0      - - error (invalid witness file) .62 .39 9.8 39 error (invalid witness file) 6.4 3.4 130 310
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 16   3.6  120 530 .15   10      unknown 8.1  4.4  110   360 false(unreach-call) 10   5.4 190 350 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   890    7900 1200 .42   19      unknown 8.1  4.3  61   350 false(unreach-call) 35   23   570 790 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 17   3.7  110 520 .24   0      timeout 92    83    1700   1700 false(unreach-call) 11   5.7 180 360 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 16   3.8  110 560 .098  0      exception 7.2  4.0  84   300 false(unreach-call) 41   27   770 800 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 14   7.2  98 500 .14   0      unknown 7.1  3.8  140   310 false(unreach-call) 11   5.8 190 360 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 19   4.1  130 680 .30   0      timeout 92    78    1400   2800 false(unreach-call) 11   5.9 190 360 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i segmentation fault 0 wit inspect 26   6.2  180 710 .049  0      - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 5.9 3.1 91 290
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   440    4800 2500 .045  0      - - timeout 900    890    15000   2400 timeout 960   900   19000 1400
list-properties/list_search_true-unreach-call_false-valid-memtrack.i segmentation fault 0 wit inspect 19   4.6  150 680 .070  .012  - - error (invalid witness file) .68 .44 7.4 40 error (invalid witness file) 6.2 3.3 110 300
list-properties/list_true-unreach-call_false-valid-memtrack.i segmentation fault 0 wit inspect 17   4.1  110 650 .049  0      - - error (invalid witness file) .64 .42 8.3 40 error (invalid witness file) 6.0 3.2 79 290
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   440    5100 3100 .045  0      - - timeout 900    890    15000   3200 timeout 960   930   20000 1900
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   440    6100 2400 .045  .0041 - - timeout 900    900    17000   2500 timeout 960   890   21000 3200
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   440    8000 5700 .053  0      - - timeout 910    880    20000   6700 timeout 960   910   17000 2000
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.0 1.2  32 300 .020  .020  false(unreach-call) 4.4  2.5  86   270 false(unreach-call) 8.3 4.5 170 340 - -
ldv-regression/alt_test.c_false-unreach-call.i unknown 0 wit inspect 7.3 1.9  48 400 .18   .84   false(unreach-call) 8.6  4.6  100   310 false(unreach-call) 10   5.4 190 360 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.4 1.1  27 290 .0082 1.6    false(unreach-call) 3.9  2.1  45   260 false(unreach-call) 7.0 3.8 130 310 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.7 1.4  39 290 .049  .80   false(unreach-call) 6.0  3.2  74   290 unknown 15   8.0 230 360 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.5 1.1  27 290 .020  .020  false(unreach-call) 4.1  2.3  73   270 false(unreach-call) 7.5 4.0 130 320 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.9 1.2  29 290 .020  3.1    false(unreach-call) 4.2  2.4  93   270 false(unreach-call) 7.8 4.2 170 320 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.6 1.1  31 280 .0082 0      false(unreach-call) 4.5  2.5  50   270 false(unreach-call) 9.1 4.7 150 330 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.3 1.3  31 290 .012  0      false(unreach-call) 4.7  2.6  66   280 false(unreach-call) 8.5 4.6 160 340 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 5.6 1.5  42 310 .049  0      false(unreach-call) 7.7  4.1  120   320 false(unreach-call) 25   15   420 660 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect 4.8 1.3  37 290 .029  0      unknown 9.1  4.9  140   310 false(unreach-call) 11   5.9 210 380 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.8 1.2  31 290 .0041 0      unknown 5.6  3.1  64   290 false(unreach-call) 10   5.4 170 350 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 3.6 1.2  29 280 .0041 0      unknown 5.0  2.7  82   290 false(unreach-call) 8.8 4.8 180 340 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect 3.1 1.1  24 270 .0041 0      - - true 3.6  2.0  69   260 true 8.4 4.6 180 320
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect 3.0 1.1  22 270 .0041 .025  - - true 3.7  2.1  72   260 true 7.6 4.1 150 310
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect 3.4 1.1  27 290 .0041 0      - - true 4.8  2.7  42   260 true 9.6 5.1 140 310
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect 3.2 1.1  24 280 .0041 0      - - true 3.5  2.0  72   260 true 7.5 4.0 150 320
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect 3.0 1.1  25 270 .0041 0      - - true 19    11    280   530 true 40   23   470 730
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect 2.7 .98 21 270 .0041 0      - - true 4.0  2.2  43   260 true 8.1 4.3 99 310
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect 3.4 1.1  25 280 .0041 0      - - true 3.5  2.0  63   260 true 8.4 4.5 150 310
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect 3.4 1.1  26 280 .0082 .0041 - - true 4.1  2.3  66   260 true 12   6.2 140 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect 3.0 1.0  25 270 .0041 .0041 - - true 3.8  2.1  59   260 true 11   6.0 180 340
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect 2.8 1.0  21 270 .0041 0      - - true 3.5  2.0  85   260 true 7.2 3.8 140 320
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect 2.8 1.0  24 270 .0041 0      - - true 3.8  2.1  57   260 true 7.5 4.0 150 320
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect 3.1 1.1  25 290 .0041 .025  - - true 4.3  2.4  39   260 true 13   7.3 250 450
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect 3.2 1.1  24 270 .0041 0      - - true 4.2  2.3  47   250 true 13   7.4 210 450
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect 3.2 1.1  27 270 .0041 .0041 - - true 4.6  2.6  43   260 true 10   5.6 200 340
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect 2.7 .97 23 270 .0041 0      - - true 4.2  2.4  50   260 true 7.8 4.2 180 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect 2.8 1.0  22 260 .0041 0      - - true 4.0  2.3  59   260 true 7.4 4.0 140 320
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect 3.2 1.1  25 270 .0041 0      - - true 4.2  2.3  77   270 true 9.2 5.0 180 340
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect 4.5 1.3  31 300 .066  0      - - true 6.2  3.4  59   260 true 11   6.0 210 350
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect 3.8 1.2  31 280 .0041 .79   - - true 4.8  2.6  95   260 true 27   16   390 650
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect 3.1 1.1  27 270 .0041 0      - - true 5.1  2.8  55   260 true 8.2 4.4 120 330
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect 3.1 1.0  22 270 .0041 0      - - true 3.8  2.1  49   260 true 8.3 4.5 130 340
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect 4.0 1.2  33 280 .033  0      - - true 4.6  2.5  99   260 true 8.0 4.3 130 320
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect 2.7 .98 22 270 .0041 0      - - true 3.6  2.0  46   250 true 7.8 4.1 160 320
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect 4.3 1.3  32 280 .033  .0041 - - true 4.4  2.4  100   260 true 8.3 4.5 160 320
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect 4.2 1.2  32 290 .033  0      - - true 4.3  2.4  86   260 true 7.9 4.3 160 320
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect 3.3 1.1  25 270 .0041 0      - - true 5.5  3.0  85   270 true 9.2 4.9 120 320
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect 2.7 1.0  22 270 .0041 0      - - true 3.6  2.0  58   250 true 7.2 3.9 150 310
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect 2.8 1.0  24 270 .0041 0      - - true 3.7  2.1  55   260 true 8.6 4.6 140 320
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect 2.7 .98 22 280 .0041 0      - - true 3.4  1.9  75   260 unknown 7.1 3.7 120 310
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect 3.1 1.1  24 270 .0041 .0041 - - true 3.5  2.0  75   260 unknown 6.0 3.2 120 300
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect 3.0 1.0  25 260 .0041 .0041 - - true 4.5  2.5  47   250 unknown 6.0 3.2 120 310
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect 2.6 .98 21 260 .0041 0      - - true 3.5  2.0  70   260 unknown 8.0 4.2 85 300
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect 3.2 1.0  23 280 .0041 0      - - true 4.1  2.3  48   260 true 10   5.3 110 310
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect 2.9 1.1  24 260 .0041 .025  - - true 4.4  2.4  49   260 true 8.3 4.5 160 310
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 1.1  26 280 .0082 0      false(unreach-call) 3.9  2.2  48   260 false(unreach-call) 7.5 3.9 150 320 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect 3.7 1.1  29 300 .0082 0      false(unreach-call) 4.3  2.4  83   270 false(unreach-call) 9.9 5.3 200 350 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect 3.6 1.1  29 290 .0041 0      false(unreach-call) 4.7  2.7  72   270 false(unreach-call) 7.2 3.8 130 310 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect 3.6 1.1  27 290 .0082 0      false(unreach-call) 4.0  2.2  69   270 false(unreach-call) 8.7 4.6 120 330 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect 3.6 1.1  28 280 .0082 0      false(unreach-call) 5.1  2.9  56   280 false(unreach-call) 8.2 4.4 170 330 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 4.8 1.3  39 340 .016  0      false(unreach-call) 5.5  3.0  60   280 false(unreach-call) 14   7.4 230 410 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 8.7 2.9  75 390 .012  .0041 false(unreach-call) 5.7  3.2  79   310 timeout 98   62   1400 4700 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 12   3.3  92 630 .016  0      unknown 67    57    610   1200 false(unreach-call) 7.5 4.0 150 320 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect 6.8 1.8  44 390 .0082 0      false(unreach-call) 4.4  2.5  81   290 timeout 98   58   1400 6400 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect 3.6 1.1  28 290 .0082 .020  false(unreach-call) 4.5  2.5  48   270 false(unreach-call) 7.2 3.9 140 320 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect 3.9 1.2  31 300 .0041 0      unknown 4.6  2.6  76   290 false(unreach-call) 8.2 4.5 180 360 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect 4.1 1.2  29 310 .012  .025  false(unreach-call) 3.6  2.0  59   280 false(unreach-call) 8.8 4.7 200 340 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect 4.1 1.2  33 320 .012  0      false(unreach-call) 3.8  2.1  67   270 false(unreach-call) 8.6 4.6 150 350 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 1.1  27 280 .0041 0      false(unreach-call) 4.7  2.6  71   270 false(unreach-call) 8.0 4.3 150 330 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect 3.3 1.1  27 270 .0041 0      - - true 3.4  1.9  60   260 true 7.5 4.0 150 310
ldv-regression/test03_true-unreach-call.c true 2 wit inspect 3.3 1.1  26 270 .0041 0      - - true 3.5  2.0  77   260 true 9.1 5.0 160 320
ldv-regression/test04_true-unreach-call.c true 2 wit inspect 3.1 1.1  24 270 .0041 .82   - - true 3.4  1.9  68   250 true 8.7 4.7 170 330
ldv-regression/test05_true-unreach-call.c true 2 wit inspect 3.6 1.1  28 280 .0041 0      - - true 3.8  2.1  59   260 true 14   8.1 220 500
ldv-regression/test07_true-unreach-call.c true 2 wit inspect 3.3 1.1  24 280 .0041 0      - - true 4.6  2.5  52   260 true 11   6.1 190 420
ldv-regression/test09_true-unreach-call.c true 2 wit inspect 3.5 1.1  27 290 .0041 0      - - true 3.8  2.2  61   260 true 11   6.3 210 440
ldv-regression/test10_true-unreach-call.c true 2 wit inspect 3.8 1.1  30 300 .0041 0      - - true 4.6  2.6  50   260 true 15   8.9 250 480
ldv-regression/test11_true-unreach-call.c true 2 wit inspect 3.4 1.1  26 280 .0041 0      - - true 4.3  2.4  49   260 true 10   5.6 210 340
ldv-regression/test13_true-unreach-call.c true 2 wit inspect 3.1 1.0  29 270 .0041 .0041 - - true 4.2  2.4  43   260 true 7.9 4.2 160 310
ldv-regression/test14_true-unreach-call.c true 2 wit inspect 3.4 1.1  25 270 .0041 0      - - true 3.6  2.0  70   260 true 10   5.5 84 320
ldv-regression/test15_true-unreach-call.c true 2 wit inspect 3.3 1.1  23 280 .0041 .0041 - - true 4.4  2.5  43   260 true 11   6.0 180 350
ldv-regression/test16_true-unreach-call.c true 2 wit inspect 3.3 1.1  26 290 .0041 0      - - true 4.4  2.4  47   260 true 10   5.4 180 350
ldv-regression/test17_true-unreach-call.c true 2 wit inspect 3.2 1.1  25 270 .0041 0      - - true 3.8  2.1  48   260 true 7.6 4.0 130 310
ldv-regression/test18_true-unreach-call.c true 2 wit inspect 3.2 1.1  26 280 .0041 0      - - true 3.9  2.2  58   260 true 10   5.6 170 330
ldv-regression/test19_true-unreach-call.c true 2 wit inspect 3.2 1.1  23 270 .0041 0      - - true 3.7  2.1  67   260 true 11   6.0 200 460
ldv-regression/test20_true-unreach-call.c true 2 wit inspect 3.2 1.1  24 270 .0041 0      - - true 4.4  2.5  46   260 true 7.8 4.2 150 320
ldv-regression/test21_true-unreach-call.c true 2 wit inspect 3.5 1.2  27 270 .0082 0      - - true 4.6  2.6  55   260 true 9.9 5.3 170 330
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 9.1 2.0  59 480 .0082 0      - - true 8.1  4.8  99   300 true 46   30   710 800
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 7.9 2.6  61 350 .0082 0      - - true 12    9.3  210   390 timeout 960   840   27000 2300
ldv-regression/test24_true-unreach-call.c true 2 wit inspect 5.7 1.7  46 320 .0041 0      - - true 6.1  3.6  100   300 true 14   8.0 220 530
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 17   5.1  140 540 .012  0      - - true 28    22    490   500 true 32   18   520 680
ldv-regression/test26_true-unreach-call.c true 2 wit inspect 3.2 1.2  23 280 .0041 8.8    - - true 3.9  2.1  51   250 true 11   5.8 200 360
ldv-regression/test27_true-unreach-call.c true 2 wit inspect 8.5 2.7  73 350 .0041 0      - - exception 4.2  2.3  81   280 true 180   160   3000 1300
ldv-regression/test28_true-unreach-call.c true 2 wit inspect 3.3 1.1  23 280 .0041 0      - - true 3.5  2.0  76   260 true 9.2 5.0 130 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect 3.5 1.1  28 280 .0041 0      - - true 3.8  2.2  46   260 true 9.7 5.2 190 330
ldv-regression/test30_true-unreach-call.c true 2 wit inspect 3.3 1.1  26 280 .0041 0      - - true 3.5  2.0  57   260 true 13   7.6 140 490
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 91   33    720 4100 .24   0      timeout 95    69    1300   3100 timeout 96   78   990 1000 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 170   74    1500 4000 10      .025  timeout 97    72    840   2700 timeout 96   80   690 1000 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 75   29    650 3100 .24   .82   timeout 97    73    1500   2800 timeout 97   81   1300 1100 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.3 2.1  57 440 0      0      - - true 14    7.6  150   430 true 12   6.3 190 430
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.5 2.1  58 430 0      0      - - true 16    8.1  170   440 true 12   6.6 240 430
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.4 2.1  52 420 0      0      - - true 12    6.3  200   440 true 16   8.7 150 430
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.6 2.1  62 450 0      .79   - - true 16    8.4  150   440 true 12   6.3 170 420
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.7 2.2  61 620 0      0      - - true 13    6.9  220   440 true 12   6.5 180 440
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.5 2.2  56 430 0      0      - - true 14    7.1  220   440 true 14   7.3 240 440
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.8 2.1  60 430 0      0      - - true 12    6.5  200   450 true 12   6.5 240 430
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.5 2.2  57 430 0      0      - - true 15    7.7  170   430 true 15   7.9 170 430
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.7 2.1  62 420 0      0      - - true 14    7.2  190   440 true 12   6.7 240 440
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 7.7 2.3  58 560 0      0      - - true 14    7.2  180   430 true 13   7.0 220 440
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 47   20    360 1300 1.7    0      unknown 7.6  4.1  120   330 false(unreach-call) 21   12   220 580 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 18   5.2  120 630 .32   .041  unknown 6.6  3.5  47   310 false(unreach-call) 16   8.9 220 560 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.0 1.7  49 360 .19   0      unknown 6.9  3.7  130   310 false(unreach-call) 8.1 4.3 120 350 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 28   8.9  200 720 1.4    0      timeout 93    80    1800   3000 false(unreach-call) 76   52   1000 1100 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 16   7.2  110 770 .29   0      unknown 6.5  3.5  100   300 false(unreach-call) 11   5.8 200 370 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 30   11    230 840 .71   0      unknown 11    6.1  120   430 error 12   6.1 190 320 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 16   4.0  110 540 .17   0      unknown 6.4  3.4  110   300 false(unreach-call) 9.8 5.3 130 350 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 130   100    1300 1600 1.9    6.0    timeout 92    79    910   3000 false(unreach-call) 13   6.8 180 360 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 18   9.0  160 660 .66   0      unknown 6.6  3.5  110   310 false(unreach-call) 18   9.8 310 560 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 64   33    510 1800 2.4    0      timeout 92    79    1600   2100 timeout (false(unreach-call)) 90   76   2000 710 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 340   300    3800 1400 1.2    0      unknown 20    11    290   550 false(unreach-call) 69   50   940 930 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 16   4.3  100 580 .24   0      unknown 6.9  3.8  110   300 false(unreach-call) 18   9.8 380 550 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 7.1 1.7  53 390 .17   .82   unknown 6.5  3.5  76   300 false(unreach-call) 9.7 5.2 150 350 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 15   3.2  100 630 1.4    8.8    timeout 92    80    1600   3200 false(unreach-call) 52   35   580 930 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i unknown 0 wit inspect 15   6.8  140 710 .32   0      unknown 6.4  3.5  77   310 false(unreach-call) 11   5.8 180 360 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 19   6.7  150 580 .37   .79   unknown 8.8  4.7  130   370 error 11   5.9 170 290 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 15   3.7  110 530 .14   10      unknown 6.2  3.3  78   300 false(unreach-call) 8.4 4.5 140 350 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 100   79    1200 1600 1.6    0      timeout 92    79    1000   3100 timeout 97   66   1900 1100 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i unknown 0 wit inspect 17   8.8  150 570 .49   0      unknown 6.4  3.4  140   300 false(unreach-call) 10   5.4 190 360 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 110   71    970 1800 5.3    10      - - out of memory 490    480    8900   7000 timeout 960   910   13000 1100
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   440    5400 4500 .045  0      - - timeout 900    890    18000   3400 timeout 960   890   23000 1200
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 65   22    560 1600 .28   0      - - unknown 30    19    410   660 timeout 960   860   17000 2000
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i segmentation fault 0 wit inspect 100   43    700 1700 1.0    .012  - - error (invalid witness file) .47 .31 11   40 error (invalid witness file) 6.4 3.4 98 290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 38   20    330 950 .51   0      - - unknown 18    11    190   550 timeout 960   880   27000 2200
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 30   11    220 860 .71   0      - - unknown 11    6.1  220   430 error 11   5.9 170 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i segmentation fault 0 wit inspect 26   7.0  190 790 .053  5.8    - - error (invalid witness file) .65 .41 7.3 39 error (invalid witness file) 6.4 3.4 130 300
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i segmentation fault 0 wit inspect 33   10    280 860 .049  .012  - - error (invalid witness file) .65 .43 9.0 41 error (invalid witness file) 7.2 3.8 110 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 960   490    7300 2000 .045  0      - - timeout 900    870    22000   5200 timeout 960   870   17000 1700
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   440    4700 2600 .045  9.0    - - timeout 900    890    20000   4100 timeout 960   890   18000 2500
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i segmentation fault 0 wit inspect 70   25    600 1500 .18   0      - - error (invalid witness file) .65 .40 6.1 39 error (invalid witness file) 6.1 3.2 120 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i segmentation fault 0 wit inspect 77   26    690 1600 .049  .012  - - error (invalid witness file) .60 .40 8.0 39 error (invalid witness file) 6.4 3.4 130 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   440    4700 2700 .045  0      - - timeout 900    890    20000   2900 timeout 960   870   18000 2000
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 59   23    450 1300 .28   19      - - unknown 23    15    430   600 timeout 960   880   16000 1700
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   440    5800 2300 1.1    0      - - timeout 900    890    15000   3500 timeout 960   890   24000 2000
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 19   5.7  130 610 .44   0      - - unknown 14    8.0  160   470 timeout 960   900   24000 2500
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 23   7.1  150 650 .49   10      - - unknown 14    7.9  230   500 error 11   6.0 220 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i segmentation fault 0 wit inspect 27   7.3  210 1000 .053  .033  - - error (invalid witness file) .61 .38 9.6 39 error (invalid witness file) 6.0 3.2 98 310
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i segmentation fault 0 wit inspect 43   16    360 1300 .045  .012  - - error (invalid witness file) .55 .36 8.7 40 error (invalid witness file) 5.7 3.1 110 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 930   470    8400 2200 .045  0      - - timeout 910    870    27000   5000 timeout 960   880   20000 1900
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   440    5600 2100 .045  0      - - timeout 900    890    18000   4000 timeout 960   890   21000 2500
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   870    11000 3900 .074  0      unknown 6.3  3.4  100   290 false(unreach-call) 15   8.1 220 400 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i segmentation fault 0 wit inspect 31   6.5  210 1300 0      .012  error (invalid witness file) .48 .32 8.6 39 error (invalid witness file) 6.9 3.6 140 320 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i timeout 0 wit inspect 900   850    12000 3400 .074  0      unknown 6.6  3.5  110   300 false(unreach-call) 10   5.6 210 360 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i segmentation fault 0 wit inspect 280   130    2700 1600 .057  5.7    error (invalid witness file) .49 .32 8.4 40 error (invalid witness file) 5.8 3.1 120 300 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i segmentation fault 0 wit inspect 36   7.6  240 960 .057  0      - - error (invalid witness file) .50 .32 13   40 error (invalid witness file) 6.3 3.3 110 300
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i unknown 0 wit inspect 91   75    1100 1400 .14   0      unknown 18    9.4  130   530 false(unreach-call) 11   6.2 190 370 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i segmentation fault 0 wit inspect 28   7.9  210 860 .045  .012  - - error (invalid witness file) .58 .37 9.6 40 error (invalid witness file) 5.8 3.1 110 300
list-ext2-properties/simple_search_value_false-unreach-call.i timeout 0 wit inspect 910   420    9300 3400 .36   0      timeout 93    85    820   1400 timeout 96   78   1000 1600 - -
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900   290    5500 3600 0      0      - - timeout 900    890    25000   2800 timeout 960   920   20000 3500
../../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 171 24000 14000 200000 150000 62    150 173 1500 1200 22000 49000   173 1900 1300 28000 45000   173 14000 13000 280000 89000   173 23000 21000 460000 81000  
    correct results 101 171 780 270 6300 42000 13    27 20 580 420 7800 20000   25 780 520 11000 24000   69 440 250 6400 21000   65 1900 1400 42000 29000  
        correct true 70 140 300 95 2400 22000 .42 11 0 0 0 0 0   0 0 0 0 0   69 440 250 6400 21000   65 1900 1400 42000 29000  
        correct false 31 31 480 180 3900 20000 13    16 20 580 420 7800 20000   25 780 520 11000 24000   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) 171
Run set sv-comp17.ReachSafety-Heap