The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_AX division as of Fri Oct 30 12:49:29 GMT
Competition benchmarks = 551
Competition industrial benchmarks = 0
| Sequential Performance | Sequential Performance (industrial) | Parallel Performance | Parallel Performance (industrial) |
|---|---|---|---|
| Yices | - | Yices | - |
| Solver | Errors | Corrects | CPU |
|---|---|---|---|
| CVC4 | 0 | 551 | 60.60 |
| CVC4 (exp) | 0 | 551 | 59.99 |
| SMTInterpol | 0 | 551 | 1001.93 |
| Yices | 0 | 551 | 5.77 |
| MathSatn | 0 | 551 | 42.03 |
| z3n | 0 | 551 | 44.19 |
| veriT | 0 | 8 | 3.51 |
| Solver | Errors | Corrects | CPU |
|---|---|---|---|
| CVC4 | 0 | 0 | 0.00 |
| CVC4 (exp) | 0 | 0 | 0.00 |
| SMTInterpol | 0 | 0 | 0.00 |
| Yices | 0 | 0 | 0.00 |
| MathSatn | 0 | 0 | 0.00 |
| z3n | 0 | 0 | 0.00 |
| veriT | 0 | 0 | 0.00 |
| Solver | Errors | Corrects | CPU | WALL |
|---|---|---|---|---|
| CVC4 | 0 | 551 | 60.60 | 61.80 |
| CVC4 (exp) | 0 | 551 | 59.99 | 61.25 |
| SMTInterpol | 0 | 551 | 1001.93 | 498.86 |
| Yices | 0 | 551 | 5.77 | 8.18 |
| MathSatn | 0 | 551 | 42.03 | 42.59 |
| z3n | 0 | 551 | 44.19 | 44.27 |
| veriT | 0 | 8 | 3.51 | 5.95 |
| Solver | Errors | Corrects | CPU | WALL |
|---|---|---|---|---|
| CVC4 | 0 | 0 | 0.00 | 0.00 |
| CVC4 (exp) | 0 | 0 | 0.00 | 0.00 |
| SMTInterpol | 0 | 0 | 0.00 | 0.00 |
| Yices | 0 | 0 | 0.00 | 0.00 |
| MathSatn | 0 | 0 | 0.00 | 0.00 |
| z3n | 0 | 0 | 0.00 | 0.00 |
| veriT | 0 | 0 | 0.00 | 0.00 |
| Solver | Not Solved | Remaining |
|---|---|---|
| CVC4 | 0 | 0 |
| CVC4 (exp) | 0 | 0 |
| SMTInterpol | 0 | 0 |
| Yices | 0 | 0 |
| MathSatn | 0 | 0 |
| z3n | 0 | 0 |
| veriT | 543 | 0 |
n. Non-competitive.