The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results as of Thu Jul 7 07:24:34 GMT
| 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 |
n. Non-competitive.