Logic |
Solvers |
Benchmarks |
Order |
QF_AUFBV | 3 | 25 | mathsat-5.4.1n; z3-4.5.0n; CVC4 |
mathsat-5.4.1n; z3-4.5.0n; CVC4 |
|
|
AUFNIRA | 2 | 1050 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|
AUFLIA | 2 | 3 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
UFIDL | 2 | 57 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|
UF | 2 | 3316 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|
QF_UFNRA | 2 | 11 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
QF_UFNIA | 2 | 7 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
QF_NIRA | 2 | 2 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
QF_BVFP | 1 | 3174 | z3-4.5.0n |
z3-4.5.0n |
|
|
UFLRA | 2 | 10 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
QF_IDL | 3 | 816 | z3-4.5.0n; CVC4; SMTInterpol |
z3-4.5.0n; CVC4; SMTInterpol |
|
|
QF_RDL | 3 | 113 | z3-4.5.0n; CVC4; SMTInterpol |
z3-4.5.0n; CVC4; SMTInterpol |
|
|
QF_UFBV | 3 | 31 | mathsat-5.4.1n; z3-4.5.0n; CVC4 |
mathsat-5.4.1n; z3-4.5.0n; CVC4 |
|
|
QF_BV | 3 | 23732 | mathsat-5.4.1n; z3-4.5.0n; CVC4 |
mathsat-5.4.1n; z3-4.5.0n; CVC4 |
|
|
QF_LRA | 4 | 671 | SMTInterpol; z3-4.5.0n; mathsat-5.4.1n; CVC4 |
SMTInterpol; z3-4.5.0n; mathsat-5.4.1n; CVC4 |
|
|
QF_LIA | 4 | 2844 | SMTInterpol; z3-4.5.0n; mathsat-5.4.1n; CVC4 |
z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4 |
|
|
UFLIA | 2 | 7714 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|
NIA | 2 | 4 | CVC4; z3-4.5.0n |
z3-4.5.0n; CVC4 |
|
|
QF_ANIA | 2 | 8 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|
QF_ABV | 3 | 4673 | z3-4.5.0n; CVC4; mathsat-5.4.1n |
z3-4.5.0n; CVC4; mathsat-5.4.1n |
|
|
QF_UF | 4 | 4101 | CVC4; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n |
CVC4; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n |
|
|
QF_AX | 4 | 279 | z3-4.5.0n; SMTInterpol; CVC4; mathsat-5.4.1n |
z3-4.5.0n; SMTInterpol; CVC4; mathsat-5.4.1n |
|
|
QF_AUFNIA | 2 | 12 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
QF_NRA | 2 | 5296 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|
QF_UFIDL | 3 | 322 | z3-4.5.0n; SMTInterpol; CVC4 |
z3-4.5.0n; SMTInterpol; CVC4 |
|
|
AUFLIRA | 2 | 19771 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
BV | 2 | 94 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
LIA | 2 | 233 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|
QF_UFLRA | 4 | 511 | mathsat-5.4.1n; z3-4.5.0n; SMTInterpol; CVC4 |
mathsat-5.4.1n; z3-4.5.0n; SMTInterpol; CVC4 |
|
|
QF_NIA | 2 | 3130 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
QF_LIRA | 3 | 5 | z3-4.5.0n; CVC4; SMTInterpol |
z3-4.5.0n; CVC4; SMTInterpol |
|
|
UFBV | 2 | 97 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
UFNIA | 2 | 2432 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|
QF_ALIA | 4 | 80 | z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4 |
z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4 |
|
|
ALIA | 2 | 41 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
QF_UFLIA | 4 | 183 | z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4 |
z3-4.5.0n; SMTInterpol; mathsat-5.4.1n; CVC4 |
|
|
QF_FP | 1 | 20028 | z3-4.5.0n |
z3-4.5.0n |
|
|
NRA | 2 | 3801 | z3-4.5.0n; CVC4 |
z3-4.5.0n; CVC4 |
|
|
QF_AUFLIA | 4 | 516 | CVC4; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n |
CVC4; z3-4.5.0n; SMTInterpol; mathsat-5.4.1n |
|
|
LRA | 2 | 1106 | CVC4; z3-4.5.0n |
CVC4; z3-4.5.0n |
|
|