Tool DepthK DepthK version 3.0 - Fri Jan 6 18:14:20 AMT 2017 CPAchecker 1.6.1-svn 26773 ULTIMATE Automizer 0.1.23-3204b741 CProver witness2test 0.1 ULTIMATE Automizer 0.1.23-3204b741
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8 timelimit: 90 s, memlimit: 7000 MB, CPU core limit: 2 timelimit: 900 s, memlimit: 7000 MB, CPU core limit: 2
Host apollon* [apollon023; apollon077; apollon078; apollon117; apollon126] [apollon077; apollon078; apollon101; apollon157] [apollon045; apollon077; apollon078; apollon158] [apollon007; apollon009; apollon077; apollon078; apollon119]
OS Linux 4.4.0-101-generic
System CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: 8, frequency: 3.8 GHz, Turbo Boost: disabled; RAM: 33553 MB CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [4; 8], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33554 MB; 33553 MB] CPU: Intel Xeon E3-1230 v5 @ 3.40 GHz, cores: [8; 4], frequency: 3.8 GHz, Turbo Boost: disabled; RAM: [33553 MB; 33554 MB]
Date of execution 2017-12-01 09:05:19 CET 2017-12-01 09:58:48 CET 2017-12-01 10:19:41 CET 2017-12-01 10:22:00 CET 2017-12-01 10:02:39 CET
Run set depthk.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.MemSafety-Other
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true -setprop cpa.smg.memoryAllocationFunctions=malloc,__kmalloc,kmalloc,kzalloc,kzalloc_node,ldv_zalloc,ldv_malloc -setprop cpa.smg.arrayAllocationFunctions=calloc,kmalloc_array,kcalloc -setprop cpa.smg.zeroingMemoryAllocation=calloc,kzalloc,kcalloc,kzalloc_node,ldv_zalloc -setprop cpa.smg.deallocationFunctions=free,kfree,kfree_const --full-output --validate ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2017-12-01_0905.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
loop-acceleration/array3_false-valid-deref.i unknown 0 wit inspect 54   27 680 error (invalid witness file) 0 wit inspect .56 43 error (2) 0 wit inspect .020 4.8 error (invalid witness file) 0 wit inspect .0011 .29 - wit inspect
ntdrivers/floppy_false-valid-deref.i.cil.c false(valid-deref) 0 wit inspect 130   790 940 true -32 wit inspect 5.0  470 unknown 0 wit inspect 4.7   220   timeout 0 wit inspect 96      19    - wit inspect
ntdrivers/kbfiltr_false-valid-deref.i.cil.c false(valid-deref) 0 wit inspect 740   1100 7100 true -32 wit inspect 5.1  260 unknown 0 wit inspect 2.8   210   error (2) 0 wit inspect .90   19    - wit inspect
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 75   4000 930 - wit inspect - wit inspect - wit inspect true 2 wit inspect 13   470
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 79   3900 950 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.4 440
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c timeout 0 wit inspect 900   4800 14000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 320
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 68   4000 680 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2 300
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 66   4000 640 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 310
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 130   4400 1200 - wit inspect - wit inspect - wit inspect true 2 wit inspect 8.6 350
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 130   4300 1200 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.7 340
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 9.3 610 80 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4 270
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 24   2000 210 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 300
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c true 2 wit inspect 23   1800 210 - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.4 280
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   7100 11000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 240
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   7200 11000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3 250
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   7100 11000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.8 230
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   7000 10000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0 220
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   3800 13000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1 250
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   6800 10000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 240
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   3700 12000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.6 240
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   6700 9900 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.3 230
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   8300 9200 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.3 230
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   9100 10000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 230
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 910   8400 9100 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 230
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   8300 11000 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9 230
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c timeout 0 wit inspect 900   7700 9900 - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.1 220
sv-benchmarks/c/ status score witness inspect witness cpu (s) mem (MB) energy (J) status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 26 18 14000 130000 170000 3 -64 11 770 3 0 7.5 440 3 0 97 38 23 46 130 6400
    correct results 9 18 600 29000 6100 0 0 0 23 46 130 6400
        correct true 9 18 600 29000 6100 0 0 0 23 46 130 6400
        correct false 0 0 0 0 0
    correct-unconfimed results 2 0 870 1900 8000 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0
        correct-unconfirmed false 2 0 870 1900 8000 0 0 0 0
    incorrect results 0 2 -64 10 730 0 0 0
        incorrect true 0 2 -64 10 730 0 0 0
        incorrect false 0 0 0 0 0
score (26 tasks, max score: 49) 18 -64 0 0 46
Run set depthk.sv-comp18.MemSafety-Other cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Other fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.MemSafety-Other uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.MemSafety-Other