Tool SMACK+Corral 1.7.2
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:19:02 CET [[ 2017-01-15 04:32:52 CET ]] [[ 2017-01-15 05:00:11 CET ]] [[ 2017-01-15 04:38:10 CET ]] [[ 2017-01-15 05:08:13 CET ]]
Run set sv-comp17.Overflows-Other
Options -w error-witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/smack.2017-01-14_0719.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/smack.2017-01-14_0719.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 1.6 1.6 20 72 .90 0   error (recursion) 3.3  1.8  68 250 false(no-overflow) 8.0 4.3 130 320 - -
recursive/Addition03_false-no-overflow.c false(no-overflow) 1 wit inspect 1.6 1.6 22 74 .90 0   error (recursion) 3.4  1.9  65 250 false(no-overflow) 7.2 3.9 130 310 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c false(no-overflow) 1 wit inspect 1.6 1.6 21 81 .89 0   false(no-overflow) 3.5  1.9  78 260 false(no-overflow) 8.0 4.3 150 320 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c true 1 wit inspect 880   880   9800 270 .91 0   - - error (recursion) 3.6  2.0  75   250 out of memory 520   400   9000 7000
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   7400 270 .91 0   - - error (recursion) 3.5  2.0  73   240 out of memory 500   390   6000 7000
recursive/Ackermann03_true-unreach-call_true-no-overflow.c true 1 wit inspect 880   880   11000 270 .91 0   - - error (recursion) 3.5  2.0  76   250 out of memory 420   320   4000 7000
recursive/Ackermann04_true-unreach-call_true-no-overflow.c true 1 wit inspect 880   880   8900 270 .91 0   - - error (recursion) 3.5  2.0  74   250 out of memory 650   530   7100 7000
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   9700 280 .91 0   - - error (recursion) 3.3  1.9  64   250 timeout 960   810   17000 4700
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   10000 280 .91 0   - - error (recursion) 3.2  1.8  45   240 timeout 960   810   17000 4800
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   11000 220 .90 0   - - error (recursion) 3.3  1.9  65   240 timeout 960   810   11000 4500
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 1.2 1.2 15 73 .86 0   - - true 3.5  2.0  74   250 true 6.9 3.7 150 310
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   11000 220 .89 0   - - error (recursion) 3.2  1.8  56   240 timeout 960   800   12000 4400
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   12000 220 .89 0   - - error (recursion) 3.4  1.9  76   250 timeout 960   800   11000 4400
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c true 1 wit inspect 880   880   9600 240 .90 0   - - error (recursion) 3.6  2.0  74   240 timeout 960   890   19000 5800
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 31   31   390 120 .88 0   - - error (recursion) 3.2  1.8  64   250 true 34   20   490 1100
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   8600 240 .89 0   - - error (recursion) 3.4  1.9  76   250 timeout 960   890   12000 5800
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   9000 250 .89 0   - - error (recursion) 3.3  1.9  65   250 timeout 960   890   12000 5800
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   9600 240 .89 0   - - error (recursion) 3.3  1.9  74   240 timeout 960   890   24000 5800
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 880   880   10000 220 .89 0   - - error (recursion) 3.4  1.9  68   240 true 9.2 5.0 120 340
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 880   880   11000 220 .89 0   - - error (recursion) 3.5  2.0  77   250 true 11   5.8 170 360
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c true 1 wit inspect 880   880   12000 250 .90 0   - - error (recursion) 4.2  2.4  47   250 timeout 960   840   11000 2000
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c true 1 wit inspect 880   880   9500 230 .98 0   - - error (recursion) 3.8  2.1  87   250 timeout 960   830   12000 2300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 880   880   10000 91 .90 0   - - error (recursion) 3.5  2.0  79   250 true 8.1 4.5 110 320
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c true 2 wit inspect 880   880   12000 120 .92 0   - - error (recursion) 3.7  2.1  76   250 true 16   9.2 160 490
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (1) 0 wit inspect 84   84   1200 180 .91 0   - - error (invalid witness file) .50 .32 5.6 41 error (invalid witness file) 5.5 3.0 56 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (1) 0 wit inspect 1.9 1.9 26 74 .89 0   - - error (invalid witness file) .53 .34 7.7 42 error (invalid witness file) 7.0 3.6 100 320
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (1) 0 wit inspect 13   13   180 85 .89 0   - - error (invalid witness file) .50 .32 4.6 41 error (invalid witness file) 5.8 3.1 100 300
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect 1.8 1.8 22 98 .88 0   false(no-overflow) 3.2  1.8  65 240 false(no-overflow) 7.0 3.7 110 310 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect 2.0 1.9 23 110 .90 0   false(no-overflow) 3.2  1.8  74 240 false(no-overflow) 7.3 3.9 140 320 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect 1.9 2.0 29 110 .93 0   false(no-overflow) 3.2  1.8  70 230 false(no-overflow) 7.4 3.9 110 320 - -
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 880   930   11000 300 .86 0   error (invalid witness file) .50 .33 10 41 error (invalid witness file) 6.1 3.3 130 290 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect 2.4 2.4 26 120 .94 0   false(no-overflow) 3.3  1.9  65 240 false(no-overflow) 7.9 4.2 150 320 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect 2.2 2.3 27 120 .94 0   false(no-overflow) 3.2  1.8  68 240 false(no-overflow) 8.1 4.2 110 330 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect 1.8 1.7 20 83 .90 0   false(no-overflow) 3.2  1.8  73 240 error (1) 7.1 3.8 110 330 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.6 2.6 29 160 1.2  0   - - true 11    5.7  170   450 true 8.6 4.7 160 330
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.6 2.5 34 150 1.2  0   - - true 12    6.0  200   460 true 8.0 4.3 130 320
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect 2.5 2.6 31 140 1.2  0   - - true 20    10    330   580 true 8.3 4.5 160 330
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.4 1.5 17 81 .91 0   - - true 5.2  3.0  120   310 true 7.5 4.1 110 320
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.4 1.5 18 80 .90 0   - - true 5.3  3.0  100   300 true 8.3 4.5 170 320
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.4 1.5 17 78 .90 0   - - true 5.2  2.9  110   310 true 8.6 4.6 140 330
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.5 1.6 21 88 .90 0   - - true 4.6  2.6  92   270 true 13   7.3 140 440
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.3 1.4 14 66 1.0  0   - - true 4.8  2.6  110   290 true 6.2 3.4 100 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.3 1.3 14 80 .86 0   - - true 4.2  2.3  86   280 true 7.0 3.7 120 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.3 1.3 17 74 .87 0   - - true 4.4  2.5  90   280 true 6.9 3.7 110 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.3 1.3 18 79 .88 0   - - true 4.3  2.5  84   280 true 6.5 3.5 88 320
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.3 1.3 15 78 .85 0   - - true 4.2  2.3  96   270 true 7.1 3.8 120 320
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.3 1.4 17 75 .88 0   - - true 4.5  2.5  94   300 true 6.1 3.3 94 300
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.3 1.4 16 76 .88 0   - - true 4.5  2.5  84   280 true 6.6 3.5 100 310
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.4 1.4 18 72 .90 0   - - true 5.8  3.2  110   290 error (1) 6.8 3.6 83 320
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.1 2.1 25 87 .89 0   - - true 4.7  2.6  110   280 true 7.0 3.8 77 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect 2.1 2.1 26 95 .90 0   - - true 5.3  3.0  75   280 true 7.0 3.7 57 320
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.4 1.4 17 77 .89 0   - - true 5.1  2.8  120   280 true 7.3 3.9 100 330
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect 1.3 1.3 16 73 .88 0   - - true 4.7  2.6  100   280 true 6.7 3.6 96 310
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.4 1.3 15 80 .88 0   - - true 4.6  2.5  81   280 true 6.7 3.6 81 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 76 18000 18000 210000 7900 49   0   54 30 17 640 2200   54 74 40 1300 3200   54 200 110 3800 12000   54 13000 11000 190000 89000  
    correct results 35 61 3600 3600 44000 3500 32   0   7 29 17 630 2200   8 68 36 1100 2900   21 140 79 2800 7800   25 240 130 3400 9400  
        correct true 26 52 3600 3600 44000 2600 24   0   0 0 0 0 0   0 0 0 0 0   21 140 79 2800 7800   25 240 130 3400 9400  
        correct false 9 9 17 17 210 870 8.2 0   7 29 17 630 2200   8 68 36 1100 2900   0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 15 15 13000 13000 150000 3700 14   0   0 0 0 0 0   0 0 0 0 0   0 52 30 1000 3700   0 13000 11000 180000 78000  
        correct-unconfirmed true 15 15 13000 13000 150000 3700 14   0   0 0 0 0 0   0 0 0 0 0   0 52 30 1000 3700   0 13000 11000 180000 78000  
        correct-unconfirmed false 0
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (54 tasks, max score: 98) 76
Run set sv-comp17.Overflows-Other