Logic |
Solvers |
Benchmarks |
Order (parallel performance) |
ANIA | 2 | 3 | z3n; CVC4n |
|
QF_ANIA | 2 | 5 | z3n; CVC4n |
|
QF_ALIA | 5 | 44 | z3n; SMTInterpol; Yices2; MathSat5n; CVC4n |
|
QF_UFNIA | 2 | 1 | z3n; CVC4n |
|
LIA | 2 | 6 | z3n; CVC4n |
|
ALIA | 2 | 24 | z3n; CVC4n |
|
QF_UFLRA | 5 | 3331 | z3n; Yices2; SMTInterpol; CVC4n; MathSat5n |
|
UFLRA | 2 | 5358 | z3n; CVC4n |
|
QF_UFLIA | 5 | 905 | z3n; CVC4n; Yices2; SMTInterpol; MathSat5n |
|
QF_NIA | 2 | 10 | CVC4n; z3n |
|
QF_BV | 10 | 18 | MathSat5n; Yices2; stp-cms-st; stp-cms-mt; stp-cms-exp; CVC4n; MapleSTP; MapleSTP-mt; stp-minisat-st; z3n |
|
QF_LRA | 5 | 10 | MathSat5n; SMTInterpol; z3n; Yices2; CVC4n |
|
QF_LIA | 5 | 69 | Yices2; z3n; SMTInterpol; MathSat5n; CVC4n |
|
QF_AUFLIA | 5 | 72 | Yices2; z3n; SMTInterpol; MathSat5n; CVC4n |
|