Tool ULTIMATE Kojak f7c3ed31
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-14 07:32:15 CET [[ 2017-01-15 06:03:36 CET ]] [[ 2017-01-15 06:19:08 CET ]] [[ 2017-01-15 06:04:26 CET ]] [[ 2017-01-15 06:20:07 CET ]]
Run set sv-comp17.Overflows-Other
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/ukojak.2017-01-14_0732.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/ukojak.2017-01-14_0732.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 6.5 1.9 50 340 2.5 0   error (recursion) 3.1  1.8  66   250 false(no-overflow) 7.5 4.0 150 310 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 6.3 1.9 41 330 2.5 0   error (recursion) 3.3  1.9  67   260 false(no-overflow) 7.6 4.0 160 310 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 5.5 1.8 46 320 2.5 0   false(no-overflow) 3.5  2.0  71   250 false(no-overflow) 7.9 4.2 160 320 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   640   10000 1300 2.3 0   - - error (invalid witness file) .51 .33 12   40 error (invalid witness file) 5.7 3.1 110 290
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   640   10000 1300 2.3 0   - - error (invalid witness file) .55 .35 11   42 error (invalid witness file) 5.6 3.0 120 300
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   640   12000 1400 2.3 0   - - error (invalid witness file) .51 .35 12   40 error (invalid witness file) 6.2 3.3 120 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   640   11000 1500 2.3 0   - - error (invalid witness file) .51 .34 11   39 error (invalid witness file) 6.6 3.5 120 310
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   740   15000 4300 2.3 0   - - error (invalid witness file) .53 .36 12   40 error (invalid witness file) 6.0 3.2 130 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   740   16000 4900 2.3 0   - - error (invalid witness file) .53 .34 12   40 error (invalid witness file) 6.0 3.2 120 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   750   13000 2000 2.3 0   - - error (invalid witness file) .51 .34 9.3 41 error (invalid witness file) 5.5 2.9 90 290
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 5.7 1.8 44 320 2.5 0   - - true 3.3  1.8  41   250 true 7.1 3.8 130 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   740   15000 4600 2.3 0   - - error (invalid witness file) .48 .30 8.6 39 error (invalid witness file) 7.0 3.7 130 310
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   740   13000 3900 2.3 0   - - error (invalid witness file) .54 .34 9.7 41 error (invalid witness file) 5.7 3.0 110 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   680   11000 1300 2.3 0   - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.2 3.3 140 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   680   12000 1100 2.3 0   - - error (invalid witness file) .51 .34 12   40 error (invalid witness file) 6.0 3.2 130 290
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   680   13000 1400 2.3 0   - - error (invalid witness file) .51 .34 12   39 error (invalid witness file) 5.9 3.1 120 300
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   680   12000 1300 2.3 0   - - error (invalid witness file) .53 .35 11   39 error (invalid witness file) 6.0 3.2 120 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   680   12000 1300 2.3 0   - - error (invalid witness file) .52 .34 10   40 error (invalid witness file) 6.4 3.4 110 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.8 2.4 60 380 2.5 0   - - error (recursion) 3.3  1.8  52   250 true 9.8 5.3 160 350
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.7 2.3 58 390 2.5 0   - - error (recursion) 3.3  1.9  71   240 true 10   5.5 160 350
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730   13000 960 2.3 0   - - error (invalid witness file) .54 .36 13   41 error (invalid witness file) 6.3 3.4 130 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   590   12000 1300 2.5 0   - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.0 3.2 130 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 8.9 2.7 64 460 2.5 0   - - error (recursion) 3.4  1.9  47   240 true 8.7 4.7 160 320
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 11   3.9 100 480 2.5 0   - - error (recursion) 3.6  2.0  38   240 true 16   9.2 220 520
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730   14000 1200 2.3 0   - - error (invalid witness file) .54 .36 12   41 error (invalid witness file) 6.2 3.3 120 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   780   13000 1600 2.3 0   - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.7 3.1 120 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   770   14000 1800 2.3 0   - - error (invalid witness file) .56 .36 11   43 error (invalid witness file) 5.8 3.1 120 290
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 5.5 1.8 38 320 2.5 0   true 3.2  1.8  62   250 false(no-overflow) 7.6 4.1 150 330 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 5.6 1.8 45 320 2.5 0   true 3.2  1.8  64   240 false(no-overflow) 7.6 4.0 150 320 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 5.5 1.8 48 320 2.5 0   true 3.3  1.9  62   250 false(no-overflow) 7.5 4.0 160 320 - -
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900   790   13000 1200 2.3 0   error (invalid witness file) .56 .35 7.5 44 error (invalid witness file) 6.1 3.3 110 300 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 5.5 1.8 50 320 2.5 0   true 3.4  1.9  69   250 false(no-overflow) 7.8 4.2 140 310 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 5.7 1.8 43 320 2.5 0   true 3.0  1.7  61   250 false(no-overflow) 7.1 3.8 160 310 - -
bitvector/modulus_false-no-overflow.i error (1) 0 wit inspect 5.8 1.9 46 320 2.5 0   error (invalid witness file) .55 .37 13   40 error (invalid witness file) 6.6 3.5 140 310 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.4 2.2 56 350 2.6 0   - - true 10    5.5  96   450 true 7.5 4.1 140 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.8 2.3 59 360 2.6 0   - - true 11    5.8  150   460 true 8.2 4.5 160 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect 8.2 2.4 63 360 2.6 0   - - true 19    9.8  260   640 true 8.3 4.5 110 330
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.4 2.1 49 320 2.5 0   - - true 5.0  2.9  41   330 true 9.4 5.0 150 340
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.3 2.0 50 320 2.5 0   - - true 5.0  2.9  71   330 true 8.1 4.4 160 320
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.5 2.0 50 330 2.5 0   - - true 5.2  2.9  97   300 true 8.3 4.4 160 320
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 20   7.3 170 530 2.5 0   - - true 5.1  2.8  59   280 true 14   7.7 240 430
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.4 1.7 43 320 2.5 0   - - true 4.9  2.7  100   290 true 7.4 3.9 140 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.2 1.7 40 310 2.5 0   - - true 3.9  2.2  53   280 true 7.1 3.8 130 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.1 1.7 40 320 2.5 0   - - true 4.1  2.3  53   280 true 6.7 3.6 130 320
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.3 1.7 47 330 2.5 0   - - true 4.4  2.5  75   280 true 6.9 3.7 140 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.3 1.7 40 320 2.5 0   - - true 4.1  2.3  94   280 true 6.8 3.6 140 310
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.0 1.8 42 340 2.5 0   - - true 4.3  2.4  44   280 true 6.9 3.7 120 320
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.0 1.8 51 330 2.5 0   - - true 4.3  2.4  63   280 true 6.5 3.5 130 310
bitvector/modulus_true-unreach-call_true-no-overflow.i error (1) 0 wit inspect 6.0 2.0 46 320 2.5 0   - - error (invalid witness file) .52 .34 12   41 error (invalid witness file) 5.8 3.1 130 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.7 1.8 47 320 2.5 0   - - true 5.0  2.8  100   280 true 7.3 3.9 150 330
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.7 1.9 46 320 2.5 0   - - true 4.4  2.5  41   280 true 7.4 4.0 140 330
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.3 1.7 46 320 2.5 0   - - true 4.9  2.7  73   270 true 6.5 3.5 130 300
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect 6.0 2.0 48 320 2.5 0   - - true 4.5  2.5  56   280 true 6.6 3.6 140 310
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect 16   12   200 330 2.5 0   - - true 4.5  2.5  91   290 true 7.5 4.0 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 56 18000 14000 250000 51000 130 0   54 27 16 540 2100   54 73 39 1500 3200   54 140 79 2100 8200   54 320 170 6000 14000  
    correct results 32 56 230 80 1900 11000 81 0   6 26 15 520 2000   8 61 32 1200 2500   20 130 72 1900 7400   24 200 110 3600 8000  
        correct true 24 48 180 65 1500 8500 61 0   5 0 0 0 0   0 0 0 0 0   20 130 72 1900 7400   24 200 110 3600 8000  
        correct false 8 8 46 15 360 2600 20 0   1 26 15 520 2000   8 61 32 1200 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) 56
Run set sv-comp17.Overflows-Other