Tool CPAchecker 1.6.1-svn 24048
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-11 11:20:09 CET [[ 2017-01-14 21:49:20 CET ]] [[ 2017-01-14 22:06:43 CET ]] [[ 2017-01-14 21:51:07 CET ]] [[ 2017-01-14 22:08:18 CET ]]
Run set sv-comp17.Overflows-Other
Options -sv-comp17-k-induction -heap 10000M -disable-java-assertions [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/cpa-kind.2017-01-11_1120.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/cpa-kind.2017-01-11_1120.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 error (recursion) 0 wit inspect 2.2 1.0  20 240 0   0   false(no-overflow) 3.6 2.1 64 250 false(no-overflow) 7.2 3.8 150 310 - -
recursive/Addition03_false-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  21 240 0   0   false(no-overflow) 3.6 2.1 67 250 false(no-overflow) 7.5 4.0 150 320 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 2.5 1.1  19 250 0   0   false(no-overflow) 3.5 2.0 71 250 false(no-overflow) 9.7 5.2 98 320 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  23 240 0   0   - - error (recursion) 3.7 2.1 81 250 out of memory 440   330   8100 7000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  20 240 0   0   - - error (recursion) 3.7 2.1 63 250 timeout 910   730   14000 7000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.1  22 250 0   0   - - error (recursion) 4.1 2.4 53 250 out of memory 820   660   11000 7000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (recursion) 0 wit inspect 2.4 1.1  20 250 0   0   - - error (recursion) 4.3 2.4 46 240 out of memory 710   570   12000 7000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.4 1.0  20 240 0   0   - - error (recursion) 3.4 2.0 58 250 timeout 960   800   20000 4700
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  21 250 0   0   - - error (recursion) 4.0 2.3 56 250 timeout 960   810   20000 4600
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.4 1.0  21 250 0   0   - - error (recursion) 3.8 2.2 67 250 timeout 960   800   16000 4700
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  19 250 0   0   - - true 3.3 1.9 59 250 true 9.2 4.9 80 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  23 240 0   0   - - error (recursion) 3.3 1.8 40 240 timeout 960   800   19000 4100
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.4 1.1  20 250 0   0   - - error (recursion) 3.4 1.9 65 240 timeout 960   780   14000 3900
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (recursion) 0 wit inspect 2.3 1.0  22 240 0   0   - - error (recursion) 4.1 2.3 47 250 timeout 960   890   18000 5600
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.2 1.0  21 240 0   0   - - error (recursion) 3.0 1.7 39 240 true 40   23   630 1100
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.4 1.0  22 250 0   0   - - error (recursion) 3.4 1.9 68 240 timeout 960   890   23000 5700
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  19 240 0   0   - - error (recursion) 3.3 1.9 64 250 timeout 960   890   18000 5600
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  19 250 0   0   - - error (recursion) 3.7 2.1 63 250 timeout 960   880   25000 5800
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.4 1.0  21 250 0   0   - - error (recursion) 3.2 1.8 69 240 true 11   5.9 170 380
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  20 240 0   0   - - error (recursion) 3.4 1.9 71 240 true 11   5.9 180 360
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  21 240 0   0   - - error (recursion) 3.5 2.0 66 250 timeout 960   840   17000 1800
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (recursion) 0 wit inspect 2.5 1.1  24 240 0   0   - - error (recursion) 3.8 2.1 72 240 timeout 960   830   16000 2200
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  21 240 0   0   - - error (recursion) 3.9 2.2 54 250 true 10   5.4 100 310
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  24 240 0   0   - - error (recursion) 3.6 2.0 54 250 true 22   12   230 530
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.6 1.1  23 260 0   0   - - false(no-overflow) 3.9 2.2 57 250 timeout 960   810   19000 4800
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  18 240 0   0   - - error (recursion) 3.4 2.0 64 250 timeout 960   800   17000 3800
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (recursion) 0 wit inspect 2.3 1.0  21 240 0   0   - - error (recursion) 4.2 2.4 49 250 timeout 960   800   13000 4100
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 2.4 1.1  22 240 0   0   false(no-overflow) 3.7 2.1 61 250 false(no-overflow) 8.2 4.3 99 330 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 2.5 1.0  21 240 0   0   false(no-overflow) 3.9 2.2 61 250 false(no-overflow) 7.7 4.1 140 320 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 2.4 1.1  21 240 0   0   false(no-overflow) 3.6 2.1 62 250 false(no-overflow) 9.4 5.0 81 320 - -
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900   870    12000 3900 0   0   true 4.4 2.5 59 280 timeout 96   64   1600 1300 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 2.4 1.1  20 240 0   0   false(no-overflow) 3.4 1.9 70 250 false(no-overflow) 8.5 4.6 110 320 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 2.3 1.0  20 240 0   0   false(no-overflow) 4.1 2.3 49 250 false(no-overflow) 8.2 4.3 130 320 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect 2.5 1.1  21 250 0   0   false(no-overflow) 3.3 1.9 67 230 error (1) 7.9 4.2 130 320 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 23   7.4  180 510 0   0   - - true 12   6.1 190 350 true 8.2 4.4 130 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 22   6.8  160 460 0   0   - - true 13   6.7 170 440 true 8.3 4.5 160 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect 86   62    1100 1500 0   0   - - true 19   9.7 230 500 true 8.4 4.6 160 330
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.9 3.2  50 290 0   0   - - true 6.4 3.7 71 310 true 9.5 5.1 96 330
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 76   71    660 430 0   0   - - true 5.2 2.9 70 300 true 9.0 4.8 140 320
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 75   70    740 430 0   0   - - true 5.9 3.3 62 300 true 7.6 4.1 150 310
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.8 1.2  23 260 0   0   - - true 4.7 2.6 92 270 true 16   8.8 190 430
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 4.2 1.5  33 280 0   0   - - true 5.6 3.1 56 270 true 8.0 4.2 160 320
bitvector/jain_1_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 910   890    7900 8800 0   0   - - true 4.9 2.7 64 280 true 6.3 3.3 87 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 910   890    8400 9700 0   0   - - true 4.9 2.8 68 280 true 6.9 3.7 120 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 910   890    8500 10000 0   0   - - true 4.6 2.6 80 280 true 6.8 3.6 92 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   860    12000 3900 0   0   - - true 4.1 2.3 84 270 true 8.5 4.5 97 320
bitvector/jain_6_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 910   890    9300 10000 0   0   - - true 4.9 2.7 77 280 true 6.2 3.3 110 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 910   890    7100 5500 0   0   - - true 4.5 2.5 82 270 true 6.6 3.5 120 310
bitvector/modulus_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   870    7400 4100 0   0   - - true 5.4 3.0 86 270 error (1) 8.8 4.7 89 320
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 3.0 1.3  24 250 0   0   - - true 5.3 2.9 76 280 true 9.1 5.0 91 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 32   15    280 760 0   0   - - true 5.8 3.2 75 290 true 8.6 4.6 100 320
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 14   3.9  120 440 0   0   - - true 7.0 3.8 65 290 true 6.6 3.5 84 320
bitvector/sum02_false-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   850    9900 1800 0   0   - - true 4.6 2.6 51 280 true 8.0 4.2 100 310
bitvector/sum02_true-unreach-call_true-no-overflow.i timeout 0 wit inspect 900   840    11000 1800 0   0   - - true 5.8 3.2 66 280 true 7.1 3.8 120 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 29 9500 9000   98000 74000 0   0   54 37 21 630 2500   54 170 100 2700 4200   54 220 120 3200 12000   54 17000 14000 300000 99000  
    correct results 18 29 360 250   3500 7300 0   0   7 26 14 440 1700   6 60 32 790 2200   11 89 48 1200 3600   11 99 53 1500 3700  
        correct true 11 22 340 240   3300 5600 0   0   0 0 0 0 0   0 0 0 0 0   11 89 48 1200 3600   11 99 53 1500 3700  
        correct false 7 7 17 7.5 140 1700 0   0   7 26 14 440 1700   6 60 32 790 2200   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) 29
Run set sv-comp17.Overflows-Other