| Logic |
Solvers |
Benchmarks |
Order (parallel performance) |
| Order (parallel performance on industrial benchmarks) |
| ALIA | 4 | 24 | [Z3]; CVC4 (exp); CVC4; CVC3 |
| [Z3]; CVC4 (exp); CVC4; CVC3 |
| ANIA | 3 | 3 | [Z3]; CVC4; CVC4 (exp) |
| [Z3]; CVC4; CVC4 (exp) |
| LIA | 4 | 6 | [Z3]; CVC4 (exp); CVC4; CVC3 |
| [Z3]; CVC4 (exp); CVC4; CVC3 |
| QF_ALIA | 6 | 44 | [Z3]; Yices; [MathSat]; CVC4 (exp); CVC4; SMTInterpol |
| [Z3]; Yices; [MathSat]; CVC4 (exp); CVC4; SMTInterpol |
| QF_ANIA | 3 | 5 | [Z3]; CVC4 (exp); CVC4 |
| [Z3]; CVC4 (exp); CVC4 |
| QF_AUFLIA | 6 | 72 | Yices; [Z3]; SMTInterpol; CVC4 (exp); [MathSat]; CVC4 |
| Yices; [Z3]; SMTInterpol; CVC4 (exp); [MathSat]; CVC4 |
| QF_BV | 11 | 18 | [MathSat]; Yices; CVC4; [Z3]; [Boolector fixed]; CVC4 (exp); Boolector; STP-CMSat4 (v15); STP-MiniSAT (v15); STP-CMSat4 (mt-v15); STP-CMSat4 |
| [MathSat]; Yices; CVC4; [Z3]; [Boolector fixed]; CVC4 (exp); Boolector; STP-CMSat4 (v15); STP-MiniSAT (v15); STP-CMSat4 (mt-v15); STP-CMSat4 |
| QF_LIA | 6 | 65 | Yices; [Z3]; SMTInterpol; [MathSat]; CVC4; CVC4 (exp) |
| Yices; [Z3]; SMTInterpol; [MathSat]; CVC4; CVC4 (exp) |
| QF_LRA | 6 | 10 | [MathSat]; Yices; [Z3]; CVC4 (exp); CVC4; SMTInterpol |
| [MathSat]; Yices; [Z3]; CVC4 (exp); CVC4; SMTInterpol |
| QF_NIA | 4 | 10 | [Z3]; CVC4; CVC4 (exp); CVC3 |
| [Z3]; CVC4; CVC4 (exp); CVC3 |
| QF_UFLIA | 6 | 905 | [Z3]; CVC4 (exp); CVC4; Yices; [MathSat]; SMTInterpol |
| [Z3]; CVC4 (exp); CVC4; Yices; [MathSat]; SMTInterpol |
| QF_UFLRA | 6 | 3331 | [Z3]; Yices; CVC4 (exp); CVC4; [MathSat]; SMTInterpol |
| [Z3]; Yices; CVC4 (exp); CVC4; [MathSat]; SMTInterpol |
| QF_UFNIA | 4 | 1 | [Z3]; CVC4 (exp); CVC4; CVC3 |
| [Z3]; CVC4 (exp); CVC4; CVC3 |
| UFLRA | 4 | 5358 | [Z3]; CVC4; CVC3; CVC4 (exp) |
| [Z3]; CVC4; CVC3; CVC4 (exp) |
