Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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:10:58 CET [[ 2017-01-15 02:01:54 CET ]] [[ 2017-01-15 02:34:25 CET ]] [[ 2017-01-15 02:04:28 CET ]] [[ 2017-01-15 03:02:21 CET ]]
Run set sv-comp17.ReachSafety-Heap
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-13_1110.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-13_1110.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 .23 .22 2.3 9.7 .11  .32   false(unreach-call) 6.3  3.4  120   300 true 8.0 4.3 130 310 - -
heap-manipulation/dll_of_dll_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 .19 2.1 9.5 .086 0      true 6.2  3.3  120   330 true 9.6 5.1 140 330 - -
heap-manipulation/merge_sort_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 .19 2.5 9.5 .086 0      false(unreach-call) 5.6  3.0  87   280 false(unreach-call) 10   5.4 140 360 - -
heap-manipulation/sll_to_dll_rev_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 .20 1.9 9.5 .074 .32   false(unreach-call) 8.4  4.5  80   350 true 9.0 4.8 170 330 - -
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .19 .18 2.2 9.4 .074 0      false(unreach-call) 5.5  3.0  110   300 true 9.0 4.9 150 340 - -
heap-manipulation/tree_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .22 .21 2.2 9.4 .074 0      false(unreach-call) 6.4  3.5  87   300 true 9.1 4.9 170 350 - -
heap-manipulation/bubble_sort_linux_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9300   770   .11  0      - - error (invalid witness file) .48 .30 11   39 error (invalid witness file) 7.8 4.1 79 300
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    13000   440   .074 0      - - error (invalid witness file) .47 .30 9.2 40 error (invalid witness file) 5.2 2.8 100 280
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    910    5000   11000   .086 0      - - error (invalid witness file) .55 .36 7.7 40 error (invalid witness file) 5.4 2.9 86 290
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    8400   970   .086 12      - - error (invalid witness file) .59 .38 11   42 error (invalid witness file) 7.0 3.8 80 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .20 .19 1.9 9.4 .074 0      - - out of memory 630    570    7800   7000 timeout 960   840   19000 3200
heap-manipulation/tree_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    9600   1300   .074 0      - - error (invalid witness file) .52 .33 9.9 39 error (invalid witness file) 5.3 2.8 110 290
list-properties/alternating_list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 .18 1.8 9.5 .074 0      false(unreach-call) 5.6  3.0  110   290 false(unreach-call) 9.2 5.0 110 350 - -
list-properties/list_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 .17 2.2 9.3 .074 0      false(unreach-call) 5.8  3.2  110   300 false(unreach-call) 18   9.8 300 510 - -
list-properties/list_flag_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 .17 2.1 9.4 .074 0      true 5.1  2.8  77   280 true 8.3 4.4 100 320 - -
list-properties/list_search_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 .17 1.7 9.2 .074 0      false(unreach-call) 5.1  2.8  99   290 true 7.6 4.0 150 320 - -
list-properties/simple_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 .18 1.7 9.3 .074 0      false(unreach-call) 5.3  2.9  110   280 false(unreach-call) 8.2 4.4 160 350 - -
list-properties/splice_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 .17 1.9 9.4 .074 0      false(unreach-call) 5.5  3.0  77   300 false(unreach-call) 11   5.9 130 360 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    8800   4000   .074 .0041 - - error (invalid witness file) .65 .41 7.2 40 error (invalid witness file) 6.1 3.3 120 290
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    12000   820   .074 0      - - error (invalid witness file) .50 .32 12   41 error (invalid witness file) 5.4 2.9 42 290
list-properties/list_search_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .30 .40 1.9 17   .11  7.8    - - true 31    17    230   650 true 46   31   870 910
list-properties/list_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    9500   2400   .074 0      - - error (invalid witness file) .49 .31 11   39 error (invalid witness file) 6.1 3.3 110 300
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    9000   3400   .074 0      - - error (invalid witness file) .55 .35 9.3 42 error (invalid witness file) 5.7 3.0 110 300
list-properties/simple_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    8300   3300   .074 0      - - error (invalid witness file) .57 .36 11   44 error (invalid witness file) 7.5 3.9 83 300
list-properties/splice_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    8700   4200   .074 0      - - error (invalid witness file) .53 .33 8.7 40 error (invalid witness file) 6.3 3.3 99 300
ldv-regression/1_3.c_false-unreach-call.i false(unreach-call) 1 wit inspect .15 .14 1.7 9.3 .012 0      false(unreach-call) 5.2  2.9  55   280 true 7.9 4.2 110 320 - -
ldv-regression/alt_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .15 .15 1.7 9.3 .098 0      false(unreach-call) 6.0  3.3  130   290 true 7.6 4.0 150 320 - -
ldv-regression/callfpointer.c_false-unreach-call.i false(unreach-call) 1 wit inspect .13 .13 1.7 9.3 .012 0      false(unreach-call) 3.4  1.9  64   270 false(unreach-call) 7.5 3.9 120 320 - -
ldv-regression/fo_test.c_false-unreach-call.i false(unreach-call) 1 wit inspect .19 .19 1.9 9.4 .090 0      false(unreach-call) 5.9  3.2  81   290 true 8.7 4.6 100 320 - -
ldv-regression/mutex_lock_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .15 .15 1.4 9.4 .012 0      false(unreach-call) 4.7  2.7  49   280 true 7.4 3.9 140 320 - -
ldv-regression/mutex_lock_struct.c_false-unreach-call.i false(unreach-call) 1 wit inspect .13 .13 1.5 9.3 .012 0      false(unreach-call) 3.7  2.1  77   270 true 6.9 3.7 130 320 - -
ldv-regression/recursive_list.c_false-unreach-call.i false(unreach-call) 1 wit inspect .18 .17 1.6 9.5 .012 0      false(unreach-call) 3.9  2.2  83   280 true 8.8 4.6 100 320 - -
ldv-regression/rule57_ebda_blast.c_false-unreach-call.i false(unreach-call) 1 wit inspect .20 .19 1.9 9.3 .012 0      true 4.2  2.3  75   270 true 9.1 4.8 89 320 - -
ldv-regression/rule60_list2.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .20 .19 1.6 9.4 .061 0      false(unreach-call) 5.4  2.9  110   300 true 7.0 3.8 100 320 - -
ldv-regression/stateful_check_false-unreach-call.i false(unreach-call) 1 wit inspect .23 .23 2.4 9.6 .012 0      true 4.1  2.3  88   270 true 9.6 5.2 100 310 - -
ldv-regression/test_while_int.c_false-unreach-call.i false(unreach-call) 1 wit inspect .16 .16 1.6 9.4 .012 0      false(unreach-call) 3.7  2.1  76   280 true 8.5 4.6 89 310 - -
ldv-regression/test_while_int.c_false-unreach-call_1.i false(unreach-call) 1 wit inspect .13 .13 1.4 9.1 .012 0      false(unreach-call) 4.6  2.6  46   280 true 9.0 4.7 100 320 - -
ldv-regression/alias_of_return.c_true-unreach-call.i true 2 wit inspect .13 .13 1.8 9.4 .012 0      - - true 4.3  2.4  54   260 true 9.4 5.0 140 340
ldv-regression/alias_of_return.c_true-unreach-call_1.i true 2 wit inspect .15 .14 1.3 9.2 .012 0      - - true 3.5  2.0  60   260 true 7.8 4.2 150 320
ldv-regression/alias_of_return_2.c_true-unreach-call.i true 2 wit inspect .16 .16 1.6 9.3 .012 0      - - true 4.4  2.5  47   260 true 8.7 4.7 110 310
ldv-regression/alias_of_return_2.c_true-unreach-call_1.i true 2 wit inspect .17 .16 1.5 9.5 .012 0      - - true 3.4  1.9  82   260 true 7.8 4.2 140 320
ldv-regression/ex3_forlist.c_true-unreach-call.i true 2 wit inspect .18 .18 1.7 9.4 .012 0      - - true 19    11    330   540 true 31   18   430 730
ldv-regression/just_assert.c_true-unreach-call.i true 2 wit inspect .15 .15 1.6 9.3 .012 0      - - true 3.9  2.2  44   250 true 8.2 4.3 130 320
ldv-regression/mutex_lock_int.c_true-unreach-call_1.i true 2 wit inspect .15 .15 1.4 9.4 .012 0      - - true 3.4  1.9  56   260 true 11   5.6 140 340
ldv-regression/mutex_lock_struct.c_true-unreach-call_1.i true 2 wit inspect .15 .15 1.2 9.5 .012 0      - - true 3.8  2.1  55   260 true 9.0 4.8 140 320
ldv-regression/nested_structure.c_true-unreach-call.i true 2 wit inspect .16 .16 1.4 9.3 .012 0      - - true 3.4  1.9  65   260 true 12   6.3 120 350
ldv-regression/nested_structure_noptr.c_true-unreach-call.i true 2 wit inspect .13 .13 1.4 9.5 .012 0      - - true 3.3  1.9  62   250 true 6.8 3.7 96 310
ldv-regression/nested_structure_noptr_true-unreach-call.i true 2 wit inspect .25 .37 1.6 17   .012 8.2    - - true 3.4  1.9  57   260 true 7.4 4.0 140 320
ldv-regression/nested_structure_ptr.c_true-unreach-call.i true 2 wit inspect .16 .16 1.4 9.3 .012 0      - - true 3.8  2.1  32   260 true 13   6.9 260 440
ldv-regression/nested_structure_ptr_true-unreach-call.i true 2 wit inspect .13 .13 1.5 9.2 .012 0      - - true 3.4  1.9  53   260 true 14   7.6 210 470
ldv-regression/nested_structure_true-unreach-call.i true 2 wit inspect .13 .13 1.7 9.3 .012 0      - - true 4.0  2.2  56   270 true 9.9 5.4 140 350
ldv-regression/oomInt.c_true-unreach-call.i true 2 wit inspect .13 .13 1.6 9.3 .012 0      - - true 4.1  2.3  39   260 true 8.8 4.8 100 320
ldv-regression/oomInt.c_true-unreach-call_1.i true 2 wit inspect .13 .13 1.5 9.2 .012 0      - - true 3.6  2.0  68   250 true 9.0 4.8 100 320
ldv-regression/rule57_ebda_blast.c_true-unreach-call_1.i true 2 wit inspect .17 .17 2.3 9.4 .012 0      - - true 4.1  2.3  79   260 true 10   5.5 130 340
ldv-regression/rule60_list.c_true-unreach-call.i true 2 wit inspect .16 .16 1.9 9.3 .049 0      - - true 4.6  2.5  72   270 true 11   5.8 150 350
ldv-regression/rule60_list2.c_true-unreach-call.i true 2 wit inspect .17 .16 2.1 9.5 .061 0      - - true 4.7  2.5  57   270 true 28   16   300 710
ldv-regression/sizeofparameters_test.c_true-unreach-call.i true 2 wit inspect .16 .16 1.6 9.3 .049 0      - - true 4.1  2.3  65   260 true 8.5 4.5 140 320
ldv-regression/structure_assignment.c_true-unreach-call.i true 2 wit inspect .13 .13 1.4 9.4 .012 0      - - true 4.5  2.5  45   260 true 7.3 3.8 140 320
ldv-regression/test_address.c_true-unreach-call.i true 2 wit inspect .15 .15 1.7 9.3 .049 0      - - true 4.7  2.6  72   270 true 8.5 4.6 140 320
ldv-regression/test_cut_trace.c_true-unreach-call.i true 2 wit inspect .13 .13 1.6 9.3 .012 0      - - true 3.7  2.1  40   260 true 8.3 4.4 120 310
ldv-regression/test_malloc-1_true-unreach-call.i true 2 wit inspect .15 .14 1.7 9.3 .061 0      - - true 5.7  3.1  62   260 true 7.9 4.2 120 320
ldv-regression/test_malloc-2_true-unreach-call.i true 2 wit inspect .16 .15 1.4 9.4 .061 0      - - true 4.6  2.5  88   260 true 8.4 4.5 120 330
ldv-regression/test_overflow.c_true-unreach-call.i true 2 wit inspect .14 .14 1.7 9.4 .098 0      - - true 5.8  3.2  81   280 true 10   5.5 110 330
ldv-regression/test_union.c_true-unreach-call.i true 2 wit inspect .15 .14 1.7 9.3 .012 0      - - true 3.3  1.9  47   260 true 8.6 4.6 120 320
ldv-regression/test_union.c_true-unreach-call_1.i true 2 wit inspect .16 .15 1.6 9.4 .012 0      - - true 3.7  2.1  61   250 true 8.1 4.3 160 330
ldv-regression/test_union_cast-1_true-unreach-call.i true 2 wit inspect .15 .15 1.4 9.5 .012 0      - - true 3.9  2.2  59   260 unknown 6.6 3.5 130 310
ldv-regression/test_union_cast-2_true-unreach-call.i true 2 wit inspect .14 .13 1.7 9.4 .012 0      - - true 4.0  2.3  51   260 unknown 5.8 3.1 90 300
ldv-regression/test_union_cast.c_true-unreach-call.i true 2 wit inspect .15 .15 1.4 9.2 .012 0      - - true 3.4  1.9  69   260 unknown 6.3 3.4 86 300
ldv-regression/test_union_cast.c_true-unreach-call_1.i true 2 wit inspect .13 .13 1.4 9.4 .012 0      - - true 3.9  2.2  62   260 unknown 7.0 3.7 91 300
ldv-regression/volatile_alias.c_true-unreach-call.i true 2 wit inspect .13 .13 1.7 9.5 .012 0      - - true 3.6  2.0  52   260 true 8.4 4.5 140 320
ldv-regression/volatile_alias.c_true-unreach-call_1.i true 2 wit inspect .15 .14 1.5 9.3 .012 0      - - true 3.4  1.9  51   260 true 7.9 4.2 160 320
ldv-regression/test02_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 1.4 9.3 .012 0      false(unreach-call) 4.7  2.6  42   270 true 8.0 4.3 78 310 - -
ldv-regression/test06_false-unreach-call.c false(unreach-call) 1 wit inspect .16 .16 1.5 9.3 .012 0      false(unreach-call) 4.3  2.4  72   290 true 8.3 4.4 120 320 - -
ldv-regression/test08_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 1.7 9.5 .012 0      false(unreach-call) 3.7  2.1  73   270 true 6.4 3.5 140 310 - -
ldv-regression/test12_false-unreach-call.c false(unreach-call) 1 wit inspect .15 .15 1.2 9.5 .012 0      false(unreach-call) 3.6  2.0  55   280 true 8.8 4.7 93 320 - -
ldv-regression/test21_false-unreach-call.c false(unreach-call) 1 wit inspect .18 .18 1.8 10   .012 0      false(unreach-call) 4.0  2.3  79   270 true 7.2 3.8 110 320 - -
ldv-regression/test22_false-unreach-call.c false(unreach-call) 1 wit inspect .21 .21 2.4 11   .012 0      true 3.8  2.1  79   270 true 7.5 4.1 140 330 - -
ldv-regression/test23_false-unreach-call.c false(unreach-call) 1 wit inspect .25 .25 2.8 12   .012 0      true 4.5  2.5  89   270 true 8.9 4.8 110 320 - -
ldv-regression/test24_false-unreach-call.c false(unreach-call) 1 wit inspect .19 .19 1.9 12   .012 0      false(unreach-call) 16    13    350   490 true 7.9 4.2 160 310 - -
ldv-regression/test25_false-unreach-call.c false(unreach-call) 1 wit inspect .14 .14 2.2 10   .012 0      true 3.6  2.0  61   270 true 8.3 4.5 110 320 - -
ldv-regression/test26_false-unreach-call.c false(unreach-call) 1 wit inspect .13 .13 1.7 9.3 .012 0      false(unreach-call) 3.7  2.1  66   280 true 9.0 4.7 110 310 - -
ldv-regression/test27_false-unreach-call.c error 0 wit inspect .26 .25 2.9 9.9 .012 0      error (invalid witness file) .63 .41 8.3 40 error (invalid witness file) 6.1 3.2 94 310 - -
ldv-regression/test28_false-unreach-call.c false(unreach-call) 1 wit inspect .16 .16 1.4 9.4 .012 0      false(unreach-call) 4.0  2.3  67   270 true 8.0 4.3 110 320 - -
ldv-regression/test29_false-unreach-call.c false(unreach-call) 1 wit inspect .14 .14 1.6 11   .012 0      false(unreach-call) 3.7  2.1  69   280 true 7.7 4.1 110 320 - -
ldv-regression/test30_false-unreach-call.c false(unreach-call) 1 wit inspect .15 .15 1.2 9.2 .012 0      false(unreach-call) 4.4  2.4  61   280 true 7.2 3.8 130 310 - -
ldv-regression/test01_true-unreach-call.c true 2 wit inspect .13 .13 1.4 9.3 .012 0      - - true 3.2  1.8  60   250 true 7.8 4.2 140 310
ldv-regression/test03_true-unreach-call.c true 2 wit inspect .13 .13 1.6 9.3 .012 0      - - true 3.7  2.1  67   260 true 8.3 4.5 160 310
ldv-regression/test04_true-unreach-call.c true 2 wit inspect .13 .13 1.3 9.2 .012 .32   - - true 3.7  2.1  52   260 true 12   6.2 110 330
ldv-regression/test05_true-unreach-call.c true 2 wit inspect .15 .15 1.8 9.2 .012 0      - - true 4.7  2.6  52   260 true 15   8.8 190 530
ldv-regression/test07_true-unreach-call.c true 2 wit inspect .15 .15 1.4 9.3 .012 0      - - true 3.5  1.9  54   260 true 10   5.8 160 430
ldv-regression/test09_true-unreach-call.c true 2 wit inspect .13 .13 1.6 9.4 .012 0      - - true 4.0  2.2  62   260 true 10   5.9 180 420
ldv-regression/test10_true-unreach-call.c true 2 wit inspect .16 .16 1.3 9.4 .012 .32   - - true 3.7  2.1  61   260 true 19   11   310 510
ldv-regression/test11_true-unreach-call.c true 2 wit inspect .18 .17 1.5 9.2 .012 0      - - true 4.1  2.3  61   260 true 9.5 5.2 170 320
ldv-regression/test13_true-unreach-call.c true 2 wit inspect .13 .13 1.6 9.3 .012 .32   - - true 3.8  2.2  46   250 true 8.4 4.5 89 310
ldv-regression/test14_true-unreach-call.c true 2 wit inspect .15 .15 1.8 9.3 .012 0      - - true 3.5  2.0  81   260 true 11   5.7 130 330
ldv-regression/test15_true-unreach-call.c true 2 wit inspect .14 .14 1.9 9.4 .012 0      - - true 3.6  2.0  51   260 true 12   6.5 140 350
ldv-regression/test16_true-unreach-call.c true 2 wit inspect .13 .13 1.4 9.4 .012 0      - - true 3.3  1.9  46   260 true 9.7 5.3 200 360
ldv-regression/test17_true-unreach-call.c true 2 wit inspect .15 .15 1.3 9.4 .012 0      - - true 4.0  2.3  49   260 true 7.5 4.1 140 320
ldv-regression/test18_true-unreach-call.c true 2 wit inspect .13 .13 1.5 9.4 .012 0      - - true 3.6  2.0  78   260 true 9.3 5.1 190 320
ldv-regression/test19_true-unreach-call.c true 2 wit inspect .17 .16 1.5 9.4 .012 0      - - true 3.7  2.0  78   250 true 11   6.1 230 450
ldv-regression/test20_true-unreach-call.c true 2 wit inspect .13 .13 1.5 9.4 .012 0      - - true 3.5  2.0  52   260 true 7.9 4.2 120 320
ldv-regression/test21_true-unreach-call.c true 2 wit inspect .18 .17 1.7 9.3 .012 0      - - true 4.5  2.5  42   260 true 9.9 5.4 180 330
ldv-regression/test22_true-unreach-call.c true 2 wit inspect .16 .15 1.8 9.3 .012 0      - - true 5.9  3.5  110   300 true 46   30   570 880
ldv-regression/test23_true-unreach-call.c true 2 wit inspect .18 .18 1.6 9.3 .012 0      - - true 10    7.9  240   390 true 220   180   3100 1000
ldv-regression/test24_true-unreach-call.c true 2 wit inspect .17 .17 1.5 9.4 .012 0      - - true 5.7  3.4  100   300 true 19   10   190 380
ldv-regression/test25_true-unreach-call.c true 2 wit inspect .14 .14 1.7 9.2 .012 .32   - - true 29    23    460   510 true 30   16   600 720
ldv-regression/test26_true-unreach-call.c true 2 wit inspect .15 .15 1.8 9.4 .012 0      - - true 3.8  2.1  70   260 true 10   5.6 180 340
ldv-regression/test27_true-unreach-call.c true 2 wit inspect .17 .17 1.6 9.5 .012 0      - - true 8.3  5.8  170   320 true 110   87   2100 900
ldv-regression/test28_true-unreach-call.c true 2 wit inspect .15 .15 1.5 9.4 .012 0      - - true 4.6  2.6  49   270 true 8.9 4.8 160 320
ldv-regression/test29_true-unreach-call.c true 2 wit inspect .17 .17 1.6 9.4 .012 0      - - true 3.4  1.9  55   260 true 8.5 4.6 160 320
ldv-regression/test30_true-unreach-call.c true 2 wit inspect .14 .14 1.7 9.2 .012 0      - - true 4.2  2.4  50   260 true 13   7.1 200 480
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .58 .57 6.8 18   .27  0      false(unreach-call) 16    9.0  230   540 true 15   7.9 130 440 - -
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .53 .52 6.5 16   .27  0      false(unreach-call) 14    7.5  230   520 true 15   8.1 160 430 - -
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(unreach-call) 1 wit inspect .56 .55 7.9 18   .27  0      false(unreach-call) 14    7.7  260   530 true 12   6.5 240 430 - -
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .48 .47 5.9 12   .27  0      - - true 12    6.2  160   430 true 12   6.5 210 420
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .50 .50 5.5 12   .27  0      - - true 11    5.6  230   440 true 14   7.7 170 430
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .48 .47 5.8 12   .27  0      - - true 11    5.9  210   430 true 12   6.4 240 420
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .48 .47 5.9 12   .27  0      - - true 10    5.5  190   440 true 12   6.4 240 420
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .51 .50 6.5 12   .27  0      - - true 11    5.7  180   430 true 12   6.7 240 420
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .50 .49 6.2 12   .27  0      - - true 12    6.1  150   430 true 14   7.7 150 420
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .49 .49 6.0 12   .27  0      - - true 11    5.5  220   430 true 13   7.1 190 430
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .51 .50 6.2 12   .27  0      - - true 13    6.6  110   420 true 16   8.4 180 430
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .52 .51 5.1 13   .27  0      - - true 12    6.1  190   440 true 16   8.4 150 440
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i true 2 wit inspect .55 .67 6.3 20   .27  7.9    - - true 10    5.6  170   440 true 15   8.1 160 420
forester-heap/dll-01_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 .20 1.9 9.6 .074 0      timeout 92    83    1500   500 true 9.6 5.1 130 330 - -
forester-heap/dll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 .19 1.9 9.5 .074 0      false(unreach-call) 5.3  2.9  96   290 false(unreach-call) 16   8.6 170 380 - -
forester-heap/dll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .17 .17 2.4 9.4 .074 0      false(unreach-call) 5.3  2.9  110   290 false(unreach-call) 9.1 4.9 180 350 - -
forester-heap/dll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 .18 2.1 9.6 .074 0      false(unreach-call) 5.8  3.1  120   290 true 9.0 4.8 140 340 - -
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .17 .16 2.0 9.4 .074 0      false(unreach-call) 4.8  2.7  94   280 true 11   5.6 100 320 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(unreach-call) 1 wit inspect .20 .19 2.1 9.4 .074 0      false(unreach-call) 6.1  3.4  110   310 error 14   7.3 130 300 - -
forester-heap/dll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .16 .16 2.2 9.4 .074 .32   false(unreach-call) 6.1  3.3  87   290 true 7.5 4.0 130 320 - -
forester-heap/dll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 .20 2.0 10   .074 0      false(unreach-call) 5.6  3.1  100   290 true 9.7 5.2 120 350 - -
forester-heap/dll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 .18 1.9 9.3 .074 0      false(unreach-call) 5.2  2.8  93   290 true 9.9 5.3 110 330 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i timeout (timeout) 0 wit inspect 900    900    6600   3500   .074 0      error (invalid witness file) .48 .30 8.8 40 error (invalid witness file) 5.8 3.1 99 290 - -
forester-heap/sll-buckets_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .20 .20 1.9 9.4 .074 .45   false(unreach-call) 6.1  3.3  96   300 true 8.5 4.5 130 320 - -
forester-heap/sll-circular_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24 .36 2.2 18   .074 8.9    false(unreach-call) 5.5  3.0  90   290 false(unreach-call) 15   7.9 220 390 - -
forester-heap/sll-optional_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 .19 2.3 9.4 .074 0      false(unreach-call) 5.4  2.9  110   300 false(unreach-call) 9.5 5.0 130 370 - -
forester-heap/sll-queue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .21 .21 2.0 9.5 .074 0      false(unreach-call) 6.1  3.3  120   300 true 8.9 4.8 160 350 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .18 .17 1.7 9.4 .074 0      false(unreach-call) 5.2  2.8  94   290 true 7.3 3.9 81 310 - -
forester-heap/sll-rb-sentinel_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .18 .18 1.9 9.3 .074 0      true 5.0  2.7  110   280 error 14   7.2 130 310 - -
forester-heap/sll-simple-white-blue_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .24 .35 1.9 17   .074 8.1    false(unreach-call) 6.1  3.3  82   300 true 10   5.3 73 320 - -
forester-heap/sll-sorted_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 .18 2.1 10   .074 0      false(unreach-call) 7.7  4.3  95   300 true 11   6.0 120 350 - -
forester-heap/sll-token_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .16 .16 2.2 9.4 .074 0      false(unreach-call) 5.2  2.9  100   280 false(unreach-call) 8.7 4.6 180 350 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    5100   7900   .074 0      - - error (invalid witness file) .49 .32 9.3 40 error (invalid witness file) 6.2 3.3 110 310
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9700   8800   .074 0      - - error (invalid witness file) .57 .36 7.1 39 error (invalid witness file) 6.8 3.6 82 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6300   5400   .074 .0041 - - error (invalid witness file) .48 .31 9.7 39 error (invalid witness file) 6.1 3.3 69 290
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   260   .074 0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 7.6 4.1 79 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6900   7600   .074 0      - - error (invalid witness file) .53 .33 12   40 error (invalid witness file) 5.5 3.0 89 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7300   7700   .074 .0041 - - error (invalid witness file) .60 .39 7.6 40 error (invalid witness file) 7.3 3.9 75 290
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9900   9800   .074 0      - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 6.5 3.5 110 300
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    10000   10000   .074 0      - - error (invalid witness file) .49 .32 8.9 40 error (invalid witness file) 6.3 3.3 110 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   690   .074 0      - - error (invalid witness file) .47 .31 7.1 40 error (invalid witness file) 5.6 3.0 120 290
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   880   .074 0      - - error (invalid witness file) .56 .36 7.8 40 error (invalid witness file) 5.8 3.1 110 290
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6300   8600   .074 0      - - error (invalid witness file) .56 .36 7.0 40 error (invalid witness file) 5.9 3.1 75 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6300   5900   .074 0      - - error (invalid witness file) .55 .36 9.7 41 error (invalid witness file) 6.8 3.6 110 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   9300   .074 0      - - error (invalid witness file) .50 .32 13   39 error (invalid witness file) 7.4 3.9 87 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6700   6000   .074 0      - - error (invalid witness file) .51 .34 11   40 error (invalid witness file) 6.5 3.4 88 310
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   270   .074 0      - - error (invalid witness file) .55 .35 12   42 error (invalid witness file) 6.9 3.7 69 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6200   7400   .074 0      - - error (invalid witness file) .50 .32 8.5 39 error (invalid witness file) 6.5 3.4 110 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6500   7800   .074 0      - - error (invalid witness file) .50 .32 11   40 error (invalid witness file) 7.7 4.1 78 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7100   9200   .074 0      - - error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.2 3.3 91 290
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    11000   11000   .074 0      - - error (invalid witness file) .57 .36 9.2 40 error (invalid witness file) 6.7 3.6 87 290
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    13000   670   .074 0      - - error (invalid witness file) .53 .33 7.9 40 error (invalid witness file) 6.0 3.2 120 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    8300   970   .074 0      - - error (invalid witness file) .66 .42 8.2 41 error (invalid witness file) 6.0 3.2 130 290
list-ext-properties/list-ext_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect .20 .19 2.1 9.3 .074 0      false(unreach-call) 5.0  2.7  100   280 true 8.5 4.5 170 320 - -
list-ext-properties/list-ext_flag_false-unreach-call_false-valid-deref.i false(unreach-call) 1 wit inspect 2.0  2.0  25   33   .074 0      timeout 96    75    1700   2400 true 9.4 5.0 100 320 - -
list-ext-properties/simple-ext_false-unreach-call_false-valid-memcleanup.i false(unreach-call) 1 wit inspect .19 .19 1.9 9.3 .074 0      false(unreach-call) 6.3  3.4  82   290 true 10   5.3 110 330 - -
list-ext2-properties/list_and_tree_cnstr_false-unreach-call.i false(unreach-call) 1 wit inspect .26 .25 2.8 11   .074 0      false(unreach-call) 6.1  3.3  100   300 true 10   5.3 110 320 - -
list-ext2-properties/list_and_tree_cnstr_true-unreach-call.i error 0 wit inspect 120    120    1400   100   .074 0      - - error (invalid witness file) .54 .35 10   40 error (invalid witness file) 6.9 3.7 78 290
list-ext2-properties/simple_and_skiplist_2lvl_false-unreach-call.i false(unreach-call) 1 wit inspect .22 .21 2.0 9.3 .074 0      false(unreach-call) 5.5  3.0  120   290 false(unreach-call) 9.8 5.3 130 350 - -
list-ext2-properties/simple_and_skiplist_2lvl_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    12000   150   .074 0      - - error (invalid witness file) .62 .39 7.7 39 error (invalid witness file) 7.1 3.8 75 300
list-ext2-properties/simple_search_value_false-unreach-call.i false(unreach-call) 1 wit inspect .20 .19 2.0 9.3 .074 0      false(unreach-call) 11    6.8  110   420 timeout 97   75   1700 1300 - -
list-ext2-properties/simple_search_value_true-unreach-call.i timeout (timeout) 0 wit inspect 900    900    9000   2000   .074 0      - - error (invalid witness file) .53 .35 8.8 40 error (invalid witness file) 7.7 4.0 78 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 208 32000 32000 310000 170000 11   55 173 550 360 9400 22000   173 700 400 10000 23000   173 1100 830 15000 30000   173 2300 1700 41000 42000  
    correct results 136 208 29 29 320 1400 8.0 43 62 550 360 9400 22000   61 690 390 10000 22000   71 1100 820 14000 28000   67 2100 1600 37000 32000  
        correct true 72 144 15 15 160 730 4.0 25 8 0 0 0 0   49 0 0 0 0   71 1100 820 14000 28000   67 2100 1600 37000 32000  
        correct false 64 64 15 15 160 680 4.1 18 54 550 360 9400 22000   12 690 390 10000 22000   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (173 tasks, max score: 280) 208
Run set sv-comp17.ReachSafety-Heap