Tool 2LS 0.5.0
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:02:28 CET [[ 2017-01-14 22:09:21 CET ]] [[ 2017-01-14 22:27:59 CET ]] [[ 2017-01-14 22:12:16 CET ]] [[ 2017-01-14 22:31:32 CET ]]
Run set sv-comp17.Overflows-Other
Options --graphml-witness witness.graphml [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/2ls.2017-01-11_1102.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/2ls.2017-01-11_1102.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 (5) 0 wit inspect .096 .092 .87 22 .0041 0    error (invalid witness file) .55 .35 13   42 error (invalid witness file) 6.5 3.4 91 300 - -
recursive/Addition03_false-no-overflow.c error (5) 0 wit inspect .13  .12  .73 22 .0041 0    error (invalid witness file) .50 .31 8.2 40 error (invalid witness file) 7.4 3.9 62 300 - -
recursive/EvenOdd03WithOverflowBug_false-no-overflow.c error (5) 0 wit inspect .11  .10  .84 22 .0041 0    error (invalid witness file) .61 .38 11   45 error (invalid witness file) 6.5 3.4 88 300 - -
recursive/Ackermann01_true-unreach-call_true-no-overflow.c error (5) 0 wit inspect .094 .092 .71 22 .0041 0    - - error (invalid witness file) .54 .34 14   40 error (invalid witness file) 6.7 3.5 140 320
recursive/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .094 .093 .64 22 .0041 0    - - error (invalid witness file) .52 .33 10   42 error (invalid witness file) 5.2 2.8 84 290
recursive/Ackermann03_true-unreach-call_true-no-overflow.c error (5) 0 wit inspect .12  .12  .78 22 .0041 0    - - error (invalid witness file) .58 .36 9.3 39 error (invalid witness file) 6.4 3.4 97 310
recursive/Ackermann04_true-unreach-call_true-no-overflow.c error (5) 0 wit inspect .095 .091 .77 22 .0041 0    - - error (invalid witness file) .52 .33 12   40 error (invalid witness file) 6.0 3.3 110 290
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .12  .12  .70 22 .0041 0    - - error (invalid witness file) .52 .32 12   40 error (invalid witness file) 5.8 3.1 100 300
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .11  .11  .89 22 .0041 0    - - error (invalid witness file) .59 .37 11   41 error (invalid witness file) 6.5 3.4 120 320
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .081 .080 .81 22 .0041 0    - - error (invalid witness file) .67 .42 7.2 40 error (invalid witness file) 6.0 3.1 66 300
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .089 .086 .90 22 .0041 0    - - error (invalid witness file) .65 .41 7.4 41 error (invalid witness file) 8.1 4.2 76 300
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .11  .10  .83 22 .0041 0    - - error (invalid witness file) .51 .32 9.3 41 error (invalid witness file) 6.3 3.3 93 310
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .098 .097 .87 22 .0041 0    - - error (invalid witness file) .52 .34 10   40 error (invalid witness file) 5.9 3.2 95 300
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c error (5) 0 wit inspect .10  .097 .76 22 .0041 0    - - error (invalid witness file) .66 .41 7.9 40 error (invalid witness file) 6.9 3.7 110 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .11  .10  .76 22 .0041 0    - - error (invalid witness file) .69 .44 8.2 44 error (invalid witness file) 6.0 3.2 110 300
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .10  .098 .75 22 .0041 0    - - error (invalid witness file) .56 .36 8.9 39 error (invalid witness file) 5.6 3.0 120 290
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .10  .10  .97 22 .0041 0    - - error (invalid witness file) .58 .37 9.6 39 error (invalid witness file) 7.4 3.9 86 300
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .094 .090 1.0  22 .0041 0    - - error (invalid witness file) .65 .42 7.3 42 error (invalid witness file) 8.6 4.5 74 310
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .084 .084 .68 22 .0041 0    - - error (invalid witness file) .50 .34 10   41 error (invalid witness file) 5.7 3.1 110 300
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .11  .11  .67 22 .0041 0    - - error (invalid witness file) .50 .33 11   39 error (invalid witness file) 7.9 4.1 90 290
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .097 .097 .85 22 .0041 0    - - error (invalid witness file) .52 .34 12   40 error (invalid witness file) 6.6 3.5 91 300
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c error (5) 0 wit inspect .13  .12  .63 22 .0041 0    - - error (invalid witness file) .50 .32 12   40 error (invalid witness file) 6.9 3.7 92 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .084 .081 1.0  22 .0041 0    - - error (invalid witness file) .51 .33 10   39 error (invalid witness file) 6.8 3.6 95 310
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .095 .092 .92 22 .0041 0    - - error (invalid witness file) .53 .34 9.9 39 error (invalid witness file) 7.6 4.0 71 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .12  .11  .67 22 .0041 0    - - error (invalid witness file) .49 .32 12   40 error (invalid witness file) 7.9 4.1 74 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .12  .12  .72 22 .0041 0    - - error (invalid witness file) .67 .43 8.4 40 error (invalid witness file) 5.7 3.1 110 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c error (5) 0 wit inspect .098 .095 .77 22 .0041 0    - - error (invalid witness file) .52 .33 10   40 error (invalid witness file) 7.2 3.8 81 300
bitvector/jain_1_false-no-overflow.i false(no-overflow) 1 wit inspect .095 .091 .86 22 0      0    false(no-overflow) 3.7  2.1  52   240 false(no-overflow) 9.4 5.0 100 340 - -
bitvector/jain_2_false-no-overflow.i false(no-overflow) 1 wit inspect .11  .10  .88 23 0      0    true 3.2  1.8  53   240 false(no-overflow) 7.8 4.2 110 310 - -
bitvector/jain_4_false-no-overflow.i false(no-overflow) 1 wit inspect .10  .10  .93 23 0      0    true 4.2  2.3  43   240 false(no-overflow) 9.9 5.2 110 330 - -
bitvector/jain_5_false-no-overflow.i timeout 0 wit inspect 900     900     8800    1300 0      0    error (invalid witness file) .51 .33 11   42 error (invalid witness file) 7.6 4.0 66 300 - -
bitvector/jain_6_false-no-overflow.i false(no-overflow) 1 wit inspect .12  .11  1.1  26 0      .16 false(no-overflow) 3.1  1.8  77   240 false(no-overflow) 7.6 4.0 130 310 - -
bitvector/jain_7_false-no-overflow.i false(no-overflow) 1 wit inspect .11  .11  1.0  24 0      0    true 3.7  2.1  51   240 false(no-overflow) 9.4 5.0 100 320 - -
bitvector/modulus_false-no-overflow.i false(no-overflow) 1 wit inspect .12  .11  1.0  25 0      0    false(no-overflow) 3.7  2.1  65   240 error (1) 9.8 5.1 120 330 - -
bitvector/byte_add_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .14  .13  .94 24 0      0    - - true 14    7.5  120   340 true 8.3 4.5 110 320
bitvector/byte_add_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .14  .13  .93 23 0      0    - - true 11    6.0  190   450 true 7.9 4.3 130 320
bitvector/byte_add_false-unreach-call_true-no-overflow.i true 2 wit inspect .13  .13  .92 23 0      0    - - true 20    10    300   650 true 9.1 4.9 110 330
bitvector/gcd_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  .11  1.1  24 0      0    - - true 5.5  3.1  69   310 true 11   5.9 110 330
bitvector/gcd_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .10  .098 .97 23 0      0    - - true 6.1  3.5  73   300 true 10   5.6 98 310
bitvector/gcd_3_true-unreach-call_true-no-overflow.i true 2 wit inspect .10  .098 .96 23 0      0    - - true 6.4  3.6  51   300 true 9.6 5.1 100 330
bitvector/gcd_4_true-unreach-call_true-no-overflow.i true 2 wit inspect 1.2   1.2   14    39 0      0    - - true 5.4  3.0  75   280 true 15   8.3 150 440
bitvector/interleave_bits_true-unreach-call_true-no-overflow.i true 2 wit inspect .13  .13  .85 24 0      0    - - true 6.3  3.4  64   290 true 7.3 4.0 120 310
bitvector/jain_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  .11  .68 22 0      0    - - true 5.6  3.1  47   300 true 7.2 3.8 120 310
bitvector/jain_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .088 .084 .72 22 0      0    - - true 5.5  3.0  58   280 true 7.2 3.8 110 310
bitvector/jain_4_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  .11  .73 22 0      0    - - true 4.3  2.4  44   280 true 7.9 4.1 150 330
bitvector/jain_5_true-unreach-call_true-no-overflow.i true 2 wit inspect .083 .082 .78 22 0      .16 - - true 4.5  2.5  58   270 true 8.7 4.6 68 310
bitvector/jain_6_true-unreach-call_true-no-overflow.i true 2 wit inspect .10  .098 .74 23 0      0    - - true 5.8  3.2  48   280 true 7.7 4.1 120 320
bitvector/jain_7_true-unreach-call_true-no-overflow.i true 2 wit inspect .12  .11  .82 22 0      0    - - true 5.2  2.9  81   280 true 8.2 4.3 110 320
bitvector/modulus_true-unreach-call_true-no-overflow.i true 2 wit inspect .13  .12  .92 24 0      0    - - true 5.3  2.9  65   290 error (1) 7.2 3.9 91 330
bitvector/num_conversion_1_true-unreach-call_true-no-overflow.i true 2 wit inspect .089 .086 .94 22 0      0    - - true 5.7  3.1  60   300 true 9.3 4.9 110 320
bitvector/num_conversion_2_true-unreach-call_true-no-overflow.i true 2 wit inspect .098 .093 .89 22 0      0    - - true 4.6  2.5  66   280 true 8.8 4.7 99 320
bitvector/parity_true-unreach-call_true-no-overflow.i true 2 wit inspect .097 .092 .86 23 0      0    - - true 5.6  3.0  77   280 true 10   5.3 91 330
bitvector/sum02_false-unreach-call_true-no-overflow.i true 2 wit inspect .081 .080 .84 23 0      0    - - true 5.5  3.0  71   270 true 8.6 4.6 81 300
bitvector/sum02_true-unreach-call_true-no-overflow.i true 2 wit inspect .11  .11  .91 24 0      .16 - - true 6.1  3.4  66   280 true 7.5 4.0 130 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 46 910    910    8800   2500 .11 .49 54 24 14 380 1600   54 82 43 990 3100   54 150 84 1900 7300   54 340 180 4500 14000  
    correct results 26 46 4.0  3.8  36   620 0    .49 6 21 12 340 1400   5 54 29 680 1900   20 140 75 1700 6300   19 180 95 2200 6500  
        correct true 20 40 3.3  3.2  30   480 0    .33 3 0 0 0 0   0 0 0 0 0   20 140 75 1700 6300   19 180 95 2200 6500  
        correct false 6 6 .67 .63 5.8 140 0    .16 3 21 12 340 1400   5 54 29 680 1900   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) 46
Run set sv-comp17.Overflows-Other