Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017
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:51:53 CET [[ 2017-01-15 00:05:22 CET ]] [[ 2017-01-15 00:31:32 CET ]] [[ 2017-01-15 00:11:25 CET ]] [[ 2017-01-15 00:39:18 CET ]]
Run set sv-comp17.MemSafety-Other
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0451.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0451.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)
loop-acceleration/array3_false-valid-deref.i unknown 0 wit inspect 53 53   690 28 260    0   error (invalid witness file) .53 .34 11 40 error (invalid witness file) 5.9 3.2 110 300 - -
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 130 130   1000 790 .86 0   true 12    6.3  170 390 unknown 8.2 4.3 150 310 - -
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 1 wit inspect 750 760   6400 1100 1.0  0   true 7.2  3.8  110 280 unknown 6.8 3.6 110 300 - -
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 79 54   780 4000 5.0  0   - - true 39   23   340 2300 true 12   6.6 180 460
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 74 52   810 4000 4.4  0   - - true 38   21   450 2400 true 13   6.9 210 460
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900 840   12000 4800 3.5  0   - - out of memory 250   140   1900 7000 true 10   5.4 150 340
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 270 160   380 4000 3.6  0   - - true 47   29   470 2800 true 9.7 5.2 170 320
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 67 41   670 3900 4.2  0   - - true 44   26   520 2700 true 9.7 5.2 150 330
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 130 86   1200 4300 4.3  0   - - true 74   45   820 3700 true 10   5.4 190 370
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 130 86   1400 4300 4.3  0   - - true 72   44   620 3500 true 10   5.5 170 370
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 39 15   43 460 3.5  0   - - true 9.3 4.9 110 350 true 9.4 4.9 130 340
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 23 9.9 230 1900 4.2  0   - - true 20   10   320 1000 true 9.0 4.9 170 320
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 23 10   220 1800 4.2  0   - - true 26   13   210 1000 true 9.1 4.8 140 320
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 720   12000 7100 4.0  0   - - timeout 910   810   14000 7000 true 7.5 4.0 120 320
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910 740   11000 7100 4.0  0   - - timeout 910   780   8900 7000 true 7.4 4.0 140 310
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910 770   1600 4600 3.4  0   - - out of memory 740   610   12000 7000 true 8.2 4.3 140 330
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 740   12000 7000 4.0  0   - - out of memory 740   600   9600 7000 true 7.7 4.1 140 320
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 860   15000 3700 4.0  0   - - out of memory 660   570   7300 7000 true 7.8 4.2 130 320
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 750   13000 6900 4.0  0   - - timeout 940   810   12000 7000 true 8.1 4.3 160 320
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 860   13000 3200 3.4  0   - - timeout 910   840   12000 6100 true 8.3 4.4 160 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 750   10000 6600 3.4  0   - - timeout 910   840   11000 6100 true 8.1 4.4 140 320
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 680   10000 8100 3.4  0   - - out of memory 860   760   15000 7000 true 7.2 3.9 150 310
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910 610   9400 8800 3.4  0   - - timeout 910   800   12000 6800 true 7.5 4.0 150 320
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 610   9400 8400 4.0  0   - - timeout 910   830   14000 6400 true 7.2 3.9 120 320
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 690   12000 8300 4.0  0   - - timeout 910   830   13000 6300 true 7.2 3.9 150 310
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900 680   10000 7500 4.0  0   - - timeout 910   810   10000 6800 true 7.2 3.9 160 310
../../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 26 20 14000 12000 170000 120000 350   0   26 20 10 290 710   26 21 11   370 910   26 12000 10000 160000 110000   26 200 110 3500 7800  
    correct results 11 20 1700 1400 13000 31000 40   0   2 19 10 270 670   0 15 7.9 260 620   9 370 220 3900 20000   9 92 50 1500 3300  
        correct true 9 18 840 520 5800 29000 38   0   2 0 0 0 0   0 0 0   0 0   9 370 220 3900 20000   9 92 50 1500 3300  
        correct false 2 2 880 880 7400 1900 1.9 0   0 19 10 270 670   0 15 7.9 260 620   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 (26 tasks, max score: 49) 20
Run set sv-comp17.MemSafety-Other