Tool symbiotic KLEE:7f3c74aa-dg:96e851cf-symbiotic:69a1d8e6-minisat:3db58943-stp:39fa956f-LLVMInstrumentation:f750b24a
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 11:37:51 CET [[ 2017-01-15 04:18:56 CET ]] [[ 2017-01-15 04:38:06 CET ]] [[ 2017-01-15 04:27:27 CET ]] [[ 2017-01-15 04:45:45 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options --witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/symbiotic4.2017-01-14_1137.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/symbiotic4.2017-01-14_1137.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 (timeout) 0 wit inspect 900    900    10000   3100 .11  0      - - error (invalid witness file) .50 .31 7.1 39 error (invalid witness file) 6.2 3.3 130 300
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9500   3900 .086 0      - - error (invalid witness file) .49 .32 7.4 41 error (invalid witness file) 7.3 3.8 130 330
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7400   2100 .086 0      - - error (invalid witness file) .51 .33 5.5 40 error (invalid witness file) 6.5 3.4 120 310
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i true 2 wit inspect .44 .43 4.8 34 .074 0      - - out of memory 150    83    1400   7000 out of memory 190   110   2300 7000
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .41 .40 5.3 28 .074 0      timeout 93    70    1500   4100 true 9.5 5.0 160 370 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect .36 .35 4.0 29 .074 0      false(valid-deref) 5.4  2.9  110   290 true 9.2 4.9 160 350 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .34 .33 4.1 17 .074 .037  timeout 93    74    1100   4000 true 11   5.9 200 460 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .36 .35 4.5 27 .074 0      timeout 95    78    1100   3900 error 9.7 5.2 94 300 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .37 .37 4.6 25 .074 0      timeout 95    76    1000   3900 unknown 20   11   230 470 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .34 .34 3.5 22 .074 0      timeout 95    76    1300   3900 unknown 20   11   210 440 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9700   2100 .074 0      - - error (invalid witness file) .49 .34 6.4 39 error (invalid witness file) 6.9 3.6 100 320
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .30 .30 4.2 17 .074 0      timeout 94    73    1700   4200 unknown 19   10   220 410 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .33 .32 3.6 18 .11  0      error 5.2  2.7  94   260 true 18   9.5 270 1200 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .32 .31 3.6 19 .074 0      timeout 98    76    2000   4100 unknown 19   10   300 410 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .27 .26 3.2 13 .074 0      timeout 93    74    1900   3800 unknown 21   11   300 510 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .29 .28 3.3 16 .074 0      timeout 93    77    1500   4200 unknown 18   9.5 220 380 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect .31 .30 3.5 20 .074 .012  timeout 94    69    1000   4400 unknown 18   9.5 230 390 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  2.1  25   150 .27  0      - - true 9.0  4.7  170   330 true 210   170   2500 1700
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.2  2.1  29   160 .27  0      - - true 8.4  4.4  150   310 true 210   160   2700 1700
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 2.1  2.1  25   150 .27  0      - - true 8.8  4.6  160   320 true 190   160   3300 1700
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.3  2.2  24   160 .27  0      true 9.0  4.7  130   330 true 20   11   130 490 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.2  2.2  27   160 .27  0      true 9.1  4.7  130   320 true 14   7.6 180 470 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.3  2.2  27   160 .27  0      true 8.9  4.7  150   330 true 14   7.8 250 480 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.3  2.2  26   160 .27  0      true 9.1  4.7  150   320 true 14   7.5 240 480 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i timeout (timeout) 0 wit inspect 900    900    8100   2100 .27  0      error (invalid witness file) .53 .36 9.6 39 error (invalid witness file) 6.3 3.3 120 290 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.2  2.2  28   160 .27  0      true 9.5  4.9  170   320 true 14   7.8 240 490 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.2  2.2  26   160 .27  0      true 9.2  4.8  140   320 true 15   8.0 220 490 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.2  2.2  26   160 .27  0      true 9.2  4.8  180   320 true 14   7.7 270 470 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.2  2.2  26   160 .27  0      true 9.4  4.9  180   330 true 17   9.4 150 480 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i false(valid-memtrack) 1 wit inspect 2.2  2.1  30   160 .27  0      true 9.1  4.8  190   320 true 15   8.0 250 490 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6600   3000 .074 0      - - error (invalid witness file) .54 .36 7.3 41 error (invalid witness file) 5.4 3.0 100 290
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    13000   3200 .074 0      - - error (invalid witness file) .55 .36 7.7 45 error (invalid witness file) 6.2 3.3 120 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7200   3200 .074 0      - - error (invalid witness file) .53 .35 13   40 error (invalid witness file) 6.2 3.3 120 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   2800 .074 .0082 - - error (invalid witness file) .49 .32 5.0 39 error (invalid witness file) 6.3 3.3 120 310
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6800   2900 .074 0      - - error (invalid witness file) .52 .33 9.6 39 error (invalid witness file) 6.0 3.2 110 290
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    8500   3000 .074 0      - - error (invalid witness file) .50 .34 6.7 40 error (invalid witness file) 6.5 3.4 130 310
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   3300 .074 0      - - error (invalid witness file) .51 .35 9.2 41 error (invalid witness file) 6.4 3.3 120 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7500   3300 .074 0      - - error (invalid witness file) .53 .34 4.4 40 error (invalid witness file) 6.2 3.3 130 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9800   2100 .074 0      - - error (invalid witness file) .51 .33 13   39 error (invalid witness file) 6.8 3.6 140 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    8200   3100 .074 0      - - error (invalid witness file) .53 .34 13   39 error (invalid witness file) 6.4 3.3 120 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6800   2600 .074 0      - - error (invalid witness file) .50 .33 4.0 39 error (invalid witness file) 5.6 3.0 95 290
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    9300   3000 .074 0      - - error (invalid witness file) .52 .33 7.1 39 error (invalid witness file) 7.0 3.6 150 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    7800   3400 .074 0      - - error (invalid witness file) .47 .31 3.8 40 error (invalid witness file) 5.5 2.9 110 290
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   2800 .074 0      - - error (invalid witness file) .52 .34 11   41 error (invalid witness file) 5.6 3.0 110 290
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6500   3100 .074 0      - - error (invalid witness file) .51 .33 6.8 39 error (invalid witness file) 7.3 3.8 140 310
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6600   3100 .074 0      - - error (invalid witness file) .47 .31 4.4 39 error (invalid witness file) 6.4 3.4 110 290
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    11000   3400 .074 0      - - error (invalid witness file) .50 .33 10   39 error (invalid witness file) 5.9 3.1 110 290
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    6900   3300 .074 0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 6.1 3.3 100 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout (timeout) 0 wit inspect 900    900    10000   2300 .074 0      - - error (invalid witness file) .49 .32 6.7 39 error (invalid witness file) 5.8 3.1 98 290
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .33 .33 4.3 22 .074 0      timeout 95    76    1300   3900 false(valid-deref) 31   19   420 710 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .39 .39 4.7 28 .074 0      timeout 97    77    1100   4000 true 37   21   570 2400 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect .31 .30 3.7 20 .074 0      timeout 95    77    1100   3900 false(valid-deref) 29   17   410 840 - -
../../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 32 22000   22000   210000 73000 6.5  .057 52 1300 1000 19000 56000   52 430 240 6100 14000   52 190 100 2000 8900   52 950 680 14000 19000  
    correct results 28 32 32   31   380 2200 4.5  .049 10 1300 1000 19000 56000   16 430 230 5900 14000   3 180 96 1800 8000   3 800 610 11000 12000  
        correct true 4 8 6.9 6.7 83 480 .88 0     9 0 0 0 0   14 0 0 0 0   3 180 96 1800 8000   3 800 610 11000 12000  
        correct false 24 24 25   25   300 1700 3.6  .049 1 1300 1000 19000 56000   2 430 230 5900 14000   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) 32
Run set sv-comp17.MemSafety-LinkedLists