The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_LRA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 582 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| OpenSMT | OpenSMT | Yices2 | OpenSMT | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| OpenSMT | 0 | 546 | 67175.82 | 67080.728 | 546 | 315 | 231 | 36 | 36 | 0 |
| 2020-OpenSMTn | 0 | 543 | 69798.963 | 69785.788 | 543 | 314 | 229 | 39 | 39 | 0 |
| cvc5 | 0 | 541 | 86611.364 | 87989.488 | 541 | 316 | 225 | 41 | 41 | 0 |
| Yices2 | 0 | 540 | 80988.036 | 80961.373 | 540 | 321 | 219 | 42 | 42 | 0 |
| 2019-Par4n | 0 | 536 | 105313.498 | 67940.747 | 536 | 319 | 217 | 46 | 46 | 0 |
| z3n | 0 | 527 | 106500.924 | 106479.681 | 527 | 309 | 218 | 55 | 55 | 0 |
| veriT | 0 | 513 | 122790.957 | 122783.776 | 513 | 299 | 214 | 69 | 69 | 0 |
| SMTInterpol | 0 | 494 | 184196.854 | 176341.757 | 494 | 304 | 190 | 88 | 88 | 0 |
| MathSAT5n | 0 | 471 | 166929.811 | 166932.874 | 471 | 289 | 182 | 111 | 111 | 0 |
| mc2 | 0 | 201 | 49389.939 | 49245.453 | 201 | 123 | 78 | 381 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 565 | 136198.308 | 49817.594 | 565 | 337 | 228 | 17 | 17 | 0 |
| OpenSMT | 0 | 546 | 67179.83 | 67079.508 | 546 | 315 | 231 | 36 | 36 | 0 |
| 2020-OpenSMTn | 0 | 543 | 69805.673 | 69784.158 | 543 | 314 | 229 | 39 | 39 | 0 |
| cvc5 | 0 | 541 | 87891.481 | 87987.028 | 541 | 316 | 225 | 41 | 41 | 0 |
| Yices2 | 0 | 540 | 80992.646 | 80960.343 | 540 | 321 | 219 | 42 | 42 | 0 |
| z3n | 0 | 527 | 106509.904 | 106477.611 | 527 | 309 | 218 | 55 | 55 | 0 |
| veriT | 0 | 513 | 122797.797 | 122781.166 | 513 | 299 | 214 | 69 | 69 | 0 |
| SMTInterpol | 0 | 497 | 184390.714 | 176238.607 | 497 | 305 | 192 | 85 | 85 | 0 |
| MathSAT5n | 0 | 471 | 166947.951 | 166928.104 | 471 | 289 | 182 | 111 | 111 | 0 |
| mc2 | 0 | 201 | 49390.409 | 49245.183 | 201 | 123 | 78 | 381 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 337 | 76444.162 | 24807.434 | 337 | 337 | 0 | 6 | 239 | 17 | 0 |
| Yices2 | 0 | 321 | 35993.441 | 35958.473 | 321 | 321 | 0 | 22 | 239 | 42 | 0 |
| cvc5 | 0 | 316 | 54364.989 | 54448.948 | 316 | 316 | 0 | 27 | 239 | 41 | 0 |
| OpenSMT | 0 | 315 | 48871.218 | 48860.237 | 315 | 315 | 0 | 28 | 239 | 36 | 0 |
| 2020-OpenSMTn | 0 | 314 | 50396.725 | 50399.487 | 314 | 314 | 0 | 29 | 239 | 39 | 0 |
| z3n | 0 | 309 | 59018.635 | 59011.143 | 309 | 309 | 0 | 34 | 239 | 55 | 0 |
| SMTInterpol | 0 | 305 | 89642.758 | 84688.706 | 305 | 305 | 0 | 38 | 239 | 85 | 0 |
| veriT | 0 | 299 | 76340.152 | 76343.37 | 299 | 299 | 0 | 44 | 239 | 69 | 0 |
| MathSAT5n | 0 | 289 | 83048.351 | 83026.4 | 289 | 289 | 0 | 54 | 239 | 111 | 0 |
| mc2 | 0 | 123 | 21834.746 | 21746.454 | 123 | 123 | 0 | 220 | 239 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | N/A | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| OpenSMT | 0 | 231 | 14708.612 | 14619.271 | 231 | 0 | 231 | 5 | 346 | 36 | 0 |
| 2020-OpenSMTn | 0 | 229 | 15808.948 | 15784.67 | 229 | 0 | 229 | 7 | 346 | 39 | 0 |
| 2019-Par4n | 0 | 228 | 56154.147 | 21410.161 | 228 | 0 | 228 | 8 | 346 | 17 | 0 |
| cvc5 | 0 | 225 | 29926.492 | 29938.08 | 225 | 0 | 225 | 11 | 346 | 41 | 0 |
| Yices2 | 0 | 219 | 41399.204 | 41401.87 | 219 | 0 | 219 | 17 | 346 | 42 | 0 |
| z3n | 0 | 218 | 43891.269 | 43866.469 | 218 | 0 | 218 | 18 | 346 | 55 | 0 |
| veriT | 0 | 214 | 42857.645 | 42837.796 | 214 | 0 | 214 | 22 | 346 | 69 | 0 |
| SMTInterpol | 0 | 192 | 91147.956 | 87949.901 | 192 | 0 | 192 | 44 | 346 | 85 | 0 |
| MathSAT5n | 0 | 182 | 80299.6 | 80301.704 | 182 | 0 | 182 | 54 | 346 | 111 | 0 |
| mc2 | 0 | 78 | 27382.043 | 27325.08 | 78 | 0 | 78 | 158 | 346 | 7 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 424 | 4960.856 | 4925.278 | 424 | 276 | 148 | 158 | 158 | 0 |
| OpenSMT | 0 | 415 | 5715.293 | 5679.345 | 415 | 238 | 177 | 167 | 167 | 0 |
| 2020-OpenSMTn | 0 | 403 | 5989.61 | 5964.999 | 403 | 227 | 176 | 179 | 179 | 0 |
| 2019-Par4n | 0 | 402 | 10611.922 | 5947.62 | 402 | 246 | 156 | 180 | 180 | 0 |
| veriT | 0 | 352 | 6711.6 | 6690.108 | 352 | 209 | 143 | 230 | 230 | 0 |
| z3n | 0 | 339 | 6878.499 | 6866.761 | 339 | 210 | 129 | 243 | 243 | 0 |
| cvc5 | 0 | 337 | 7066.762 | 7034.204 | 337 | 211 | 126 | 245 | 245 | 0 |
| MathSAT5n | 0 | 334 | 6778.403 | 6778.814 | 334 | 207 | 127 | 248 | 248 | 0 |
| SMTInterpol | 0 | 284 | 10347.698 | 8514.985 | 284 | 187 | 97 | 298 | 298 | 0 |
| mc2 | 0 | 175 | 8963.543 | 8962.922 | 175 | 102 | 73 | 407 | 273 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.