Tool ULTIMATE Automizer f7c3ed31
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 06:16:04 CET [[ 2017-01-15 05:34:44 CET ]] [[ 2017-01-15 05:49:53 CET ]] [[ 2017-01-15 05:35:06 CET ]] [[ 2017-01-15 05:51:11 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0616.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0616.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   880   12000 960 2.3 0   - - error (invalid witness file) .51 .34 10   41 error (invalid witness file) 6.4 3.4 120 310
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   11000 2300 2.3 0   - - error (invalid witness file) .52 .35 8.4 40 error (invalid witness file) 6.7 3.5 120 300
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   12000 990 2.3 0   - - error (invalid witness file) .60 .40 8.0 40 error (invalid witness file) 6.1 3.3 110 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   170   3500 13000 2.3 0   - - error (invalid witness file) .62 .39 8.5 40 error (invalid witness file) 6.1 3.2 110 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 290   260   4100 610 2.5 0   exception 3.1  1.7  71   180 false(valid-deref) 12   6.4 190 370 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 6.6 2.1 53 360 2.5 0   false(valid-deref) 6.2  3.3  42   270 true 9.8 5.2 180 350 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   870   10000 1000 2.5 0   error (invalid witness file) .53 .35 9.4 43 error (invalid witness file) 6.2 3.2 120 300 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error 0 wit inspect 8.4 2.7 65 320 2.6 0   error (invalid witness file) .53 .35 11   40 error (invalid witness file) 5.7 3.1 120 290 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 200   170   2300 1000 2.5 0   error (invalid witness file) .64 .40 9.8 43 error (invalid witness file) 6.2 3.2 120 290 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 170   140   2200 1000 2.5 0   error (invalid witness file) .52 .33 8.7 39 error (invalid witness file) 6.4 3.3 130 300 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   11000 1100 2.3 0   - - error (invalid witness file) .55 .36 10   40 error (invalid witness file) 6.2 3.2 120 300
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 13   4.2 100 330 2.6 0   error (invalid witness file) .64 .41 9.4 41 error (invalid witness file) 5.8 3.1 97 290 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   800   10000 1000 2.5 0   error (invalid witness file) .52 .33 9.5 39 error (invalid witness file) 6.5 3.4 140 300 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 20   7.4 170 480 2.6 0   error (invalid witness file) .62 .40 7.2 41 error (invalid witness file) 5.7 3.1 110 300 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 15   4.6 100 390 2.6 0   error (invalid witness file) .62 .38 7.5 40 error (invalid witness file) 6.1 3.3 100 290 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 19   6.3 180 470 2.6 0   error (invalid witness file) .65 .40 7.9 41 error (invalid witness file) 6.0 3.1 130 290 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 14   4.6 110 350 2.6 0   error (invalid witness file) .51 .31 8.9 39 error (invalid witness file) 7.1 3.7 130 320 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 180   140   1200 1600 3.2 0   - - true 11    5.6  160   320 true 210   170   2600 1700
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 170   130   1100 1500 3.2 0   - - true 9.7  5.1  130   310 true 210   170   2700 1700
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 170   130   1400 1700 3.2 0   - - true 9.1  4.8  110   320 true 210   160   2400 1700
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 630   560   4800 5500 2.5 0   error (invalid witness file) .50 .31 9.2 40 error (invalid witness file) 6.1 3.2 120 300 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 630   560   5000 4900 2.5 0   error (invalid witness file) .59 .38 8.0 39 error (invalid witness file) 6.6 3.5 120 300 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 630   560   4800 5500 2.5 0   error (invalid witness file) .54 .35 8.1 40 error (invalid witness file) 8.5 4.5 120 300 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 620   550   5600 5700 2.5 0   error (invalid witness file) .58 .37 9.6 39 error (invalid witness file) 5.7 3.1 100 290 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 630   560   4800 5500 2.5 0   error (invalid witness file) .56 .37 9.8 41 error (invalid witness file) 6.8 3.5 110 300 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 610   550   4900 5600 2.5 0   error (invalid witness file) .52 .33 9.1 40 error (invalid witness file) 6.5 3.5 110 300 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 640   550   4800 5500 2.5 0   error (invalid witness file) .65 .41 8.2 41 error (invalid witness file) 7.1 3.7 130 310 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 620   550   4600 5600 2.5 0   error (invalid witness file) .56 .37 9.0 39 error (invalid witness file) 6.4 3.3 130 290 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 620   550   4900 5500 2.5 0   error (invalid witness file) .64 .41 8.1 39 error (invalid witness file) 6.1 3.3 110 300 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 620   550   5600 5600 2.5 0   error (invalid witness file) .66 .41 8.4 40 error (invalid witness file) 6.3 3.3 130 300 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   12000 820 2.3 0   - - error (invalid witness file) .56 .37 7.7 40 error (invalid witness file) 5.8 3.1 120 290
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   11000 700 2.3 0   - - error (invalid witness file) .65 .42 8.1 39 error (invalid witness file) 6.1 3.2 120 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   820   11000 820 2.3 0   - - error (invalid witness file) .49 .32 8.7 40 error (invalid witness file) 6.0 3.2 130 300
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1500 2.3 0   - - error (invalid witness file) .52 .34 12   42 error (invalid witness file) 5.6 3.0 120 290
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   12000 880 2.3 0   - - error (invalid witness file) .62 .38 9.2 42 error (invalid witness file) 5.9 3.1 120 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 9.1 2.9 65 320 2.6 0   - - error (invalid witness file) .61 .39 9.3 39 error (invalid witness file) 6.1 3.2 110 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   11000 960 2.3 0   - - error (invalid witness file) .52 .34 10   40 error (invalid witness file) 8.5 4.5 110 310
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   11000 780 2.3 0   - - error (invalid witness file) .49 .31 9.9 39 error (invalid witness file) 6.0 3.1 110 300
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   14000 900 2.3 0   - - error (invalid witness file) .56 .36 11   40 error (invalid witness file) 6.2 3.3 120 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   860   11000 820 2.3 0   - - error (invalid witness file) .48 .31 11   39 error (invalid witness file) 6.1 3.2 120 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   860   14000 940 2.3 0   - - error (invalid witness file) .51 .33 11   40 error (invalid witness file) 6.8 3.6 130 320
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   11000 940 2.3 0   - - error (invalid witness file) .53 .35 9.0 39 error (invalid witness file) 6.1 3.2 120 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   10000 970 2.7 0   - - error (invalid witness file) .56 .35 8.6 40 error (invalid witness file) 6.1 3.3 120 310
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   12000 1400 2.3 0   - - error (invalid witness file) .51 .32 11   39 error (invalid witness file) 5.5 3.0 95 300
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   820   12000 1100 2.3 0   - - error (invalid witness file) .50 .33 7.8 39 error (invalid witness file) 6.2 3.3 130 290
forester-heap/sll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 8.7 2.7 64 330 2.6 0   - - error (invalid witness file) .70 .45 6.4 39 error (invalid witness file) 6.4 3.4 110 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   820   11000 920 2.5 0   - - error (invalid witness file) .69 .44 8.3 43 error (invalid witness file) 6.0 3.2 130 290
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   11000 1100 2.3 0   - - error (invalid witness file) .53 .33 11   42 error (invalid witness file) 6.1 3.2 130 300
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   840   13000 1300 2.3 0   - - error (invalid witness file) .62 .40 7.7 39 error (invalid witness file) 8.8 4.6 92 310
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 48   24   460 750 2.5 0   true 6.5  3.4  65   270 false(valid-deref) 12   6.4 210 370 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 140   120   1700 610 2.5 0   true 5.9  3.1  66   270 true 18   9.5 300 480 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 37   18   360 840 2.5 0   true 6.7  3.5  60   270 false(valid-deref) 11   5.9 200 370 - -
../../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 11 29000 26000 330000 110000 130   0   52 40 22 480 2100   52 190 100 3500 7900   52 43 24 620 1900   52 790 580 11000 12000  
    correct results 8 11 1000 820 10000 8000 22   0   4 28 15 300 1300   5 63 33 1100 1900   3 30 15 390 950   3 640 500 7700 5100  
        correct true 3 6 520 390 3600 4800 9.5 0   3 0 0 0 0   2 0 0 0 0   3 30 15 390 950   3 640 500 7700 5100  
        correct false 5 5 520 430 6700 3200 13   0   1 28 15 300 1300   3 63 33 1100 1900   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) 11
Run set sv-comp17.MemSafety-LinkedLists