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-BitVectors cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-BitVectors
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
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i false(unreach-call) 1 wit inspect 2.2  110 33   true -32 wit inspect 6.6  420 true -32 wit inspect 5.9   250   unknown 0 wit inspect 3.1  210 false(unreach-call) 1 wit inspect .67   19    - wit inspect - wit inspect
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 70    75 990   error (invalid witness file) 0 wit inspect .54 41 error (2) 0 wit inspect .019 5.0 error (invalid witness file) 0 wit inspect .87 49 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 74    1700 820   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.2  330 timeout 0 wit inspect 960     1100  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 28    910 330   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 10    340 timeout 0 wit inspect 960     1100  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 490    310 7300   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.0  300 timeout 0 wit inspect 960     710  
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 230    280 3000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    460 timeout 0 wit inspect 960     1100  
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 470    330 5000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 160    460 timeout 0 wit inspect 960     1000  
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i true 2 wit inspect 490    260 6000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.5  300 true 2 wit inspect 36     570  
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 16    410 190   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.0  310 true 2 wit inspect 140     610  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 300    290 2800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .63 41 error (2) 0 wit inspect .018 4.8
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 890    260 7900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .019 5.0
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 900    270 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 43 error (2) 0 wit inspect .018 4.9
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 59    75 740   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .69 41 error (2) 0 wit inspect .020 4.9
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 900    330 7100   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .60 46 error (2) 0 wit inspect .020 4.9
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 900    370 8800   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .019 4.8
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 890    380 7900   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .61 43 error (2) 0 wit inspect .020 4.9
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.0  260 89   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.9  270 true 2 wit inspect 55     620  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 22    550 270   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0  270 timeout 0 wit inspect 960     1100  
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 890    150 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .64 41 error (2) 0 wit inspect .019 4.9
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 170    480 1700   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .65 44 error (2) 0 wit inspect .018 4.9
bitvector/s3_clnt_1_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 34    100 370   true -32 wit inspect 5.0  270 true -32 wit inspect 6.4   270   unknown 0 wit inspect 4.2  220 false(unreach-call) 1 wit inspect .74   19    - wit inspect - wit inspect
bitvector/s3_clnt_2_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 55    110 790   true -32 wit inspect 5.0  270 true -32 wit inspect 4.3   280   unknown 0 wit inspect 4.0  220 false(unreach-call) 1 wit inspect .71   19    - wit inspect - wit inspect
bitvector/s3_clnt_3_false-unreach-call_true-no-overflow.BV.c.cil.c false(unreach-call) 1 wit inspect 18    85 220   true -32 wit inspect 4.8  270 true -32 wit inspect 6.0   270   unknown 0 wit inspect 3.9  220 false(unreach-call) 1 wit inspect .72   19    - wit inspect - wit inspect
bitvector/s3_clnt_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 170    1300 2000   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 71    770 true 2 wit inspect 39     760  
bitvector/s3_clnt_2_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 140    1600 1700   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 15    560 true 2 wit inspect 44     900  
bitvector/s3_clnt_3_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 140    1300 2100   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 14    510 true 2 wit inspect 30     860  
bitvector/s3_srvr_1_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 890    390 7100   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    2900 timeout 0 wit inspect 960     1900  
bitvector/s3_srvr_1_true-unreach-call_true-no-overflow.BV.c.cil.c true 2 wit inspect 46    2300 550   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    5200 true 2 wit inspect 41     1200  
bitvector/s3_srvr_2_alt_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unknown 0 wit inspect 890    360 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .020 4.8
bitvector/s3_srvr_2_true-unreach-call_true-no-overflow_false-termination.BV.c.cil.c unknown 0 wit inspect 890    370 12000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .55 44 error (2) 0 wit inspect .018 4.9
bitvector/s3_srvr_3_alt_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 900    300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .59 45 error (2) 0 wit inspect .018 5.0
bitvector/s3_srvr_3_true-unreach-call_true-no-overflow.BV.c.cil.c unknown 0 wit inspect 890    300 11000   - wit inspect - wit inspect - wit inspect - wit inspect error (invalid witness file) 0 wit inspect .53 43 error (2) 0 wit inspect .022 5.1
bitvector/soft_float_1_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 14    390 150   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 900    6400 true 2 wit inspect 120     780  
bitvector/soft_float_2_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 120    1200 1300   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 56     700  
bitvector/soft_float_3_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 1 wit inspect 120    1200 1500   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 920    6300 timeout 0 wit inspect 960     890  
bitvector/soft_float_4_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 230    380 3200   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 240    630 true 2 wit inspect 290     840  
bitvector/soft_float_5_true-unreach-call_true-no-overflow_true-termination.c.cil.c true 2 wit inspect 120    1200 1500   - wit inspect - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 910    6300 true 2 wit inspect 24     500  
bitvector-regression/implicitfloatconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .35 48 4.3 true -32 wit inspect 3.0  260 true -32 wit inspect 4.1   210   unknown 0 wit inspect 2.7  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 48 4.4 true -32 wit inspect 2.9  250 true -32 wit inspect 4.7   210   unknown 0 wit inspect 1.9  210 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/integerpromotion_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .38 48 4.2 true -32 wit inspect 3.0  260 true -32 wit inspect 4.5   210   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .59   18    - wit inspect - wit inspect
bitvector-regression/recHanoi03_false-unreach-call_true-termination.c unknown 0 wit inspect 4.6  300 46   true -32 wit inspect 2.3  260 true -32 wit inspect 13     300   unknown 0 wit inspect 2.9  190 true -32 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/signextension2_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect 480    70 5800   true -32 wit inspect 2.9  260 true -32 wit inspect 4.3   210   unknown 0 wit inspect 2.9  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
bitvector-regression/signextension_false-unreach-call_true-termination.c false(unreach-call) 1 wit inspect .39 48 4.2 true -32 wit inspect 3.1  260 true -32 wit inspect 4.3   210   unknown 0 wit inspect 2.9  180 false(unreach-call) 1 wit inspect .57   18    - wit inspect - wit inspect
bitvector-regression/implicitunsignedconversion_true-unreach-call_true-termination.c true 2 wit inspect 3.1  260 29   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 4.7   240  
bitvector-regression/integerpromotion_true-unreach-call_true-termination.c true 2 wit inspect 3.2  250 28   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.8  250 true 2 wit inspect 9.1   230  
bitvector-regression/signextension2_true-unreach-call_true-termination.c true 2 wit inspect 480    250 6100   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9  250 true 2 wit inspect 6.6   320  
bitvector-regression/signextension_true-unreach-call_true-termination.c true 2 wit inspect 3.0  250 31   - wit inspect - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0  250 true 2 wit inspect 5.6   250  
bitvector-loops/diamond_false-unreach-call2.i false(unreach-call) 1 wit inspect 1.2  77 14   true -32 wit inspect 3.4  260 true -32 wit inspect 5.1   240   unknown 0 wit inspect 3.0  210 false(unreach-call) 1 wit inspect .58   18    - wit inspect - wit inspect
bitvector-loops/overflow_false-unreach-call1.i unknown 0 wit inspect 54    75 710   error (invalid witness file) 0 wit inspect .57 44 error (2) 0 wit inspect .019 4.9 error (invalid witness file) 0 wit inspect .87 47 error (invalid witness file) 0 wit inspect .0013 .26 - wit inspect - wit inspect
bitvector-loops/verisec_sendmail__tTflag_arr_one_loop_false-unreach-call_true-termination.i false(unreach-call) 0 wit inspect 8.0  100 100   true -32 wit inspect 3.9  260 true -32 wit inspect 5.1   230   unknown 0 wit inspect 3.1  210 error (2) 0 wit inspect .63   19    - wit inspect - wit inspect
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 50 53 15000   22000 160000 14 -384 47 3400 14 -384 68 2900 14 0 39 2500 14 -22 7.5  220 36 34 6200 41000 36 30 8600 18000
    correct results 31 52 3900   16000 49000 0 0 0 10 10 6.3  190 17 34 720 6500 15 30 890 9400
        correct true 21 42 3300   16000 42000 0 0 0 0 17 34 720 6500 15 30 890 9400
        correct false 10 10 590   740 7200 0 0 0 10 10 6.3  190 0 0
    correct-unconfimed results 2 1 130   1300 1600 0 0 0 0 0 0
        correct-unconfirmed true 1 1 120   1200 1500 0 0 0 0 0 0
        correct-unconfirmed false 1 0 8.0 100 100 0 0 0 0 0 0
    incorrect results 0 12 -384 46 3300 12 -384 68 2900 0 1 -32 .57 18 0 0
        incorrect true 0 12 -384 46 3300 12 -384 68 2900 0 1 -32 .57 18 0 0
        incorrect false 0 0 0 0 0 0 0
score (50 tasks, max score: 86) 53 -384 -384 0 -22 34 30
Run set depthk.sv-comp18.ReachSafety-BitVectors cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-BitVectors uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-BitVectors fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.ReachSafety-BitVectors cpa-seq-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-BitVectors uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.ReachSafety-BitVectors