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 |