Tool | CBMC 4.5 | CPAchecker 1.2.11-svcomp14b | ESBMC 1.22.1 | LLBMC | Predator 2013-10-30 | Symbiotic | UltimateAutomizer | UltimateKojak | ||||||||||||||||
Limits | timelimit: 900 s, memlimit: 15360 MB, CPU core limit: 8 | |||||||||||||||||||||||
OS | Linux 3.2.0-56-generic x86_64 | |||||||||||||||||||||||
System | CPU: Intel Core i7-2600 CPU @ 3.40GHz with 8 cores, frequency: 3401 MHz; RAM: 32827640 kB | |||||||||||||||||||||||
Date of execution | 13-11-18 23:43 | 13-11-18 14:59 | 13-11-18 23:26 | 13-11-21 13:28 | 13-11-19 22:09 | 13-11-24 22:54 | 13-11-19 23:49 | 13-11-21 12:52 | ||||||||||||||||
Options | --propertyfile ${sourcefile_path}/ALL.prp --32 |
-sv-comp14 -heap 10000M -spec ${sourcefile_path}/ALL.prp -disable-java-assertions |
-c ${sourcefile_path}/ALL.prp | -spec ${sourcefile_path}/ALL.prp -witness ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt |
--propertyfile ${sourcefile_path}/ALL.prp --trace ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt -m32 |
${sourcefile_path}/ALL.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt | ${sourcefile_path}/ALL.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt | |||||||||||||||||
../../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) |
Ackermann02_false.c | false(label) | 0.73 | 31 | error (recursion) | 1.9 | 130 | false(label) | 900 | 2500 | unknown | 0.15 | 2.0 | unknown | 20 | 200 | timeout | 900 | 2300 | false(label) | 3.3 | 200 | timeout | 920 | 370 |
Addition02_false.c | false(label) | 0.18 | 16 | error (recursion) | 1.9 | 130 | false(label) | 900 | 4800 | false(label) | 0.16 | 3.0 | unknown | 0.13 | 5.0 | timeout | 900 | 130 | false(label) | 3.1 | 200 | false(label) | 3.0 | 200 |
Addition03_false.c | true | 850 | 1100 | error (recursion) | 2.0 | 130 | false(label) | 900 | 4800 | unknown | 0.15 | 3.0 | unknown | 0.11 | 5.0 | timeout | 900 | 140 | timeout | 920 | 710 | timeout | 920 | 310 |
EvenOdd03_false.c | false(label) | 0.20 | 16 | error (recursion) | 1.9 | 130 | false(label) | 0.40 | 14 | false(label) | 0.12 | 2.0 | unknown | 0.11 | 5.0 | timeout | 900 | 170 | false(label) | 2.4 | 140 | false(label) | 2.7 | 160 |
Fibonacci04_false.c | false(label) | 0.36 | 19 | error (recursion) | 1.9 | 130 | false(label) | 410 | 4500 | unknown | 0.11 | 3.0 | unknown | 0.24 | 7.0 | timeout | 900 | 320 | false(label) | 6.7 | 240 | false(label) | 11 | 240 |
Fibonacci05_false.c | false(label) | 450 | 660 | error (recursion) | 1.9 | 130 | false(label) | 900 | 600 | unknown | 0.12 | 3.0 | unknown | 0.23 | 7.0 | timeout | 900 | 320 | false(label) | 650 | 390 | false(label) | 21 | 260 |
McCarthy91_false.c | false(label) | 0.19 | 16 | error (recursion) | 1.9 | 130 | false(label) | 900 | 4100 | false(label) | 0.10 | 2.0 | unknown | 0.53 | 17 | timeout | 900 | 78 | false(label) | 2.3 | 130 | false(label) | 2.5 | 150 |
Ackermann01_true.c | true | 850 | 440 | error (recursion) | 1.9 | 130 | false(label) | 900 | 2500 | unknown | 0.12 | 2.0 | unknown | 0.66 | 18 | timeout | 900 | 17 | timeout | 920 | 1500 | timeout | 920 | 430 |
Ackermann03_true.c | true | 850 | 440 | error (recursion) | 1.9 | 130 | false(label) | 900 | 2200 | unknown | 0.15 | 2.0 | unknown | 0.66 | 18 | timeout | 900 | 17 | unknown | 49 | 370 | timeout | 920 | 520 |
Ackermann04_true.c | true | 850 | 440 | error (recursion) | 1.9 | 130 | false(label) | 900 | 2500 | unknown | 0.13 | 2.0 | unknown | 0.66 | 18 | timeout | 900 | 17 | timeout | 920 | 930 | timeout | 920 | 520 |
Addition01_true.c | true | 850 | 1100 | error (recursion) | 2.0 | 130 | false(label) | 900 | 4800 | unknown | 0.16 | 3.0 | unknown | 0.10 | 5.0 | timeout | 900 | 120 | timeout | 920 | 420 | timeout | 920 | 300 |
EvenOdd01_true.c | true | 0.96 | 22 | error (recursion) | 1.9 | 130 | false(label) | 0.40 | 14 | unknown | 0.14 | 2.0 | unknown | 0.12 | 5.0 | timeout | 900 | 180 | timeout | 920 | 440 | timeout | 920 | 290 |
Fibonacci01_true.c | true | 850 | 660 | error (recursion) | 1.9 | 130 | false(label) | 400 | 4600 | unknown | 0.15 | 3.0 | false(label) | 2.0 | 37 | timeout | 900 | 4.0 | timeout | 920 | 490 | timeout | 920 | 600 |
Fibonacci02_true.c | true | 0.72 | 16 | error (recursion) | 1.9 | 130 | false(label) | 0.28 | 12 | unknown | 0.13 | 2.0 | true | 0.12 | 3.0 | true | 0.36 | 2.0 | true | 80 | 330 | unknown | 67 | 280 |
Fibonacci03_true.c | true | 850 | 660 | error (recursion) | 1.9 | 130 | false(label) | 900 | 600 | unknown | 0.12 | 3.0 | false(label) | 2.0 | 37 | timeout | 900 | 4.0 | timeout | 920 | 430 | timeout | 920 | 410 |
McCarthy91_true.c | true | 850 | 590 | error (recursion) | 1.9 | 130 | false(label) | 900 | 4100 | unknown | 0.11 | 2.0 | unknown | 0.55 | 17 | timeout | 900 | 79 | true | 84 | 320 | true | 6.8 | 240 |
MultCommutative_true.c | true | 850 | 420 | error (recursion) | 1.9 | 130 | false(label) | 900 | 5200 | unknown | 0.17 | 3.0 | unknown | 0.13 | 6.0 | timeout | 900 | 75 | timeout | 920 | 540 | timeout | 920 | 400 |
Primes_true.c | true | 850 | 560 | error (recursion) | 1.9 | 130 | unknown | 620 | 15000 | unknown | 0.18 | 4.0 | timeout | 900 | 370 | timeout | 900 | 98 | timeout | 920 | 460 | timeout | 920 | 310 |
gcd01_true.c | true | 850 | 1700 | error (recursion) | 1.9 | 130 | false(label) | 900 | 4800 | unknown | 0.17 | 3.0 | unknown | 0.15 | 5.0 | timeout | 900 | 89 | true | 16 | 240 | true | 7.2 | 240 |
gcd02_true.c | true | 850 | 1700 | error (recursion) | 1.9 | 130 | false(label) | 280 | 4600 | unknown | 0.19 | 3.0 | unknown | 0.12 | 5.0 | timeout | 900 | 52 | timeout | 920 | 1700 | timeout | 920 | 350 |
recHanoi01_true.c | true | 850 | 340 | error (recursion) | 1.9 | 130 | false(label) | 900 | 6000 | unknown | 0.13 | 2.0 | false(label) | 0.18 | 7.0 | timeout | 900 | 3.0 | timeout | 920 | 1200 | timeout | 920 | 440 |
recHanoi02_true.c | true | 0.68 | 18 | error (recursion) | 1.9 | 130 | false(label) | 0.30 | 12 | unknown | 0.11 | 2.0 | false(label) | 0.10 | 4.0 | true | 0.33 | 3.0 | timeout | 920 | 520 | timeout | 920 | 300 |
recHanoi03_true.c | true | 0.67 | 18 | error (recursion) | 1.9 | 130 | false(label) | 0.29 | 12 | unknown | 0.12 | 2.0 | false(label) | 0.12 | 4.0 | true | 0.24 | 3.0 | timeout | 920 | 520 | timeout | 920 | 290 |
../../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) |
total files | 23 | 12000 | 11000 | 23 | 44 | 2900 | 23 | 14000 | 78000 | 23 | 3.2 | 58 | 23 | 930 | 810 | 23 | 18000 | 4300 | 23 | 13000 | 12000 | 23 | 14000 | 7600 |
correct results | 22 | 11000 | 9900 | 0 | 0 | 0 | 7 | 4900 | 21000 | 3 | 0.38 | 7.0 | 1 | 0.12 | 3.0 | 3 | 0.93 | 8.0 | 9 | 850 | 2200 | 7 | 54 | 1500 |
false negatives | 1 | 850 | 1100 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
false positives | 0 | 0 | 0 | 0 | 0 | 0 | 15 | 8700 | 42000 | 0 | 0 | 0 | 5 | 4.3 | 89 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 | 0 |
score (23 files, max score: 39) | 30 | 0 | -53 | 3 | -18 | 6 | 12 | 9 |