Tool AProVE FuncTion T2 Tan UltimateCommandline
Limits timelimit: 900 s, memlimit: 15360 MB, CPU core limit: 8
OS Linux 3.2.0-58-generic x86_64
System CPU: Intel Core i7-2600 CPU @ 3.40GHz with 8 cores, frequency: 3401 MHz; RAM: 32827636 kB
Date of execution 14-01-15 15:46 14-01-15 15:41 14-01-16 12:47 14-01-16 12:48
Options ${logfile_path}/${rundefinition_name}.${sourcefile_name}.proof ../../../../sv-benchmarks/c/PropertyTermination.prp -x ${logfile_path}/${rundefinition_name}.${sourcefile_name}.cex ../../../../sv-benchmarks/c/PropertyTermination.prp ../../../../sv-benchmarks/c/PropertyTermination.prp ${logfile_path}/${rundefinition_name}.${sourcefile_name}_errorpath.txt
../../sv-benchmarks/c/termination-crafted/ 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)
BradleyMannaSipma-2005CAV-Fig1-modified_false-termination.c unknown 120    1700   unknown 0.43 18   unknown 8.6  82   false(termination) 2.2  29   false(termination) 6.6  190  
HarrisLalNoriRajamani-2010SAS-Fig2_false-termination.c unknown 320    1800   unknown 0.34 25   unknown 21    280   false(termination) 0.85 20   false(termination) 3.5  160  
Urban-2013WST-Fig1_false-termination.c unknown 27    280   unknown 0.12 17   error(aborted) 10    94   unknown 0.71 20   false(termination) 3.3  150  
Velroyen_false-termination.c unknown 6.4  240   unknown 0.84 43   unknown 19    230   unknown 1.7  19   false(termination) 3.3  150  
joey_false-termination.c error(recursion) 2.4  190   error(exception) 0.07 1.00 error(aborted) 6.0  38   true 0.23 15   false(termination) 36    1600  
Avery-2006FLOPS-Table1_true-termination.c true 19    1400   unknown 0.15 22   true 0.75 17   true 0.84 20   true 3.6  150  
Ben-Amram-2010LMCS-Ex2.3_true-termination.c true 6.8  250   unknown 0.67 33   true 14    170   unknown 6.7  23   true 5.1  220  
BradleyMannaSipma-2005CAV-Fig1_true-termination.c unknown 280    3300   unknown 0.13 16   true 6.1  38   cegar error 4.1  22   timeout 900    12000  
BradleyMannaSipma-2005ICALP-Fig1_true-termination.c timeout 920    8200   unknown 0.12 13   unknown 1.1  27   cegar error 4.7  21   unknown 900    9800  
BrockschmidtCookFuhs-2013CAV-Fig1_true-termination.c true 7.7  260   unknown 0.11 5.0 true 5.0  17   cegar error 2.0  20   true 3.2  150  
BrockschmidtCookFuhs-2013CAV-Introduction_true-termination.c true 3.4  220   true 0.11 8.0 true 1.0  27   cegar error 10    23   true 2.7  130  
ChenFlurMukhopadhyay-2012SAS-Fig1_true-termination.c true 6.8  240   unknown 0.09 14   true 5.3  26   cegar error 6.9  23   true 3.1  140  
CookSeeZuleger-2013TACAS-Fig3_true-termination.c true 5.7  230   true 1.4  62   true 0.79 18   timeout 920    110   true 4.0  200  
CookSeeZuleger-2013TACAS-Fig7a_true-termination.c true 7.4  230   true 42    110   true 0.82 18   timeout 920    140   true 4.8  230  
CookSeeZuleger-2013TACAS-Fig7b_true-termination.c true 26    630   true 140    240   true 0.88 20   timeout 900    120   true 7.9  250  
GulwaniJainKoskinen-2009PLDI-Fig1_true-termination.c unknown 340    3000   unknown 0.13 18   unknown 18    240   unknown 0.90 19   unknown 8.9  260  
HarrisLalNoriRajamani-2010SAS-Fig1_true-termination.c true 40    1200   parse error (invalid token) 0.08 1.00 unknown 0.94 22   cegar error 7.0  22   true 13    260  
HarrisLalNoriRajamani-2010SAS-Fig3_true-termination.c true 3.2  180   true 0.09 8.0 error(aborted) 6.1  50   true 0.76 19   true 2.8  130  
KroeningSharyginaTsitovichWintersteiger-2010CAV-Fig1_true-termination.c true 26    480   unknown 0.09 12   error(aborted) 6.1  34   unknown 0.89 20   unknown 900    11000  
LarrazOliverasRodriguez-CarbonellRubio-2013FMCAD-Fig1_true-termination.c unknown 540    4600   unknown 0.13 17   true 5.4  31   false(termination) 1.4  21   true 12    270  
LeeJonesBen-Amram-2001POPL-Ex1_true-termination.c error(recursion) 2.3  200   error(exception) 0.09 1.00 true 5.4  30   true 0.23 15   true 4.9  200  
LeeJonesBen-Amram-2001POPL-Ex2_true-termination.c error(recursion) 1.9  130   unknown 0.11 1.00 true 5.8  33   true 0.23 16   true 6.7  240  
LeeJonesBen-Amram-2001POPL-Ex3_true-termination.c error(recursion) 2.5  210   error(exception) 0.09 1.00 true 0.78 21   true 0.23 16   unknown 900    12000  
LeeJonesBen-Amram-2001POPL-Ex4_true-termination.c error(recursion) 2.7  220   error(exception) 0.09 1.00 true 4.9  19   true 0.40 16   true 22    580  
LeeJonesBen-Amram-2001POPL-Ex5_true-termination.c error(recursion) 2.4  200   error(exception) 0.08 1.00 true 7.1  49   true 0.22 15   unknown 8.1  240  
LeeJonesBen-Amram-2001POPL-Ex6_true-termination.c error(recursion) 2.3  190   unknown 0.08 1.00 true 6.2  37   true 0.24 16   true 7.4  240  
Masse_true-termination.c unknown 440    2200   true 26    110   error(segfault) 5.8  33   cegar error 1.6  20   unknown 3.3  150  
NoriSharma-2013FSE-Fig7_true-termination.c true 17    1400   unknown 0.10 12   true 4.9  19   true 0.68 21   true 3.0  140  
NoriSharma-2013FSE-Fig8_true-termination.c true 12    1400   unknown 0.12 14   true 0.79 18   cegar error 17    26   true 4.1  210  
PodelskiRybalchenko-2004VMCAI-Ex2_true-termination.c true 2.3  160   true 0.14 26   error(aborted) 5.7  33   cegar error 1.5  20   unknown 3.5  150  
TelAviv-Amir-Minimum_true-termination.c unknown 450    3300   timed out 580    620   true 0.77 20   unknown 330    35   true 9.3  260  
Toulouse-BranchesToLoop_true-termination.c true 4.1  220   unknown 0.21 14   unknown 22    390   cegar error 5.6  21   true 3.7  170  
Toulouse-MultiBranchesToLoop_true-termination.c true 4.0  210   unknown 0.56 29   unknown 22    360   cegar error 14    25   true 10.0  260  
Urban-2013WST-Fig2-modified1000_true-termination.c true 4.1  220   true 0.17 25   true 0.76 17   true 0.78 19   unknown 340    1400  
Urban-2013WST-Fig2_true-termination.c true 3.8  210   true 0.16 25   true 0.74 17   true 0.75 19   true 5.5  230  
Urban_true-termination.c true 21    440   true 8.0  77   unknown 19    440   cegar error 150    26   true 18    640  
aviad_true-termination.c unknown 37    1500   unknown 0.15 18   error(aborted) 6.1  35   true 1.0  21   true 5.0  230  
gcd1_true-termination.c true 15    450   unknown 0.16 19   true 0.75 17   false(termination) 4.9  23   true 9.6  260  
genady_true-termination.c true 6.0  280   unknown 0.14 7.0 true 0.73 16   cegar error 6.4  22   true 2.9  130  
min_rf_true-termination.c true 22    1100   timed out 670    850   unknown 19    220   timeout 920    110   true 18    540  
svcomp_cstrcmp_true-termination.c true 4.5  240   parse error (invalid token) 0.10 1.00 unknown 0.39 6.0 cegar error 8.6  30   unknown 2.4  99  
svcomp_cstrcspn_true-termination.c true 43    1400   parse error (invalid token) 0.08 1.00 unknown 2.0  38   cegar error 53    32   unknown 2.6  99  
svcomp_cstrlen_true-termination.c true 2.9  200   parse error (invalid token) 0.07 1.00 error(aborted) 5.8  35   cegar error 2.4  26   unknown 2.3  99  
svcomp_cstrncmp_true-termination.c true 5.5  320   parse error (invalid token) 0.06 1.00 unknown 0.37 6.0 true 24    33   unknown 2.3  100  
svcomp_cstrpbrk_true-termination.c true 21    470   parse error (invalid token) 0.10 1.00 unknown 2.0  40   cegar error 53    32   unknown 2.3  100  
svcomp_cstrspn_true-termination.c true 19    530   parse error (invalid token) 0.07 1.00 unknown 2.0  38   cegar error 53    32   unknown 2.2  99  
svcomp_strchr_true-termination.c true 3.6  220   parse error (invalid token) 0.09 1.00 error(segfault) 6.1  34   cegar error 2.7  26   unknown 2.5  99  
../../sv-benchmarks/c/termination-crafted/ 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 47 3800 46000 47 1500 2500 47 290 3500 47 4400 1400 47 4200 56000
correct results 29 360 15000 10 220 690 23 80 690 15 33 300 31 250 8700
false negatives 0 0 0 0 0 0 0 0 0 1 0.23 15 0 0 0
false positives 0 0 0 0 0 0 0 0 0 2 6.3 44 0 0 0
score (47 files, max score: 89) 58 20 46 12 57