Tool Beagle 1.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 CPArec v0.1-alpha ESBMC 1.24 Seahorn SMACK Ultimate Automizer r12950 Ultimate Kojak r12950
Limits timelimit: 900 s, memlimit: 15000 MB, CPU core limit: 8
Host cayman[1-8]
OS Linux 3.13.0
System CPU: Intel Core i7-4770 @ 3.40 GHz with 8 cores, frequency: 3.4 GHz; RAM: 33 GB
Date of execution 14-12-20 11:35 14-12-04 12:41 14-11-15 15:53 14-11-12 16:46 14-12-13 18:39 14-12-20 18:50 14-11-26 16:05 14-11-12 22:41 14-11-16 20:08
Options -t 895 --32 -sv-comp15 -disable-java-assertions -heap 10000m -o ./output --cex=witness.graphml --errorwitness witness.graphml 32bit precise 32bit precise
../../sv-benchmarks/c/recursive/ status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB)
Ackermann02_false-unreach-call_false-termination.c error 11    15 false(reach) 1.7  74 false(reach) 3.1  210 false(reach) 18    370 out of memory 170    15000 false(reach) 0.24 35 false(reach) 29    1200 false(reach) 6.2  250 false(reach) 7.7  270
Addition02_false-unreach-call_false-termination.c error 52    200 false(reach) 0.14 26 false(reach) 2.4  210 false(reach) 5.2  170 false(reach) 88    6000 false(reach) 0.34 35 false(reach) 2.7  160 false(reach) 6.3  250 false(reach) 5.8  250
Addition03_false-unreach-call.c error 14    21 true 850    12000 timeout 920    4500 timeout 920    1700 true 85    6000 false(reach) 0.21 35 true 57    2200 timeout 920    990 timeout 920    970
BallRajamani-SPIN2000-Fig1_false-unreach-call.c unknown 1.3  14 false(reach) 0.12 23 false(reach) 1.7  170 false(reach) 5.0  170 false(reach) 0.15 12 false(reach) 0.17 32 false(reach) 1.1  61 false(reach) 6.1  250 false(reach) 6.0  250
EvenOdd03_false-unreach-call_false-termination.c false(reach) 6.0  13 unknown 0.10 24 false(reach) 2.3  210 false(reach) 1.7  170 false(reach) 0.20 12 false(reach) 0.18 33 false(reach) 0.96 57 false(reach) 5.1  250 false(reach) 5.7  250
Fibonacci04_false-unreach-call_true-termination.c error 9.1  14 true 0.52 32 false(reach) 3.7  210 false(reach) 24    390 false(reach) 72    7900 false(reach) 0.20 34 false(reach) 2.1  130 false(reach) 9.8  400 false(reach) 170    1200
Fibonacci05_false-unreach-call_true-termination.c error 9.0  13 true 850    240 timeout 920    6900 timeout 920    410 false(reach) 77    8100 false(reach) 0.20 35 false(reach) 2.5  130 false(reach) 29    1200 timeout 920    1200
McCarthy91_false-unreach-call_false-termination.c false(reach) 2.5  12 false(reach) 0.13 24 false(reach) 2.2  210 false(reach) 1.7  160 false(reach) 73    3700 false(reach) 0.30 34 false(reach) 1.7  110 false(reach) 5.3  250 false(reach) 5.3  250
Ackermann01_true-unreach-call.c timeout 920    1700 true 850    350 timeout 920    1700 true 3.3  150 out of memory 160    15000 false(reach) 0.27 36 true 330    10000 true 8.7  290 timeout 920    970
Ackermann03_true-unreach-call.c error 64    340 true 850    340 timeout 920    7200 timeout 920    1600 out of memory 160    15000 false(reach) 0.24 36 true 330    10000 true 27    660 timeout 920    1200
Ackermann04_true-unreach-call.c error 64    340 true 850    340 timeout 920    7900 timeout 920    1600 out of memory 160    15000 false(reach) 0.27 36 true 330    10000 true 22    660 timeout 920    1200
Addition01_true-unreach-call_true-termination.c timeout 920    3900 true 850    10000 timeout 920    4900 true 7.2  170 false(reach) 89    6100 false(reach) 0.23 33 true 58    2200 timeout 920    660 timeout 920    970
EvenOdd01_true-unreach-call_true-termination.c error 120    720 true 0.95 32 true 3.7  220 unknown 1.7  160 true 0.091 12 false(reach) 0.19 31 true 1.4  56 timeout 920    990 timeout 920    1200
Fibonacci01_true-unreach-call.c error 25    70 true 850    240 timeout 920    4800 true 65    920 false(reach) 76    8100 false(reach) 0.23 35 true 37    1500 true 89    640 timeout 920    960
Fibonacci02_true-unreach-call_true-termination.c true 7.7  12 true 0.65 23 timeout 920    6900 timeout 920    4300 true 0.072 12 false(reach) 0.18 33 true 38    1600 true 38    720 timeout 920    960
Fibonacci03_true-unreach-call_true-termination.c error 17    20 true 850    240 timeout 920    7100 timeout 920    400 false(reach) 77    8100 false(reach) 0.22 35 true 38    1500 true 43    670 timeout 920    1200
McCarthy91_true-unreach-call.c error 16    53 true 850    1200 true 2.3  210 true 6.7  160 false(reach) 78    3700 false(reach) 0.20 34 true 23    1100 true 6.2  250 true 6.1  250
MultCommutative_true-unreach-call_true-termination.c timeout 920    5000 true 850    370 timeout 920    450 unknown 20    180 false(reach) 160    8900 false(reach) 0.24 35 true 110    3100 timeout 920    660 timeout 920    970
Primes_true-unreach-call.c unknown 480    9600 true 850    250 timeout 920    360 timeout 920    1100 out of memory 160    15000 false(reach) 0.67 41 true 510    6000 timeout 920    1300 timeout 920    1000
gcd01_true-unreach-call_true-termination.c unknown 240    4200 true 850    3500 timeout 920    4700 true 3.3  150 out of memory 200    15000 false(reach) 0.25 33 true 80    2300 true 7.1  270 timeout 920    970
gcd02_true-unreach-call.c timeout 920    2300 true 850    220 timeout 920    1700 timeout 920    8900 timeout 920    8700 false(reach) 0.29 36 true 280    3700 timeout 920    1000 timeout 920    660
recHanoi01_true-unreach-call_true-termination.c error 28    65 true 850    670 true 2.3  210 timeout 920    2500 false(reach) 220    6800 false(reach) 0.23 35 true 44    1900 unknown 250    3300 timeout 920    1200
recHanoi02_true-unreach-call_true-termination.c true 12    19 true 0.56 25 true 2.2  210 true 3.1  150 false(reach) 0.16 12 false(reach) 0.29 33 true 1.3  51 true 5.9  250 true 5.9  250
recHanoi03_true-unreach-call_true-termination.c error 17    58 true 0.64 26 true 5.6  250 timeout 920    1000 false(reach) 0.12 12 false(reach) 0.28 33 true 1.3  51 unknown 43    320 timeout 920    340
../../sv-benchmarks/c/recursive/ status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB) status time(s) memory(MB)
total files 24 4900 29000 24 12000 30000 24 12000 62000 24 9400 27000 24 3000 170000 24 6.1 830 24 2300 60000 24 6100 16000 24 15000 19000
correct results 4 28 56 20 10000 18000 11 31 2300 12 140 3100 8 310 26000 8 1.9 270 23 2300 58000 16 310 7200 8 220 2900
false negatives 0 - - 3 1700 12000 0 - - 0 - - 1 85 6000 0 - - 1 57 2200 0 - - 0 - -
false positives 0 - - 0 - - 0 - - 0 - - 8 700 42000 16 4.3 560 0 - - 0 - - 0 - -
false properties 0 - - 0 - - 0 - - 0 - - 0 - - 0 - - 0 - - 0 - - 0 - -
score (24 files, max score: 40) 6 - - 0 - - 16 - - 18 - - -50 - - -88 - - 27 - - 25 - - 10 - -
Tool Beagle 1.1 CBMC 4.9 CPAchecker 1.3.10-svcomp15 CPArec v0.1-alpha ESBMC 1.24 Seahorn SMACK Ultimate Automizer r12950 Ultimate Kojak r12950