Tool ESBMC ESBMC version 2.0.0 64-bit x86_64 linux
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host [zeus01; zeus02; zeus03; zeus04; zeus05; zeus06; zeus07; zeus08; zeus09; zeus10; zeus11; zeus12; zeus13; zeus14; zeus15; zeus16; zeus17; zeus18; zeus19; zeus20; zeus21; zeus22; zeus23; zeus24]
OS Linux 4.2.0-23-generic
System CPU: Intel Xeon E5-2650 v2 @ 2.60 GHz, cores: 32, frequency: 3.4 GHz; RAM: 135149 MB
Date of execution 2016-01-16 17:45:19 CET [[ 2016-01-17 00:36:28 CET ]] [[ 2016-01-17 00:39:38 CET ]]
Run set sv-comp16.Recursive
Options [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/esbmc.2016-01-16_1745.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]]
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
recursive/Ackermann02_false-unreach-call_false-termination.c out of memory 330     330     15000 wit - -
recursive/Addition02_false-unreach-call_false-termination.c out of memory 250     250     15000 wit - -
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c error (1) 4.7   10     210 wit - -
recursive/EvenOdd03_false-unreach-call_false-termination.c false(reach) 13     12     470 wit false(reach) 7.1 4.1 360 true 11   6.6 330
recursive/Fibonacci04_false-unreach-call_true-termination.c out of memory 210     200     15000 wit - -
recursive/Fibonacci05_false-unreach-call_true-termination.c out of memory 210     210     15000 wit - -
recursive/McCarthy91_false-unreach-call_false-termination.c out of memory 240     240     15000 wit - -
recursive/Ackermann01_true-unreach-call.c out of memory 340     340     15000 wit - -
recursive/Ackermann03_true-unreach-call.c out of memory 310     310     15000 wit - -
recursive/Ackermann04_true-unreach-call.c out of memory 330     330     15000 wit - -
recursive/Addition01_true-unreach-call_true-termination.c out of memory 230     230     15000 wit - -
recursive/Addition03_true-unreach-call.c out of memory 250     250     15000 wit - -
recursive/EvenOdd01_true-unreach-call_true-termination.c true 1.1   1.1   83 wit - -
recursive/Fibonacci01_true-unreach-call.c out of memory 200     200     15000 wit - -
recursive/Fibonacci02_true-unreach-call_true-termination.c true .11  .12  13 wit - -
recursive/Fibonacci03_true-unreach-call_true-termination.c out of memory 210     210     15000 wit - -
recursive/McCarthy91_true-unreach-call.c out of memory 230     230     15000 wit - -
recursive/MultCommutative_true-unreach-call_true-termination.c out of memory 290     290     15000 wit - -
recursive/Primes_true-unreach-call.c out of memory 330     330     15000 wit - -
recursive/gcd01_true-unreach-call_true-termination.c out of memory 190     190     15000 wit - -
recursive/gcd02_true-unreach-call.c out of memory 120     120     15000 wit - -
recursive/recHanoi01_true-unreach-call_true-termination.c out of memory 190     190     15000 wit - -
recursive/recHanoi02_true-unreach-call_true-termination.c false(reach) 68     40     2900 wit - -
recursive/recHanoi03_true-unreach-call_true-termination.c false(reach) 68     40     2000 wit - -
recursive-simple/afterrec_2calls_false-unreach-call.c false(reach) 4.2   10     230 wit false(reach) 6.6 3.7 350 true 12   7.0 340
recursive-simple/afterrec_false-unreach-call.c error (1) 3.7   10     200 wit - -
recursive-simple/fibo_10_false-unreach-call.c witness timeout 74     40     2900 wit timeout 90   65   4200 true 12   7.7 330
recursive-simple/fibo_15_false-unreach-call.c witness timeout 88     41     4100 wit timeout 91   54   2100 true 12   8.1 330
recursive-simple/fibo_20_false-unreach-call.c timeout 910     140     11000 wit - -
recursive-simple/fibo_25_false-unreach-call.c timeout 910     220     12000 wit - -
recursive-simple/fibo_2calls_10_false-unreach-call.c witness timeout 76     50     3300 wit timeout 90   70   1700 true 11   6.6 330
recursive-simple/fibo_2calls_15_false-unreach-call.c witness timeout 89     41     3200 wit timeout 90   60   2600 true 15   8.9 330
recursive-simple/fibo_2calls_20_false-unreach-call.c timeout 910     140     11000 wit - -
recursive-simple/fibo_2calls_25_false-unreach-call.c timeout 900     230     11000 wit - -
recursive-simple/fibo_2calls_2_false-unreach-call.c false(reach) 7.7   10     320 wit false(reach) 5.4 3.2 230 true 11   6.2 330
recursive-simple/fibo_2calls_4_false-unreach-call.c false(reach) 84     40     3300 wit false(reach) 11   6.0 440 true 9.5 5.3 320
recursive-simple/fibo_2calls_5_false-unreach-call.c false(reach) 69     30     2600 wit false(reach) 31   16   820 true 11   6.6 340
recursive-simple/fibo_2calls_6_false-unreach-call.c false(reach) 69     40     2300 wit false(reach) 59   33   1600 true 10   6.8 320
recursive-simple/fibo_2calls_8_false-unreach-call.c witness timeout 73     40     2400 wit timeout 91   72   1600 true 11   7.2 320
recursive-simple/fibo_5_false-unreach-call.c false(reach) 70     30     2700 wit false(reach) 19   10   540 true 11   7.9 310
recursive-simple/fibo_7_false-unreach-call.c false(reach) 70     30     2300 wit false(reach) 67   37   1600 true 11   7.4 340
recursive-simple/id2_b3_o2_false-unreach-call.c false(reach) 37     11     840 wit false(reach) 8.1 4.6 380 true 12   8.0 350
recursive-simple/id2_i5_o5_false-unreach-call.c false(reach) 53     20     1700 wit false(reach) 7.0 4.1 360 true 11   6.4 320
recursive-simple/id_b3_o2_false-unreach-call.c false(reach) 12     10     440 wit false(reach) 8.6 4.8 390 true 11   6.4 330
recursive-simple/id_i10_o10_false-unreach-call.c false(reach) 31     10     690 wit false(reach) 9.4 5.2 410 true 9.4 5.2 340
recursive-simple/id_i15_o15_false-unreach-call.c false(reach) 42     10     960 wit false(reach) 16   8.3 490 true 11   6.2 320
recursive-simple/id_i20_o20_false-unreach-call.c false(reach) 44     10     970 wit false(reach) 25   13   630 true 10   6.4 310
recursive-simple/id_i25_o25_false-unreach-call.c false(reach) 47     20     1100 wit false(reach) 33   17   830 true 11   7.1 320
recursive-simple/id_i5_o5_false-unreach-call.c false(reach) 12     10     480 wit false(reach) 7.0 3.9 350 true 10   7.2 330
recursive-simple/id_o1000_false-unreach-call.c witness timeout 67     30     1900 wit timeout 91   70   2800 true 10   6.6 320
recursive-simple/id_o100_false-unreach-call.c witness timeout 67     40     1900 wit timeout 91   68   2700 true 10   6.8 320
recursive-simple/id_o10_false-unreach-call.c false(reach) 39     10     870 wit false(reach) 31   16   790 true 11   7.1 310
recursive-simple/id_o200_false-unreach-call.c witness timeout 68     40     2000 wit timeout 91   69   2800 true 11   6.1 330
recursive-simple/id_o20_false-unreach-call.c false(reach) 56     30     1500 wit false(reach) 46   26   1300 true 11   7.8 330
recursive-simple/id_o3_false-unreach-call.c false(reach) 13     10     490 wit false(reach) 11   5.9 440 true 10   7.5 310
recursive-simple/sum_10x0_false-unreach-call.c false(reach) 43     10     930 wit false(reach) 26   14   680 true 11   6.3 350
recursive-simple/sum_15x0_false-unreach-call.c false(reach) 51     20     1400 wit false(reach) 37   19   880 true 9.8 5.7 330
recursive-simple/sum_20x0_false-unreach-call.c false(reach) 72     30     2100 wit false(reach) 51   30   1500 true 10   6.0 330
recursive-simple/sum_25x0_false-unreach-call.c false(reach) 71     30     2000 wit false(reach) 80   50   1600 true 9.8 6.1 340
recursive-simple/sum_2x3_false-unreach-call.c false(reach) 13     10     500 wit false(reach) 6.5 3.7 350 true 12   6.8 340
recursive-simple/sum_non_eq_false-unreach-call.c witness timeout 79     40     3200 wit timeout 90   71   1300 true 14   7.7 350
recursive-simple/sum_non_false-unreach-call.c witness timeout 82     40     3900 wit timeout 90   71   1500 true 12   6.8 340
recursive-simple/afterrec_2calls_true-unreach-call.c true .078 .088 13 wit - -
recursive-simple/afterrec_true-unreach-call.c true .096 .11  13 wit - -
recursive-simple/fibo_10_true-unreach-call.c true .080 .089 13 wit - -
recursive-simple/fibo_15_true-unreach-call.c true .32  .33  13 wit - -
recursive-simple/fibo_20_true-unreach-call.c true 2.7   2.7   67 wit - -
recursive-simple/fibo_25_true-unreach-call.c true 29     29     700 wit - -
recursive-simple/fibo_2calls_10_true-unreach-call.c true .078 .089 13 wit - -
recursive-simple/fibo_2calls_15_true-unreach-call.c true .33  .34  13 wit - -
recursive-simple/fibo_2calls_20_true-unreach-call.c true 2.8   2.8   67 wit - -
recursive-simple/fibo_2calls_25_true-unreach-call.c true 30     30     700 wit - -
recursive-simple/fibo_2calls_2_true-unreach-call.c true .087 .10  13 wit - -
recursive-simple/fibo_2calls_4_true-unreach-call.c true .094 .11  13 wit - -
recursive-simple/fibo_2calls_5_true-unreach-call.c true .091 .10  13 wit - -
recursive-simple/fibo_2calls_6_true-unreach-call.c true .090 .10  13 wit - -
recursive-simple/fibo_2calls_8_true-unreach-call.c true .066 .077 13 wit - -
recursive-simple/fibo_5_true-unreach-call.c true .090 .10  13 wit - -
recursive-simple/fibo_7_true-unreach-call.c true .068 .079 13 wit - -
recursive-simple/id2_b2_o3_true-unreach-call.c true .94  .95  55 wit - -
recursive-simple/id2_b3_o5_true-unreach-call.c true .97  .99  55 wit - -
recursive-simple/id2_b5_o10_true-unreach-call.c true .95  .96  55 wit - -
recursive-simple/id2_i5_o5_true-unreach-call.c true .075 .086 13 wit - -
recursive-simple/id_b2_o3_true-unreach-call.c true .29  .30  16 wit - -
recursive-simple/id_b3_o5_true-unreach-call.c true .22  .23  16 wit - -
recursive-simple/id_b5_o10_true-unreach-call.c true .30  .32  16 wit - -
recursive-simple/id_i10_o10_true-unreach-call.c true .076 .088 13 wit - -
recursive-simple/id_i15_o15_true-unreach-call.c true .063 .070 13 wit - -
recursive-simple/id_i20_o20_true-unreach-call.c true .070 .080 13 wit - -
recursive-simple/id_i25_o25_true-unreach-call.c true .064 .071 13 wit - -
recursive-simple/id_i5_o5_true-unreach-call.c true .060 .068 13 wit - -
recursive-simple/sum_10x0_true-unreach-call.c true .063 .072 13 wit - -
recursive-simple/sum_15x0_true-unreach-call.c true .084 .097 13 wit - -
recursive-simple/sum_20x0_true-unreach-call.c true .10  .12  13 wit - -
recursive-simple/sum_25x0_true-unreach-call.c true .10  .11  13 wit - -
recursive-simple/sum_2x3_true-unreach-call.c true .10  .12  13 wit - -
recursive-simple/sum_non_eq_true-unreach-call.c false(reach) 74     40     2900 wit - -
recursive-simple/sum_non_true-unreach-call.c false(reach) 76     40     2500 wit - -
../../sv-benchmarks/c/ status cputime (s) walltime (s) memUsage (MB) witness wit1_status wit1_cputime (s) wit1_walltime (s) wit1_memUsage (MB) wit2_status wit2_cputime (s) wit2_walltime (s) wit2_memUsage (MB)
total tasks 98 10000 6300 390000 98 1500   1000   41000   98 370   230   11000  
    correct results 60 1100 530 33000 24 610   340   17000   24 260   160   7900  
        correct true 36 72 72 2200 0 0   0   0   24 0   0   0  
        correct false 24 1000 460 31000 24 610   340   17000   0 260   160   7900  
    incorrect results 4 290 160 10000 0 0   0   0   0 0   0   0  
        incorrect true 0
        incorrect false 4 290 160 10000 0 0   0   0   0 0   0   0  
score (98 tasks, max score: 151) 32
Run set sv-comp16.Recursive