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 05:51:33 CET [[ 2017-01-15 01:19:13 CET ]] [[ 2017-01-15 01:22:10 CET ]] [[ 2017-01-15 01:20:47 CET ]] [[ 2017-01-15 01:23:25 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options -s incr [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-incr.2017-01-13_0551.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-incr.2017-01-13_0551.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 900    900    9600   1400 .99 0   - - error (invalid witness file) .52 .34 13   41 error (invalid witness file) 6.3 3.3 120 290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9000   630 .99 0   - - error (invalid witness file) .57 .36 12   44 error (invalid witness file) 6.3 3.3 130 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   700 .99 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.2 3.3 130 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9700   490 .84 0   - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.3 3.3 140 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .26 .25 3.4 26 .99 0   error (invalid witness file) .53 .35 12   39 error (invalid witness file) 7.0 3.7 120 320 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .12 .11 1.2 25 .99 0   error (invalid witness file) .54 .35 13   40 error (invalid witness file) 6.0 3.2 100 290 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .20 .19 1.7 25 .99 0   error (invalid witness file) .52 .34 7.7 42 error (invalid witness file) 6.0 3.2 110 300 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .48 .47 5.5 33 .99 0   error (invalid witness file) .58 .38 13   43 error (invalid witness file) 5.7 3.1 85 300 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .30 .29 3.7 30 .99 0   error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.2 3.3 130 290 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .28 .27 2.9 27 .99 0   error (invalid witness file) .51 .33 11   41 error (invalid witness file) 6.4 3.4 120 300 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9200   1400 .99 0   - - error (invalid witness file) .55 .37 13   41 error (invalid witness file) 6.3 3.3 130 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .12 .12 1.3 24 .99 0   error (invalid witness file) .50 .33 11   40 error (invalid witness file) 6.0 3.2 120 300 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .34 .34 3.8 30 .99 0   error (invalid witness file) .48 .31 7.6 40 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 .12 .12 1.4 24 .99 0   error (invalid witness file) .53 .33 12   40 error (invalid witness file) 6.1 3.2 120 300 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .13 .13 1.5 24 .99 0   error (invalid witness file) .55 .36 12   40 error (invalid witness file) 5.5 3.0 110 300 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .16 .16 1.6 24 .99 0   error (invalid witness file) .54 .35 14   43 error (invalid witness file) 6.7 3.5 140 320 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .12 .12 1.4 25 .99 0   error (invalid witness file) .57 .37 13   44 error (invalid witness file) 6.0 3.2 120 300 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   620 .99 0   - - error (invalid witness file) .53 .32 11   41 error (invalid witness file) 6.2 3.3 130 290
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i false(valid-memtrack) -16 wit inspect 620    620    6900   860 .84 0   - - error (invalid witness file) .53 .35 12   39 error (invalid witness file) 6.3 3.3 120 310
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    10000   1000 .86 0   - - error (invalid witness file) .54 .34 12   39 error (invalid witness file) 6.3 3.4 140 300
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 460    460    5400   890 .99 0   error (invalid witness file) .52 .35 11   40 error (invalid witness file) 7.4 3.8 150 320 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900    900    12000   630 .84 0   error (invalid witness file) .50 .33 11   40 error (invalid witness file) 7.0 3.7 120 300 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900    900    9800   910 .84 0   error (invalid witness file) .51 .33 10   41 error (invalid witness file) 6.5 3.4 150 300 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900    900    12000   830 .84 0   error (invalid witness file) .52 .35 11   42 error (invalid witness file) 6.2 3.3 140 300 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 410    410    4900   810 .84 0   error (invalid witness file) .50 .33 11   39 error (invalid witness file) 6.3 3.4 130 300 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 640    640    6800   820 .84 0   error (invalid witness file) .54 .34 12   44 error (invalid witness file) 6.3 3.3 130 310 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 690    690    8000   960 .84 0   error (invalid witness file) .53 .34 9.9 40 error (invalid witness file) 6.1 3.2 110 290 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900    900    10000   1000 .99 0   error (invalid witness file) .49 .32 9.4 39 error (invalid witness file) 5.9 3.1 120 290 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900    900    10000   770 .99 0   error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.5 3.4 130 300 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 620    620    6400   890 .84 0   error (invalid witness file) .51 .35 12   41 error (invalid witness file) 6.4 3.4 120 300 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9600   450 .84 0   - - error (invalid witness file) .49 .32 12   39 error (invalid witness file) 6.5 3.4 120 310
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9200   4600 .99 0   - - error (invalid witness file) .54 .34 13   39 error (invalid witness file) 7.0 3.7 130 330
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    7700   420 .84 0   - - error (invalid witness file) .49 .32 11   40 error (invalid witness file) 5.8 3.1 120 290
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9100   1600 .99 0   - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.3 3.3 130 310
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   500 .99 0   - - error (invalid witness file) .55 .35 12   40 error (invalid witness file) 6.0 3.2 120 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9100   510 .99 0   - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 6.1 3.2 120 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    5400   530 .84 0   - - error (invalid witness file) .54 .36 12   41 error (invalid witness file) 6.3 3.3 120 310
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    12000   850 .99 0   - - error (invalid witness file) .48 .32 11   39 error (invalid witness file) 6.9 3.6 130 310
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    12000   1300 .99 0   - - error (invalid witness file) .52 .34 14   41 error (invalid witness file) 5.8 3.1 120 290
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    7700   420 .93 0   - - error (invalid witness file) .49 .30 11   39 error (invalid witness file) 6.8 3.6 130 310
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    8800   560 .84 0   - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.3 3.3 120 310
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    10000   5100 .99 0   - - error (invalid witness file) .49 .32 13   39 error (invalid witness file) 6.1 3.2 130 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    7700   430 .84 0   - - error (invalid witness file) .50 .32 9.8 40 error (invalid witness file) 5.7 3.1 120 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    10000   1700 .84 0   - - error (invalid witness file) .51 .32 12   39 error (invalid witness file) 6.2 3.3 130 310
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   590 .99 0   - - error (invalid witness file) .56 .35 12   43 error (invalid witness file) 6.0 3.1 110 290
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   540 .84 0   - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 5.6 3.0 110 290
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    9900   950 .99 0   - - error (invalid witness file) .50 .34 12   39 error (invalid witness file) 7.0 3.6 120 320
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    11000   1400 .84 0   - - error (invalid witness file) .54 .36 11   40 error (invalid witness file) 6.0 3.3 110 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900    900    8100   1600 .99 0   - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.4 3.3 120 300
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .39 .38 4.7 31 .84 0   error (invalid witness file) .51 .34 14   41 error (invalid witness file) 6.0 3.1 120 300 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .16 .16 1.8 25 .84 0   error (invalid witness file) .51 .33 12   39 error (invalid witness file) 6.6 3.5 140 310 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .30 .30 3.5 26 .99 0   error (invalid witness file) .51 .32 12   40 error (invalid witness file) 6.0 3.1 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 4 31000 31000 340000 40000 48    0   52 13 8.4 280 1000   52 160 83 3100 7500   52 14    9.0  320 1100   52 170   89   3300 8200  
    correct results 20 20 2800 2800 31000 4800 19    0   0 10 6.8 230 810   0 120 66 2400 6000   0 0    0    0 0   0 0   0   0 0  
        correct true 0
        correct false 20 20 2800 2800 31000 4800 19    0   0 10 6.8 230 810   0 120 66 2400 6000   0 0    0    0 0   0 0   0   0 0  
    correct-unconfimed results 0
        correct-unconfirmed true 0
        correct-unconfirmed false 0
    incorrect results 1 -16 620 620 6900 860 .84 0   0 0 0   0 0   0 0 0 0 0   0 .53 .35 12 39   0 6.3 3.3 120 310  
        incorrect true 0
        incorrect false 1 -16 620 620 6900 860 .84 0   0 0 0   0 0   0 0 0 0 0   0 .53 .35 12 39   0 6.3 3.3 120 310  
score (52 tasks, max score: 79) 4
Run set sv-comp17.MemSafety-LinkedLists