The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results as of Wed Jun 29 20:25:52 GMT
| 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 |
n. Non-competitive.