Tool 2LS 0.5.0
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host apollon*
OS Linux 4.4.0-59-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB
Date of execution 2017-01-11 09:48:02 CET [[ 2017-01-14 21:34:09 CET ]] [[ 2017-01-14 21:49:16 CET ]] [[ 2017-01-14 21:34:25 CET ]] [[ 2017-01-14 21:52:20 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_0948.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_0948.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_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .47 .46 5.0 46 .0082 0    - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 8.1 4.2 86 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i error (5) 0 wit inspect .37 .37 3.1 27 .0082 0    - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 7.4 3.8 150 310
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 25    25    260   1000 .0082 0    - - timeout 910    820    25000   6400 timeout 960   880   20000 1800
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i false(valid-deref) -16 wit inspect .31 .31 3.3 31 .0082 0    - - error 5.2  2.8  110   290 true 9.2 4.9 170 320
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .57 .60 4.9 46 .0082 13    error 5.6  3.0  90   310 true 13   6.7 140 350 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .29 .28 2.4 30 .0082 0    error 4.3  2.4  92   260 false(valid-deref) 11   5.7 130 320 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i error (5) 0 wit inspect .20 .20 1.4 26 .0082 0    error (invalid witness file) .58 .36 7.1 40 error (invalid witness file) 6.1 3.3 120 300 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .51 .50 5.1 37 .0082 .16 error 4.9  2.7  73   260 error 12   6.6 150 290 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .45 .45 4.2 31 .0082 0    error (invalid witness file) .55 .35 10   39 error (invalid witness file) 7.3 3.8 72 290 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .41 .40 3.9 30 .0082 0    error (invalid witness file) .51 .33 9.2 39 error (invalid witness file) 6.3 3.3 95 300 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .41 .41 4.1 30 .0082 0    - - error (invalid witness file) .55 .35 12   39 error (invalid witness file) 6.1 3.2 120 290
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .20 1.8 26 .0082 .16 error 4.7  2.5  70   270 true 9.9 5.2 120 330 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i true -32 wit inspect .38 .38 3.6 32 .0082 0    error 4.5  2.5  81   260 timeout 97   63   1100 970 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 1.9 27 .0082 0    error 4.1  2.3  62   260 true 9.4 5.0 110 320 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .29 .29 2.8 27 .0082 0    error 4.6  2.5  90   270 true 8.6 4.6 130 320 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i error (134) 0 wit inspect .23 .23 2.9 28 .0082 .10 error (invalid witness file) .50 .31 9.2 40 error (invalid witness file) 6.8 3.7 75 290 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .21 .21 1.9 27 .0082 0    error 4.2  2.3  66   260 true 12   6.2 120 350 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i false(valid-deref) -16 wit inspect 65    65    550   1000 .0082 0    - - error 8.2  4.3  120   310 true 20   11   240 470
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(valid-deref) -16 wit inspect 67    67    450   960 .0082 0    - - error 8.7  4.5  110   310 true 19   10   200 480
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 63    63    480   980 .0082 .10 - - error 8.1  4.3  120   310 true 17   9.2 190 470
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 62    62    490   950 .0082 0    error 10    5.5  180   350 true 17   9.4 220 470 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 63    63    500   960 .0082 12    error 9.6  5.0  140   330 true 18   9.7 250 490 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 62    62    530   950 .0082 .10 error 8.9  4.7  180   330 true 15   7.9 280 480 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 62    62    530   950 .0082 0    error 8.7  4.6  160   330 true 16   8.7 280 480 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 62    62    450   950 .0082 0    error 9.7  5.1  130   340 true 15   8.2 300 490 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 61    61    510   950 .0082 0    error 9.1  4.8  130   330 true 18   9.9 190 470 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 61    61    490   940 .0082 .27 error 9.3  4.9  160   320 true 15   8.5 230 480 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 63    63    450   950 .0082 0    error 11    5.7  120   340 true 15   8.2 280 470 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 62    62    420   950 .0082 0    error 9.0  4.7  130   330 true 17   9.0 180 480 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 68    68    500   950 .0082 0    error 8.6  4.5  140   310 true 20   11   190 480 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect 1.2  1.2  12   68 .0082 0    - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 6.6 3.5 80 290
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    5900   1800 .0082 .13 - - error (invalid witness file) .52 .33 13   40 error (invalid witness file) 8.1 4.3 76 290
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .58 .60 5.4 47 .0082 7.6  - - error (invalid witness file) .51 .33 8.1 42 error (invalid witness file) 6.6 3.5 99 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9200   8700 .0082 12    - - error (invalid witness file) .64 .41 9.1 40 error (invalid witness file) 5.8 3.1 110 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .70 .70 7.6 48 .0082 0    - - error (invalid witness file) .52 .33 12   39 error (invalid witness file) 8.4 4.4 98 320
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    6100   7800 .0082 .10 - - error (invalid witness file) .58 .37 14   44 error (invalid witness file) 6.5 3.4 94 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9300   8900 .0082 0    - - error (invalid witness file) .53 .35 12   41 error (invalid witness file) 6.4 3.4 120 310
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .79 .79 8.5 40 .0082 0    - - error (invalid witness file) .55 .36 9.6 39 error (invalid witness file) 6.7 3.5 84 290
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .36 .36 3.7 30 .0082 0    - - error (invalid witness file) .50 .31 9.1 39 error (invalid witness file) 6.0 3.1 110 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect 1.2  1.2  14   66 .0082 .10 - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 7.1 3.7 70 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .63 .62 6.4 49 .0082 0    - - error (invalid witness file) .49 .31 12   39 error (invalid witness file) 7.6 4.0 76 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    5900   1800 .0082 0    - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.0 3.2 120 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .56 .56 5.9 38 .0082 0    - - error (invalid witness file) .49 .31 8.2 41 error (invalid witness file) 6.2 3.3 86 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    7100   9000 .0082 .10 - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 6.9 3.6 81 290
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .41 .41 5.0 33 .0082 0    - - error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.9 3.6 86 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    7700   7600 .0082 .10 - - error (invalid witness file) .51 .32 14   41 error (invalid witness file) 7.0 3.6 110 310
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    8700   8700 .0082 .10 - - error (invalid witness file) .55 .35 7.9 39 error (invalid witness file) 5.7 3.1 100 290
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .62 .62 7.3 40 .0082 0    - - error (invalid witness file) .57 .36 12   44 error (invalid witness file) 7.6 4.0 98 310
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i error (134) 0 wit inspect .33 .33 3.3 30 .0082 0    - - error (invalid witness file) .65 .41 7.0 40 error (invalid witness file) 7.1 3.8 79 290
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i error (134) 0 wit inspect .53 .53 5.0 37 .0082 0    error (invalid witness file) .53 .35 9.8 39 error (invalid witness file) 7.3 3.8 61 300 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .28 .28 3.1 28 .0082 0    error 4.4  2.4  63   260 false(valid-deref) 16   8.2 280 380 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i error (134) 0 wit inspect .50 .50 5.0 34 .0082 0    error (invalid witness file) .49 .31 9.5 39 error (invalid witness file) 5.9 3.1 110 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 52 -246 8100    8100    67000   69000 .43   46   52 140   74   2200 5900   52 390 220 5200 10000   52 950 840 26000 8600   52 1200 1000 23000 10000  
    correct results 9 10 27    27    290   1300 .074  13   0 37   20   610 2100   7 91 48 1200 2700   0 910 820 25000 6400   0 960 880 20000 1800  
        correct true 1 2 25    25    260   1000 .0082 0   0 0   0   0 0   5 0 0 0 0   0 910 820 25000 6400   0 960 880 20000 1800  
        correct false 8 8 2.6  2.6  24   250 .066  13   0 37   20   610 2100   2 91 48 1200 2700   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 15 -256 820    820    6300   12000 .12   13   0 99   52   1500 3600   10 260 150 3500 5800   0 30 16 460 1200   4 65 35 810 1700  
        incorrect true 1 -32 .38 .38 3.6 32 .0082 0   0 4.5 2.5 81 260   10 97 63 1100 970   0 0 0 0 0   4 0 0 0 0  
        incorrect false 14 -224 820    820    6300   12000 .11   13   0 95   50   1500 3300   0 170 90 2400 4800   0 30 16 460 1200   0 65 35 810 1700  
score (52 tasks, max score: 79) -246
Run set sv-comp17.MemSafety-LinkedLists