Tool |
Beagle 1.1 |
Cascade 0.1 |
CBMC 4.9 |
CPAchecker 1.3.10-svcomp15 |
ESBMC 1.24 |
Seahorn |
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-06 00:00 ]] |
14-12-20 11:27 [[ 14-12-20 14:02 ]] |
14-12-19 16:19 [[ 14-12-21 23:26 ]] |
14-12-19 16:18 [[ 14-12-20 10:06 ]] |
14-12-19 16:19 [[ 14-12-20 10:07 ]] |
14-12-20 18:50 [[ 14-12-21 21:13 ]] |
14-12-19 17:19 [[ 14-12-21 23:15 ]] |
14-12-19 17:19 [[ 14-12-20 10:09 ]] |
Options |
-t 895 -b [[ -witness-check -noout -spec ../../results-2015/blast.14-11-25_0345.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/blast-2.7.3/bin/witness.graphml -setprop spec.singlePathMatching=true -setprop parser.transformTokensToLines=false -tokenize -useTokenizer ]] |
-trace [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cascade.14-12-20_1127.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/Cascade-4113-patch/out/${sourcefile_name}/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] |
--32 [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cbmc.14-12-19_1619.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/cbmc-sv-comp-2015/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] |
-sv-comp15 -disable-java-assertions -heap 10000m [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cpachecker.14-12-19_1618.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/CPAchecker-1.3.10-svcomp15-unix/output/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=true ]] |
[[ -witness-check -noout -timelimit 90 -spec ../../results-2015/esbmc.14-12-19_1619.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/esbmc-v1.24.1/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] |
--cex=witness.graphml [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/seahorn.14-12-20_1850.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/seahorn-svcomp15/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] |
32bit precise [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimateautomizer.14-12-19_1719.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/UltimateAutomizer/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] |
32bit precise [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/ultimatekojak.14-12-19_1719.logfiles/sv-comp15.${sourcefile_name}.files/SV-Competition/comp/bin-2015/UltimateKojak/witness.graphml -setprop spec.singlePathMatching=false -setprop parser.transformTokensToLines=false ]] |
../../sv-benchmarks/c/ |
status |
time(s) |
memory(MB) |
time(s) for witness |
status |
time(s) |
memory(MB) |
time(s) for witness |
status |
time(s) |
memory(MB) |
time(s) for witness |
status |
time(s) |
memory(MB) |
time(s) for witness |
status |
time(s) |
memory(MB) |
time(s) for witness |
status |
time(s) |
memory(MB) |
time(s) for witness |
status |
time(s) |
memory(MB) |
time(s) for witness |
status |
time(s) |
memory(MB) |
time(s) for witness |
bitvector/byte_add_false-unreach-call.i |
timeout |
920 |
580 |
- |
witness invalid (error (invalid c code)) |
1.8 |
130 |
1.5 |
witness confirmed |
0.22 |
26 |
2.8 |
witness confirmed |
64 |
1200 |
2.6 |
witness confirmed |
0.36 |
14 |
1.8 |
witness confirmed |
0.47 |
46 |
2.5 |
unknown |
14 |
410 |
- |
witness unconfirmed |
7.9 |
280 |
1.8 |
bitvector/byte_add_1_true-unreach-call.i |
timeout |
920 |
570 |
- |
true |
860 |
2200 |
- |
true |
0.74 |
27 |
- |
true |
35 |
1200 |
- |
true |
0.10 |
13 |
- |
false(reach) |
0.42 |
46 |
- |
unknown |
14 |
420 |
- |
false(reach) |
7.6 |
270 |
- |
bitvector/byte_add_2_true-unreach-call.i |
timeout |
920 |
570 |
- |
true |
860 |
3400 |
- |
true |
0.77 |
28 |
- |
true |
78 |
1300 |
- |
true |
0.11 |
13 |
- |
false(reach) |
0.41 |
44 |
- |
unknown |
13 |
410 |
- |
false(reach) |
7.8 |
270 |
- |
bitvector/gcd_1_true-unreach-call.i |
true |
19 |
37 |
- |
true |
850 |
8900 |
- |
true |
2.4 |
64 |
- |
true |
2.3 |
200 |
- |
true |
0.59 |
24 |
- |
false(reach) |
0.21 |
35 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.4 |
250 |
- |
bitvector/gcd_2_true-unreach-call.i |
unknown |
0.088 |
2.0 |
- |
true |
850 |
4900 |
- |
true |
2.5 |
63 |
- |
true |
2.3 |
210 |
- |
true |
19 |
32 |
- |
false(reach) |
0.21 |
35 |
- |
unknown |
5.0 |
240 |
- |
unknown |
5.1 |
240 |
- |
bitvector/gcd_3_true-unreach-call.i |
unknown |
0.087 |
2.0 |
- |
true |
850 |
4900 |
- |
true |
2.7 |
63 |
- |
true |
2.3 |
210 |
- |
true |
19 |
32 |
- |
false(reach) |
0.19 |
35 |
- |
unknown |
5.6 |
240 |
- |
unknown |
5.3 |
240 |
- |
bitvector/gcd_4_true-unreach-call.i |
true |
6.3 |
18 |
- |
true |
5.1 |
230 |
- |
true |
0.50 |
23 |
- |
true |
1.4 |
140 |
- |
true |
0.074 |
12 |
- |
timeout |
920 |
32 |
- |
unknown |
5.5 |
250 |
- |
unknown |
5.5 |
250 |
- |
bitvector/interleave_bits_true-unreach-call.i |
true |
0.30 |
10.0 |
- |
true |
4.9 |
230 |
- |
true |
0.53 |
23 |
- |
true |
17 |
430 |
- |
true |
0.065 |
12 |
- |
false(reach) |
0.29 |
39 |
- |
unknown |
20 |
650 |
- |
false(reach) |
15 |
660 |
- |
bitvector/jain_1_true-unreach-call.i |
true |
0.14 |
10.0 |
- |
true |
680 |
1200 |
- |
true |
0.83 |
69 |
- |
true |
2.5 |
210 |
- |
true |
0.076 |
11 |
- |
unknown |
0.16 |
29 |
- |
true |
6.0 |
250 |
- |
true |
5.9 |
250 |
- |
bitvector/jain_2_true-unreach-call.i |
true |
0.15 |
10.0 |
- |
true |
860 |
1000 |
- |
true |
1.2 |
140 |
- |
true |
2.6 |
210 |
- |
true |
0.076 |
11 |
- |
false(reach) |
0.17 |
32 |
- |
true |
6.1 |
250 |
- |
true |
10 |
260 |
- |
bitvector/jain_4_true-unreach-call.i |
true |
0.15 |
10.0 |
- |
true |
130 |
12000 |
- |
true |
1.6 |
200 |
- |
true |
2.6 |
210 |
- |
true |
0.063 |
11 |
- |
out of memory |
790 |
15000 |
- |
true |
18 |
440 |
- |
timeout |
920 |
630 |
- |
bitvector/jain_5_true-unreach-call.i |
true |
0.18 |
11 |
- |
true |
150 |
2400 |
- |
true |
0.50 |
23 |
- |
timeout |
920 |
1800 |
- |
true |
0.056 |
11 |
- |
true |
0.19 |
30 |
- |
true |
6.3 |
250 |
- |
true |
7.3 |
270 |
- |
bitvector/jain_6_true-unreach-call.i |
true |
0.18 |
10.0 |
- |
out of memory |
60 |
15000 |
- |
true |
1.3 |
150 |
- |
true |
2.6 |
210 |
- |
true |
0.066 |
11 |
- |
timeout |
920 |
10000 |
- |
unknown |
150 |
530 |
- |
timeout |
920 |
790 |
- |
bitvector/jain_7_true-unreach-call.i |
true |
0.14 |
10.0 |
- |
true |
860 |
1200 |
- |
true |
0.89 |
59 |
- |
true |
5.0 |
230 |
- |
true |
0.063 |
11 |
- |
timeout |
920 |
11000 |
- |
unknown |
93 |
470 |
- |
timeout |
920 |
610 |
- |
bitvector/modulus_true-unreach-call.i |
true |
1.8 |
11 |
- |
unknown |
850 |
1100 |
- |
true |
250 |
1100 |
- |
timeout |
900 |
410 |
- |
true |
4.7 |
59 |
- |
false(reach) |
0.17 |
33 |
- |
unknown |
5.4 |
250 |
- |
unknown |
5.5 |
250 |
- |
bitvector/num_conversion_1_true-unreach-call.i |
true |
0.62 |
10.0 |
- |
true |
12 |
2100 |
- |
true |
0.53 |
23 |
- |
true |
1.4 |
130 |
- |
true |
0.063 |
12 |
- |
false(reach) |
0.28 |
36 |
- |
unknown |
7.4 |
270 |
- |
false(reach) |
6.8 |
270 |
- |
bitvector/num_conversion_2_true-unreach-call.i |
true |
0.61 |
10.0 |
- |
true |
12 |
1900 |
- |
true |
0.55 |
23 |
- |
true |
17 |
250 |
- |
true |
0.071 |
12 |
- |
false(reach) |
0.26 |
36 |
- |
unknown |
7.1 |
270 |
- |
false(reach) |
8.3 |
280 |
- |
bitvector/parity_true-unreach-call.i |
true |
1.3 |
10.0 |
- |
true |
850 |
2500 |
- |
true |
2.8 |
27 |
- |
timeout |
910 |
1300 |
- |
true |
0.21 |
13 |
- |
false(reach) |
0.15 |
33 |
- |
unknown |
5.3 |
250 |
- |
false(reach) |
5.7 |
250 |
- |
bitvector/sum02_true-unreach-call.i |
true |
27 |
31 |
- |
true |
420 |
1900 |
- |
true |
0.61 |
25 |
- |
timeout |
900 |
760 |
- |
true |
0.074 |
12 |
- |
false(reach) |
0.16 |
34 |
- |
unknown |
5.2 |
250 |
- |
unknown |
5.3 |
240 |
- |
bitvector/s3_clnt_1_false-unreach-call.BV.c.cil.c |
timeout |
920 |
1000 |
- |
witness invalid (error (invalid c code)) |
6.2 |
360 |
1.8 |
witness confirmed |
4.7 |
180 |
9.9 |
witness confirmed |
5.7 |
290 |
15 |
witness confirmed |
6.9 |
170 |
5.7 |
witness confirmed |
5.4 |
70 |
9.6 |
unknown |
5.4 |
250 |
- |
unknown |
5.8 |
240 |
- |
bitvector/s3_clnt_2_false-unreach-call.BV.c.cil.c |
out of memory |
83 |
15000 |
- |
witness invalid (error (invalid c code)) |
6.4 |
320 |
1.8 |
witness confirmed |
4.3 |
150 |
29 |
witness confirmed |
87 |
1500 |
3.1 |
witness confirmed |
6.0 |
140 |
21 |
witness confirmed |
6.7 |
110 |
29 |
unknown |
12 |
430 |
- |
witness confirmed |
49 |
1200 |
42 |
bitvector/s3_clnt_3_false-unreach-call.BV.c.cil.c |
out of memory |
85 |
15000 |
- |
witness invalid (error (invalid c code)) |
3.6 |
250 |
1.9 |
witness confirmed |
1.0 |
53 |
3.3 |
witness confirmed |
4.5 |
260 |
4.1 |
witness confirmed |
6.7 |
150 |
3.5 |
witness confirmed |
1.6 |
54 |
3.1 |
unknown |
7.7 |
270 |
- |
witness confirmed |
9.3 |
300 |
5.1 |
bitvector/s3_clnt_1_true-unreach-call.BV.c.cil.c |
timeout |
920 |
1000 |
- |
true |
890 |
6800 |
- |
true |
54 |
760 |
- |
true |
33 |
700 |
- |
true |
3.1 |
180 |
- |
timeout |
920 |
52 |
- |
unknown |
5.5 |
240 |
- |
unknown |
5.8 |
240 |
- |
bitvector/s3_clnt_2_true-unreach-call.BV.c.cil.c |
out of memory |
84 |
15000 |
- |
timeout |
920 |
7700 |
- |
true |
50 |
640 |
- |
true |
30 |
1200 |
- |
true |
2.8 |
150 |
- |
false(reach) |
6.9 |
110 |
- |
unknown |
13 |
430 |
- |
false(reach) |
62 |
1200 |
- |
bitvector/s3_clnt_3_true-unreach-call.BV.c.cil.c |
out of memory |
85 |
15000 |
- |
timeout |
920 |
7900 |
- |
true |
47 |
590 |
- |
true |
35 |
1200 |
- |
true |
3.3 |
150 |
- |
true |
9.1 |
51 |
- |
true |
16 |
700 |
- |
timeout |
920 |
1400 |
- |
bitvector/s3_srvr_1_alt_true-unreach-call.BV.c.cil.c |
out of memory |
130 |
15000 |
- |
true |
860 |
2200 |
- |
true |
850 |
620 |
- |
aborted |
130 |
1200 |
- |
true |
380 |
280 |
- |
unknown |
570 |
760 |
- |
unknown |
6.0 |
240 |
- |
unknown |
5.5 |
250 |
- |
bitvector/s3_srvr_1_true-unreach-call.BV.c.cil.c |
out of memory |
130 |
15000 |
- |
timeout |
890 |
5800 |
- |
true |
92 |
770 |
- |
true |
64 |
700 |
- |
true |
1.8 |
190 |
- |
true |
79 |
73 |
- |
true |
17 |
690 |
- |
timeout |
920 |
1900 |
- |
bitvector/s3_srvr_2_alt_true-unreach-call.BV.c.cil.c |
out of memory |
120 |
15000 |
- |
true |
860 |
3800 |
- |
true |
93 |
670 |
- |
true |
63 |
1200 |
- |
true |
1.8 |
160 |
- |
true |
320 |
120 |
- |
true |
40 |
1000 |
- |
unknown |
850 |
1400 |
- |
bitvector/s3_srvr_2_true-unreach-call.BV.c.cil.c |
out of memory |
120 |
15000 |
- |
true |
860 |
3800 |
- |
true |
95 |
690 |
- |
true |
63 |
710 |
- |
true |
1.9 |
170 |
- |
true |
130 |
85 |
- |
true |
37 |
1200 |
- |
timeout |
920 |
1400 |
- |
bitvector/s3_srvr_3_alt_true-unreach-call.BV.c.cil.c |
out of memory |
120 |
15000 |
- |
true |
870 |
7300 |
- |
true |
89 |
710 |
- |
true |
64 |
710 |
- |
true |
1.6 |
180 |
- |
unknown |
2.5 |
42 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.1 |
240 |
- |
bitvector/s3_srvr_3_true-unreach-call.BV.c.cil.c |
out of memory |
120 |
15000 |
- |
true |
870 |
7100 |
- |
true |
95 |
710 |
- |
true |
64 |
700 |
- |
true |
1.6 |
180 |
- |
unknown |
2.5 |
48 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.7 |
240 |
- |
bitvector/soft_float_1_true-unreach-call.c.cil.c |
timeout |
920 |
7000 |
- |
true |
860 |
2200 |
- |
true |
2.9 |
43 |
- |
true |
11 |
340 |
- |
true |
0.18 |
17 |
- |
false(reach) |
0.40 |
44 |
- |
unknown |
8.1 |
270 |
- |
false(reach) |
9.5 |
300 |
- |
bitvector/soft_float_2_true-unreach-call.c.cil.c |
unknown |
870 |
9400 |
- |
true |
25 |
1900 |
- |
true |
2.3 |
42 |
- |
true |
13 |
300 |
- |
true |
0.070 |
14 |
- |
false(reach) |
0.82 |
59 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.3 |
240 |
- |
bitvector/soft_float_3_true-unreach-call.c.cil.c |
timeout |
920 |
15000 |
- |
true |
850 |
410 |
- |
true |
2.2 |
41 |
- |
timeout |
920 |
8900 |
- |
true |
0.084 |
14 |
- |
false(reach) |
1.8 |
77 |
- |
unknown |
5.6 |
240 |
- |
unknown |
5.6 |
240 |
- |
bitvector/soft_float_4_true-unreach-call.c.cil.c |
timeout |
920 |
5500 |
- |
true |
860 |
2200 |
- |
true |
5.6 |
48 |
- |
true |
64 |
260 |
- |
true |
4.1 |
22 |
- |
false(reach) |
0.38 |
44 |
- |
unknown |
6.1 |
240 |
- |
false(reach) |
9.0 |
300 |
- |
bitvector/soft_float_5_true-unreach-call.c.cil.c |
timeout |
900 |
15000 |
- |
true |
25 |
1900 |
- |
true |
2.3 |
43 |
- |
true |
13 |
300 |
- |
true |
0.062 |
14 |
- |
false(reach) |
0.87 |
61 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.1 |
240 |
- |
bitvector-regression/implicitfloatconversion_false-unreach-call.i |
unknown |
0.040 |
1.00 |
- |
witness confirmed |
0.85 |
86 |
1.4 |
unknown |
0.12 |
23 |
- |
witness confirmed |
1.6 |
170 |
1.3 |
witness unconfirmed |
0.083 |
11 |
1.4 |
witness confirmed |
0.15 |
32 |
1.4 |
unknown |
5.4 |
240 |
- |
unknown |
5.2 |
240 |
- |
bitvector-regression/implicitunsignedconversion_false-unreach-call.i |
witness missing |
0.11 |
10.0 |
- |
witness confirmed |
0.80 |
86 |
1.4 |
unknown |
0.093 |
23 |
- |
witness confirmed |
1.6 |
160 |
1.4 |
witness confirmed |
0.065 |
11 |
1.7 |
witness confirmed |
0.12 |
32 |
1.4 |
witness confirmed |
5.0 |
250 |
1.4 |
witness confirmed |
5.6 |
250 |
1.3 |
bitvector-regression/integerpromotion_false-unreach-call.i |
witness missing |
0.16 |
13 |
- |
witness invalid (error (invalid c code)) |
1.2 |
99 |
1.5 |
witness confirmed |
0.13 |
25 |
1.6 |
witness confirmed |
2.3 |
200 |
1.9 |
witness confirmed |
2.0 |
17 |
1.7 |
witness confirmed |
0.30 |
32 |
1.6 |
unknown |
5.5 |
250 |
- |
witness confirmed |
5.6 |
250 |
1.7 |
bitvector-regression/signextension2_false-unreach-call.i |
witness missing |
0.34 |
10.0 |
- |
witness invalid (error (invalid c code)) |
1.1 |
97 |
1.5 |
witness confirmed |
0.13 |
25 |
1.7 |
witness confirmed |
2.1 |
200 |
1.8 |
witness confirmed |
0.97 |
16 |
1.7 |
witness confirmed |
0.17 |
32 |
1.6 |
witness confirmed |
6.5 |
250 |
1.7 |
witness confirmed |
5.5 |
250 |
1.7 |
bitvector-regression/signextension_false-unreach-call.i |
true |
0.25 |
10.0 |
- |
witness invalid (error (invalid c code)) |
1.3 |
110 |
1.5 |
witness confirmed |
0.13 |
25 |
2.0 |
witness confirmed |
2.2 |
200 |
1.9 |
witness confirmed |
2.0 |
19 |
1.7 |
witness confirmed |
0.14 |
32 |
1.6 |
true |
5.3 |
250 |
- |
true |
5.5 |
250 |
- |
bitvector-regression/implicitunsignedconversion_true-unreach-call.i |
true |
0.087 |
10.0 |
- |
true |
0.54 |
73 |
- |
true |
0.50 |
23 |
- |
true |
1.4 |
140 |
- |
true |
0.067 |
11 |
- |
true |
0.14 |
27 |
- |
true |
5.1 |
250 |
- |
true |
5.2 |
250 |
- |
bitvector-regression/integerpromotion_true-unreach-call.i |
true |
0.094 |
10.0 |
- |
true |
0.86 |
79 |
- |
true |
0.57 |
25 |
- |
true |
1.6 |
140 |
- |
true |
0.079 |
16 |
- |
true |
0.16 |
27 |
- |
unknown |
5.2 |
240 |
- |
false(reach) |
5.5 |
250 |
- |
bitvector-regression/signextension2_true-unreach-call.i |
true |
0.30 |
9.0 |
- |
true |
0.83 |
78 |
- |
true |
0.59 |
25 |
- |
true |
1.5 |
140 |
- |
true |
0.065 |
16 |
- |
true |
0.25 |
27 |
- |
true |
5.5 |
250 |
- |
true |
5.7 |
250 |
- |
bitvector-regression/signextension_true-unreach-call.i |
false(reach) |
0.35 |
10.0 |
- |
true |
0.92 |
85 |
- |
true |
0.55 |
26 |
- |
true |
1.6 |
140 |
- |
true |
0.079 |
16 |
- |
true |
0.26 |
27 |
- |
false(reach) |
5.6 |
250 |
- |
false(reach) |
5.3 |
250 |
- |
bitvector-loops/diamond_false-unreach-call2.i |
true |
2.9 |
12 |
- |
witness invalid (error (invalid c code)) |
0.96 |
98 |
1.7 |
witness confirmed |
0.13 |
24 |
1.9 |
witness confirmed |
1.8 |
170 |
2.4 |
witness confirmed |
0.60 |
12 |
2.4 |
witness confirmed |
0.35 |
43 |
1.9 |
witness confirmed |
5.6 |
250 |
1.5 |
witness confirmed |
7.3 |
240 |
2.3 |
bitvector-loops/overflow_false-unreach-call1.i |
unknown |
0.027 |
0 |
- |
true |
2.7 |
150 |
- |
true |
0.49 |
23 |
- |
true |
120 |
1100 |
- |
true |
0.065 |
11 |
- |
timeout |
920 |
220 |
- |
timeout |
920 |
660 |
- |
timeout |
920 |
1200 |
- |