| QF_UF |
eq_diamond |
crafted |
100 |
79 |
|
NEQ |
crafted |
48 |
15 |
|
PEQ |
crafted |
48 |
23 |
|
QG-classification/loops6 |
crafted |
448 |
0 |
|
QG-classification/qg5 |
crafted |
5286 |
10 |
|
QG-classification/qg6 |
crafted |
244 |
36 |
|
QG-classification/qg7 |
crafted |
426 |
27 |
|
SEQ |
crafted |
56 |
10 |
| QF_RDL |
check |
check |
2 |
2 |
|
sal |
industrial |
60 |
60 |
|
scheduling |
crafted |
106 |
72 |
|
skdmxa |
industrial |
4 |
4 |
|
skdmxa2 |
industrial |
32 |
32 |
| QF_IDL |
Averest/binary_search |
industrial |
323 |
0 |
|
Averest/buble_sort |
industrial |
52 |
1 |
|
Averest/sorting_network |
industrial |
49 |
4 |
|
cellar |
industrial |
14 |
1 |
|
check |
check |
3 |
3 |
|
diamonds |
crafted |
36 |
2 |
|
DTP |
random |
60 |
0 |
|
job_shop |
crafted |
120 |
11 |
|
mathsat/fischer |
industrial |
119 |
18 |
|
parity |
crafted |
248 |
37 |
|
qlock |
industrial |
72 |
38 |
|
queens_bench/n_queen |
crafted |
99 |
6 |
|
queens_bench/super_queen |
crafted |
99 |
1 |
|
queens_bench/toroidal_bench |
crafted |
99 |
57 |
|
schedulingIDL |
crafted |
280 |
24 |
| QF_UFIDL |
bcnscheduling |
crafted |
13 |
9 |
|
check |
check |
3 |
3 |
|
mathsat/EufLaArithmetic/vhard |
crafted |
19 |
11 |
|
pete |
industrial |
23 |
17 |
|
pete2 |
industrial |
210 |
97 |
|
pete3 |
industrial |
6 |
6 |
|
RDS |
industrial |
28 |
12 |
|
RTCL/b13_tf_100 |
industrial |
17 |
0 |
|
uclid |
industrial |
37 |
11 |
|
UCLID-pred/bakery |
industrial |
19 |
10 |
|
UCLID-pred/DLX |
industrial |
6 |
2 |
|
UCLID-pred/ibm_cache |
industrial |
28 |
11 |
|
UCLID-pred/OOO |
industrial |
10 |
6 |
|
uclid2 |
industrial |
13 |
8 |
| QF_UFLIA |
check |
check |
2 |
2 |
|
mathsat/EufLaArithmetic/hard |
crafted |
17 |
16 |
|
mathsat/EufLaArithmetic/medium |
crafted |
16 |
16 |
|
mathsat/Hash |
crafted |
198 |
39 |
|
mathsat/Wisa |
industrial |
223 |
42 |
|
wisas |
industrial |
108 |
87 |
| QF_LRA |
check |
check |
2 |
2 |
|
clock_synchro |
industrial |
36 |
14 |
|
miplib |
industrial |
42 |
31 |
|
sal/carpark |
industrial |
102 |
0 |
|
sal/pursuit |
industrial |
20 |
8 |
|
sal/tgc |
industrial |
27 |
2 |
|
sc |
industrial |
144 |
64 |
|
TM |
industrial |
25 |
8 |
|
tta_startup |
industrial |
72 |
30 |
|
uart |
industrial |
73 |
43 |
| QF_LIA |
Averest/parallel_prefix_sum |
industrial |
19 |
1 |
|
check |
check |
5 |
5 |
|
CIRC/multiplier |
industrial |
176 |
0 |
|
CIRC/multiplier_prime |
industrial |
17 |
1 |
|
CIRC/simplebitadder |
industrial |
17 |
2 |
|
nec-smt/large/bftpd_login |
industrial |
361 |
22 |
|
nec-smt/large/checkpass |
industrial |
242 |
12 |
|
nec-smt/large/checkpass_pwd |
industrial |
642 |
30 |
|
nec-smt/large/getoption |
industrial |
20 |
2 |
|
nec-smt/large/getoption_directories |
industrial |
65 |
5 |
|
nec-smt/large/getoption_group |
industrial |
356 |
19 |
|
nec-smt/large/getoption_user |
industrial |
259 |
22 |
|
nec-smt/large/handler_sigchld |
industrial |
130 |
13 |
|
nec-smt/large/int_from_list |
industrial |
173 |
12 |
|
nec-smt/large/mygetpwnam |
industrial |
8 |
1 |
|
nec-smt/large/user_is_in_group |
industrial |
125 |
12 |
|
nec-smt/med/checkpass_pwd |
industrial |
215 |
18 |
|
nec-smt/med/config_read_line |
industrial |
28 |
3 |
|
nec-smt/med/int_from_list |
industrial |
111 |
4 |
|
nec-smt/small/checkpass_pwd |
industrial |
14 |
1 |
|
rings |
crafted |
294 |
20 |
| QF_AUFLIA |
array_benchmarks/misc |
industrial |
27 |
0 |
|
array_benchmarks/pointer |
industrial |
8 |
3 |
|
array_benchmarks/qlock |
industrial |
11 |
8 |
|
check |
check |
6 |
6 |
|
cvc |
crafted |
32 |
0 |
|
cvc |
industrial |
22 |
3 |
|
qlock2 |
industrial |
52 |
44 |
|
storecomm |
crafted |
1404 |
70 |
|
storeinv |
crafted |
76 |
8 |
|
swap |
crafted |
606 |
64 |
| QF_BV |
bench_ab |
industrial |
560 |
0 |
|
brummayerbiere |
crafted |
13 |
10 |
|
brummayerbiere2 |
industrial |
65 |
43 |
|
crafted |
crafted |
22 |
0 |
|
spear/cvs_v1.11.22 |
industrial |
29 |
1 |
|
spear/openldap_v2.3.35 |
industrial |
8 |
2 |
|
spear/samba_v3.0.24 |
industrial |
1386 |
3 |
|
stp |
industrial |
1 |
1 |
|
tacas07 |
industrial |
5 |
4 |
|
uclid/catchconv |
industrial |
414 |
135 |
|
uclid/tcas |
industrial |
2 |
1 |
| QF_AUFBV |
bench_ab |
industrial |
8024 |
0 |
|
brummayerbiere |
crafted |
293 |
92 |
|
platania/bellford |
industrial |
19 |
16 |
|
platania/bubble_sort |
industrial |
15 |
10 |
|
platania/copy_array |
industrial |
19 |
15 |
|
platania/no_init_bubble_sort |
industrial |
12 |
10 |
|
platania/no_init_selection_sort |
industrial |
12 |
9 |
|
platania/prim |
industrial |
9 |
7 |
|
platania/selection_sort |
industrial |
18 |
11 |
|
stp |
industrial |
40 |
30 |
| AUFLIRA |
misc |
crafted |
7 |
2 |
|
nasa/fol_simplify |
industrial |
1583 |
0 |
|
nasa/fol_simplify_arithmetics |
industrial |
1043 |
4 |
|
nasa/fol_simplify_array |
industrial |
1602 |
4 |
|
nasa/fol_simplify_array_only |
industrial |
14412 |
4 |
|
nasa/fol_simplify_structure_forall |
industrial |
6088 |
4 |
|
nasa/fol_simplify_structure_prop |
industrial |
1431 |
4 |
|
nasa/vc_normalize_subst |
industrial |
345 |
1 |
|
peter |
crafted |
198 |
61 |
|
why |
industrial |
1325 |
116 |
| QF_UFLRA |
mathsat/RandomCoupled |
random |
400 |
111 |
|
mathsat/RandomDecoupled |
random |
500 |
89 |
| QF_AX |
cvc |
crafted |
1 |
1 |
|
storecomm |
crafted |
626 |
69 |
|
storeinv |
crafted |
96 |
48 |
|
swap |
crafted |
762 |
82 |
| AUFLIA-p |
boogie |
industrial |
1254 |
43 |
|
Burns |
industrial |
14 |
5 |
|
check |
check |
1 |
1 |
|
misc |
crafted |
26 |
20 |
|
misc |
industrial |
34 |
0 |
|
piVC |
industrial |
42 |
14 |
|
RicartAgrawala |
industrial |
14 |
3 |
|
simplify |
industrial |
833 |
47 |
|
simplify2/front_end_suite |
industrial |
2332 |
65 |
|
simplify2/small_suite |
industrial |
16 |
3 |
| AUFLIA+p |
boogie |
industrial |
1254 |
51 |
|
Burns |
industrial |
14 |
4 |
|
check |
check |
1 |
1 |
|
misc |
crafted |
26 |
20 |
|
misc |
industrial |
2 |
0 |
|
piVC |
industrial |
42 |
14 |
|
RicartAgrawala |
industrial |
14 |
2 |
|
sexpr |
industrial |
32 |
4 |
|
simplify |
industrial |
833 |
52 |
|
simplify2/front_end_suite |
industrial |
2332 |
49 |
|
simplify2/small_suite |
industrial |
16 |
4 |