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