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