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 04:52:43 CET [[ 2017-01-15 00:23:14 CET ]] [[ 2017-01-15 00:35:58 CET ]] [[ 2017-01-15 00:29:47 CET ]] [[ 2017-01-15 00:40:29 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options -s fixed [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc.2017-01-13_0452.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc.2017-01-13_0452.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 out of memory 0 wit inspect 490 490 5900 15000 .99 0   - - error (invalid witness file) .52 .34 10   42 error (invalid witness file) 6.6 3.5 120 310
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 740 740 4200 15000 .99 0   - - error (invalid witness file) .53 .36 11   40 error (invalid witness file) 6.9 3.6 120 310
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 320 320 3300 15000 .99 0   - - error (invalid witness file) .53 .35 10   40 error (invalid witness file) 5.8 3.1 120 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 2200 4600 .99 0   - - error (invalid witness file) .52 .33 7.8 41 error (invalid witness file) 5.6 3.0 120 280
heap-manipulation/tree_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 110 110 1200 15000 .84 0   error (invalid witness file) .51 .34 4.0 40 error (invalid witness file) 6.4 3.4 110 310 - -
heap-manipulation/tree_false-valid-deref.i out of memory 0 wit inspect 110 100 1500 15000 .99 0   error (invalid witness file) .56 .37 3.7 42 error (invalid witness file) 6.3 3.3 120 300 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 300 300 3500 15000 .99 0   error (invalid witness file) .51 .33 7.0 41 error (invalid witness file) 6.7 3.5 130 320 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 91 91 1200 15000 .99 0   error (invalid witness file) .53 .36 4.8 40 error (invalid witness file) 6.4 3.4 120 310 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 500 500 5900 15000 .99 0   error (invalid witness file) .50 .31 9.0 40 error (invalid witness file) 6.0 3.2 120 300 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 760 760 8200 15000 1.7  0   error (invalid witness file) .49 .31 7.2 40 error (invalid witness file) 6.0 3.2 120 290 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 7100 3900 .99 0   - - error (invalid witness file) .51 .34 10   40 error (invalid witness file) 6.0 3.2 110 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 240 240 2600 15000 1.8  0   error (invalid witness file) .52 .34 7.5 39 error (invalid witness file) 6.6 3.4 130 290 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 39 39 480 1100 1.7  0   error (invalid witness file) .49 .33 6.7 40 error (invalid witness file) 6.2 3.3 120 300 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 450 450 5000 15000 .84 0   error (invalid witness file) .51 .34 4.1 40 error (invalid witness file) 5.9 3.1 110 290 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 170 170 1700 15000 2.0  0   error (invalid witness file) .52 .34 7.5 42 error (invalid witness file) 6.3 3.3 120 300 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 530 530 5300 15000 1.8  0   error (invalid witness file) .51 .33 9.9 40 error (invalid witness file) 5.9 3.2 110 300 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 530 530 6100 15000 2.0  0   error (invalid witness file) .47 .32 4.3 39 error (invalid witness file) 5.9 3.2 120 300 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 120 120 1300 15000 .84 0   - - error (invalid witness file) .50 .32 10   39 error (invalid witness file) 6.3 3.4 120 300
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 120 120 1500 15000 .99 0   - - error (invalid witness file) .51 .34 4.3 39 error (invalid witness file) 6.5 3.4 130 300
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 120 120 1400 15000 .84 0   - - error (invalid witness file) .48 .31 9.8 39 error (invalid witness file) 7.0 3.7 99 300
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1400 15000 .84 0   error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.3 3.3 120 300 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 490 490 1000 15000 .99 0   error (invalid witness file) .53 .35 9.0 40 error (invalid witness file) 6.7 3.5 130 310 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1400 15000 .84 0   error (invalid witness file) .49 .32 8.6 41 error (invalid witness file) 6.5 3.4 120 300 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1400 15000 .99 0   error (invalid witness file) .54 .35 6.7 39 error (invalid witness file) 6.6 3.5 130 300 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1400 15000 .99 0   error (invalid witness file) .52 .34 7.6 40 error (invalid witness file) 6.7 3.5 130 300 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1400 15000 .84 0   error (invalid witness file) .48 .31 8.7 40 error (invalid witness file) 6.0 3.2 130 290 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1500 15000 .99 0   error (invalid witness file) .52 .35 7.4 40 error (invalid witness file) 6.9 3.6 120 310 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1700 15000 .84 0   error (invalid witness file) .49 .32 9.6 40 error (invalid witness file) 6.7 3.5 140 300 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1400 15000 .84 0   error (invalid witness file) .52 .34 6.3 40 error (invalid witness file) 6.5 3.4 120 300 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i out of memory 0 wit inspect 120 120 1400 15000 .84 0   error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.6 3.5 130 300 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 5900 8100 .84 0   - - error (invalid witness file) .51 .34 7.3 40 error (invalid witness file) 5.7 3.1 120 290
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 480 480 870 15000 .84 0   - - error (invalid witness file) .51 .33 12   39 error (invalid witness file) 7.0 3.7 94 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 6600 12000 .99 0   - - error (invalid witness file) .51 .33 8.9 39 error (invalid witness file) 6.7 3.5 120 320
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 8000 5900 .99 0   - - error (invalid witness file) .57 .35 12   43 error (invalid witness file) 6.2 3.3 130 300
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 83 83 980 15000 .84 0   - - error (invalid witness file) .51 .35 5.2 40 error (invalid witness file) 5.9 3.2 120 290
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 91 90 1100 15000 .84 0   - - error (invalid witness file) .49 .31 7.0 39 error (invalid witness file) 5.9 3.1 120 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 190 190 2100 15000 .84 0   - - error (invalid witness file) .49 .33 8.7 40 error (invalid witness file) 6.3 3.3 130 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 110 110 990 15000 .99 0   - - error (invalid witness file) .49 .33 3.9 39 error (invalid witness file) 6.2 3.3 130 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 7000 10000 .84 0   - - error (invalid witness file) .49 .32 4.9 42 error (invalid witness file) 6.2 3.3 110 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 2100 5500 .99 0   - - error (invalid witness file) .51 .33 3.9 40 error (invalid witness file) 6.0 3.2 110 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 320 320 760 15000 .99 0   - - error (invalid witness file) .55 .35 11   41 error (invalid witness file) 6.2 3.3 120 310
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 140 140 1500 15000 .99 0   - - error (invalid witness file) .53 .35 13   42 error (invalid witness file) 6.3 3.3 130 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 6300 11000 .84 0   - - error (invalid witness file) .50 .32 4.5 42 error (invalid witness file) 6.7 3.5 130 320
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 5800 4300 .84 0   - - error (invalid witness file) .55 .35 11   43 error (invalid witness file) 5.7 3.1 110 290
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 340 340 4400 15000 .84 0   - - error (invalid witness file) .48 .32 9.7 39 error (invalid witness file) 6.0 3.2 120 300
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 880 880 11000 15000 .99 0   - - error (invalid witness file) .48 .32 8.4 39 error (invalid witness file) 6.5 3.5 120 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 130 130 1300 15000 .99 0   - - error (invalid witness file) .50 .33 12   40 error (invalid witness file) 5.9 3.2 110 300
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i out of memory 0 wit inspect 88 87 1000 15000 .99 0   - - error (invalid witness file) .49 .33 4.3 41 error (invalid witness file) 6.2 3.3 120 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900 900 2500 5400 .99 0   - - error (invalid witness file) .53 .35 14   39 error (invalid witness file) 6.0 3.1 140 300
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 93 92 1100 15000 .84 0   error (invalid witness file) .54 .36 8.8 40 error (invalid witness file) 6.3 3.3 130 300 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900 900 8100 6400 .99 0   error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.3 3.3 130 300 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i out of memory 0 wit inspect 330 330 3900 15000 .84 0   error (invalid witness file) .50 .33 4.5 40 error (invalid witness file) 6.1 3.2 130 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 1 21000 20000 170000 680000 53   0   52 13    8.4  190   1000 52 160   84   3100 7500 52 14 9.0 240 1100   52 170 89 3200 8100  
    correct results 1 1 39 39 480 1100 1.7 0   0 .49 .33 6.7 40 0 6.2 3.3 120 300 0 0 0   0 0   0 0 0 0 0  
        correct true 0
        correct false 1 1 39 39 480 1100 1.7 0   0 .49 .33 6.7 40 0 6.2 3.3 120 300 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) 1
Run set sv-comp17.MemSafety-LinkedLists