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 09:01:17 CET [[ 2017-01-15 01:00:51 CET ]] [[ 2017-01-15 01:12:27 CET ]] [[ 2017-01-15 01:06:42 CET ]] [[ 2017-01-15 01:18:39 CET ]]
Run set sv-comp17.Overflows-Other
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/depthk.2017-01-13_0901.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0901.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_0901.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/depthk.2017-01-13_0901.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)
recursive/Addition02WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect .57 .57 7.1 50 1.7 0   error (recursion) 3.2  1.8  67   250 false(no-overflow) 7.4 4.0 120 320 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect .56 .56 5.8 49 2.0 0   error (recursion) 3.3  1.8  72   250 false(no-overflow) 7.2 3.9 130 310 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c unknown 0 wit inspect 64    63    900   73 100   0   error (invalid witness file) .52 .33 11   41 error (invalid witness file) 6.4 3.3 130 300 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 450    440    6100   15000 4.4 0   - - error (recursion) 3.3  1.9  57   250 out of memory 600   470   8200 7000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 450    440    5900   15000 5.0 0   - - error (recursion) 3.4  2.0  71   250 out of memory 250   180   2100 7000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 450    440    6600   15000 5.0 0   - - error (recursion) 3.4  1.9  55   250 out of memory 640   520   8800 7000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c out of memory (false(no-overflow)) 0 wit inspect 450    440    6200   15000 4.2 0   - - error (recursion) 3.4  2.0  78   250 out of memory 550   440   9500 7000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 400    390    5100   15000 19   0   - - error (recursion) 3.4  2.0  81   240 timeout 960   810   22000 4600
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 400    390    6200   15000 19   0   - - error (recursion) 3.6  2.0  82   250 timeout 960   810   17000 4700
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 400    400    5400   15000 19   0   - - error (recursion) 3.5  2.0  69   240 timeout 960   810   17000 4900
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 1.3  1.0  16   49 3.4 0   - - true 3.5  2.0  79   250 true 7.1 3.8 150 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 64    64    820   75 85   0   - - error (invalid witness file) .49 .32 8.5 40 error (invalid witness file) 6.2 3.3 120 300
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 64    64    970   75 100   0   - - error (invalid witness file) .51 .33 11   39 error (invalid witness file) 6.3 3.3 110 310
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c unknown 0 wit inspect 860    850    11000   15000 23   0   - - error (recursion) 3.4  1.9  71   250 timeout 960   890   16000 5800
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 1.5  1.2  17   49 5.0 0   - - error (recursion) 3.3  1.9  65   240 true 36   21   500 1200
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 380    370    5300   15000 26   0   - - error (recursion) 3.3  1.9  53   250 timeout 960   880   22000 5800
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 380    370    4900   15000 22   0   - - error (recursion) 4.8  2.7  60   250 timeout 960   890   25000 5800
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 380    370    4600   15000 28   0   - - error (recursion) 3.3  1.9  62   240 timeout 960   890   20000 5800
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 510    490    5900   15000 5.0 0   - - error (recursion) 3.4  2.0  73   240 true 10   5.6 180 360
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 500    490    7100   15000 5.0 0   - - error (recursion) 3.4  1.9  60   240 true 10   5.5 170 350
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 480    470    6400   15000 24   0   - - error (recursion) 3.5  2.0  72   250 timeout 960   830   17000 2100
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c unknown 0 wit inspect 530    520    7600   15000 32   0   - - error (recursion) 4.9  2.6  97   300 timeout 960   840   11000 2100
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 420    410    5400   15000 17   0   - - error (recursion) 3.6  2.0  74   250 true 8.4 4.5 150 310
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 420    420    5300   15000 17   0   - - error (recursion) 3.6  2.0  74   250 true 17   9.5 280 540
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c out of memory (false(no-overflow)) 0 wit inspect 410    390    5000   15000 5.0 0   - - false(no-overflow) 3.8  2.2  81   260 timeout 960   810   11000 4900
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 1.9  1.7  20   49 5.0 0   - - error (recursion) 3.3  1.9  69   240 timeout 960   790   9200 4100
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c unknown 0 wit inspect 1.7  1.6  19   49 5.0 0   - - error (recursion) 3.6  2.1  61   250 timeout 960   810   21000 4600
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .56 .55 5.7 75 2.0 0   false(no-overflow) 3.2  1.8  60   240 false(no-overflow) 7.2 3.9 100 320 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .63 .63 8.2 76 2.0 0   true 3.2  1.8  78   240 false(no-overflow) 7.1 3.8 140 310 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 29    29    320   85 1.8 0   true 3.2  1.8  70   230 false(no-overflow) 7.5 4.0 150 310 - -
bitvector/jain_5_false-no-overflow.i unknown 0 wit inspect 900    900    8000   2200 200   0   error (invalid witness file) .49 .31 6.2 40 error (invalid witness file) 5.3 2.8 89 280 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 24    24    260   80 2.0 0   true 3.2  1.8  66   240 false(no-overflow) 7.8 4.1 130 320 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 93    93    990   96 2.0 0   true 3.1  1.8  54   230 false(no-overflow) 7.6 4.1 130 330 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .48 .48 6.0 100 1.0 0   false(no-overflow) 3.2  1.8  75   240 error (1) 7.2 3.8 120 320 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.8  1.6  21   110 4.2 0   - - true 11    5.6  160   440 true 8.5 4.5 140 330
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.8  1.6  20   110 5.0 0   - - true 12    6.0  200   450 true 8.4 4.5 170 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 2.1  1.9  26   110 4.2 0   - - true 19    9.8  210   630 true 8.1 4.4 160 330
bitvector/gcd_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 500    500    6600   98 84   0   - - error (invalid witness file) .48 .31 7.0 39 error (invalid witness file) 6.4 3.4 130 300
bitvector/gcd_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 20    20    240   75 99   0   - - error (invalid witness file) .51 .33 10   42 error (invalid witness file) 6.2 3.3 120 300
bitvector/gcd_3_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 20    20    250   76 99   0   - - error (invalid witness file) .52 .34 7.4 41 error (invalid witness file) 5.7 3.0 110 300
bitvector/gcd_4_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 500    500    6400   110 110   0   - - error (invalid witness file) .48 .30 9.7 39 error (invalid witness file) 6.2 3.3 140 300
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.4  1.2  16   76 5.0 0   - - true 4.9  2.7  96   300 true 7.1 3.8 140 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  1.0  13   75 4.0 0   - - true 4.4  2.4  96   280 true 6.8 3.6 120 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  1.0  14   75 3.5 0   - - true 4.2  2.4  86   280 true 6.6 3.6 150 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  1.0  13   75 4.0 0   - - true 4.4  2.5  90   280 true 6.7 3.6 140 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  1.0  15   75 3.4 0   - - true 4.1  2.3  78   270 true 6.5 3.6 130 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  1.0  13   75 4.0 0   - - true 4.5  2.5  85   280 true 6.2 3.4 130 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  1.0  14   75 3.9 0   - - true 4.6  2.5  90   280 true 6.8 3.6 140 300
bitvector/modulus_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 900    900    7100   620 42   0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 5.9 3.2 120 290
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.4  1.2  15   76 5.0 0   - - true 4.7  2.6  93   280 true 7.6 4.0 140 330
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.4  1.2  16   76 5.0 0   - - true 4.8  2.7  86   280 true 7.2 3.9 150 320
bitvector/parity_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.4  1.2  15   75 4.5 0   - - true 5.5  3.0  91   290 true 7.0 3.8 140 310
bitvector/sum02_false-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  1.0  13   75 4.0 0   - - true 4.7  2.6  89   270 true 6.9 3.7 140 310
bitvector/sum02_true-unreach-call_true-no-overflow.i unknown 0 wit inspect 1.2  1.0  16   75 4.0 0   - - true 4.9  2.7  91   280 true 7.1 3.8 150 320
../../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 54 8 11000 11000 140000 280000 1300 0   54 27 15 560 2000 54 71 38 1200 3100 54 180 99 3200 11000   54 14000 12000 240000 93000  
    correct results 8 8 150 150 1600 610 14 0   6 26 15 540 1900 7 59 32 1000 2500 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 8 8 150 150 1600 610 14 0   2 26 15 540 1900 7 59 32 1000 2500 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 (54 tasks, max score: 98) 8
Run set sv-comp17.Overflows-Other