Tool ESBMC ESBMC version 3.1 64-bit x86_64 linux
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 15:09:43 CET [[ 2017-01-14 22:26:56 CET ]] [[ 2017-01-14 23:59:25 CET ]] [[ 2017-01-14 22:42:14 CET ]] [[ 2017-01-15 00:15:34 CET ]]
Run set sv-comp17.ReachSafety-Recursive
Options -s falsi [[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ -witnessValidation -setprop witness.checkProgramHash=false -disable-java-assertions -heap 10000m -witness ../../results-verified/esbmc-falsi.2017-01-11_1509.logfiles/sv-comp17.${inputfile_name}.files/witness.graphml ]][[ --validate ../../results-verified/esbmc-falsi.2017-01-11_1509.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/Ackermann02_false-unreach-call_true-no-overflow_true-termination.c 1 .47  .46  1.3  23 .84 0   6.6  3.6  84 290 10   5.5 150 350
recursive/Addition02_false-unreach-call_true-no-overflow_true-termination.c 1 .091 .090 .93 23 .84 0   5.1  2.8  75 290 7.6 4.1 92 320
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call_true-no-overflow_true-termination.c 1 .073 .072 .88 23 .84 0   3.7  2.0  74 280 9.0 4.8 100 320
recursive/EvenOdd03_false-unreach-call_true-no-overflow_true-termination.c 1 .11  .11  .73 23 .84 0   4.8  2.6  75 280 7.0 3.7 140 310
recursive/Fibonacci04_false-unreach-call_true-no-overflow_true-termination.c 1 .12  .12  1.2  23 .84 0   64    43    600 1500 96   65   1300 5200
recursive/Fibonacci05_false-unreach-call_true-no-overflow_true-termination.c 0 2.3   2.2   6.4  73 .84 0   97    70    1300 4200 97   74   1300 5100
recursive/McCarthy91_false-unreach-call_true-no-overflow_true-termination.c 1 .074 .074 .83 23 .84 0   4.5  2.4  68 290 7.2 3.8 110 310
recursive/Ackermann01_true-unreach-call_true-no-overflow.c 0 260     260     3000    15000 .84 0   .52 .34 8.9 41 6.4 3.4 130 310
recursive/Ackermann03_true-unreach-call_true-no-overflow.c 0 290     290     3500    15000 .84 0   .52 .32 12   39 5.9 3.1 120 290
recursive/Ackermann04_true-unreach-call_true-no-overflow.c 0 380     380     3900    15000 .84 0   .51 .33 11   40 5.9 3.1 120 290
recursive/Addition01_true-unreach-call_true-no-overflow_true-termination.c 0 470     470     3400    15000 .84 0   .49 .32 10   40 6.5 3.4 130 310
recursive/Addition03_true-unreach-call_true-no-overflow_true-termination.c 0 240     230     2200    15000 .84 0   .56 .37 13   44 5.7 3.0 110 290
recursive/EvenOdd01_true-unreach-call_true-no-overflow_true-termination.c 0 800     790     9500    15000 .84 0   .75 .48 9.1 43 7.1 3.7 120 330
recursive/Fibonacci01_true-unreach-call_true-no-overflow.c 0 900     900     11000    3200 .84 0   .49 .34 6.1 39 6.4 3.4 120 300
recursive/Fibonacci02_true-unreach-call_true-no-overflow_true-termination.c 0 900     860     11000    11000 .84 0   .53 .35 11   39 5.8 3.1 110 290
recursive/Fibonacci03_true-unreach-call_true-no-overflow_true-termination.c 0 900     900     12000    5800 .84 0   .53 .34 4.1 41 5.4 2.9 89 290
recursive/McCarthy91_true-unreach-call_true-no-overflow_true-termination.c 0 900     900     10000    7000 .84 0   .52 .33 11   40 6.3 3.3 120 300
recursive/MultCommutative_true-unreach-call_true-no-overflow_true-termination.c 0 900     900     8100    9800 .84 0   .47 .30 6.2 39 6.0 3.1 100 290
recursive/Primes_true-unreach-call_true-no-overflow_false-termination.c 0 310     310     3400    15000 .84 0   .49 .32 7.2 40 5.7 3.0 100 300
recursive/gcd01_true-unreach-call_true-no-overflow_true-termination.c 0 900     900     11000    160 .84 0   .52 .33 7.6 40 6.4 3.3 120 300
recursive/gcd02_true-unreach-call_true-no-overflow_true-termination.c 0 900     900     12000    850 .84 0   .53 .36 4.1 41 6.4 3.4 130 300
recursive/recHanoi01_true-unreach-call_true-no-overflow_true-termination.c 0 380     380     3200    15000 .84 0   .52 .34 4.5 40 6.4 3.4 120 300
recursive/recHanoi02_true-unreach-call_true-no-overflow_true-termination.c 0 440     440     5400    15000 .84 0   .50 .31 7.6 39 5.7 3.1 120 300
recursive/recHanoi03_true-unreach-call_true-no-overflow_true-termination.c 0 460     450     5100    15000 .84 0   .50 .32 11   39 6.1 3.3 120 300
recursive-simple/afterrec_2calls_false-unreach-call_true-termination.c 1 .074 .073 .74 23 .84 0   3.7  2.1  67 280 6.7 3.6 130 300
recursive-simple/afterrec_false-unreach-call_true-termination.c 1 .11  .11  .57 23 .84 0   3.7  2.1  59 270 5.9 3.2 86 310
recursive-simple/fibo_10_false-unreach-call.c 1 .54  .50  1.5  23 .84 0   10    5.4  120 450 7.6 4.1 130 320
recursive-simple/fibo_15_false-unreach-call.c 1 .96  .92  15    33 .88 0   61    46    870 2000 6.8 3.7 110 320
recursive-simple/fibo_20_false-unreach-call.c 0 63     56     120    260 .84 0   97    82    950 1500 7.3 3.9 130 320
recursive-simple/fibo_25_false-unreach-call.c 0 210     210     2900    3000 .84 0   97    66    1200 6100 6.6 3.5 81 310
recursive-simple/fibo_2calls_10_false-unreach-call.c 1 .13  .13  1.4  23 .84 0   9.2  4.9  140 460 7.6 4.0 110 320
recursive-simple/fibo_2calls_15_false-unreach-call.c 1 .65  .62  7.5  25 .84 0   39    28    410 1900 8.7 4.6 95 310
recursive-simple/fibo_2calls_20_false-unreach-call.c 0 7.8   7.5   99    170 .84 0   97    85    1500 1700 7.1 3.8 120 310
recursive-simple/fibo_2calls_25_false-unreach-call.c 0 130     130     1600    2000 .84 0   97    56    1300 4700 8.2 4.3 100 310
recursive-simple/fibo_2calls_2_false-unreach-call_true-termination.c 1 .082 .081 .74 23 .84 0   4.5  2.5  56 280 7.1 3.8 110 320
recursive-simple/fibo_2calls_4_false-unreach-call_true-termination.c 1 .10  .099 .83 23 .84 0   4.6  2.5  76 280 6.7 3.6 77 310
recursive-simple/fibo_2calls_5_false-unreach-call_true-termination.c 1 .076 .075 .95 23 .84 0   4.6  2.5  56 290 7.0 3.7 96 310
recursive-simple/fibo_2calls_6_false-unreach-call_true-termination.c 1 .095 .094 .80 23 .84 0   6.4  3.5  72 280 7.1 3.8 120 320
recursive-simple/fibo_2calls_8_false-unreach-call.c 1 .12  .12  .76 23 .84 0   6.6  3.6  110 300 9.2 4.9 97 320
recursive-simple/fibo_5_false-unreach-call_true-termination.c 1 .078 .077 .82 23 .84 0   4.8  2.7  98 280 6.7 3.7 120 310
recursive-simple/fibo_7_false-unreach-call.c 1 .091 .090 .97 23 .84 0   5.5  3.0  120 290 7.3 3.8 150 320
recursive-simple/id2_b3_o2_false-unreach-call.c 1 .081 .081 .87 23 .84 0   5.1  2.8  90 290 8.2 4.4 160 340
recursive-simple/id2_i5_o5_false-unreach-call_true-termination.c 1 .11  .11  .65 23 .84 0   5.1  2.8  61 280 9.2 4.9 100 320
recursive-simple/id_b3_o2_false-unreach-call.c 1 .10  .10  .86 23 .84 0   4.4  2.4  36 280 9.8 5.3 180 350
recursive-simple/id_i10_o10_false-unreach-call_true-termination.c 1 .087 .087 .97 23 .84 0   4.3  2.3  56 290 9.6 5.1 110 320
recursive-simple/id_i15_o15_false-unreach-call_true-termination.c 1 .093 .092 .99 23 .84 0   4.6  2.5  72 290 6.8 3.7 110 320
recursive-simple/id_i20_o20_false-unreach-call_true-termination.c 1 .12  .12  1.0  23 .84 0   5.3  2.9  82 280 6.5 3.5 120 310
recursive-simple/id_i25_o25_false-unreach-call_true-termination.c 1 .12  .12  1.3  23 .84 0   5.3  2.9  110 280 6.7 3.5 98 310
recursive-simple/id_i5_o5_false-unreach-call_true-termination.c 1 .078 .077 .81 23 .84 0   4.1  2.2  47 290 6.7 3.6 76 320
recursive-simple/id_o1000_false-unreach-call.c 0 900     900     13000    6200 .84 0   .49 .32 11 40 7.5 3.9 82 300
recursive-simple/id_o100_false-unreach-call.c 0 8.8   8.7   130    250 .84 0   97    75    1100 4100 96   71   1100 5400
recursive-simple/id_o10_false-unreach-call.c 1 .11  .11  1.4  23 .84 0   7.9  4.2  84 330 97   62   1300 6500
recursive-simple/id_o200_false-unreach-call.c 0 67     66     940    1000 .84 0   96    76    2200 4100 97   70   1100 6000
recursive-simple/id_o20_false-unreach-call.c 1 .26  .25  2.5  28 .84 0   15    7.8  170 550 97   64   1100 5800
recursive-simple/id_o3_false-unreach-call.c 1 .11  .11  .89 23 .84 0   4.4  2.4  59 280 9.9 5.3 150 340
recursive-simple/sum_10x0_false-unreach-call_true-termination.c 1 .12  .12  .82 23 .84 0   4.4  2.4  69 290 6.6 3.5 130 310
recursive-simple/sum_15x0_false-unreach-call_true-termination.c 1 .36  .35  .94 23 .84 0   5.3  2.9  76 290 7.2 3.8 120 320
recursive-simple/sum_20x0_false-unreach-call_true-termination.c 1 .12  .11  1.4  23 .84 0   6.0  3.3  79 290 6.9 3.7 140 320
recursive-simple/sum_25x0_false-unreach-call_true-termination.c 1 .48  .45  1.2  23 .99 0   6.0  3.3  57 280 7.0 3.7 81 310
recursive-simple/sum_2x3_false-unreach-call_true-termination.c 1 .10  .10  .82 23 .84 0   5.0  2.8  53 270 6.9 3.7 140 310
recursive-simple/sum_non_eq_false-unreach-call.c 1 .073 .073 .89 23 .84 0   3.8  2.1  87 270 7.1 3.8 130 310
recursive-simple/sum_non_false-unreach-call_true-termination.c 1 .077 .077 .79 23 .84 0   3.7  2.1  81 270 6.9 3.7 81 320
recursive-simple/afterrec_2calls_true-unreach-call_true-termination.c 0 880     800     11000    15000 .84 0   .50 .33 12   40 6.0 3.2 120 310
recursive-simple/afterrec_true-unreach-call_true-termination.c 0 880     800     11000    15000 .84 0   .53 .33 4.3 39 5.8 3.1 110 290
recursive-simple/fibo_10_true-unreach-call.c 0 900     860     12000    11000 .84 0   .52 .33 13   42 6.3 3.3 120 310
recursive-simple/fibo_15_true-unreach-call.c 0 900     860     12000    9800 .84 0   .62 .39 7.5 40 5.5 2.9 110 290
recursive-simple/fibo_20_true-unreach-call.c 0 900     870     11000    8400 .84 0   .51 .33 12   39 5.5 3.0 110 280
recursive-simple/fibo_25_true-unreach-call.c 0 900     870     11000    8500 .84 0   .57 .37 9.9 43 5.7 3.1 110 290
recursive-simple/fibo_2calls_10_true-unreach-call.c 0 900     860     12000    11000 .84 0   .52 .34 13   39 5.7 3.0 100 290
recursive-simple/fibo_2calls_15_true-unreach-call.c 0 900     860     12000    9500 .84 0   .53 .33 8.0 41 6.9 3.6 130 320
recursive-simple/fibo_2calls_20_true-unreach-call.c 0 900     870     11000    8200 .84 0   .50 .32 4.8 41 6.5 3.4 120 310
recursive-simple/fibo_2calls_25_true-unreach-call.c 0 900     870     11000    7900 .84 0   .50 .31 8.8 40 5.6 3.0 120 290
recursive-simple/fibo_2calls_2_true-unreach-call_true-termination.c 0 900     860     12000    11000 .84 0   .51 .33 12   41 5.4 2.9 110 290
recursive-simple/fibo_2calls_4_true-unreach-call_true-termination.c 0 900     860     14000    11000 .84 0   .52 .33 11   41 5.8 3.1 120 290
recursive-simple/fibo_2calls_5_true-unreach-call_true-termination.c 0 900     860     13000    12000 .84 0   .55 .35 6.9 39 6.3 3.3 130 300
recursive-simple/fibo_2calls_6_true-unreach-call_true-termination.c 0 900     860     13000    11000 .84 0   .50 .33 9.4 39 6.4 3.4 120 290
recursive-simple/fibo_2calls_8_true-unreach-call_true-termination.c 0 900     860     14000    11000 .84 0   .51 .33 13   40 6.2 3.2 120 300
recursive-simple/fibo_5_true-unreach-call_true-termination.c 0 900     850     12000    12000 .84 0   .50 .33 7.9 40 5.9 3.2 120 300
recursive-simple/fibo_7_true-unreach-call.c 0 900     850     12000    12000 .84 0   .61 .40 7.9 40 5.9 3.2 100 300
recursive-simple/id2_b2_o3_true-unreach-call.c 0 570     560     6900    15000 .84 0   .51 .35 5.2 41 5.7 3.0 110 300
recursive-simple/id2_b3_o5_true-unreach-call.c 0 900     900     11000    12000 .84 0   .50 .32 8.9 39 6.0 3.2 120 300
recursive-simple/id2_b5_o10_true-unreach-call.c 0 900     900     11000    14000 .84 0   .51 .33 12   39 5.8 3.1 110 300
recursive-simple/id2_i5_o5_true-unreach-call_true-termination.c 0 900     850     11000    13000 .84 0   .49 .33 8.1 40 6.1 3.2 120 290
recursive-simple/id_b2_o3_true-unreach-call.c 0 540     540     6600    15000 .84 0   .55 .34 12   42 6.1 3.2 110 310
recursive-simple/id_b3_o5_true-unreach-call.c 0 820     810     9900    15000 .84 0   .54 .36 5.6 41 6.0 3.2 110 290
recursive-simple/id_b5_o10_true-unreach-call.c 0 630     630     7700    15000 .84 0   .53 .33 11   39 5.6 3.0 110 300
recursive-simple/id_i10_o10_true-unreach-call_true-termination.c 0 900     850     13000    13000 .84 0   .48 .32 3.9 40 5.2 2.8 100 290
recursive-simple/id_i15_o15_true-unreach-call_true-termination.c 0 900     850     12000    12000 .84 0   .49 .32 9.2 40 6.2 3.2 120 310
recursive-simple/id_i20_o20_true-unreach-call_true-termination.c 0 900     850     12000    12000 .84 0   .63 .39 10   43 5.8 3.1 100 300
recursive-simple/id_i25_o25_true-unreach-call_true-termination.c 0 900     860     14000    11000 .84 0   .57 .37 8.0 39 5.9 3.1 120 300
recursive-simple/id_i5_o5_true-unreach-call_true-termination.c 0 900     850     14000    13000 .84 0   .54 .34 12   41 6.4 3.4 110 300
recursive-simple/sum_10x0_true-unreach-call_true-termination.c 0 900     860     12000    14000 .84 0   .53 .34 12   42 6.2 3.3 110 290
recursive-simple/sum_15x0_true-unreach-call_true-termination.c 0 900     860     11000    13000 .84 0   .58 .39 9.8 43 5.5 2.9 110 280
recursive-simple/sum_20x0_true-unreach-call_true-termination.c 0 900     860     14000    12000 .84 0   .62 .39 10   43 5.9 3.1 120 300
recursive-simple/sum_25x0_true-unreach-call_true-termination.c 0 900     870     12000    11000 .84 0   .54 .35 12   43 6.3 3.3 120 300
recursive-simple/sum_2x3_true-unreach-call_true-termination.c 0 900     850     11000    13000 .84 0   .51 .33 7.6 41 5.8 3.1 130 300
recursive-simple/sum_non_eq_true-unreach-call.c 0 900     900     11000    1100 .84 0   .50 .33 11   41 6.4 3.4 130 310
recursive-simple/sum_non_true-unreach-call_true-termination.c 0 580     570     7700    15000 .84 0   .58 .38 4.7 44 5.9 3.2 110 300
../../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 98 37 43000   41000   550000 620000 82   0   98 1000 730 14000 42000 98 870 560 12000 46000 98 28 18 480 2200   98 320 170 6100 16000  
    correct results 37 37 6.6 6.5 57 870 31   0   37 350 220 4600 16000 34 550 330 7700 28000 0 0 0 0 0   0 0 0 0 0  
        correct true 0
        correct false 37 37 6.6 6.5 57 870 31   0   36 350 220 4600 16000 10 550 330 7700 28000 0 0 0 0 0   0 0 0 0 0  
    correct-unconfimed results 7 0 490   470   5800 6700 5.9 0   0 680 510 9600 26000 4 320 230 4000 18000 0 0 0 0 0   0 0 0 0 0  
        correct-unconfirmed true 0
        correct-unconfirmed false 7 0 490   470   5800 6700 5.9 0   0 680 510 9600 26000 0 320 230 4000 18000 0 0 0 0 0   0 0 0 0 0  
    incorrect results 0
        incorrect true 0
        incorrect false 0
score (98 tasks, max score: 151) 37
Run set sv-comp17.ReachSafety-Recursive