Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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 06:35:22 CET [[ 2017-01-15 01:30:25 CET ]] [[ 2017-01-15 01:30:43 CET ]] [[ 2017-01-15 01:30:33 CET ]] [[ 2017-01-15 01:30:54 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options -s kinduction [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-kind.2017-01-13_0635.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-kind.2017-01-13_0635.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 unknown 0 wit inspect 3.4  3.4  44   150 .99 0   - - error (invalid witness file) .63 .41 7.8 40 error (invalid witness file) 6.6 3.5 130 310
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect 2.8  2.8  34   72 .84 0   - - error (invalid witness file) .60 .39 8.0 39 error (invalid witness file) 6.6 3.4 100 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .34 .34 4.0 34 .84 0   - - error (invalid witness file) .59 .39 9.3 43 error (invalid witness file) 6.6 3.5 130 310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .55 .54 7.0 35 .84 0   - - error (invalid witness file) .55 .36 12   41 error (invalid witness file) 7.0 3.6 130 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .27 .27 3.4 26 .84 0   error (invalid witness file) .56 .36 13   42 error (invalid witness file) 5.7 3.1 110 300 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .11 .11 1.5 25 .84 0   error (invalid witness file) .50 .33 11   39 error (invalid witness file) 5.4 2.9 110 300 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .19 .19 2.1 25 .99 0   error (invalid witness file) .53 .35 13   40 error (invalid witness file) 5.5 3.0 110 290 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .50 .50 5.4 33 .99 0   error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.9 3.1 120 300 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .30 .30 3.7 30 .84 0   error (invalid witness file) .50 .32 10   40 error (invalid witness file) 6.0 3.1 120 300 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .28 .27 3.5 27 .99 0   error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.4 3.4 100 300 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .12 .12 1.4 24 .84 0   - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.0 3.2 130 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .12 .12 1.7 24 .99 0   error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.4 3.4 140 310 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .41 .40 6.1 36 .99 0   error (invalid witness file) .50 .34 12   40 error (invalid witness file) 5.9 3.1 120 290 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .12 .12 1.4 24 .99 0   error (invalid witness file) .53 .33 12   39 error (invalid witness file) 6.3 3.3 120 300 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 .16 1.3 24 .99 0   error (invalid witness file) .51 .33 11   39 error (invalid witness file) 5.6 3.0 110 290 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 .16 1.4 24 .99 0   error (invalid witness file) .50 .32 12   39 error (invalid witness file) 7.1 3.7 79 300 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .13 .13 1.4 24 .99 0   error (invalid witness file) .50 .33 6.4 41 error (invalid witness file) 6.3 3.3 140 300 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .38 .37 4.1 69 .84 0   - - error (invalid witness file) .58 .39 12   40 error (invalid witness file) 6.4 3.4 130 310
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .33 .33 3.6 68 .99 0   - - error (invalid witness file) .49 .33 7.4 40 error (invalid witness file) 6.4 3.4 120 300
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .34 .34 4.0 69 .99 0   - - error (invalid witness file) .53 .34 14   40 error (invalid witness file) 6.7 3.6 120 300
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .33 .32 3.7 67 .84 0   error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.4 3.4 130 300 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .34 .33 3.8 67 .99 0   error (invalid witness file) .51 .32 13   39 error (invalid witness file) 6.3 3.3 120 300 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .34 .34 4.1 67 .99 0   error (invalid witness file) .63 .40 8.9 42 error (invalid witness file) 6.9 3.6 120 310 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .32 .32 3.7 67 .84 0   error (invalid witness file) .52 .34 13   41 error (invalid witness file) 6.2 3.3 110 310 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .34 .34 3.4 67 .99 0   error (invalid witness file) .53 .34 13   40 error (invalid witness file) 7.7 4.1 84 300 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .32 .32 3.7 67 .84 0   error (invalid witness file) .55 .36 9.2 40 error (invalid witness file) 7.1 3.7 140 310 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .32 .32 3.6 67 .84 0   error (invalid witness file) .51 .33 12   41 error (invalid witness file) 6.5 3.4 130 300 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .32 .32 3.6 67 .99 0   error (invalid witness file) .52 .35 14   42 error (invalid witness file) 6.7 3.5 140 300 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .32 .32 3.5 67 .99 0   error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.9 3.7 82 290 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect .35 .35 3.4 67 .84 0   error (invalid witness file) .53 .34 12   41 error (invalid witness file) 6.6 3.5 130 300 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .49 .49 5.9 35 .84 0   - - error (invalid witness file) .48 .31 9.1 39 error (invalid witness file) 5.8 3.1 110 290
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .16 .16 2.0 27 .99 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.7 3.5 130 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .31 .31 4.1 32 .84 0   - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.9 3.6 110 310
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .13 .13 1.5 25 .84 0   - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 6.0 3.2 110 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .34 .34 3.8 36 .99 0   - - error (invalid witness file) .53 .34 11   41 error (invalid witness file) 5.7 3.0 110 290
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .46 .46 5.3 39 .99 0   - - error (invalid witness file) .50 .33 10   39 error (invalid witness file) 6.2 3.2 120 310
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .27 .27 3.6 32 .84 0   - - error (invalid witness file) .51 .31 12   39 error (invalid witness file) 6.4 3.4 130 310
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .15 .15 2.0 25 .84 0   - - error (invalid witness file) .61 .41 11   40 error (invalid witness file) 5.8 3.1 110 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .19 .19 2.3 29 .99 0   - - error (invalid witness file) .53 .35 12   40 error (invalid witness file) 5.9 3.2 120 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .31 .31 4.5 29 .84 0   - - error (invalid witness file) .58 .37 9.4 40 error (invalid witness file) 7.2 3.8 82 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .25 .24 3.5 28 .99 0   - - error (invalid witness file) .55 .34 12   42 error (invalid witness file) 5.5 3.0 120 280
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .15 .15 1.7 25 .84 0   - - error (invalid witness file) .59 .40 12   40 error (invalid witness file) 6.3 3.3 140 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .36 .36 4.2 30 .99 0   - - error (invalid witness file) .54 .34 11   40 error (invalid witness file) 5.8 3.1 110 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .16 .16 1.3 25 .99 0   - - error (invalid witness file) .53 .34 12   39 error (invalid witness file) 6.4 3.4 130 310
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .22 .22 2.4 28 .84 0   - - error (invalid witness file) .51 .34 7.9 40 error (invalid witness file) 6.1 3.2 120 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .22 .22 2.8 29 .99 0   - - error (invalid witness file) .61 .39 9.7 43 error (invalid witness file) 6.0 3.2 120 290
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .24 .24 3.0 28 .99 0   - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 6.1 3.2 110 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .15 .15 1.9 25 .99 0   - - error (invalid witness file) .52 .34 12   42 error (invalid witness file) 6.0 3.2 120 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i unknown 0 wit inspect .18 .18 1.7 26 .84 0   - - error (invalid witness file) .49 .30 9.9 39 error (invalid witness file) 7.0 3.7 120 310
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .38 .38 4.1 31 .99 0   error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.2 3.3 130 300 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .17 .17 1.9 25 .84 0   error (invalid witness file) .55 .35 11   42 error (invalid witness file) 6.3 3.3 130 300 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .31 .31 2.9 26 .99 0   error (invalid witness file) .53 .35 13   39 error (invalid witness file) 6.4 3.4 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 15 20   20   240 2200 48 0   52 13   8.5 290 1000 52 160 84 2900 7500 52 15 9.5 290 1100   52 170 90 3200 8100  
    correct results 15 15 3.6 3.6 42 400 14 0   0 7.8 5.0 170 600 0 91 48 1700 4500 0 0 0   0 0   0 0 0 0 0  
        correct true 0
        correct false 15 15 3.6 3.6 42 400 14 0   0 7.8 5.0 170 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 0
        incorrect true 0
        incorrect false 0
score (52 tasks, max score: 79) 15
Run set sv-comp17.MemSafety-LinkedLists