Tool ULTIMATE Automizer 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:34:03 CET [[ 2017-01-15 06:02:28 CET ]] [[ 2017-01-15 06:17:25 CET ]] [[ 2017-01-15 06:02:42 CET ]] [[ 2017-01-15 06:18:28 CET ]]
Run set sv-comp17.Overflows-Other
Options [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/uautomizer.2017-01-14_0734.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/uautomizer.2017-01-14_0734.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 5.5 1.7 47 330 2.5 0   error (recursion) 3.1  1.8  60   250 false(no-overflow) 7.6 4.0 140 310 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 6.5 1.9 49 360 2.5 0   error (recursion) 3.4  1.9  69   250 false(no-overflow) 7.7 4.1 140 320 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 6.1 1.9 46 320 2.5 0   false(no-overflow) 3.7  2.1  74   260 false(no-overflow) 8.0 4.2 140 320 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   720   11000 7100 2.3 0   - - error (invalid witness file) .49 .32 9.4 40 error (invalid witness file) 6.2 3.3 120 310
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730   12000 6500 2.4 0   - - error (invalid witness file) .57 .36 11   42 error (invalid witness file) 6.2 3.2 120 300
recursive/Ackermann03_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   730   12000 6600 2.3 0   - - error (invalid witness file) .60 .39 7.9 40 error (invalid witness file) 5.7 3.1 120 300
recursive/Ackermann04_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   730   11000 6300 2.3 0   - - error (invalid witness file) .58 .36 12   43 error (invalid witness file) 6.5 3.4 140 300
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   750   12000 3700 2.5 0   - - error (invalid witness file) .51 .33 9.9 39 error (invalid witness file) 6.6 3.5 120 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   740   13000 4000 2.3 0   - - error (invalid witness file) .53 .35 10   40 error (invalid witness file) 6.5 3.5 120 300
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   750   14000 3500 2.3 0   - - error (invalid witness file) .54 .34 10   41 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.4 1.7 45 320 2.5 0   - - true 3.4  1.9  75   240 true 7.1 3.7 140 320
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   740   13000 4700 2.3 0   - - error (invalid witness file) .52 .36 9.6 42 error (invalid witness file) 6.1 3.2 130 300
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   740   13000 5200 2.3 0   - - error (invalid witness file) .55 .36 7.2 39 error (invalid witness file) 6.0 3.2 110 290
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c timeout 0 wit inspect 900   820   11000 5800 2.3 0   - - error (invalid witness file) .51 .33 10   41 error (invalid witness file) 7.1 3.7 140 310
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 27   8.4 210 1400 2.5 0   - - error (recursion) 3.3  1.9  59   240 true 36   20   420 1300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   820   11000 5800 2.3 0   - - error (invalid witness file) .48 .32 11   39 error (invalid witness file) 5.8 3.1 100 300
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   820   13000 5700 2.4 0   - - error (invalid witness file) .48 .31 10   42 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   820   12000 5600 2.3 0   - - error (invalid witness file) .52 .33 11   41 error (invalid witness file) 5.8 3.1 130 300
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.8 2.4 62 390 2.5 0   - - error (recursion) 3.5  2.0  53   240 true 10   5.4 160 350
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.8 2.4 56 380 2.5 0   - - error (recursion) 3.2  1.8  42   250 true 9.7 5.3 170 350
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   780   14000 1000 2.3 0   - - error (invalid witness file) .50 .33 12   39 error (invalid witness file) 5.7 3.1 110 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c timeout 0 wit inspect 900   780   11000 1500 2.3 0   - - error (invalid witness file) .52 .34 10   42 error (invalid witness file) 5.9 3.2 110 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 7.4 2.2 60 340 2.5 0   - - error (recursion) 3.5  2.0  76   240 true 8.5 4.6 130 330
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 13   3.9 88 510 2.5 0   - - error (recursion) 3.6  2.1  77   240 true 17   9.5 240 530
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   790   13000 5300 2.3 0   - - error (invalid witness file) .54 .34 14   41 error (invalid witness file) 6.4 3.4 120 310
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   720   13000 2200 2.3 0   - - error (invalid witness file) .52 .32 9.8 39 error (invalid witness file) 6.7 3.5 140 310
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c timeout 0 wit inspect 900   730   14000 2200 2.3 0   - - error (invalid witness file) .49 .32 6.5 39 error (invalid witness file) 6.1 3.3 120 300
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 5.4 1.8 38 320 2.5 0   true 3.2  1.8  65   250 false(no-overflow) 6.9 3.7 120 320 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 5.4 1.8 39 320 2.5 0   true 3.2  1.8  70   250 false(no-overflow) 7.7 4.1 140 320 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 5.8 1.8 48 320 2.5 0   true 3.2  1.8  68   250 false(no-overflow) 7.1 3.9 140 310 - -
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900   750   14000 4800 2.3 0   error (invalid witness file) .51 .34 12   40 error (invalid witness file) 5.9 3.1 130 300 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 5.5 1.8 48 320 2.5 0   true 3.2  1.8  62   250 false(no-overflow) 7.4 4.0 160 310 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 5.4 1.8 45 320 2.5 0   true 3.1  1.8  70   250 false(no-overflow) 7.5 4.0 140 320 - -
bitvector/modulus_false-no-overflow.i error (1) 0 wit inspect 5.6 1.8 48 330 2.5 0   error (invalid witness file) .47 .30 8.9 39 error (invalid witness file) 5.8 3.1 130 300 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.2 2.0 47 320 2.6 0   - - true 10    5.3  74   440 true 8.4 4.5 180 330
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.2 2.1 60 340 2.6 0   - - true 11    5.6  100   450 true 8.0 4.4 150 320
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect 6.7 2.1 54 330 2.6 0   - - true 19    9.7  170   650 true 8.4 4.5 180 320
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.1 2.0 44 320 2.5 0   - - true 6.3  3.5  76   300 true 8.3 4.5 150 320
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.0 2.0 49 340 2.5 0   - - true 5.0  2.9  81   320 true 7.6 4.1 130 310
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 7.0 2.1 52 340 2.5 0   - - true 4.9  2.8  66   300 true 7.9 4.3 160 330
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 9.9 2.8 77 480 2.5 0   - - true 4.9  2.8  100   280 true 14   7.8 210 420
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.3 1.7 43 320 2.5 0   - - true 4.8  2.6  76   310 true 7.2 3.8 130 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.8 1.8 40 320 2.5 0   - - true 4.2  2.3  72   280 true 6.5 3.5 130 300
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.9 1.8 42 330 2.5 0   - - true 4.1  2.3  47   280 true 6.6 3.5 120 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.5 1.8 47 330 2.5 0   - - true 4.3  2.4  76   280 true 7.1 3.8 150 310
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.0 1.8 44 330 2.5 0   - - true 3.9  2.2  46   280 true 6.4 3.4 120 300
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.7 1.8 44 330 2.5 0   - - true 4.4  2.4  100   280 true 6.3 3.4 120 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.3 1.8 52 340 2.5 0   - - true 4.4  2.4  73   280 true 7.9 4.2 140 330
bitvector/modulus_true-unreach-call_true-no-overflow.i error (1) 0 wit inspect 5.5 1.7 40 310 2.5 0   - - error (invalid witness file) .53 .36 10   41 error (invalid witness file) 6.0 3.2 120 300
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.4 1.8 46 310 2.5 0   - - true 4.6  2.6  82   280 true 7.3 3.9 130 330
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 6.8 1.9 47 340 2.5 0   - - true 4.5  2.5  53   280 true 7.2 3.9 150 310
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.6 1.8 38 320 2.5 0   - - true 5.0  2.7  79   280 true 7.6 4.0 140 320
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect 5.8 1.8 45 330 2.5 0   - - true 4.7  2.6  77   280 true 6.9 3.7 130 310
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect 5.4 1.7 42 320 2.5 0   - - true 4.7  2.6  77   280 true 7.4 3.9 150 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 58 17000 15000 240000 100000 130 0   54 27 15 560 2100   54 72 38 1400 3100   54 140 80 2100 8400   54 350 190 6400 15000  
    correct results 33 58 230 72 1800 12000 84 0   6 26 15 540 2000   8 60 32 1100 2500   20 130 74 1900 7600   25 230 130 4000 9300  
        correct true 25 50 190 57 1400 9700 64 0   5 0 0 0 0   0 0 0 0 0   20 130 74 1900 7600   25 230 130 4000 9300  
        correct false 8 8 46 14 360 2600 20 0   1 26 15 540 2000   8 60 32 1100 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) 58
Run set sv-comp17.Overflows-Other