Tool SMACK+Corral 1.7.2
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-14 05:56:27 CET [[ 2017-01-15 04:08:20 CET ]] [[ 2017-01-15 04:18:47 CET ]] [[ 2017-01-15 04:12:29 CET ]] [[ 2017-01-15 04:25:58 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0556.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0556.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 timeout 0 wit inspect 880   930   7200 570 2.5 0      - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 6.5 3.4 120 290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   7800 320 2.6 0      - - error (invalid witness file) .59 .37 13   43 error (invalid witness file) 6.0 3.2 120 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   7700 510 2.4 0      - - error (invalid witness file) .50 .34 9.7 40 error (invalid witness file) 5.9 3.2 110 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   11000 250 2.3 0      - - error (invalid witness file) .51 .33 4.0 40 error (invalid witness file) 6.2 3.3 130 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 5.1 5.0 58 100 1.4 0      error (invalid witness file) .52 .34 9.1 40 error (invalid witness file) 6.3 3.3 130 300 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 2.2 2.2 23 91 1.4 0      error (invalid witness file) .51 .34 7.9 39 error (invalid witness file) 6.3 3.3 120 300 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 750   750   8900 220 2.0 .0041 error (invalid witness file) .51 .33 4.0 40 error (invalid witness file) 5.6 2.9 90 280 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   6900 280 2.1 0      error (invalid witness file) .49 .32 7.4 40 error (invalid witness file) 6.7 3.5 140 320 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   7300 350 2.1 0      error (invalid witness file) .50 .33 11   42 error (invalid witness file) 5.9 3.2 120 300 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 830   830   7200 330 2.0 0      error (invalid witness file) .50 .34 3.6 39 error (invalid witness file) 6.2 3.3 94 310 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   9900 320 2.0 0      - - error (invalid witness file) .56 .36 11   40 error (invalid witness file) 6.1 3.2 110 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 750   750   5400 320 1.9 0      error (invalid witness file) .54 .33 12   40 error (invalid witness file) 5.4 3.0 110 290 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 14   14   210 110 2.0 0      error (invalid witness file) .47 .31 6.8 39 error (invalid witness file) 6.0 3.2 110 300 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 750   750   6500 290 2.0 0      error (invalid witness file) .51 .32 9.4 40 error (invalid witness file) 5.8 3.1 120 300 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 750   750   7800 310 1.9 0      error (invalid witness file) .50 .33 7.3 39 error (invalid witness file) 5.4 2.9 78 290 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 750   750   6300 270 1.9 0      error (invalid witness file) .53 .34 4.2 42 error (invalid witness file) 6.2 3.3 130 300 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 750   750   6800 340 2.0 0      error (invalid witness file) .49 .31 9.3 39 error (invalid witness file) 6.4 3.4 130 310 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 88   88   1100 250 6.3 0      - - error (invalid witness file) .48 .32 9.3 40 error (invalid witness file) 6.6 3.5 130 300
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 87   87   1100 250 6.2 0      - - error (invalid witness file) .50 .33 13   40 error (invalid witness file) 6.5 3.4 130 310
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 89   88   1100 250 6.2 0      - - error (invalid witness file) .50 .33 7.4 40 error (invalid witness file) 6.4 3.4 110 300
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 680   680   7200 360 3.7 0      error (invalid witness file) .55 .35 12   39 error (invalid witness file) 6.5 3.4 140 300 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 670   670   7900 360 3.7 0      error (invalid witness file) .51 .33 13   40 error (invalid witness file) 6.3 3.4 110 300 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 680   680   8100 360 3.7 0      error (invalid witness file) .50 .32 10   39 error (invalid witness file) 7.0 3.7 140 310 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 680   670   7600 360 3.7 0      error (invalid witness file) .51 .34 3.8 40 error (invalid witness file) 6.0 3.3 90 300 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 690   680   7700 360 3.7 0      error (invalid witness file) .54 .35 11   41 error (invalid witness file) 6.7 3.5 120 300 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 650   650   9000 360 3.8 0      error (invalid witness file) .47 .30 5.7 39 error (invalid witness file) 6.5 3.4 130 300 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 670   660   6900 360 3.8 0      error (invalid witness file) .51 .33 4.1 40 error (invalid witness file) 6.6 3.5 140 300 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 640   640   9400 360 3.7 0      error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.7 3.5 120 300 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 680   680   7900 350 3.8 0      error (invalid witness file) .54 .33 13   40 error (invalid witness file) 6.4 3.4 130 300 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-deref) -16 wit inspect 660   660   7300 350 3.8 0      error (invalid witness file) .48 .31 8.7 40 error (invalid witness file) 6.3 3.4 87 310 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   6500 300 2.3 0      - - error (invalid witness file) .54 .35 8.2 43 error (invalid witness file) 6.0 3.2 98 290
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   6700 270 2.0 0      - - error (invalid witness file) .52 .35 4.3 40 error (invalid witness file) 6.2 3.3 130 290
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   6700 290 2.1 0      - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 6.2 3.3 110 310
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   9300 330 2.2 0      - - error (invalid witness file) .46 .31 3.9 39 error (invalid witness file) 6.0 3.2 97 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   10000 340 2.1 0      - - error (invalid witness file) .55 .36 8.6 41 error (invalid witness file) 5.9 3.2 110 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   6900 320 2.1 0      - - error (invalid witness file) .51 .31 7.2 39 error (invalid witness file) 6.5 3.4 120 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   7900 350 2.1 0      - - error (invalid witness file) .52 .34 10   42 error (invalid witness file) 5.9 3.1 120 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   8200 330 2.2 0      - - error (invalid witness file) .63 .39 5.9 39 error (invalid witness file) 6.4 3.4 120 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   7200 340 2.0 0      - - error (invalid witness file) .50 .32 6.5 43 error (invalid witness file) 6.0 3.2 110 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   11000 280 2.2 0      - - error (invalid witness file) .49 .32 8.4 39 error (invalid witness file) 6.2 3.3 120 290
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   7700 310 2.2 0      - - error (invalid witness file) .47 .32 3.7 40 error (invalid witness file) 6.2 3.3 110 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   10000 250 2.0 0      - - error (invalid witness file) .49 .32 7.5 39 error (invalid witness file) 6.2 3.3 120 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   7700 260 2.1 0      - - error (invalid witness file) .48 .31 5.0 39 error (invalid witness file) 5.9 3.2 120 310
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   12000 320 2.2 0      - - error (invalid witness file) .49 .32 6.0 40 error (invalid witness file) 6.1 3.2 110 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   11000 310 2.0 0      - - error (invalid witness file) .50 .33 8.5 40 error (invalid witness file) 7.0 3.7 130 320
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   7200 310 2.0 0      - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.1 3.2 110 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   8000 330 2.1 0      - - error (invalid witness file) .47 .31 5.2 40 error (invalid witness file) 6.1 3.3 130 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 880   930   7800 340 2.2 0      - - error (invalid witness file) .52 .34 6.9 40 error (invalid witness file) 5.9 3.1 120 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i true 2 wit inspect 880   880   7300 300 2.0 0      - - error (invalid witness file) .49 .32 7.1 39 error (invalid witness file) 6.5 3.4 130 320
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 3.6 3.5 41 100 1.3 0      error (invalid witness file) .51 .34 6.1 39 error (invalid witness file) 6.1 3.3 120 300 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 4.1 4.0 48 110 1.5 0      error (invalid witness file) .49 .33 7.5 39 error (invalid witness file) 6.4 3.4 120 300 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 3.3 3.3 38 92 1.3 0      error (invalid witness file) .50 .32 9.2 39 error (invalid witness file) 5.9 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 52 -121 35000 36000 350000 15000 140 .0041 52 13   8.2 210 990   52 160 83 2900 7500   52 14   8.9 210 1100   52 170 89 3200 8100  
    correct results 27 39 15000 15000 150000 6900 64 .0041 0 7.6 4.9 110 600   0 91 48 1700 4500   0 6.0 3.9 92 480   0 75 40 1400 3600  
        correct true 12 24 8200 8200 81000 3600 38 0      0 0   0   0 0   0 0 0 0 0   0 6.0 3.9 92 480   0 75 40 1400 3600  
        correct false 15 15 7100 7000 64000 3300 27 .0041 0 7.6 4.9 110 600   0 91 48 1700 4500   0 0   0   0 0   0 0 0 0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 10 -160 6700 6700 79000 3600 38 0      0 5.1 3.3 94 400   0 65 34 1200 3000   0 0   0   0 0   0 0 0 0 0  
        incorrect true 0
        incorrect false 10 -160 6700 6700 79000 3600 38 0      0 5.1 3.3 94 400   0 65 34 1200 3000   0 0   0   0 0   0 0 0 0 0  
score (52 tasks, max score: 79) -121
Run set sv-comp17.MemSafety-LinkedLists