The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LRA division as of Fri Jul 13 00:02:11 GMT
Benchmarks in this division : 1649
Time limit: 1200s
| Sequential Performance | Parallel Performance |
|---|---|
| CVC4 | CVC4 |
| Solver | Error Score | Correctly Solved Score | CPU time Score | Solved | Unsolved |
|---|---|---|---|---|---|
| CVC4 | 0.000 | 1586.833 | 69.006 | 1566 | 83 |
| Ctrl-Ergo | 0.000 | 1450.082 | 172.097 | 1354 | 295 |
| MathSATn | 0.000 | 1536.458 | 107.673 | 1461 | 188 |
| SMTInterpol | 0.000 | 1548.476 | 102.257 | 1521 | 128 |
| SMTRAT-MCSAT | 0.000 | 1090.526 | 409.015 | 711 | 938 |
| SMTRAT-Rat | 0.000 | 1297.891 | 275.918 | 984 | 665 |
| SPASS-SATT | 0.000 | 1586.396 | 64.292 | 1590 | 59 |
| Yices 2.6.0 | 0.000 | 1583.186 | 63.901 | 1567 | 82 |
| opensmt2 | 0.000 | 1498.663 | 131.674 | 1329 | 320 |
| veriT | 0.000 | 1568.212 | 79.840 | 1527 | 122 |
| z3-4.7.1n | 0.000 | 1527.249 | 113.154 | 1435 | 214 |
| Solver | Error Score | Correctly Solved Score | CPU time Score | WALL time Score | Solved | Unsolved |
|---|---|---|---|---|---|---|
| CVC4 | 0.000 | 1586.833 | 69.007 | 69.191 | 1566 | 83 |
| Ctrl-Ergo | 0.000 | 1487.857 | 550.944 | 138.566 | 1438 | 211 |
| MathSATn | 0.000 | 1536.458 | 107.673 | 107.679 | 1461 | 188 |
| SMTInterpol | 0.000 | 1553.375 | 111.861 | 96.992 | 1531 | 118 |
| SMTRAT-MCSAT | 0.000 | 1090.526 | 409.020 | 409.048 | 711 | 938 |
| SMTRAT-Rat | 0.000 | 1297.891 | 275.921 | 275.936 | 984 | 665 |
| SPASS-SATT | 0.000 | 1586.396 | 64.293 | 64.281 | 1590 | 59 |
| Yices 2.6.0 | 0.000 | 1583.186 | 63.901 | 63.896 | 1567 | 82 |
| opensmt2 | 0.000 | 1498.663 | 131.674 | 131.683 | 1329 | 320 |
| veriT | 0.000 | 1568.212 | 79.840 | 79.846 | 1527 | 122 |
| z3-4.7.1n | 0.000 | 1527.249 | 113.155 | 113.146 | 1435 | 214 |
n. Non-competing.
1. Scores are computed according to Section 7 of the rules.