Tool ULTIMATE Taipan 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 16:52:13 CET [[ 2017-01-15 06:05:33 CET ]] [[ 2017-01-15 06:20:29 CET ]] [[ 2017-01-15 06:05:48 CET ]] [[ 2017-01-15 06:21:18 CET ]]
Run set sv-comp17.Overflows-Other
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/utaipan.2017-01-14_1652.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/utaipan.2017-01-14_1652.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.9 1.9 48 330 2.5 0      error (recursion) 3.3  1.8  71 250 false(no-overflow) 7.1 3.8 150 310 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 6.3 1.8 46 330 2.5 0      error (recursion) 3.4  1.9  65 250 false(no-overflow) 7.0 3.8 140 310 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 5.9 1.9 47 320 2.5 0      false(no-overflow) 3.4  2.0  71 250 false(no-overflow) 7.7 4.1 140 310 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 910   180   4600 13000 2.3 0      - - error (invalid witness file) .55 .35 12   41 error (invalid witness file) 6.2 3.3 130 310
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 910   180   4600 13000 2.3 0      - - error (invalid witness file) .56 .39 11   39 error (invalid witness file) 5.5 3.0 100 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 910   180   5100 13000 2.3 0      - - error (invalid witness file) .52 .33 12   41 error (invalid witness file) 6.1 3.2 120 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 910   180   4400 13000 2.3 0      - - error (invalid witness file) .53 .34 13   41 error (invalid witness file) 6.1 3.3 130 300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730   11000 3400 2.3 0      - - error (invalid witness file) .55 .36 13   40 error (invalid witness file) 5.6 3.0 110 290
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730   13000 3500 2.3 0      - - error (invalid witness file) .53 .34 11   40 error (invalid witness file) 5.5 3.0 110 290
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   740   14000 2900 2.3 0      - - error (invalid witness file) .49 .31 11   40 error (invalid witness file) 6.1 3.2 130 300
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 5.5 1.7 41 320 2.5 0      - - true 3.5  2.0  45   250 true 6.6 3.6 140 310
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730   13000 3800 2.3 0      - - error (invalid witness file) .51 .33 12   41 error (invalid witness file) 5.8 3.1 120 290
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730   13000 4200 2.3 0      - - error (invalid witness file) .56 .35 13   41 error (invalid witness file) 6.8 3.5 140 310
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   760   11000 5400 2.3 0      - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 6.0 3.2 120 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 910   260   5400 13000 2.3 0      - - error (invalid witness file) .52 .33 11   40 error (invalid witness file) 5.4 2.9 120 290
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   760   10000 5300 2.3 0      - - error (invalid witness file) .53 .34 11   42 error (invalid witness file) 6.6 3.5 130 320
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   750   11000 5300 2.3 0      - - error (invalid witness file) .49 .32 9.6 39 error (invalid witness file) 5.6 3.0 110 290
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   750   12000 5400 2.3 0      - - error (invalid witness file) .54 .36 13   40 error (invalid witness file) 6.5 3.4 120 310
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 8.4 2.3 60 400 2.5 0      - - error (recursion) 3.3  1.9  56   240 true 9.9 5.4 160 350
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.8 2.3 59 390 2.5 0      - - error (recursion) 3.2  1.8  50   250 true 9.9 5.4 180 340
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (1) 0 wit inspect 400   380   5500 830 2.5 0      - - error (invalid witness file) .50 .32 12   39 error (invalid witness file) 5.9 3.1 130 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   750   9800 6900 2.3 0      - - error (invalid witness file) .49 .33 13   39 error (invalid witness file) 6.2 3.3 130 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.3 2.0 53 340 2.5 0      - - error (recursion) 3.4  1.9  47   250 true 8.0 4.4 160 310
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 23   10   220 790 2.6 0      - - error (recursion) 3.7  2.1  60   250 true 17   9.7 230 530
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 910   350   6000 13000 2.3 .0082 - - error (invalid witness file) .55 .36 11   40 error (invalid witness file) 5.5 3.0 100 290
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   850   11000 2700 2.3 0      - - error (invalid witness file) .55 .35 14   41 error (invalid witness file) 6.1 3.2 120 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   850   11000 2600 2.3 0      - - error (invalid witness file) .49 .32 10   40 error (invalid witness file) 5.7 3.1 130 300
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 5.8 1.7 42 340 2.5 0      true 3.3  1.8  64 240 false(no-overflow) 6.9 3.7 140 310 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 5.6 1.8 39 320 2.5 0      true 3.3  1.9  73 250 false(no-overflow) 7.3 4.0 150 310 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 6.2 1.9 42 320 2.5 0      true 3.3  1.8  60 250 false(no-overflow) 7.8 4.2 160 310 - -
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900   880   12000 740 2.3 0      error (invalid witness file) .53 .36 12 40 error (invalid witness file) 6.0 3.2 120 290 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 5.3 1.8 41 320 2.5 0      true 3.3  1.9  72 250 false(no-overflow) 7.6 4.1 140 330 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 5.5 1.8 41 320 2.5 0      true 3.5  2.0  73 250 false(no-overflow) 7.9 4.2 160 320 - -
bitvector/modulus_false-no-overflow.i error (1) 0 wit inspect 6.1 1.8 50 350 2.5 0      error (invalid witness file) .48 .31 10 39 error (invalid witness file) 6.9 3.6 140 320 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.4 2.1 61 370 2.6 0      - - true 11    5.9  96   350 true 8.0 4.4 150 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.0 2.1 55 340 2.6 0      - - true 11    5.8  150   340 true 7.6 4.2 150 330
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect 6.2 2.0 48 330 2.6 0      - - true 21    11    210   660 true 7.7 4.2 140 310
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.8 2.1 64 380 2.5 0      - - true 5.1  2.9  68   310 true 8.0 4.3 140 330
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.2 2.0 47 330 2.5 0      - - true 5.3  3.0  100   300 true 7.9 4.2 140 320
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.6 2.0 49 330 2.5 0      - - true 5.1  2.9  71   300 true 8.3 4.4 150 320
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 11   3.7 97 480 2.5 0      - - true 5.1  2.8  84   270 true 13   7.3 210 440
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.9 1.8 44 330 2.5 0      - - true 4.4  2.5  60   280 true 6.8 3.7 130 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.2 1.7 43 320 2.5 0      - - true 4.0  2.3  58   280 true 6.9 3.7 140 320
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.1 1.9 50 330 2.5 0      - - true 4.2  2.3  54   280 true 6.5 3.6 130 300
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.3 1.9 43 330 2.5 0      - - true 4.3  2.4  62   280 true 6.5 3.6 140 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.2 1.7 44 320 2.5 0      - - true 4.1  2.3  77   280 true 6.4 3.5 140 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.8 1.8 40 320 2.5 0      - - true 4.3  2.4  34   300 true 7.1 3.8 140 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.3 1.7 41 320 2.5 0      - - true 4.4  2.5  78   270 true 7.5 3.9 140 310
bitvector/modulus_true-unreach-call_true-no-overflow.i error (1) 0 wit inspect 5.7 1.7 41 320 2.5 0      - - error (invalid witness file) .49 .31 10   39 error (invalid witness file) 6.0 3.2 130 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.8 1.8 48 320 2.5 0      - - true 4.7  2.6  87   280 true 7.5 4.0 140 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.6 1.9 54 340 2.5 0      - - true 4.6  2.5  59   280 true 7.9 4.2 150 330
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.6 1.8 46 320 2.7 0      - - true 5.7  3.1  110   280 true 7.8 4.1 140 320
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect 5.7 1.8 40 320 2.5 0      - - true 4.6  2.5  66   280 true 6.6 3.6 140 300
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.6 1.7 45 320 2.5 0      - - true 4.5  2.5  54   270 true 6.7 3.6 120 310
../../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 12000 190000 150000 130 .0082 54 28 16 570 2100   54 72 39 1400 3100   54 140 80 2100 7900   54 310 170 6000 14000  
    correct results 32 56 220 70 1700 11000 81 0      6 27 15 550 2000   8 59 32 1200 2500   20 130 73 1800 7100   24 200 110 3600 8000  
        correct true 24 48 170 56 1400 8700 61 0      5 0 0 0 0   0 0 0 0 0   20 130 73 1800 7100   24 200 110 3600 8000  
        correct false 8 8 48 15 350 2600 20 0      1 27 15 550 2000   8 59 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