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 CPA-witness2test 1.6.1-svn 26773 CProver witness2test 0.1 CPAchecker 1.6.1-svn 26773 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*
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]
Date of execution 2017-11-30 16:01:31 CET 2017-12-01 08:31:47 CET 2017-12-01 08:56:50 CET 2017-12-01 08:59:39 CET 2017-12-01 09:01:39 CET 2017-12-01 08:10:33 CET 2017-12-01 08:38:18 CET
Run set depthk.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-ControlFlow
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.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-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witness2test -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop analysis.summaryEdges=true -setprop cpa.callstack.skipVoidRecursion=true -setprop cpa.callstack.skipFunctionPointerRecursion=true --graphml-witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-11-30_1601.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml -setprop cpa.predicate.memoryAllocationsAlwaysSucceed=true --full-output --validate ../../results-verified/depthk.2017-11-30_1601.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 status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
ntdrivers-simplified/cdaudio_simpl1_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 3.3  88 46   -32 7.1  270 -32 8.8   420   0 4.9  270 1 .89   19    - -
ntdrivers-simplified/floppy_simpl3_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 1.6  94 23   -32 3.8  270 -32 7.7   330   0 4.3  220 1 .78   19    - -
ntdrivers-simplified/floppy_simpl4_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 2.6  100 32   -32 6.2  270 -32 6.0   390   0 4.9  270 1 .82   19    - -
ntdrivers-simplified/kbfiltr_simpl2_false-unreach-call_true-valid-memsafety_true-termination.cil.c 1 1.2  63 15   -32 5.3  260 -32 6.8   310   0 4.0  220 1 .74   19    - -
ntdrivers-simplified/cdaudio_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 18    350 190   - - - - 2 11    520 2 98     1200  
ntdrivers-simplified/diskperf_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 0 140    100 1700   - - - - 0 .69 42 0 .019 4.8
ntdrivers-simplified/floppy_simpl3_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 10    350 89   - - - - 2 8.4  360 2 73     880  
ntdrivers-simplified/floppy_simpl4_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 13    370 120   - - - - 2 8.0  460 2 70     930  
ntdrivers-simplified/kbfiltr_simpl1_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 5.3  270 47   - - - - 2 5.6  260 2 17     500  
ntdrivers-simplified/kbfiltr_simpl2_true-unreach-call_true-valid-memsafety_true-termination.cil.c 2 7.1  290 75   - - - - 2 5.1  270 2 17     530  
ssh-simplified/s3_clnt_1_false-unreach-call_true-termination.cil.c 1 20    92 320   -32 5.1  270 -32 6.7   280   0 3.8  220 1 .73   19    - -
ssh-simplified/s3_clnt_2_false-unreach-call_true-termination.cil.c 1 20    85 260   -32 4.8  270 -32 6.4   280   0 3.8  220 1 .75   19    - -
ssh-simplified/s3_clnt_3_false-unreach-call_true-termination.cil.c 0 24    95 390   -32 5.1  270 -32 6.2   290   0 2.7  220 0 .73   19    - -
ssh-simplified/s3_clnt_4_false-unreach-call_true-termination.cil.c 1 21    85 290   -32 5.1  270 -32 6.5   290   0 2.5  220 1 .72   19    - -
ssh-simplified/s3_srvr_10_false-unreach-call_false-termination.cil.c 1 4.0  87 49   -32 5.1  270 -32 6.6   290   0 4.1  230 1 .75   19    - -
ssh-simplified/s3_srvr_11_false-unreach-call_false-termination.cil.c 1 24    88 330   -32 5.2  270 -32 6.4   280   0 4.1  220 1 .76   19    - -
ssh-simplified/s3_srvr_12_false-unreach-call_false-termination.cil.c 1 42    98 620   -32 5.3  270 -32 6.3   280   0 4.0  220 1 .77   19    - -
ssh-simplified/s3_srvr_13_false-unreach-call_false-termination.cil.c 1 16    94 200   -32 5.3  270 -32 6.8   280   0 4.1  220 1 .72   18    - -
ssh-simplified/s3_srvr_14_false-unreach-call_false-termination.cil.c 1 14    90 170   -32 3.3  270 -32 6.9   280   0 3.8  220 1 .78   19    - -
ssh-simplified/s3_srvr_1_false-unreach-call_false-termination.cil.c 1 21    320 280   -32 4.9  270 -32 6.1   270   0 3.8  220 1 .73   19    - -
ssh-simplified/s3_srvr_2_false-unreach-call_false-termination.cil.c 1 10    89 120   -32 4.8  270 -32 6.4   280   0 3.8  220 1 .73   19    - -
ssh-simplified/s3_srvr_6_false-unreach-call_false-termination.cil.c 1 14    92 180   -32 5.1  270 -32 6.5   280   0 4.0  220 1 .68   19    - -
ssh-simplified/s3_clnt_1_true-unreach-call_true-termination.cil.c 2 150    1300 1800   - - - - 2 11    510 2 35     950  
ssh-simplified/s3_clnt_2_true-unreach-call_true-termination.cil.c 2 150    1300 1900   - - - - 2 12    510 2 37     1100  
ssh-simplified/s3_clnt_3_true-unreach-call_true-termination.cil.c 2 180    1300 2000   - - - - 2 12    410 2 39     1200  
ssh-simplified/s3_clnt_4_true-unreach-call_true-termination.cil.c 2 160    1300 2300   - - - - 2 10    390 2 46     1100  
ssh-simplified/s3_srvr_1_true-unreach-call_false-termination.cil.c 0 890    470 10000   - - - - 0 .56 44 0 .020 4.8
ssh-simplified/s3_srvr_1a_true-unreach-call_false-termination.cil.c 0 370    110 4800   - - - - 0 .54 43 0 .018 4.8
ssh-simplified/s3_srvr_1b_true-unreach-call_false-termination.cil.c 0 120    77 1600   - - - - 0 .54 41 0 .019 4.8
ssh-simplified/s3_srvr_2_true-unreach-call_false-termination.cil.c 2 44    2300 470   - - - - 0 910    5200 2 45     1100  
ssh-simplified/s3_srvr_3_true-unreach-call_false-termination.cil.c 0 890    460 10000   - - - - 0 .64 43 0 .022 4.9
ssh-simplified/s3_srvr_4_true-unreach-call_false-termination.cil.c 0 890    460 14000   - - - - 0 .58 43 0 .018 4.8
ssh-simplified/s3_srvr_6_true-unreach-call_false-termination.cil.c 0 890    450 13000   - - - - 0 .70 46 0 .020 4.9
ssh-simplified/s3_srvr_7_true-unreach-call_false-termination.cil.c 0 890    470 11000   - - - - 0 .61 41 0 .018 4.9
ssh-simplified/s3_srvr_8_true-unreach-call_false-termination.cil.c 2 49    2300 590   - - - - 0 900    4900 2 41     1100  
locks/test_locks_14_false-unreach-call_true-valid-memsafety_false-termination.c 1 .48 79 6.1 -32 3.5  260 -32 5.3   240   0 3.4  210 1 .65   18    - -
locks/test_locks_15_false-unreach-call_true-valid-memsafety_false-termination.c 1 .50 79 6.5 -32 3.6  260 -32 5.2   240   0 3.3  220 1 .65   19    - -
locks/test_locks_10_true-unreach-call_true-valid-memsafety_false-termination.c 2 30    1300 300   - - - - 2 6.5  280 2 16     680  
locks/test_locks_11_true-unreach-call_true-valid-memsafety_false-termination.c 2 89    2200 1200   - - - - 2 4.8  280 2 18     980  
locks/test_locks_12_true-unreach-call_true-valid-memsafety_false-termination.c 2 160    2300 2000   - - - - 2 6.7  280 2 29     2100  
locks/test_locks_13_true-unreach-call_true-valid-memsafety_false-termination.c 2 160    2300 1900   - - - - 2 4.9  290 2 40     3600  
locks/test_locks_14_true-unreach-call_true-valid-memsafety_false-termination.c 2 160    2200 1800   - - - - 2 6.4  280 2 67     6200  
locks/test_locks_15_true-unreach-call_true-valid-memsafety_false-termination.c 2 160    2200 2100   - - - - 2 5.5  290 0 97     7000  
locks/test_locks_5_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.3  260 44   - - - - 2 4.6  270 2 7.1   280  
locks/test_locks_6_true-unreach-call_true-valid-memsafety_false-termination.c 2 4.9  270 50   - - - - 2 5.0  280 2 8.5   320  
locks/test_locks_7_true-unreach-call_true-valid-memsafety_false-termination.c 2 6.3  300 62   - - - - 2 6.0  280 2 9.4   380  
locks/test_locks_8_true-unreach-call_true-valid-memsafety_false-termination.c 2 9.5  450 80   - - - - 2 5.4  280 2 11     500  
locks/test_locks_9_true-unreach-call_true-valid-memsafety_false-termination.c 2 14    720 140   - - - - 2 5.8  280 2 13     490  
ntdrivers/cdaudio_false-unreach-call.i.cil.c 0 890    350 11000   0 .52 43 0 .018 4.8 0 .84 47 0 .0013 .29 - -
ntdrivers/diskperf_false-unreach-call.i.cil.c 0 480    170 6900   0 92    2100 -32 13     470   0 5.5  280 0 96      19    - -
ntdrivers/floppy_false-unreach-call.i.cil.c 0 590    830 7000   -32 11    430 -32 25     570   0 6.5  290 0 96      19    - -
ntdrivers/kbfiltr_false-unreach-call.i.cil.c 0 890    540 9700   0 .54 43 0 .020 5.0 0 .91 49 0 .0014 .29 - -
ntdrivers/parport_false-unreach-call.i.cil.c 0 590    960 7900   0 7.5  290 -32 27     700   0 7.0  290 0 1.5    22    - -
ntdrivers/cdaudio_true-unreach-call.i.cil.c 0 900    350 11000   - - - - 0 .58 44 0 .019 4.8
ntdrivers/diskperf_true-unreach-call.i.cil.c 0 640    170 8400   - - - - 0 .53 43 0 .019 4.8
ntdrivers/floppy2_true-unreach-call_true-termination.i.cil.c 0 890    14000 13000   - - - - 0 .57 44 0 .019 4.8
ntdrivers/floppy_true-unreach-call_true-valid-memsafety.i.cil.c 0 890    1300 8700   - - - - 0 .61 43 0 .019 4.9
ntdrivers/parport_true-unreach-call.i.cil.c 0 890    2000 11000   - - - - 0 .67 42 0 .019 4.9
ssh/s3_clnt.blast.01_false-unreach-call.i.cil.c 0 890    1600 8200   0 .57 44 0 .018 4.8 0 .85 50 0 .0013 .29 - -
ssh/s3_clnt.blast.02_false-unreach-call.i.cil.c 0 890    1600 8500   0 .53 44 0 .019 5.0 0 .85 49 0 .0014 .26 - -
ssh/s3_clnt.blast.03_false-unreach-call.i.cil.c 0 890    1600 11000   0 .58 43 0 .020 4.9 0 .66 49 0 .0013 .26 - -
ssh/s3_clnt.blast.04_false-unreach-call.i.cil.c 0 890    1600 10000   0 .51 43 0 .020 4.8 0 .85 48 0 .0015 .29 - -
ssh/s3_srvr.blast.01_false-unreach-call.i.cil.c 0 340    1000 4600   -32 5.4  260 -32 8.4   330   0 4.4  260 0 .78   19    - -
ssh/s3_srvr.blast.02_false-unreach-call.i.cil.c 0 440    1000 5400   -32 5.6  260 -32 8.6   330   0 4.2  260 0 .79   19    - -
ssh/s3_srvr.blast.03_false-unreach-call.i.cil.c 0 460    1000 5200   -32 5.4  260 -32 8.7   330   0 3.9  240 0 .79   19    - -
ssh/s3_srvr.blast.04_false-unreach-call.i.cil.c 0 350    1000 3600   -32 5.3  270 -32 8.5   330   0 4.0  220 0 .78   19    - -
ssh/s3_srvr.blast.06_false-unreach-call.i.cil.c 0 890    1200 9100   0 .59 43 0 .018 5.0 0 .85 49 0 .0013 .29 - -
ssh/s3_srvr.blast.07_false-unreach-call.i.cil.c 0 890    1700 9100   0 .40 44 0 .019 4.8 0 .88 49 0 .0014 .29 - -
ssh/s3_srvr.blast.08_false-unreach-call.i.cil.c 0 890    1500 9100   0 .54 44 0 .018 4.8 0 .87 47 0 .0013 .29 - -
ssh/s3_srvr.blast.09_false-unreach-call.i.cil.c 0 890    1700 7700   0 .52 43 0 .019 4.8 0 .89 47 0 .0013 .27 - -
ssh/s3_srvr.blast.10_false-unreach-call.i.cil.c 0 890    1700 8500   0 .57 46 0 .020 4.9 0 .90 50 0 .0012 .32 - -
ssh/s3_srvr.blast.11_false-unreach-call.i.cil.c 0 700    1300 7000   -32 3.6  270 -32 8.4   330   0 4.2  260 0 .78   19    - -
ssh/s3_srvr.blast.12_false-unreach-call.i.cil.c 0 890    1300 9400   0 .54 43 0 .020 4.9 0 .89 48 0 .0015 .26 - -
ssh/s3_srvr.blast.13_false-unreach-call.i.cil.c 0 840    1600 8600   -32 5.3  260 -32 8.1   330   0 4.2  260 0 .78   19    - -
ssh/s3_srvr.blast.14_false-unreach-call.i.cil.c 0 890    1300 9300   0 .40 43 0 .019 4.9 0 .84 47 0 .0012 .34 - -
ssh/s3_srvr.blast.15_false-unreach-call.i.cil.c 0 890    1500 8400   0 .50 43 0 .019 4.9 0 .86 47 0 .0013 .26 - -
ssh/s3_srvr.blast.16_false-unreach-call.i.cil.c 0 890    1300 8800   0 .41 44 0 .020 4.9 0 .88 49 0 .0011 .34 - -
ssh/s3_clnt.blast.01_true-unreach-call.i.cil.c 0 890    1600 12000   - - - - 0 .54 42 0 .019 5.0
ssh/s3_clnt.blast.02_true-unreach-call.i.cil.c 0 890    1600 9000   - - - - 0 .61 43 0 .020 4.9
ssh/s3_clnt.blast.03_true-unreach-call.i.cil.c 0 890    1600 11000   - - - - 0 .54 42 0 .020 5.0
ssh/s3_clnt.blast.04_true-unreach-call.i.cil.c 0 890    1600 9500   - - - - 0 .56 43 0 .019 4.9
ssh/s3_srvr.blast.01_true-unreach-call.i.cil.c 0 890    1700 8700   - - - - 0 .52 41 0 .018 4.9
ssh/s3_srvr.blast.02_true-unreach-call.i.cil.c 0 890    1700 12000   - - - - 0 .53 43 0 .019 4.9
ssh/s3_srvr.blast.06_true-unreach-call.i.cil.c 0 890    1500 9300   - - - - 0 .54 45 0 .021 4.9
ssh/s3_srvr.blast.07_true-unreach-call.i.cil.c 0 890    1600 7500   - - - - 0 .53 41 0 .041 4.8
ssh/s3_srvr.blast.08_true-unreach-call.i.cil.c 0 890    1700 9000   - - - - 0 .59 43 0 .021 4.9
ssh/s3_srvr.blast.09_true-unreach-call.i.cil.c 0 890    1700 12000   - - - - 0 .52 42 0 .020 5.0
ssh/s3_srvr.blast.10_true-unreach-call.i.cil.c 0 890    1700 9700   - - - - 0 .55 44 0 .020 5.0
ssh/s3_srvr.blast.11_true-unreach-call.i.cil.c 0 890    1700 11000   - - - - 0 .52 41 0 .018 4.8
ssh/s3_srvr.blast.12_true-unreach-call.i.cil.c 0 890    1600 8400   - - - - 0 .72 44 0 .019 4.8
ssh/s3_srvr.blast.13_true-unreach-call.i.cil.c 0 890    1700 8700   - - - - 0 .62 41 0 .019 4.9
ssh/s3_srvr.blast.14_true-unreach-call.i.cil.c 0 890    1500 8300   - - - - 0 .54 43 0 .019 5.0
ssh/s3_srvr.blast.15_true-unreach-call.i.cil.c 0 890    1700 9500   - - - - 0 .54 45 0 .022 4.9
ssh/s3_srvr.blast.16_true-unreach-call.i.cil.c 0 890    1500 8100   - - - - 0 .68 44 0 .019 4.8
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 status score witness inspect witness cpu (s) mem (MB) energy status score witness inspect witness cpu (s) mem (MB) energy
total 94 61 45000 100000 500000 42 -800 240 9800 42 -864 230 9100 42 0 130 7100 42 17 210 520 52 40 2000 18000 52 42 830 33000
    correct results 39 61 1800 27000 22000 0 0 0 17 17 13 320 20 40 140 6800 21 42 740 26000
        correct true 22 44 1600 26000 19000 0 0 0 0 20 40 140 6800 21 42 740 26000
        correct false 17 17 220 1700 2900 0 0 0 17 17 13 320 0 0
    correct-unconfimed results 10 0 4800 9000 57000 0 0 0 0 0 0
        correct-unconfirmed true 0 0 0 0 0 0 0
        correct-unconfirmed false 10 0 4800 9000 57000 0 0 0 0 0 0
    incorrect results 0 25 -800 130 6900 27 -864 230 9000 0 0 0 0
        incorrect true 0 25 -800 130 6900 27 -864 230 9000 0 0 0 0
        incorrect false 0 0 0 0 0 0 0
score (94 tasks, max score: 146) 61 -800 -864 0 17 40 42
Run set depthk.sv-comp18.ReachSafety-ControlFlow cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ControlFlow uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ControlFlow fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-ControlFlow cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-ControlFlow uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-ControlFlow