Tool |
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-04 12:41 [[ 14-12-21 23:21 ]] |
14-11-15 15:53 [[ 14-12-21 23:23 ]] |
14-12-13 18:39 [[ 14-12-19 11:24 ]] |
14-12-20 18:50 [[ 14-12-21 21:13 ]] |
14-12-02 13:00 [[ 14-12-21 23:12 ]] |
14-12-02 13:02 [[ 14-12-21 23:18 ]] |
Options |
--32 [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cbmc.14-12-04_1241.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 -setprop cpa.predicate.handlePointerAliasing=false [[ -witness-check -noout -timelimit 90 -spec ../../results-2015/cpachecker.14-11-15_1553.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-13_1839.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-11-12_2241.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-02_1302.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 |
floats-cdfpl/newton_1_4_false-unreach-call.i |
witness confirmed |
5.8 |
53 |
1.4 |
witness confirmed |
650 |
8700 |
1.5 |
witness unconfirmed |
0.61 |
31 |
1.4 |
witness confirmed |
0.17 |
32 |
1.4 |
unknown |
5.0 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cdfpl/newton_1_5_false-unreach-call.i |
witness confirmed |
8.2 |
52 |
1.4 |
witness confirmed |
9.0 |
280 |
1.5 |
witness unconfirmed |
0.33 |
25 |
1.7 |
witness confirmed |
0.19 |
32 |
1.4 |
unknown |
5.0 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cdfpl/newton_1_6_false-unreach-call.i |
witness confirmed |
5.4 |
50 |
1.5 |
witness confirmed |
3.9 |
280 |
1.4 |
witness unconfirmed |
0.42 |
31 |
1.4 |
witness confirmed |
0.15 |
32 |
1.7 |
unknown |
5.3 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cdfpl/newton_1_7_false-unreach-call.i |
witness confirmed |
10 |
59 |
1.4 |
witness confirmed |
3.9 |
280 |
1.4 |
witness unconfirmed |
0.33 |
31 |
1.4 |
witness confirmed |
0.16 |
32 |
1.7 |
unknown |
5.1 |
240 |
- |
unknown |
5.4 |
240 |
- |
floats-cdfpl/newton_1_8_false-unreach-call.i |
witness confirmed |
13 |
65 |
1.4 |
witness confirmed |
4.1 |
280 |
1.4 |
witness unconfirmed |
0.27 |
25 |
1.4 |
witness confirmed |
0.29 |
32 |
1.4 |
unknown |
5.2 |
240 |
- |
unknown |
5.1 |
240 |
- |
floats-cdfpl/newton_2_6_false-unreach-call.i |
witness confirmed |
130 |
220 |
1.5 |
out of memory |
860 |
15000 |
- |
witness unconfirmed |
0.65 |
41 |
1.4 |
witness confirmed |
0.16 |
32 |
1.4 |
unknown |
5.2 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cdfpl/newton_2_7_false-unreach-call.i |
witness confirmed |
49 |
150 |
1.4 |
witness confirmed |
33 |
400 |
1.4 |
witness unconfirmed |
0.74 |
41 |
1.5 |
witness confirmed |
0.14 |
32 |
1.4 |
unknown |
5.2 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cdfpl/newton_2_8_false-unreach-call.i |
witness confirmed |
52 |
140 |
1.5 |
witness confirmed |
15 |
390 |
1.4 |
witness unconfirmed |
0.44 |
41 |
1.5 |
witness confirmed |
0.15 |
32 |
1.7 |
unknown |
5.2 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cdfpl/newton_3_6_false-unreach-call.i |
unknown |
510 |
580 |
- |
timeout |
920 |
880 |
- |
witness unconfirmed |
2.2 |
69 |
1.5 |
witness confirmed |
0.16 |
32 |
1.4 |
unknown |
5.2 |
240 |
- |
unknown |
5.1 |
240 |
- |
floats-cdfpl/newton_3_7_false-unreach-call.i |
unknown |
250 |
370 |
- |
out of memory |
710 |
15000 |
- |
witness unconfirmed |
0.62 |
69 |
1.5 |
witness confirmed |
0.14 |
32 |
1.4 |
unknown |
5.4 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cdfpl/newton_3_8_false-unreach-call.i |
unknown |
48 |
170 |
- |
witness confirmed |
22 |
510 |
1.5 |
witness unconfirmed |
0.43 |
68 |
1.5 |
witness confirmed |
0.28 |
32 |
1.4 |
unknown |
5.1 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cdfpl/sine_1_false-unreach-call.i |
witness confirmed |
5.2 |
45 |
1.4 |
witness confirmed |
4.4 |
210 |
1.7 |
witness unconfirmed |
0.27 |
24 |
1.4 |
witness confirmed |
0.16 |
32 |
1.4 |
unknown |
5.2 |
240 |
- |
unknown |
5.3 |
250 |
- |
floats-cdfpl/sine_2_false-unreach-call.i |
witness confirmed |
1.7 |
36 |
1.4 |
witness confirmed |
8.1 |
220 |
1.4 |
witness unconfirmed |
0.34 |
23 |
1.4 |
witness confirmed |
0.15 |
32 |
1.4 |
unknown |
5.1 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cdfpl/sine_3_false-unreach-call.i |
witness confirmed |
3.9 |
41 |
1.4 |
witness confirmed |
700 |
5200 |
1.5 |
witness unconfirmed |
0.45 |
23 |
1.4 |
witness confirmed |
0.30 |
32 |
1.4 |
unknown |
5.3 |
240 |
- |
unknown |
5.5 |
240 |
- |
floats-cdfpl/square_1_false-unreach-call.i |
witness confirmed |
1.0 |
35 |
1.4 |
witness confirmed |
67 |
380 |
1.5 |
witness unconfirmed |
0.15 |
14 |
1.4 |
witness confirmed |
0.16 |
32 |
1.4 |
unknown |
5.2 |
240 |
- |
unknown |
5.4 |
240 |
- |
floats-cdfpl/square_2_false-unreach-call.i |
witness confirmed |
1.0 |
35 |
1.4 |
witness confirmed |
300 |
700 |
1.5 |
witness unconfirmed |
0.11 |
14 |
1.4 |
witness confirmed |
0.17 |
32 |
1.4 |
unknown |
5.0 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cdfpl/square_3_false-unreach-call.i |
witness confirmed |
1.6 |
36 |
1.7 |
witness confirmed |
62 |
380 |
1.4 |
witness unconfirmed |
0.16 |
14 |
1.4 |
witness confirmed |
0.15 |
29 |
1.4 |
unknown |
5.5 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cdfpl/newton_1_1_true-unreach-call.i |
true |
850 |
93 |
- |
true |
640 |
640 |
- |
true |
150 |
55 |
- |
false(reach) |
0.29 |
32 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cdfpl/newton_1_2_true-unreach-call.i |
true |
300 |
100 |
- |
timeout |
920 |
570 |
- |
true |
300 |
64 |
- |
false(reach) |
0.29 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
4.9 |
240 |
- |
floats-cdfpl/newton_1_3_true-unreach-call.i |
true |
200 |
83 |
- |
timeout |
920 |
600 |
- |
true |
490 |
63 |
- |
false(reach) |
0.28 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cdfpl/newton_2_1_true-unreach-call.i |
true |
680 |
210 |
- |
timeout |
920 |
620 |
- |
true |
460 |
100 |
- |
false(reach) |
0.14 |
32 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.1 |
240 |
- |
floats-cdfpl/newton_2_2_true-unreach-call.i |
true |
770 |
210 |
- |
timeout |
920 |
720 |
- |
true |
840 |
120 |
- |
false(reach) |
0.16 |
32 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cdfpl/newton_2_3_true-unreach-call.i |
true |
720 |
220 |
- |
timeout |
920 |
740 |
- |
timeout |
920 |
120 |
- |
false(reach) |
0.18 |
32 |
- |
unknown |
5.8 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cdfpl/newton_2_4_true-unreach-call.i |
true |
850 |
270 |
- |
timeout |
920 |
710 |
- |
timeout |
920 |
120 |
- |
false(reach) |
0.16 |
32 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cdfpl/newton_2_5_true-unreach-call.i |
true |
850 |
320 |
- |
timeout |
920 |
760 |
- |
timeout |
920 |
120 |
- |
false(reach) |
0.25 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.4 |
240 |
- |
floats-cdfpl/newton_3_1_true-unreach-call.i |
true |
850 |
810 |
- |
timeout |
920 |
840 |
- |
true |
550 |
150 |
- |
false(reach) |
0.16 |
31 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.4 |
240 |
- |
floats-cdfpl/newton_3_2_true-unreach-call.i |
true |
850 |
510 |
- |
timeout |
920 |
790 |
- |
timeout |
920 |
150 |
- |
false(reach) |
0.16 |
32 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.4 |
240 |
- |
floats-cdfpl/newton_3_3_true-unreach-call.i |
true |
850 |
510 |
- |
timeout |
920 |
880 |
- |
timeout |
920 |
150 |
- |
false(reach) |
0.17 |
32 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cdfpl/newton_3_4_true-unreach-call.i |
true |
850 |
530 |
- |
timeout |
920 |
790 |
- |
timeout |
920 |
150 |
- |
false(reach) |
0.17 |
32 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cdfpl/newton_3_5_true-unreach-call.i |
true |
850 |
540 |
- |
timeout |
920 |
770 |
- |
timeout |
920 |
150 |
- |
false(reach) |
0.19 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cdfpl/sine_4_true-unreach-call.i |
error |
850 |
140 |
- |
timeout |
920 |
490 |
- |
timeout |
920 |
64 |
- |
false(reach) |
0.16 |
32 |
- |
unknown |
5.4 |
250 |
- |
unknown |
5.1 |
240 |
- |
floats-cdfpl/sine_5_true-unreach-call.i |
true |
30 |
50 |
- |
timeout |
920 |
440 |
- |
true |
840 |
56 |
- |
false(reach) |
0.13 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.1 |
240 |
- |
floats-cdfpl/sine_6_true-unreach-call.i |
true |
850 |
91 |
- |
timeout |
890 |
590 |
- |
true |
810 |
60 |
- |
false(reach) |
0.17 |
31 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cdfpl/sine_7_true-unreach-call.i |
true |
32 |
55 |
- |
true |
470 |
480 |
- |
true |
890 |
55 |
- |
false(reach) |
0.14 |
32 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cdfpl/sine_8_true-unreach-call.i |
true |
470 |
96 |
- |
true |
270 |
380 |
- |
timeout |
910 |
65 |
- |
false(reach) |
0.27 |
32 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.4 |
240 |
- |
floats-cdfpl/square_4_true-unreach-call.i |
true |
850 |
130 |
- |
true |
600 |
520 |
- |
false(reach) |
0.16 |
14 |
- |
false(reach) |
0.29 |
32 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.4 |
240 |
- |
floats-cdfpl/square_5_true-unreach-call.i |
true |
850 |
130 |
- |
true |
520 |
530 |
- |
true |
1.8 |
16 |
- |
false(reach) |
0.28 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cdfpl/square_6_true-unreach-call.i |
true |
850 |
130 |
- |
true |
360 |
460 |
- |
true |
3.5 |
17 |
- |
false(reach) |
0.15 |
32 |
- |
unknown |
5.2 |
240 |
- |
unknown |
6.0 |
240 |
- |
floats-cdfpl/square_7_true-unreach-call.i |
true |
390 |
140 |
- |
true |
240 |
440 |
- |
true |
3.0 |
17 |
- |
false(reach) |
0.15 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
6.1 |
240 |
- |
floats-cdfpl/square_8_true-unreach-call.i |
true |
7.2 |
36 |
- |
true |
57 |
300 |
- |
true |
0.082 |
13 |
- |
false(reach) |
0.15 |
31 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cbmc-regression/float-flags-simp1_true-unreach-call.i |
true |
1.5 |
37 |
- |
exception |
24 |
370 |
- |
false(reach) |
1.0 |
28 |
- |
unknown |
0.032 |
9.0 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.5 |
240 |
- |
floats-cbmc-regression/float-no-simp1_true-unreach-call.i |
true |
0.49 |
24 |
- |
true |
1.4 |
130 |
- |
true |
0.058 |
11 |
- |
true |
0.14 |
23 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.4 |
240 |
- |
floats-cbmc-regression/float-no-simp2_true-unreach-call.i |
true |
8.4 |
32 |
- |
true |
14 |
250 |
- |
true |
0.16 |
19 |
- |
unknown |
0.055 |
9.0 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cbmc-regression/float-no-simp3_true-unreach-call.i |
true |
0.48 |
23 |
- |
true |
1.4 |
140 |
- |
false(reach) |
0.10 |
11 |
- |
true |
0.14 |
27 |
- |
false(reach) |
5.2 |
250 |
- |
false(reach) |
5.6 |
250 |
- |
floats-cbmc-regression/float-no-simp4_true-unreach-call.i |
true |
1.3 |
28 |
- |
true |
3.9 |
250 |
- |
false(reach) |
1.1 |
19 |
- |
unknown |
0.059 |
9.0 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.5 |
240 |
- |
floats-cbmc-regression/float-no-simp6_true-unreach-call.i |
true |
0.52 |
23 |
- |
true |
1.4 |
140 |
- |
unknown |
0.040 |
2.0 |
- |
true |
0.16 |
27 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.5 |
250 |
- |
floats-cbmc-regression/float-no-simp7_true-unreach-call.i |
true |
0.50 |
23 |
- |
true |
1.4 |
140 |
- |
unknown |
0.040 |
2.0 |
- |
true |
0.21 |
27 |
- |
unknown |
5.6 |
240 |
- |
unknown |
6.2 |
240 |
- |
floats-cbmc-regression/float-no-simp8_true-unreach-call.i |
true |
0.59 |
26 |
- |
true |
1.6 |
140 |
- |
unknown |
0.022 |
6.0 |
- |
unknown |
0.049 |
9.0 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cbmc-regression/float-rounding1_true-unreach-call.i |
true |
1.2 |
29 |
- |
unknown |
3.3 |
230 |
- |
unknown |
0.045 |
6.0 |
- |
unknown |
0.048 |
9.0 |
- |
false(reach) |
5.3 |
240 |
- |
false(reach) |
5.6 |
240 |
- |
floats-cbmc-regression/float-to-double1_true-unreach-call.i |
true |
0.68 |
26 |
- |
false(reach) |
2.2 |
200 |
- |
true |
0.099 |
17 |
- |
unknown |
0.043 |
9.0 |
- |
true |
5.7 |
250 |
- |
true |
6.2 |
250 |
- |
floats-cbmc-regression/float-to-double2_true-unreach-call.i |
true |
0.48 |
23 |
- |
true |
1.4 |
130 |
- |
unknown |
0.028 |
2.0 |
- |
true |
0.12 |
21 |
- |
unknown |
5.5 |
250 |
- |
true |
5.5 |
240 |
- |
floats-cbmc-regression/float-zero-sum1_true-unreach-call.i |
true |
0.51 |
23 |
- |
true |
1.4 |
140 |
- |
unknown |
0.031 |
2.0 |
- |
true |
0.17 |
21 |
- |
false(reach) |
5.5 |
250 |
- |
false(reach) |
5.4 |
250 |
- |
floats-cbmc-regression/float11_true-unreach-call.i |
true |
0.53 |
24 |
- |
true |
1.4 |
140 |
- |
true |
0.056 |
12 |
- |
true |
0.14 |
22 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.1 |
240 |
- |
floats-cbmc-regression/float12_true-unreach-call.i |
true |
0.53 |
24 |
- |
true |
2.4 |
210 |
- |
true |
0.054 |
12 |
- |
false(reach) |
0.15 |
32 |
- |
unknown |
5.0 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cbmc-regression/float13_true-unreach-call.i |
true |
0.51 |
24 |
- |
true |
2.1 |
200 |
- |
false(reach) |
0.12 |
12 |
- |
true |
0.14 |
27 |
- |
unknown |
5.5 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cbmc-regression/float14_true-unreach-call.i |
true |
1.1 |
27 |
- |
true |
3.3 |
210 |
- |
false(reach) |
0.96 |
17 |
- |
unknown |
0.057 |
9.0 |
- |
unknown |
5.1 |
240 |
- |
unknown |
4.9 |
240 |
- |
floats-cbmc-regression/float18_true-unreach-call.i |
true |
1.1 |
27 |
- |
true |
1.5 |
140 |
- |
false(reach) |
1.0 |
17 |
- |
unknown |
0.048 |
9.0 |
- |
unknown |
5.6 |
240 |
- |
unknown |
5.5 |
250 |
- |
floats-cbmc-regression/float19_true-unreach-call.i |
true |
1.1 |
27 |
- |
true |
3.1 |
210 |
- |
unknown |
0.075 |
8.0 |
- |
unknown |
0.054 |
9.0 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cbmc-regression/float1_true-unreach-call.i |
true |
0.50 |
23 |
- |
true |
1.4 |
140 |
- |
true |
0.067 |
12 |
- |
true |
0.15 |
27 |
- |
unknown |
5.0 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cbmc-regression/float20_true-unreach-call.i |
true |
0.60 |
27 |
- |
true |
1.4 |
130 |
- |
unknown |
0.041 |
2.0 |
- |
false(reach) |
0.32 |
32 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cbmc-regression/float22_true-unreach-call.i |
true |
0.55 |
24 |
- |
true |
1.5 |
140 |
- |
unknown |
0.054 |
4.0 |
- |
true |
0.19 |
22 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.3 |
240 |
- |
floats-cbmc-regression/float2_true-unreach-call.i |
true |
0.51 |
23 |
- |
true |
1.4 |
130 |
- |
unknown |
0.015 |
2.0 |
- |
true |
0.15 |
27 |
- |
unknown |
5.0 |
240 |
- |
unknown |
4.9 |
240 |
- |
floats-cbmc-regression/float3_true-unreach-call.i |
true |
0.59 |
25 |
- |
true |
1.4 |
130 |
- |
true |
0.086 |
12 |
- |
false(reach) |
0.18 |
31 |
- |
unknown |
5.4 |
240 |
- |
unknown |
5.1 |
240 |
- |
floats-cbmc-regression/float4_true-unreach-call.i |
true |
35 |
46 |
- |
true |
37 |
320 |
- |
true |
0.16 |
18 |
- |
unknown |
0.052 |
9.0 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.5 |
240 |
- |
floats-cbmc-regression/float5_true-unreach-call.i |
true |
0.54 |
24 |
- |
true |
1.4 |
130 |
- |
true |
0.072 |
12 |
- |
false(reach) |
0.13 |
33 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.2 |
240 |
- |
floats-cbmc-regression/float6_true-unreach-call.i |
true |
0.56 |
24 |
- |
true |
1.4 |
130 |
- |
true |
0.081 |
13 |
- |
false(reach) |
0.19 |
33 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.0 |
240 |
- |
floats-cbmc-regression/float7_true-unreach-call.i |
true |
0.47 |
23 |
- |
false(reach) |
1.6 |
160 |
- |
true |
0.054 |
11 |
- |
true |
0.16 |
27 |
- |
false(reach) |
5.5 |
250 |
- |
false(reach) |
5.7 |
250 |
- |
floats-cbmc-regression/float8_true-unreach-call.i |
true |
2.6 |
29 |
- |
true |
7.0 |
220 |
- |
true |
0.089 |
17 |
- |
unknown |
0.042 |
9.0 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.1 |
240 |
- |
float-benchs/float_int_inv_square_false-unreach-call.c |
witness confirmed |
0.13 |
25 |
1.5 |
witness confirmed |
1.7 |
170 |
1.4 |
unknown |
0.055 |
11 |
- |
witness confirmed |
0.17 |
32 |
1.5 |
unknown |
5.1 |
240 |
- |
unknown |
5.2 |
240 |
- |
float-benchs/inv_square_false-unreach-call.c |
witness confirmed |
0.14 |
25 |
1.4 |
witness confirmed |
1.7 |
170 |
1.4 |
unknown |
0.057 |
12 |
- |
witness confirmed |
0.17 |
32 |
1.5 |
unknown |
5.2 |
240 |
- |
unknown |
5.3 |
240 |
- |
float-benchs/nan_double_false-unreach-call.c |
witness confirmed |
0.12 |
23 |
1.4 |
witness confirmed |
1.6 |
160 |
1.4 |
true |
0.067 |
12 |
- |
witness confirmed |
0.14 |
32 |
1.4 |
true |
5.7 |
250 |
- |
true |
5.2 |
250 |
- |
float-benchs/nan_float_false-unreach-call.c |
witness confirmed |
0.12 |
23 |
1.4 |
witness confirmed |
1.6 |
160 |
1.4 |
true |
0.073 |
12 |
- |
witness confirmed |
0.14 |
32 |
1.4 |
true |
5.6 |
250 |
- |
true |
5.4 |
240 |
- |
float-benchs/sin_interpolated_index_false-unreach-call.c |
witness confirmed |
3.9 |
210 |
1.7 |
unknown |
2.8 |
200 |
- |
unknown |
0.081 |
14 |
- |
witness confirmed |
0.34 |
32 |
1.6 |
unknown |
5.4 |
240 |
- |
unknown |
5.1 |
240 |
- |
float-benchs/inv_square_int_true-unreach-call.c |
true |
0.68 |
27 |
- |
true |
2.8 |
220 |
- |
unknown |
0.075 |
12 |
- |
false(reach) |
0.16 |
32 |
- |
unknown |
5.5 |
240 |
- |
unknown |
5.2 |
240 |
- |
float-benchs/inv_square_true-unreach-call.c |
true |
0.64 |
27 |
- |
true |
2.4 |
220 |
- |
unknown |
0.077 |
12 |
- |
false(reach) |
0.16 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.2 |
240 |
- |
float-benchs/nan_double_range_true-unreach-call.c |
true |
0.53 |
23 |
- |
true |
2.1 |
210 |
- |
true |
0.060 |
12 |
- |
false(reach) |
0.16 |
32 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.1 |
240 |
- |
float-benchs/nan_float_range_true-unreach-call.c |
true |
0.53 |
23 |
- |
true |
2.2 |
210 |
- |
true |
0.074 |
12 |
- |
false(reach) |
0.13 |
32 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.5 |
240 |
- |
float-benchs/sin_interpolated_bigrange_loose_true-unreach-call.c |
error |
850 |
710 |
- |
unknown |
2.9 |
210 |
- |
unknown |
0.090 |
14 |
- |
false(reach) |
0.23 |
34 |
- |
unknown |
5.3 |
240 |
- |
unknown |
5.5 |
240 |
- |
float-benchs/sin_interpolated_bigrange_tight_true-unreach-call.c |
error |
850 |
660 |
- |
unknown |
2.8 |
210 |
- |
unknown |
0.072 |
14 |
- |
false(reach) |
0.23 |
34 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.1 |
240 |
- |
float-benchs/sin_interpolated_index_true-unreach-call.c |
error |
850 |
660 |
- |
unknown |
2.7 |
210 |
- |
unknown |
0.089 |
14 |
- |
false(reach) |
0.22 |
32 |
- |
unknown |
5.1 |
240 |
- |
unknown |
5.3 |
240 |
- |
float-benchs/sin_interpolated_smallrange_true-unreach-call.c |
true |
850 |
3800 |
- |
unknown |
2.9 |
200 |
- |
unknown |
0.12 |
14 |
- |
unknown |
0.25 |
30 |
- |
unknown |
5.2 |
240 |
- |
unknown |
5.0 |
240 |
- |