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 0 53 53   690 28 260    0   .53 .34 11 40 5.9 3.2 110 300
ntdrivers/floppy_false-valid-deref.i.cil.c 1 130 130   1000 790 .86 0   12    6.3  170 390 8.2 4.3 150 310
ntdrivers/kbfiltr_false-valid-deref.i.cil.c 1 750 760   6400 1100 1.0  0   7.2  3.8  110 280 6.8 3.6 110 300
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 79 54   780 4000 5.0  0   39   23   340 2300 12   6.6 180 460
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 74 52   810 4000 4.4  0   38   21   450 2400 13   6.9 210 460
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 900 840   12000 4800 3.5  0   250   140   1900 7000 10   5.4 150 340
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 270 160   380 4000 3.6  0   47   29   470 2800 9.7 5.2 170 320
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 67 41   670 3900 4.2  0   44   26   520 2700 9.7 5.2 150 330
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 130 86   1200 4300 4.3  0   74   45   820 3700 10   5.4 190 370
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 130 86   1400 4300 4.3  0   72   44   620 3500 10   5.5 170 370
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 39 15   43 460 3.5  0   9.3 4.9 110 350 9.4 4.9 130 340
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 2 23 9.9 230 1900 4.2  0   20   10   320 1000 9.0 4.9 170 320
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 23 10   220 1800 4.2  0   26   13   210 1000 9.1 4.8 140 320
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 0 900 720   12000 7100 4.0  0   910   810   14000 7000 7.5 4.0 120 320
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 0 910 740   11000 7100 4.0  0   910   780   8900 7000 7.4 4.0 140 310
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 0 910 770   1600 4600 3.4  0   740   610   12000 7000 8.2 4.3 140 330
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 0 900 740   12000 7000 4.0  0   740   600   9600 7000 7.7 4.1 140 320
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 0 900 860   15000 3700 4.0  0   660   570   7300 7000 7.8 4.2 130 320
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 0 900 750   13000 6900 4.0  0   940   810   12000 7000 8.1 4.3 160 320
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 0 900 860   13000 3200 3.4  0   910   840   12000 6100 8.3 4.4 160 320
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 0 900 750   10000 6600 3.4  0   910   840   11000 6100 8.1 4.4 140 320
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 0 900 680   10000 8100 3.4  0   860   760   15000 7000 7.2 3.9 150 310
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 0 910 610   9400 8800 3.4  0   910   800   12000 6800 7.5 4.0 150 320
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 0 900 610   9400 8400 4.0  0   910   830   14000 6400 7.2 3.9 120 320
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 0 900 690   12000 8300 4.0  0   910   830   13000 6300 7.2 3.9 150 310
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 0 900 680   10000 7500 4.0  0   910   810   10000 6800 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