Tool ULTIMATE Taipan 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 16:15:06 CET [[ 2017-01-15 05:45:52 CET ]] [[ 2017-01-15 06:00:59 CET ]] [[ 2017-01-15 05:46:10 CET ]] [[ 2017-01-15 06:02:27 CET ]]
Run set sv-comp17.MemSafety-LinkedLists
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1615.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1615.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   840   11000 5000 2.3 0     - - error (invalid witness file) .54 .36 13   42 error (invalid witness file) 5.8 3.2 120 290
heap-manipulation/dll_of_dll_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   12000 770 2.3 0     - - error (invalid witness file) .50 .32 9.9 40 error (invalid witness file) 6.8 3.6 120 320
heap-manipulation/merge_sort_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   850   12000 1500 2.3 0     - - error (invalid witness file) .53 .34 12   42 error (invalid witness file) 6.2 3.3 120 300
heap-manipulation/sll_to_dll_rev_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   680   8900 8500 2.5 0     - - error (invalid witness file) .53 .36 11   40 error (invalid witness file) 6.1 3.3 120 300
heap-manipulation/tree_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   370   5400 13000 2.3 0     error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.0 3.2 130 310 - -
heap-manipulation/tree_false-valid-deref.i false(valid-deref) 1 wit inspect 6.7 2.1 50 360 2.5 0     false(valid-deref) 4.8  2.6  47   270 true 9.6 5.1 190 350 - -
heap-manipulation/dancing_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   800   10000 1500 2.3 0     error (invalid witness file) .54 .35 13   40 error (invalid witness file) 5.8 3.2 120 310 - -
forester-heap/dll-rb-sentinel_false-unreach-call_false-valid-memtrack.i error 0 wit inspect 8.6 2.7 60 300 2.6 0     error (invalid witness file) .50 .32 13   40 error (invalid witness file) 5.9 3.1 120 300 - -
forester-heap/dll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 910   250   4400 14000 2.3 0     error (invalid witness file) .52 .32 9.0 41 error (invalid witness file) 6.7 3.5 91 300 - -
forester-heap/sll-simple-white-blue_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   750   6100 7600 2.5 0     error (invalid witness file) .53 .34 9.4 40 error (invalid witness file) 6.1 3.2 120 300 - -
list-properties/alternating_list_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   720   7300 6400 2.3 0     - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 6.4 3.4 75 310
list-properties/list_flag_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 13   4.2 97 350 2.6 0     error (invalid witness file) .51 .33 12   40 error (invalid witness file) 6.0 3.2 120 300 - -
list-properties/list_search_true-unreach-call_false-valid-memtrack.i timeout 0 wit inspect 900   850   8800 4400 2.3 0     error (invalid witness file) .55 .36 11   43 error (invalid witness file) 6.4 3.4 130 300 - -
list-properties/list_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 21   7.3 170 510 2.6 0     error (invalid witness file) .54 .34 12   41 error (invalid witness file) 6.3 3.3 140 300 - -
list-properties/simple_built_from_end_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 15   4.6 110 400 2.6 0     error (invalid witness file) .51 .33 9.4 40 error (invalid witness file) 6.0 3.1 120 300 - -
list-properties/simple_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 20   6.6 160 470 2.6 0     error (invalid witness file) .52 .34 12   39 error (invalid witness file) 6.9 3.7 93 290 - -
list-properties/splice_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 14   4.4 110 360 2.9 0     error (invalid witness file) .50 .33 8.6 40 error (invalid witness file) 6.0 3.2 120 300 - -
ddv-machzwd/ddv_machzwd_all_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 320   270   1500 1600 3.2 0     - - true 9.2  4.8  180   320 true 220   180   1500 1800
ddv-machzwd/ddv_machzwd_inw_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 290   240   1500 1600 3.2 0     - - true 9.4  4.9  180   310 true 200   160   1800 1700
ddv-machzwd/ddv_machzwd_outb_false-unreach-call_true-valid-memsafety.i true 2 wit inspect 290   240   1700 1600 3.2 0     - - true 9.2  4.8  170   320 true 200   160   1300 1700
ddv-machzwd/ddv_machzwd_inb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 480   400   4300 1600 2.5 0     error (invalid witness file) .49 .31 9.2 39 error (invalid witness file) 6.5 3.4 130 310 - -
ddv-machzwd/ddv_machzwd_inb_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 480   390   3200 1700 2.5 0     error (invalid witness file) .52 .34 12   40 error (invalid witness file) 7.0 3.7 130 310 - -
ddv-machzwd/ddv_machzwd_inl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 470   400   2900 1900 2.5 0     error (invalid witness file) .66 .42 8.1 42 error (invalid witness file) 6.8 3.5 130 290 - -
ddv-machzwd/ddv_machzwd_inl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 480   400   3300 1600 2.5 0     error (invalid witness file) .53 .34 11   40 error (invalid witness file) 6.6 3.4 130 300 - -
ddv-machzwd/ddv_machzwd_inw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 480   400   3800 1600 2.5 0     error (invalid witness file) .48 .31 12   39 error (invalid witness file) 6.5 3.5 130 310 - -
ddv-machzwd/ddv_machzwd_outb_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 470   390   3800 1600 2.5 0     error (invalid witness file) .53 .34 11   40 error (invalid witness file) 6.1 3.2 130 290 - -
ddv-machzwd/ddv_machzwd_outl_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 470   390   3200 1700 2.5 0     error (invalid witness file) .55 .35 13   40 error (invalid witness file) 6.2 3.3 120 300 - -
ddv-machzwd/ddv_machzwd_outl_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 470   390   3000 1700 2.5 0     error (invalid witness file) .49 .31 12   39 error (invalid witness file) 6.9 3.6 120 300 - -
ddv-machzwd/ddv_machzwd_outw_p_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 470   390   3600 1500 2.5 0     error (invalid witness file) .53 .35 12   39 error (invalid witness file) 6.9 3.6 130 310 - -
ddv-machzwd/ddv_machzwd_pthread_mutex_unlock_true-unreach-call_false-valid-memtrack.i unknown 0 wit inspect 470   390   3500 1600 2.5 0     error (invalid witness file) .59 .38 9.1 41 error (invalid witness file) 6.1 3.2 130 290 - -
forester-heap/dll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   540   7200 11000 2.3 0     - - error (invalid witness file) .50 .34 11   43 error (invalid witness file) 5.9 3.2 130 300
forester-heap/dll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   12000 700 2.3 0     - - error (invalid witness file) .60 .39 8.4 41 error (invalid witness file) 5.9 3.1 92 300
forester-heap/dll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   860   9500 2400 2.3 0     - - error (invalid witness file) .48 .31 8.0 39 error (invalid witness file) 5.9 3.1 130 290
forester-heap/dll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   560   7900 8900 2.3 0     - - error (invalid witness file) .51 .34 12   41 error (invalid witness file) 6.2 3.3 120 310
forester-heap/dll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   460   5500 12000 2.3 0     - - error (invalid witness file) .53 .34 12   43 error (invalid witness file) 6.0 3.2 120 300
forester-heap/dll-rb-sentinel_true-unreach-call_true-valid-memsafety.i error 0 wit inspect 8.2 2.7 66 310 2.6 0     - - error (invalid witness file) .54 .35 11   41 error (invalid witness file) 6.0 3.2 120 300
forester-heap/dll-reverse_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   430   5200 12000 2.3 0     - - error (invalid witness file) .52 .34 11   42 error (invalid witness file) 6.1 3.2 120 300
forester-heap/dll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   860   12000 1600 2.3 0     - - error (invalid witness file) .54 .35 13   42 error (invalid witness file) 6.1 3.2 94 310
forester-heap/dll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   250   4500 14000 2.3 0     - - error (invalid witness file) .56 .36 12   40 error (invalid witness file) 6.2 3.2 120 300
forester-heap/sll-01_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   860   8600 2200 2.7 0     - - error (invalid witness file) .50 .31 12   39 error (invalid witness file) 6.2 3.3 130 300
forester-heap/sll-buckets_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 910   170   3500 13000 2.3 0     - - error (invalid witness file) .53 .33 8.8 41 error (invalid witness file) 6.0 3.2 130 300
forester-heap/sll-circular_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   13000 1100 2.3 0     - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 8.2 4.3 99 300
forester-heap/sll-optional_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   11000 2000 2.3 0     - - error (invalid witness file) .51 .35 12   40 error (invalid witness file) 6.1 3.2 110 300
forester-heap/sll-queue_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   860   7000 1100 2.3 0     - - error (invalid witness file) .55 .36 13   40 error (invalid witness file) 6.4 3.4 130 290
forester-heap/sll-rb-cnstr_1_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   8100 2000 2.3 0     - - error (invalid witness file) .50 .33 11   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.0 2.6 61 310 2.6 0     - - error (invalid witness file) .50 .34 5.5 39 error (invalid witness file) 6.5 3.5 140 300
forester-heap/sll-reverse_simple_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   830   6000 4700 2.3 0     - - error (invalid witness file) .54 .36 12   39 error (invalid witness file) 6.6 3.5 140 310
forester-heap/sll-sorted_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   870   8700 2100 2.4 0     - - error (invalid witness file) .51 .32 12   40 error (invalid witness file) 7.2 3.8 92 290
forester-heap/sll-token_true-unreach-call_true-valid-memsafety.i timeout 0 wit inspect 900   680   6000 8100 2.3 .033 - - error (invalid witness file) .53 .35 12   39 error (invalid witness file) 6.3 3.3 130 310
forester-heap/dll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 900   620   9800 8300 2.3 0     error (invalid witness file) .50 .32 11   40 error (invalid witness file) 5.7 3.0 110 290 - -
forester-heap/sll-01_false-unreach-call_false-valid-deref.i false(valid-deref) 1 wit inspect 130   110   1600 650 2.5 0     true 5.4  2.9  70   280 true 19   10   290 490 - -
forester-heap/sll-rb-cnstr_1_false-unreach-call_false-valid-deref.i timeout 0 wit inspect 910   540   6700 11000 2.3 0     error (invalid witness file) .48 .31 11   39 error (invalid witness file) 5.9 3.2 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 8 32000 25000 280000 210000 130   .033 52 22 13   370 1500   52 170 92 3300 7800   52 40 23 800 1900   52 770 580 7500 12000  
    correct results 5 8 1000 860 6500 5800 15   0     2 10 5.5 120 550   2 29 15 480 840   3 28 15 530 960   3 620 500 4600 5100  
        correct true 3 6 890 750 4800 4800 9.5 0     1 0 0   0 0   2 0 0 0 0   3 28 15 530 960   3 620 500 4600 5100  
        correct false 2 2 140 120 1700 1000 5.0 0     1 10 5.5 120 550   0 29 15 480 840   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) 8
Run set sv-comp17.MemSafety-LinkedLists