Tool CPAchecker 1.6.1-svn 23987
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 20:44:08 CET [[ 2017-01-14 18:01:01 CET ]] [[ 2017-01-14 20:09:29 CET ]] [[ 2017-01-14 18:26:00 CET ]] [[ 2017-01-14 20:41:28 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options -sv-comp17-bam-bnb -disable-java-assertions -heap 10000m [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-bam-bnb.2017-01-10_2044.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-bam-bnb.2017-01-10_2044.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 false(unreach-call) 1 wit inspect 9.5 2.9 75 470 .078  0      timeout 92    83    1200   470 false(unreach-call) 12   6.4 180 370 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i error 0 wit inspect 4.1 1.6 35 290 .057  0      error (invalid witness file) .49 .32 3.8 40 error (invalid witness file) 6.7 3.5 120 300 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.2 1.8 40 310 .053  0      true 5.8  3.1  130   330 false(unreach-call) 11   6.0 200 380 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i true -32 wit inspect 39   16   350 1600 0      0      unknown 9.3  5.0  180   380 false(unreach-call) 11   5.6 220 380 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 5.9 2.1 50 330 .053  8.1    true 5.0  2.7  85   280 true 8.2 4.4 150 320 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.8 2.0 48 320 .053  0      true 5.6  3.0  83   280 true 8.6 4.6 160 320 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 12   3.5 89 510 .078  0      - - error (invalid witness file) .56 .36 9.9 40 error (invalid witness file) 6.0 3.2 110 300
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 13   3.7 92 460 0      0      - - error (recursion) 4.4  2.4  57   270 true 870   830   17000 910
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 4.2 1.6 33 290 .057  0      - - error (invalid witness file) .47 .31 12   39 error (invalid witness file) 6.2 3.3 120 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 6.1 2.0 45 320 0      0      - - timeout 900    830    19000   6200 timeout 960   900   24000 1500
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 27   7.5 200 800 0      0      - - timeout 910    840    17000   6400 timeout 960   850   21000 3600
heap-manipulation/tree_true-unreach-call.i true 2 wit inspect 9.8 2.9 94 470 0      0      - - out of memory 870    840    15000   7000 timeout 960   920   16000 890
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.5 1.7 44 310 .049  0      true 4.4  2.4  53   280 false(unreach-call) 7.9 4.2 110 320 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 6.6 2.1 58 360 .049  0      true 4.4  2.4  71   280 false(unreach-call) 8.6 4.6 140 330 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.4 1.6 39 300 .049  0      true 4.3  2.3  48   270 false(unreach-call) 7.8 4.2 140 330 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.7 1.7 39 310 .053  2.3    true 5.0  2.7  99   290 false(unreach-call) 34   23   360 700 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.3 1.7 38 300 .049  8.1    true 4.3  2.4  50   280 false(unreach-call) 7.7 4.1 160 320 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 5.0 1.8 39 310 .049  0      true 4.7  2.5  63   280 false(unreach-call) 8.3 4.5 160 330 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 5.2 1.9 39 300 0      0      - - out of memory 460    340    11000   7000 timeout 960   920   18000 2500
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 5.4 1.9 45 300 0      0      - - out of memory 510    380    9100   7000 false(unreach-call) 8.4 4.5 180 350
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(unreach-call) -16 wit inspect 5.0 1.8 44 300 .074  0      - - true 6.2  3.4  97   300 true 23   14   400 630
list-properties/list_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.9 2.2 50 450 0      0      - - out of memory 190    160    3800   7000 timeout 960   880   19000 1800
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 4.0 1.6 36 290 0      0      - - out of memory 590    420    10000   7000 timeout 960   930   24000 1900
list-properties/simple_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 5.0 1.8 38 290 0      0      - - out of memory 440    330    12000   7000 timeout 960   900   16000 2300
list-properties/splice_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.4 2.1 48 330 0      0      - - timeout 900    870    15000   6300 timeout 960   900   19000 1900
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.3 1.4 31 300 .0041 4.2    false(unreach-call) 3.8  2.1  49   270 false(unreach-call) 7.5 4.0 130 320 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.8 1.7 43 310 .066  0      false(unreach-call) 5.4  2.9  110   280 false(unreach-call) 10   5.5 140 350 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.1 1.2 26 290 .0041 0      false(unreach-call) 3.6  2.0  48   270 false(unreach-call) 7.7 4.0 130 330 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect 4.0 1.5 33 300 .053  0      true 4.8  2.6  79   280 unknown 15   8.0 310 350 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.0 1.3 30 280 .0041 0      false(unreach-call) 3.6  2.0  66   270 false(unreach-call) 8.6 4.5 150 320 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 1.3 29 280 .0041 .029  false(unreach-call) 3.6  2.0  48   270 false(unreach-call) 7.7 4.1 140 320 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.3 1.4 28 300 .0082 0      false(unreach-call) 4.2  2.4  58   280 false(unreach-call) 8.8 4.7 130 330 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.7 1.5 30 290 .0082 0      true 4.2  2.3  75   270 false(unreach-call) 8.3 4.5 140 350 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 5.0 1.7 42 300 .041  0      true 19    9.9  210   620 false(unreach-call) 9.0 4.8 170 350 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect 3.8 1.5 34 290 .025  0      true 4.0  2.2  65   270 false(unreach-call) 8.8 4.7 170 340 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect 3.2 1.3 28 280 .0041 0      true 3.5  2.0  62   270 false(unreach-call) 8.7 4.5 110 320 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect 3.1 1.3 29 290 .0041 0      false(unreach-call) 4.0  2.2  83   270 false(unreach-call) 6.9 3.7 120 310 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect 2.6 1.2 27 270 0      0      - - true 3.9  2.2  60   260 true 9.5 5.1 99 310
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect 2.5 1.1 22 270 0      0      - - true 3.5  1.9  88   260 true 7.8 4.2 150 330
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect 2.6 1.2 23 270 0      0      - - true 4.0  2.3  53   260 true 9.8 5.2 120 320
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect 2.5 1.1 25 260 0      0      - - true 3.6  2.0  72   260 true 7.6 4.0 140 320
ldv-regression/ex3_forlist.c_true-unreach-call.i error 0 wit inspect 5.1 1.9 46 310 .0082 0      - - error (invalid witness file) .65 .41 7.6 40 error (invalid witness file) 6.4 3.4 130 310
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect 2.5 1.1 24 260 0      0      - - true 4.2  2.3  52   260 true 6.8 3.6 130 300
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect 2.9 1.2 27 270 0      0      - - true 3.7  2.1  83   260 true 9.1 4.9 130 320
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect 2.8 1.2 27 270 0      0      - - true 4.3  2.4  50   260 true 8.5 4.6 150 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect 2.8 1.2 26 280 0      0      - - true 4.2  2.4  50   260 true 10   5.4 210 330
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect 2.5 1.1 21 260 0      0      - - true 3.4  1.9  60   260 true 7.3 3.9 130 310
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect 2.7 1.2 25 280 0      0      - - true 3.4  1.9  61   250 true 7.4 3.9 140 320
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect 2.6 1.2 23 260 0      0      - - true 4.4  2.5  46   260 true 15   8.0 150 450
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect 2.7 1.2 25 270 0      0      - - true 3.4  1.9  69   260 true 13   7.3 250 470
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect 2.9 1.2 28 280 0      0      - - true 3.9  2.2  56   250 true 12   6.5 150 360
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect 2.6 1.2 25 270 0      0      - - true 3.4  1.9  54   260 true 7.7 4.1 150 330
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect 2.6 1.2 26 270 0      0      - - true 3.8  2.1  62   260 true 7.7 4.1 120 320
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect 3.3 1.3 29 280 0      0      - - true 4.4  2.5  56   270 true 9.3 5.0 180 350
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect 3.9 1.5 37 290 0      2.3    - - true 5.5  3.0  66   260 true 14   7.5 160 350
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect 4.0 1.5 36 280 0      0      - - true 4.8  2.7  91   270 true 28   16   380 680
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect 3.1 1.3 25 280 0      0      - - true 4.4  2.4  81   260 true 8.9 4.7 120 310
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect 2.5 1.1 22 270 0      0      - - true 3.3  1.8  62   260 true 7.5 4.0 150 310
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect 3.2 1.4 29 270 0      .0041 - - true 5.2  2.9  68   260 true 7.6 4.1 120 330
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect 2.6 1.1 23 270 0      0      - - true 3.4  1.9  65   250 true 7.5 4.0 150 310
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect 3.5 1.4 28 290 0      0      - - true 4.9  2.7  69   260 true 12   6.4 120 320
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect 3.3 1.3 32 280 0      0      - - true 6.0  3.3  65   270 true 9.1 4.9 140 320
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect 3.6 1.4 31 290 0      0      - - true 6.5  3.5  63   270 true 7.7 4.1 140 320
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect 2.5 1.1 22 270 0      0      - - true 3.4  1.9  61   260 true 7.3 3.9 120 310
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect 2.5 1.1 25 270 0      0      - - true 3.8  2.1  59   250 true 8.5 4.5 100 320
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect 2.7 1.2 22 260 0      0      - - true 3.6  2.0  65   260 unknown 6.4 3.4 130 300
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect 2.7 1.2 27 270 0      0      - - true 4.6  2.5  54   260 unknown 6.8 3.6 75 290
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect 2.5 1.1 25 270 0      0      - - true 4.1  2.3  44   260 unknown 6.1 3.3 130 300
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect 2.6 1.1 22 270 0      0      - - true 3.8  2.1  67   260 unknown 6.4 3.4 130 300
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect 2.5 1.1 24 270 0      0      - - true 3.5  1.9  59   260 true 7.6 4.1 120 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect 2.6 1.1 23 270 0      0      - - true 3.8  2.1  62   260 true 8.3 4.4 170 320
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect 2.9 1.2 23 270 .0041 0      false(unreach-call) 4.4  2.5  53   280 false(unreach-call) 7.3 3.9 150 320 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 1.4 29 290 .0041 0      false(unreach-call) 4.2  2.4  75   280 false(unreach-call) 8.4 4.4 170 320 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect 3.2 1.3 32 290 .0041 .0041 true 3.5  2.0  76   270 false(unreach-call) 7.4 3.9 110 320 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect 3.0 1.3 26 280 .0041 0      false(unreach-call) 3.5  2.0  61   270 false(unreach-call) 7.0 3.8 140 310 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect 3.3 1.4 30 300 .0082 .020  false(unreach-call) 4.0  2.2  79   280 false(unreach-call) 7.4 4.0 150 310 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 1.4 33 290 .0082 0      timeout 92    84    2200   1100 false(unreach-call) 12   6.5 140 400 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect 5.7 2.2 53 330 .012  0      false(unreach-call) 5.3  3.0  75   310 timeout 97   63   2000 4200 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect 5.1 2.3 43 350 .012  8.1    false(unreach-call) 15    12    190   510 timeout 91   57   1200 7000 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect 5.6 1.9 50 320 .0082 0      false(unreach-call) 4.0  2.2  60   280 timeout 98   57   1400 6400 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect 3.2 1.3 29 290 .0041 0      false(unreach-call) 3.7  2.1  87   270 false(unreach-call) 8.8 4.6 190 350 - -
ldv-regression/test27_false-unreach-call.c false(unreach-call) 1 wit inspect 3.5 1.4 33 300 .0041 0      false(unreach-call) 3.9  2.2  53   290 false(unreach-call) 8.7 4.6 160 320 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect 3.2 1.3 28 280 .0041 0      false(unreach-call) 3.5  2.0  28   270 false(unreach-call) 9.0 4.8 160 340 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect 3.2 1.3 27 290 .0041 0      true 3.4  1.9  46   270 false(unreach-call) 9.1 4.8 190 330 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect 3.2 1.3 28 300 .0041 0      false(unreach-call) 3.4  1.9  48   270 false(unreach-call) 8.1 4.3 160 320 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect 2.6 1.1 21 270 0      0      - - true 4.4  2.5  43   260 true 7.5 4.1 140 320
ldv-regression/test03_true-unreach-call.c true 2 wit inspect 2.6 1.2 23 270 0      0      - - true 3.4  1.9  67   260 true 8.4 4.5 170 310
ldv-regression/test04_true-unreach-call.c true 2 wit inspect 2.6 1.2 22 270 0      0      - - true 4.3  2.4  50   260 true 9.1 4.9 170 330
ldv-regression/test05_true-unreach-call.c true 2 wit inspect 2.9 1.3 26 270 0      0      - - true 4.4  2.5  53   260 true 14   7.9 230 510
ldv-regression/test07_true-unreach-call.c true 2 wit inspect 2.9 1.3 30 270 0      0      - - true 3.5  2.0  71   260 true 12   6.5 230 440
ldv-regression/test09_true-unreach-call.c true 2 wit inspect 2.9 1.3 27 270 0      0      - - true 3.4  1.9  66   260 true 11   6.0 210 400
ldv-regression/test10_true-unreach-call.c true 2 wit inspect 2.9 1.3 27 270 0      0      - - true 4.6  2.6  48   260 true 15   8.9 260 500
ldv-regression/test11_true-unreach-call.c true 2 wit inspect 3.0 1.3 27 280 0      .0082 - - true 4.3  2.4  55   260 true 9.5 5.1 170 340
ldv-regression/test13_true-unreach-call.c true 2 wit inspect 2.6 1.2 25 270 0      0      - - true 3.9  2.2  60   260 true 8.1 4.3 130 310
ldv-regression/test14_true-unreach-call.c true 2 wit inspect 3.0 1.3 25 290 0      .0041 - - true 3.9  2.2  73   270 true 8.9 4.8 170 320
ldv-regression/test15_true-unreach-call.c true 2 wit inspect 2.7 1.2 24 270 0      .0041 - - true 3.8  2.1  65   260 true 9.5 5.3 190 330
ldv-regression/test16_true-unreach-call.c true 2 wit inspect 2.7 1.2 26 270 0      0      - - true 4.6  2.5  48   260 true 10   5.5 200 350
ldv-regression/test17_true-unreach-call.c true 2 wit inspect 2.7 1.2 24 270 0      0      - - true 3.4  1.9  72   260 true 9.0 4.8 150 330
ldv-regression/test18_true-unreach-call.c true 2 wit inspect 2.9 1.3 23 280 0      8.0    - - true 4.2  2.4  44   260 true 9.8 5.3 190 320
ldv-regression/test19_true-unreach-call.c true 2 wit inspect 2.7 1.2 25 270 0      0      - - true 3.5  2.0  63   260 true 11   6.3 220 460
ldv-regression/test20_true-unreach-call.c true 2 wit inspect 2.7 1.2 23 270 0      0      - - true 4.4  2.5  43   250 true 8.3 4.4 160 320
ldv-regression/test21_true-unreach-call.c true 2 wit inspect 3.0 1.3 25 280 0      0      - - true 4.7  2.6  51   260 true 10   5.5 210 340
ldv-regression/test22_true-unreach-call.c true 2 wit inspect 6.0 2.0 56 340 0      0      - - true 6.8  4.1  110   300 true 38   25   800 840
ldv-regression/test23_true-unreach-call.c true 2 wit inspect 27   13   250 1800 0      .0041 - - true 13    9.7  170   390 true 190   160   4000 1000
ldv-regression/test24_true-unreach-call.c true 2 wit inspect 29   13   280 1800 0      0      - - true 5.7  3.3  110   300 true 14   7.8 270 370
ldv-regression/test25_true-unreach-call.c true 2 wit inspect 5.5 1.8 46 310 0      0      - - true 22    17    560   500 true 27   15   430 730
ldv-regression/test26_true-unreach-call.c true 2 wit inspect 2.7 1.2 23 270 0      0      - - true 3.8  2.1  65   260 true 9.9 5.4 200 330
ldv-regression/test27_true-unreach-call.c true 2 wit inspect 59   41   630 2400 0      0      - - true 11    7.4  130   310 true 91   72   2400 900
ldv-regression/test28_true-unreach-call.c true 2 wit inspect 2.9 1.2 26 280 0      0      - - true 4.3  2.4  51   260 true 8.1 4.5 130 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect 2.8 1.3 24 290 0      8.0    - - true 4.3  2.4  48   260 true 8.8 4.8 190 320
ldv-regression/test30_true-unreach-call.c true 2 wit inspect 2.8 1.2 23 270 0      0      - - true 4.3  2.4  53   260 true 11   6.3 220 450
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 8.6 2.7 67 480 .12   0      false(unreach-call) 13    7.3  280   530 timeout 97   79   1500 1100 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 8.5 2.6 67 490 .12   0      false(unreach-call) 14    7.5  110   550 timeout 97   79   1200 940 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect 8.9 2.8 65 490 .12   0      false(unreach-call) 14    7.5  180   540 timeout 96   81   820 1100 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.1 2.0 47 280 0      0      - - true 14    7.5  200   460 true 12   6.4 220 420
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.1 2.1 49 290 0      0      - - true 15    7.9  160   460 true 13   6.8 220 440
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.0 2.0 48 290 0      0      - - true 15    7.7  130   460 true 12   6.4 220 430
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.1 2.0 49 300 0      0      - - true 15    8.1  150   460 true 12   6.7 210 440
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.1 2.0 49 290 0      0      - - true 16    8.1  160   460 true 16   8.5 230 440
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.0 2.0 49 290 0      0      - - true 15    7.8  170   440 true 14   7.3 140 440
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.3 2.1 60 300 0      0      - - true 15    8.0  150   460 true 14   7.5 180 430
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.2 2.0 53 290 0      0      - - true 15    8.1  170   460 true 12   6.7 210 430
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.2 2.1 54 290 0      0      - - true 15    8.0  170   460 true 12   6.6 190 440
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect 6.2 2.0 55 300 0      0      - - true 16    8.4  170   460 true 12   6.4 240 410
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.0 1.5 36 300 .045  0      timeout 91    83    1100   600 true 11   5.9 200 360 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.3 1.6 36 300 .049  0      true 4.8  2.6  83   290 true 17   9.4 350 540 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.3 1.6 36 300 .049  0      true 4.8  2.6  66   280 false(unreach-call) 10   5.5 190 360 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.4 1.6 39 300 .049  0      true 5.1  2.8  110   290 true 11   6.1 190 380 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 4.2 1.5 33 300 .045  0      false(unreach-call) 5.5  3.1  87   300 true 9.7 5.2 190 350 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect 4.2 1.6 38 290 .049  0      true 4.4  2.4  44   280 error 12   6.1 170 310 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.3 1.6 34 300 .049  0      true 4.7  2.6  65   290 false(unreach-call) 9.2 4.9 170 340 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.2 1.6 40 290 .049  0      true 6.1  3.3  120   290 true 9.4 5.0 190 350 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.2 1.5 34 300 .045  0      true 4.4  2.4  61   280 true 11   6.2 200 360 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 4.1 1.5 33 300 .045  .0041 timeout 91    83    1400   620 true 11   5.8 190 370 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.6 1.7 35 310 .049  .025  true 4.9  2.7  100   280 true 8.0 4.3 150 310 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.2 1.5 40 300 .049  0      true 4.7  2.6  73   280 true 12   6.5 170 380 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.4 1.6 39 310 .049  0      true 4.5  2.5  100   280 false(unreach-call) 9.0 4.8 170 350 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.4 1.6 37 300 .049  0      true 5.7  3.1  59   280 true 11   5.7 190 370 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 4.1 1.5 33 290 .045  0      false(unreach-call) 5.4  3.0  76   290 true 10   5.4 190 350 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.1 1.5 38 300 .045  .025  false(unreach-call) 5.1  2.9  120   290 error 11   5.6 190 300 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.2 1.6 38 300 .049  0      true 5.0  2.7  99   280 false(unreach-call) 8.5 4.5 140 330 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.5 1.7 39 300 .049  0      true 5.7  3.0  130   280 true 9.4 5.0 170 350 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.1 1.5 35 300 .045  0      true 4.8  2.6  110   280 true 9.7 5.3 120 350 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.3 1.7 35 300 .045  8.1    - - false(unreach-call) 12    6.6  110   330 true 11   6.0 210 360
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.3 1.6 38 310 .049  0      - - true 5.8  3.1  60   280 true 61   54   1400 470
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 5.2 1.9 45 310 .053  0      - - true 5.0  2.7  85   280 out of memory 130   81   1300 7000
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.3 1.6 39 300 .049  0      - - true 6.8  3.7  68   290 true 12   6.2 210 380
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.3 1.6 36 300 .049  0      - - true 4.5  2.4  85   280 true 13   6.9 210 420
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.4 1.6 36 300 .049  0      - - true 6.0  3.3  61   290 error 11   5.9 180 320
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.5 1.6 34 310 .049  0      - - true 4.7  2.6  86   280 true 12   6.3 220 380
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(unreach-call) -16 wit inspect 5.7 1.9 46 310 .049  0      - - true 4.5  2.5  91   280 true 27   16   690 550
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.4 1.6 35 300 .049  .020  - - true 5.8  3.2  89   280 true 12   6.4 140 360
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.2 1.5 39 300 .045  0      - - true 5.9  3.2  59   290 true 10   5.6 150 360
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.1 1.5 35 300 .045  0      - - timeout 900    890    17000   940 true 11   5.8 160 370
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.7 1.7 39 310 .049  0      - - true 6.0  3.3  65   280 true 8.3 4.4 150 320
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.3 1.6 34 300 .049  .0041 - - true 4.8  2.6  82   290 true 14   7.9 170 370
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 5.2 1.8 47 320 .049  .029  - - true 6.3  3.4  63   290 out of memory 130   81   1900 7000
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.2 1.6 34 300 .049  0      - - true 5.1  2.8  100   290 true 10   5.6 180 360
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.0 1.5 36 300 .045  0      - - false(unreach-call) 6.5  3.6  96   290 true 9.6 5.1 170 350
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.1 1.6 33 290 .045  2.3    - - false(unreach-call) 6.5  3.5  75   300 error 13   7.1 140 310
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.4 1.6 38 300 .049  0      - - true 4.8  2.6  91   280 true 13   7.0 240 370
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(unreach-call) -16 wit inspect 6.3 2.1 53 330 .049  1.6    - - true 5.6  3.1  66   280 true 560   500   10000 1400
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.3 1.7 36 300 .049  0      - - true 5.6  3.1  110   280 true 9.8 5.2 180 350
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i false(unreach-call) -16 wit inspect 4.0 1.6 34 300 .045  8.1    - - true 4.5  2.5  82   280 true 8.6 4.6 170 340
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 7.6 2.4 63 400 .049  0      timeout 98    82    1500   2500 false(unreach-call) 8.5 4.5 140 330 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   880   7600 3300 .082  0      error (invalid witness file) .50 .31 8.8 40 error (invalid witness file) 6.1 3.2 110 300 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect 4.7 1.7 38 300 .049  0      false(unreach-call) 5.1  2.8  93   290 false(unreach-call) 8.2 4.4 170 330 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i false(unreach-call) 1 wit inspect 6.6 2.1 52 380 .053  0      true 5.2  2.8  65   280 true 9.8 5.2 170 350 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i true 2 wit inspect 7.5 2.3 54 460 0      0      - - out of memory 480    370    8800   7000 timeout 960   870   21000 1900
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect 4.7 1.7 38 330 .049  0      true 5.2  2.8  73   310 false(unreach-call) 8.7 4.7 170 320 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i true 2 wit inspect 5.3 1.9 41 300 0      .029  - - out of memory 400    310    11000   7000 timeout 960   880   17000 3600
list-ext2-properties/simple_search_value_false-unreach-call.i timeout 0 wit inspect 900   890   8300 1200 .057  0      error (invalid witness file) .52 .35 12   40 error (invalid witness file) 7.0 3.7 140 310 - -
list-ext2-properties/simple_search_value_true-unreach-call.i timeout 0 wit inspect 900   890   9600 1300 .057  .0041 - - error (invalid witness file) .53 .34 12   44 error (invalid witness file) 6.2 3.2 120 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 -160 3600 3000 33000 64000 3.8 69   173 790   600   12000 23000   173 1200 730   18000 41000   173 8100 6900 160000 100000   173 13000 11000 250000 74000  
    correct results 143 224 720 290 6300 48000 2.3 49   57 780   590   12000 23000   53 1100 710   18000 40000   69 7100 5900 140000 96000   67 11000 10000 230000 50000  
        correct true 81 162 440 190 3900 29000 0   18   32 0   0   0 0   16 0 0   0 0   69 7100 5900 140000 96000   66 11000 10000 230000 50000  
        correct false 62 62 280 100 2400 20000 2.3 31   25 780   590   12000 23000   37 1100 710   18000 40000   0 0 0 0 0   1 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 23 -384 140 52 1200 8300 1.1 20   0 9.3 5.0 180 380   1 11 5.6 220 380   21 1000 960 19000 7000   18 1100 840 18000 23000  
        incorrect true 1 -32 39 16 350 1600 0   0   0 9.3 5.0 180 380   0 11 5.6 220 380   18 0 0 0 0   18 0 0 0 0  
        incorrect false 22 -352 100 37 840 6700 1.1 20   0 0   0   0 0   1 0 0   0 0   3 1000 960 19000 7000   0 1100 840 18000 23000  
score (173 tasks, max score: 280) -160
Run set sv-comp17.ReachSafety-Heap