Logic |
Solvers |
Benchmarks |
Order |
QF_AUFBV | 2 | 31 | z3n; MathSat5n |
|
AUFNIRA | 1 | 1046 | z3n |
|
AUFLIA | 2 | 3 | z3n; veriTn |
|
UFIDL | 2 | 62 | z3n; veriTn |
|
UF | 2 | 2039 | z3n; veriTn |
|
QF_UFNIA | 1 | 7 | z3n |
|
QF_UFNRA | 1 | 18 | z3n |
|
QF_NIRA | 1 | 2 | z3n |
|
QF_BVFP | 2 | 6 | z3n; MathSat5n |
|
UFLRA | 2 | 20 | z3n; veriTn |
|
QF_IDL | 3 | 816 | z3n; veriTn; SMTInterpol |
|
QF_RDL | 4 | 113 | veriTn; z3n; SMTInterpol; toysmtn |
|
QF_UFBV | 2 | 31 | MathSat5n; z3n |
|
QF_BV | 2 | 17172 | MathSat5n; z3n |
|
QF_LRA | 5 | 633 | SMTInterpol; MathSat5n; z3n; toysmtn; veriTn |
|
QF_LIA | 4 | 2840 | z3n; SMTInterpol; MathSat5n; veriTn |
|
UFLIA | 2 | 8377 | z3n; veriTn |
|
NIA | 1 | 3 | z3n |
|
QF_ANIA | 1 | 8 | z3n |
|
QF_ABV | 2 | 4644 | z3n; MathSat5n |
|
QF_UF | 5 | 4100 | MathSat5n; z3n; SMTInterpol; toysmtn; veriTn |
|
QF_AX | 3 | 279 | z3n; SMTInterpol; MathSat5n |
|
QF_AUFNIA | 1 | 15 | z3n |
|
QF_NRA | 1 | 4948 | z3n |
|
QF_UFIDL | 3 | 335 | z3n; SMTInterpol; veriTn |
|
AUFLIRA | 2 | 19749 | z3n; veriTn |
|
BV | 1 | 56 | z3n |
|
LIA | 2 | 191 | veriTn; z3n |
|
QF_UFLRA | 5 | 853 | z3n; MathSat5n; SMTInterpol; toysmtn; veriTn |
|
QF_NIA | 1 | 316 | z3n |
|
QF_LIRA | 2 | 5 | z3n; SMTInterpol |
|
UFBV | 1 | 53 | z3n |
|
UFNIA | 1 | 2318 | z3n |
|
QF_ALIA | 4 | 80 | z3n; SMTInterpol; MathSat5n; veriTn |
|
ALIA | 2 | 41 | z3n; veriTn |
|
QF_UFLIA | 4 | 195 | MathSat5n; z3n; SMTInterpol; veriTn |
|
QF_FP | 1 | 17213 | MathSat5n |
|
NRA | 1 | 3788 | z3n |
|
QF_AUFLIA | 4 | 516 | z3n; SMTInterpol; veriTn; MathSat5n |
|
LRA | 2 | 319 | veriTn; z3n |
|