Tool CBMC
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-22-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-03 00:42:25 CET [[ 2016-01-15 08:22:02 CET ]] [[ 2016-01-15 21:54:19 CET ]]
Run set sv-comp16.Recursive
Options --graphml-cex error-witness.graphml [[ -witness-check -disable-java-assertions -heap 10000m -setprop cpa.arg.errorPath.graphml=error-witness.graphml -spec ../../results-verified/cbmc.2016-01-03_0042.logfiles/sv-comp16.${inputfile_name}.files/error-witness.graphml ]][[ ../../results-verified/cbmc.2016-01-03_0042.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 2.1  2.1  78 11   6.0 440 13 7.3 340
recursive/Addition02_false-unreach-call_false-termination.c .11 .12 25 7.3 4.1 370 13 8.0 330
recursive/BallRajamani-SPIN2000-Fig1_false-unreach-call.c .16 .18 24 6.5 3.6 360 14 8.1 360
recursive/EvenOdd03_false-unreach-call_false-termination.c .18 .19 25 8.0 4.4 380 14 7.6 340
recursive/Fibonacci04_false-unreach-call_true-termination.c .74 .76 34 90   60   1400 40 22   860
recursive/Fibonacci05_false-unreach-call_true-termination.c 850    850    270
recursive/McCarthy91_false-unreach-call_false-termination.c .14 .15 24 4.9 3.1 220 11 6.2 330
recursive/Ackermann01_true-unreach-call.c 850    850    520
recursive/Ackermann03_true-unreach-call.c 850    850    510
recursive/Ackermann04_true-unreach-call.c 850    850    520
recursive/Addition01_true-unreach-call_true-termination.c 850    850    12000
recursive/Addition03_true-unreach-call.c 850    850    13000
recursive/EvenOdd01_true-unreach-call_true-termination.c 66    66    420
recursive/Fibonacci01_true-unreach-call.c 850    850    270
recursive/Fibonacci02_true-unreach-call_true-termination.c 1.2  1.2  24
recursive/Fibonacci03_true-unreach-call_true-termination.c 850    850    270
recursive/McCarthy91_true-unreach-call.c 850    850    1200
recursive/MultCommutative_true-unreach-call_true-termination.c 850    850    400
recursive/Primes_true-unreach-call.c 850    850    290
recursive/gcd01_true-unreach-call_true-termination.c 850    850    2900
recursive/gcd02_true-unreach-call.c 850    850    190
recursive/recHanoi01_true-unreach-call_true-termination.c 850    850    660
recursive/recHanoi02_true-unreach-call_true-termination.c 12    12    78
recursive/recHanoi03_true-unreach-call_true-termination.c 5.0  5.0  88
recursive-simple/afterrec_2calls_false-unreach-call.c .13 .14 24 6.6 3.9 350 12 7.5 330
recursive-simple/afterrec_false-unreach-call.c .15 .16 24 5.8 3.3 340 13 6.9 360
recursive-simple/fibo_10_false-unreach-call.c .31 .33 27 91   70   2000 77 47   860
recursive-simple/fibo_15_false-unreach-call.c 3.3  3.4  90 27   14   1100 91 58   2100
recursive-simple/fibo_20_false-unreach-call.c 310    310    970 92   47   4400 91 58   2100
recursive-simple/fibo_25_false-unreach-call.c 850    850    480
recursive-simple/fibo_2calls_10_false-unreach-call.c .31 .33 27 7.0 3.9 290 91 55   1400
recursive-simple/fibo_2calls_15_false-unreach-call.c 3.3  3.3  94 14   7.6 810 91 59   2000
recursive-simple/fibo_2calls_20_false-unreach-call.c 250    250    1000 65   33   2900 91 58   1700
recursive-simple/fibo_2calls_25_false-unreach-call.c 850    850    490
recursive-simple/fibo_2calls_2_false-unreach-call.c .13 .14 24 4.7 2.7 210 14 7.8 330
recursive-simple/fibo_2calls_4_false-unreach-call.c .12 .13 24 4.4 2.5 220 38 22   530
recursive-simple/fibo_2calls_5_false-unreach-call.c .14 .15 24 5.1 3.0 230 28 18   490
recursive-simple/fibo_2calls_6_false-unreach-call.c .12 .13 24 5.2 2.9 220 38 22   680
recursive-simple/fibo_2calls_8_false-unreach-call.c .26 .28 25 5.6 3.2 240 92 55   1300
recursive-simple/fibo_5_false-unreach-call.c .28 .30 24 19   9.7 530 20 12   500
recursive-simple/fibo_7_false-unreach-call.c .24 .25 24 70   46   2000 34 20   590
recursive-simple/id2_b3_o2_false-unreach-call.c .13 .14 24 7.9 4.4 360 13 7.7 330
recursive-simple/id2_i5_o5_false-unreach-call.c .12 .13 24 4.0 2.3 220 15 8.4 350
recursive-simple/id_b3_o2_false-unreach-call.c .12 .13 24 7.2 4.0 360 14 8.3 340
recursive-simple/id_i10_o10_false-unreach-call.c .38 .40 24 8.8 4.9 410 12 7.6 330
recursive-simple/id_i15_o15_false-unreach-call.c .38 .40 24 10   5.7 440 15 9.0 360
recursive-simple/id_i20_o20_false-unreach-call.c .53 .56 24 13   6.8 510 13 7.7 370
recursive-simple/id_i25_o25_false-unreach-call.c .69 .72 24 18   9.4 540 14 8.4 370
recursive-simple/id_i5_o5_false-unreach-call.c .24 .26 24 7.0 3.9 360 16 9.0 340
recursive-simple/id_o1000_false-unreach-call.c 3.6  3.7  70
recursive-simple/id_o100_false-unreach-call.c 1.9  2.0  39 90   62   2000 20 11   580
recursive-simple/id_o10_false-unreach-call.c .40 .43 24 10   5.5 440 12 6.3 330
recursive-simple/id_o200_false-unreach-call.c 1.8  1.8  37 90   73   1400 26 14   690
recursive-simple/id_o20_false-unreach-call.c .67 .70 25 19   10   550 14 7.6 360
recursive-simple/id_o3_false-unreach-call.c .24 .25 24 7.5 4.2 350 11 5.9 350
recursive-simple/sum_10x0_false-unreach-call.c .36 .38 24 9.0 4.9 400 25 17   490
recursive-simple/sum_15x0_false-unreach-call.c .52 .55 24 11   5.9 440 24 16   500
recursive-simple/sum_20x0_false-unreach-call.c .62 .65 24 12   6.3 510 34 22   680
recursive-simple/sum_25x0_false-unreach-call.c .75 .79 24 14   7.5 590 44 30   750
recursive-simple/sum_2x3_false-unreach-call.c .12 .13 24 6.5 3.7 360 14 7.9 340
recursive-simple/sum_non_eq_false-unreach-call.c .12 .13 24 6.4 3.6 360 11 6.0 330
recursive-simple/sum_non_false-unreach-call.c .12 .13 24 6.4 3.6 350 13 6.8 350
recursive-simple/afterrec_2calls_true-unreach-call.c .97 1.0  24
recursive-simple/afterrec_true-unreach-call.c .84 .88 24
recursive-simple/fibo_10_true-unreach-call.c 1.2  1.3  24
recursive-simple/fibo_15_true-unreach-call.c 13    13    32
recursive-simple/fibo_20_true-unreach-call.c 850    850    320
recursive-simple/fibo_25_true-unreach-call.c 850    850    460
recursive-simple/fibo_2calls_10_true-unreach-call.c 1.4  1.4  24
recursive-simple/fibo_2calls_15_true-unreach-call.c 15    15    32
recursive-simple/fibo_2calls_20_true-unreach-call.c 850    850    330
recursive-simple/fibo_2calls_25_true-unreach-call.c 850    850    470
recursive-simple/fibo_2calls_2_true-unreach-call.c .90 .95 24
recursive-simple/fibo_2calls_4_true-unreach-call.c .85 .90 24
recursive-simple/fibo_2calls_5_true-unreach-call.c .93 .97 24
recursive-simple/fibo_2calls_6_true-unreach-call.c .69 .71 24
recursive-simple/fibo_2calls_8_true-unreach-call.c 1.1  1.1  24
recursive-simple/fibo_5_true-unreach-call.c .69 .73 24
recursive-simple/fibo_7_true-unreach-call.c 1.0  1.0  24
recursive-simple/id2_b2_o3_true-unreach-call.c 19    19    320
recursive-simple/id2_b3_o5_true-unreach-call.c 19    19    320
recursive-simple/id2_b5_o10_true-unreach-call.c 19    19    320
recursive-simple/id2_i5_o5_true-unreach-call.c .87 .93 24
recursive-simple/id_b2_o3_true-unreach-call.c 5.5  5.6  130
recursive-simple/id_b3_o5_true-unreach-call.c 5.6  5.6  120
recursive-simple/id_b5_o10_true-unreach-call.c 5.5  5.6  120
recursive-simple/id_i10_o10_true-unreach-call.c 1.0  1.1  24
recursive-simple/id_i15_o15_true-unreach-call.c .89 .94 24
recursive-simple/id_i20_o20_true-unreach-call.c .88 .93 24
recursive-simple/id_i25_o25_true-unreach-call.c .89 .93 24
recursive-simple/id_i5_o5_true-unreach-call.c .96 1.0  24
recursive-simple/sum_10x0_true-unreach-call.c .85 .90 24
recursive-simple/sum_15x0_true-unreach-call.c .93 .97 24
recursive-simple/sum_20x0_true-unreach-call.c .88 .92 24
recursive-simple/sum_25x0_true-unreach-call.c .96 1.0  24
recursive-simple/sum_2x3_true-unreach-call.c .98 1.0  24
recursive-simple/sum_non_eq_true-unreach-call.c 850    850    320
recursive-simple/sum_non_true-unreach-call.c 850    850    320
../../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 19000 20000 42000 98 910   570   30000   98 1300   780   26000  
    correct results 87 16000 16000 38000 32 610   380   19000   34 710   420   15000  
        correct true 53 16000 16000 37000 7 0   0   0   8 0   0   0  
        correct false 34 13 14 900 25 610   380   19000   26 710   420   15000  
    incorrect results 4 2600 2600 1300 0 0   0   0   0 0   0   0  
        incorrect true 4 2600 2600 1300 0 0   0   0   0 0   0   0  
        incorrect false 0
score (98 tasks, max score: 151) 12
Run set sv-comp16.Recursive