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* [apollon075; apollon077; apollon078] [apollon016; apollon038; apollon064; apollon078; apollon084; apollon107] [apollon016; apollon038; apollon078; apollon084; apollon107] 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-12-01 13:07:37 CET 2017-12-01 14:46:42 CET 2017-12-01 15:12:32 CET 2017-12-01 15:13:50 CET 2017-12-01 14:48:36 CET
Run set depthk.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.NoOverflows-Other
Options -witnessValidation -setprop witness.checkProgramHash=false -heap 5000m -benchmark -witness ../../results-verified/depthk.2017-12-01_1307.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_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --graphml-witness ../../results-verified/depthk.2017-12-01_1307.logfiles/sv-comp18.${inputfile_name}.files/witness.graphml --full-output --validate ../../results-verified/depthk.2017-12-01_1307.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
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .56 49 7.6 true -32 wit inspect 3.1  260 true -32 wit inspect 4.7   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .56 49 7.1 true -32 wit inspect 2.7  270 true -32 wit inspect 4.6   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c unknown 0 wit inspect 64    73 750   error (invalid witness file) 0 wit inspect .48 41 error (2) 0 wit inspect .019 4.8 error (invalid witness file) 0 wit inspect .0013 .29 - wit inspect
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 450    15000 5400   - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 440     7000  
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 460    15000 5300   - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480     7000  
recursive/Ackermann03_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 460    15000 5500   - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 450     7000  
recursive/Ackermann04_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 460    15000 5900   - wit inspect - wit inspect - wit inspect out of memory 0 wit inspect 480     7000  
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 400    15000 5400   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4700  
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 400    15000 5100   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4600  
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 400    15000 5000   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4700  
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 1.2  49 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   220  
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 64    74 900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 5.0
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 64    75 710   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 860    15000 11000   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4900  
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 1.4  49 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 44     3900  
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 380    15000 5100   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5000  
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 380    15000 4700   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5000  
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 380    15000 5100   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     5300  
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 510    15000 6900   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.6   270  
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 510    15000 6100   - wit inspect - wit inspect - wit inspect true 2 wit inspect 7.9   270  
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 480    15000 6400   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     3500  
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 wit inspect 530    15000 6700   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4700  
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 420    15000 4600   - wit inspect - wit inspect - wit inspect true 2 wit inspect 6.5   270  
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 420    15000 5400   - wit inspect - wit inspect - wit inspect true 2 wit inspect 9.5   520  
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 410    15000 4700   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     4600  
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 1.9  49 21   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2900  
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 1.8  49 20   - wit inspect - wit inspect - wit inspect timeout 0 wit inspect 960     2700  
recursive-simple/id_b3_o2_false-no-overflow.c false(no-overflow) 1 wit inspect .54 49 8.3 true -32 wit inspect 2.8  260 true -32 wit inspect 4.3   210   false(no-overflow) 1 wit inspect .60   18    - wit inspect
recursive-simple/id_b3_o5_false-no-overflow.c false(no-overflow) 1 wit inspect .56 49 7.3 true -32 wit inspect 3.2  260 true -32 wit inspect 4.7   220   false(no-overflow) 1 wit inspect .60   18    - wit inspect
recursive-simple/id_b5_o10_false-no-overflow.c false(no-overflow) 1 wit inspect .57 49 6.4 true -32 wit inspect 2.3  270 true -32 wit inspect 4.9   210   false(no-overflow) 1 wit inspect .75   18    - wit inspect
recursive-simple/sum_non_eq_false-no-overflow.c false(no-overflow) 1 wit inspect .56 49 6.4 true -32 wit inspect 2.5  260 true -32 wit inspect 4.3   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
recursive-simple/sum_non_false-no-overflow.c false(no-overflow) 1 wit inspect .57 49 8.8 timeout 0 wit inspect 97    2400 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
recursive-simple/id2_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  49 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   230  
recursive-simple/id2_b3_o2_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  49 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   230  
recursive-simple/id2_b3_o5_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  49 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   220  
recursive-simple/id2_b5_o10_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.5  49 20   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   230  
recursive-simple/id_b2_o3_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.4  49 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   230  
recursive-simple/id_b3_o2_false-unreach-call_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect .53 49 5.9 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   230  
recursive-simple/id_b3_o5_true-unreach-call_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect .56 49 7.0 - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1   220  
recursive-simple/id_b5_o10_true-unreach-call_true-termination_true-no-overflow.c false(no-overflow) -16 wit inspect .56 49 6.3 - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   230  
recursive-simple/id_o1000_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  49 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   210  
recursive-simple/id_o100_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  49 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   210  
recursive-simple/id_o10_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  49 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   210  
recursive-simple/id_o200_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  49 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.1   210  
recursive-simple/id_o20_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  49 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.9   220  
recursive-simple/id_o3_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  49 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.3   210  
recursive-simple/sum_non_eq_false-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  49 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.9   230  
recursive-simple/sum_non_eq_true-unreach-call_true-termination_true-no-overflow.c unknown 0 wit inspect 1.2  49 14   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   220  
bitvector/byte_add_1_false-no-overflow.i unknown 0 wit inspect 1.8  100 23   error (1) 0 wit inspect .60 45 error 0 wit inspect 23     570   error (1) 0 wit inspect .073  9.0  - wit inspect
bitvector/byte_add_2_false-no-overflow.i unknown 0 wit inspect 1.8  100 21   error (1) 0 wit inspect .48 48 error 0 wit inspect 37     660   error (1) 0 wit inspect .071  9.1  - wit inspect
bitvector/byte_add_false-no-overflow.i unknown 0 wit inspect 2.1  110 23   error (1) 0 wit inspect .60 46 error 0 wit inspect 48     730   error (1) 0 wit inspect .071  9.1  - wit inspect
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .56 75 6.5 true -32 wit inspect 2.8  260 true -32 wit inspect 4.1   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .63 75 8.3 true -32 wit inspect 2.7  260 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .61   18    - wit inspect
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 29    80 330   true -32 wit inspect 3.2  260 true -32 wit inspect 4.8   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
bitvector/jain_5_false-no-overflow.i unknown 0 wit inspect 900    2300 11000   error (invalid witness file) 0 wit inspect .50 44 error (2) 0 wit inspect .018 5.0 error (invalid witness file) 0 wit inspect .0014 .29 - wit inspect
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 24    80 320   true -32 wit inspect 2.8  260 true -32 wit inspect 4.9   230   false(no-overflow) 1 wit inspect .62   19    - wit inspect
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 93    97 1300   true -32 wit inspect 2.3  270 true -32 wit inspect 5.0   230   false(no-overflow) 1 wit inspect .62   18    - wit inspect
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .50 100 5.3 true -32 wit inspect 2.3  260 true -32 wit inspect 5.4   230   false(no-overflow) 1 wit inspect .60   18    - wit inspect
bitvector/byte_add_1_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect 1.9  100 21   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.0   270  
bitvector/byte_add_2_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect 1.8  100 23   - wit inspect - wit inspect - wit inspect true 2 wit inspect 5.2   280  
bitvector/byte_add_false-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect 2.0  110 25   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.2   280  
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 500    99 6600   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .018 4.9
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 20    75 270   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.9
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 21    75 250   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .020 4.9
bitvector/gcd_4_true-unreach-call_true-no-overflow_true-termination.i unknown 0 wit inspect 500    110 7100   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.4  76 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   220  
bitvector/jain_1_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 1.2  75 16   - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   220  
bitvector/jain_2_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.6   210  
bitvector/jain_4_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 1.2  75 15   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.1   220  
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.5   210  
bitvector/jain_6_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.4   210  
bitvector/jain_7_true-unreach-call_true-no-overflow_false-termination.i unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 3.0   220  
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 900    630 6900   - wit inspect - wit inspect - wit inspect error (2) 0 wit inspect .019 4.8
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.4  75 15   - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.0   220  
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.4  75 16   - wit inspect - wit inspect - wit inspect error 0 wit inspect 4.8   220  
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.4  76 19   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.5   220  
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  75 13   - wit inspect - wit inspect - wit inspect true 2 wit inspect 2.9   220  
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  75 17   - wit inspect - wit inspect - wit inspect true 2 wit inspect 4.7   230  
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 78 -35 12000   280000 140000 18 -384 130 5800 18 -416 170 4900 18 13 8.3 270 60 70 14000 93000
    correct results 13 13 150   850 2000 0 0 13 13 8.1 240 35 70 200 12000
        correct true 0 0 0 0 35 70 200 12000
        correct false 13 13 150   850 2000 0 0 13 13 8.1 240 0
    incorrect results 3 -48 1.6 150 19 12 -384 33 3100 13 -416 61 2900 0 0
        incorrect true 0 12 -384 33 3100 13 -416 61 2900 0 0
        incorrect false 3 -48 1.6 150 19 0 0 0 0
score (78 tasks, max score: 138) -35 -384 -416 13 70
Run set depthk.sv-comp18.NoOverflows-Other cpa-seq-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-Other fshell-witness2test-validate-violation-witnesses-depthk.sv-comp18-violation-witness.NoOverflows-Other uautomizer-validate-correctness-witnesses-depthk.sv-comp18-correctness-witness.NoOverflows-Other