Logic |
Solvers |
Benchmarks |
Order |
ALIA | 2 | 41 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
AUFBVDTLIA | 1 | 25 | CVC4 |
CVC4 |
|
|
AUFLIA | 2 | 3 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
AUFLIRA | 2 | 19771 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
AUFNIRA | 2 | 1053 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
BV | 2 | 4937 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
LIA | 2 | 233 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
LRA | 2 | 1539 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
NIA | 2 | 4 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
NRA | 2 | 3801 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
QF_ABV | 4 | 4677 | Yices 2.6.0; z3-4.7.1n; mathsat-5.5.2n; CVC4 |
Yices 2.6.0; z3-4.7.1n; mathsat-5.5.2n; CVC4 |
|
|
QF_ABVFP | 1 | 3934 | CVC4 |
CVC4 |
|
|
QF_ALIA | 5 | 80 | z3-4.7.1n; Yices 2.6.0; mathsat-5.5.2n; SMTInterpol; CVC4 |
z3-4.7.1n; Yices 2.6.0; mathsat-5.5.2n; SMTInterpol; CVC4 |
|
|
QF_ANIA | 2 | 8 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
QF_AUFBV | 4 | 25 | mathsat-5.5.2n; Yices 2.6.0; CVC4; z3-4.7.1n |
mathsat-5.5.2n; Yices 2.6.0; CVC4; z3-4.7.1n |
|
|
QF_AUFLIA | 5 | 516 | CVC4; z3-4.7.1n; Yices 2.6.0; mathsat-5.5.2n; SMTInterpol |
CVC4; z3-4.7.1n; Yices 2.6.0; mathsat-5.5.2n; SMTInterpol |
|
|
QF_AUFNIA | 2 | 12 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
QF_AX | 5 | 279 | Yices 2.6.0; z3-4.7.1n; CVC4; mathsat-5.5.2n; SMTInterpol |
Yices 2.6.0; z3-4.7.1n; CVC4; mathsat-5.5.2n; SMTInterpol |
|
|
QF_BV | 4 | 25700 | Yices 2.6.0; mathsat-5.5.2n; CVC4; z3-4.7.1n |
Yices 2.6.0; mathsat-5.5.2n; CVC4; z3-4.7.1n |
|
|
QF_BVFP | 2 | 3174 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
QF_DT | 2 | 4422 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
QF_FP | 2 | 20026 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
QF_IDL | 5 | 816 | z3-4.7.1n; CVC4; Yices 2.6.0; SMTInterpol; mathsat-5.5.2n |
z3-4.7.1n; CVC4; Yices 2.6.0; SMTInterpol; mathsat-5.5.2n |
|
|
QF_LIA | 5 | 3019 | SMTInterpol; Yices 2.6.0; mathsat-5.5.2n; z3-4.7.1n; CVC4 |
SMTInterpol; Yices 2.6.0; mathsat-5.5.2n; z3-4.7.1n; CVC4 |
|
|
QF_LIRA | 4 | 5 | z3-4.7.1n; CVC4; Yices 2.6.0; SMTInterpol |
z3-4.7.1n; CVC4; Yices 2.6.0; SMTInterpol |
|
|
QF_LRA | 5 | 683 | SMTInterpol; Yices 2.6.0; z3-4.7.1n; mathsat-5.5.2n; CVC4 |
SMTInterpol; Yices 2.6.0; z3-4.7.1n; mathsat-5.5.2n; CVC4 |
|
|
QF_NIA | 2 | 4842 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
QF_NIRA | 2 | 2 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
QF_NRA | 2 | 5357 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
QF_RDL | 5 | 113 | z3-4.7.1n; CVC4; Yices 2.6.0; mathsat-5.5.2n; SMTInterpol |
z3-4.7.1n; CVC4; Yices 2.6.0; mathsat-5.5.2n; SMTInterpol |
|
|
QF_UF | 5 | 4330 | CVC4; z3-4.7.1n; SMTInterpol; Yices 2.6.0; mathsat-5.5.2n |
CVC4; z3-4.7.1n; SMTInterpol; Yices 2.6.0; mathsat-5.5.2n |
|
|
QF_UFBV | 4 | 575 | z3-4.7.1n; Yices 2.6.0; mathsat-5.5.2n; CVC4 |
z3-4.7.1n; Yices 2.6.0; mathsat-5.5.2n; CVC4 |
|
|
QF_UFIDL | 5 | 322 | Yices 2.6.0; z3-4.7.1n; SMTInterpol; mathsat-5.5.2n; CVC4 |
Yices 2.6.0; z3-4.7.1n; SMTInterpol; mathsat-5.5.2n; CVC4 |
|
|
QF_UFLIA | 5 | 183 | z3-4.7.1n; SMTInterpol; Yices 2.6.0; mathsat-5.5.2n; CVC4 |
z3-4.7.1n; SMTInterpol; Yices 2.6.0; mathsat-5.5.2n; CVC4 |
|
|
QF_UFLRA | 5 | 511 | mathsat-5.5.2n; z3-4.7.1n; Yices 2.6.0; SMTInterpol; CVC4 |
mathsat-5.5.2n; z3-4.7.1n; Yices 2.6.0; SMTInterpol; CVC4 |
|
|
QF_UFNIA | 2 | 7 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
QF_UFNRA | 2 | 11 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
UF | 2 | 3442 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
UFBV | 2 | 97 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
UFDT | 1 | 1863 | CVC4 |
CVC4 |
|
|
UFIDL | 2 | 57 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
UFLIA | 2 | 7743 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|
UFLRA | 2 | 10 | z3-4.7.1n; CVC4 |
z3-4.7.1n; CVC4 |
|
|
UFNIA | 2 | 2457 | CVC4; z3-4.7.1n |
CVC4; z3-4.7.1n |
|
|