The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_Equality+NonLinearArith division in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 430 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | cvc5 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 397 | 27325.596 | 27310.074 | 397 | 310 | 87 | 33 | 0 | 21 | 0 |
| z3n | 0 | 377 | 66133.207 | 66138.967 | 377 | 286 | 91 | 53 | 0 | 53 | 0 |
| 2019-CVC4n | 0 | 372 | 14033.518 | 14037.025 | 372 | 297 | 75 | 22 | 36 | 11 | 0 |
| cvc5 - fixedn | 0 | 368 | 44715.64 | 44714.752 | 368 | 286 | 82 | 62 | 0 | 35 | 0 |
| cvc5 | 0 | 368 | 44726.468 | 44721.783 | 368 | 286 | 82 | 62 | 0 | 35 | 0 |
| MathSAT5n | 0 | 343 | 61301.069 | 61285.981 | 343 | 274 | 69 | 87 | 0 | 49 | 0 |
| Yices2 | 0 | 305 | 33223.218 | 33228.997 | 305 | 241 | 64 | 22 | 103 | 22 | 0 |
| 2019-Par4n | 0 | 23 | 5785.319 | 5295.525 | 23 | 21 | 2 | 4 | 403 | 4 | 0 |
| 2019-MathSAT-defaultn | 0 | 9 | 3.687 | 3.69 | 9 | 2 | 7 | 0 | 421 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 31196.858 | 31200.841 | 1 | 1 | 0 | 26 | 403 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 397 | 27329.826 | 27309.194 | 397 | 310 | 87 | 33 | 0 | 21 | 0 |
| z3n | 0 | 377 | 66145.427 | 66136.717 | 377 | 286 | 91 | 53 | 0 | 53 | 0 |
| 2019-CVC4n | 0 | 372 | 14036.438 | 14036.595 | 372 | 297 | 75 | 22 | 36 | 11 | 0 |
| cvc5 - fixedn | 0 | 368 | 44719.78 | 44713.232 | 368 | 286 | 82 | 62 | 0 | 35 | 0 |
| cvc5 | 0 | 368 | 44732.058 | 44720.283 | 368 | 286 | 82 | 62 | 0 | 35 | 0 |
| MathSAT5n | 0 | 343 | 61308.209 | 61284.111 | 343 | 274 | 69 | 87 | 0 | 49 | 0 |
| Yices2 | 0 | 305 | 33226.948 | 33228.107 | 305 | 241 | 64 | 22 | 103 | 22 | 0 |
| 2019-Par4n | 0 | 25 | 6813.049 | 4609.66 | 25 | 23 | 2 | 2 | 403 | 2 | 0 |
| 2019-MathSAT-defaultn | 0 | 9 | 3.687 | 3.69 | 9 | 2 | 7 | 0 | 421 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 31200.008 | 31200.011 | 1 | 1 | 0 | 26 | 403 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 310 | 23282.214 | 23261.472 | 310 | 310 | 0 | 23 | 97 | 21 | 0 |
| 2019-CVC4n | 0 | 297 | 10317.308 | 10317.482 | 297 | 297 | 0 | 10 | 123 | 11 | 0 |
| cvc5 - fixedn | 0 | 286 | 40630.807 | 40624.271 | 286 | 286 | 0 | 47 | 97 | 35 | 0 |
| cvc5 | 0 | 286 | 40643.694 | 40631.802 | 286 | 286 | 0 | 47 | 97 | 35 | 0 |
| z3n | 0 | 286 | 58871.474 | 58862.737 | 286 | 286 | 0 | 47 | 97 | 53 | 0 |
| MathSAT5n | 0 | 274 | 39444.648 | 39420.177 | 274 | 274 | 0 | 59 | 97 | 49 | 0 |
| Yices2 | 0 | 241 | 11617.118 | 11618.087 | 241 | 241 | 0 | 4 | 185 | 22 | 0 |
| 2019-Par4n | 0 | 23 | 5613.036 | 3409.296 | 23 | 23 | 0 | 1 | 406 | 2 | 0 |
| 2019-MathSAT-defaultn | 0 | 2 | 0.441 | 0.442 | 2 | 2 | 0 | 0 | 428 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 27600.008 | 27600.011 | 1 | 1 | 0 | 23 | 406 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 91 | 2473.952 | 2473.98 | 91 | 0 | 91 | 2 | 337 | 53 | 0 |
| 2020-CVC4n | 0 | 87 | 2799.741 | 2799.844 | 87 | 0 | 87 | 6 | 337 | 21 | 0 |
| cvc5 | 0 | 82 | 2887.804 | 2887.922 | 82 | 0 | 82 | 11 | 337 | 35 | 0 |
| cvc5 - fixedn | 0 | 82 | 2888.355 | 2888.342 | 82 | 0 | 82 | 11 | 337 | 35 | 0 |
| 2019-CVC4n | 0 | 75 | 3707.75 | 3707.734 | 75 | 0 | 75 | 9 | 346 | 11 | 0 |
| MathSAT5n | 0 | 69 | 17063.561 | 17063.934 | 69 | 0 | 69 | 24 | 337 | 49 | 0 |
| Yices2 | 0 | 64 | 16809.83 | 16810.021 | 64 | 0 | 64 | 14 | 352 | 22 | 0 |
| 2019-MathSAT-defaultn | 0 | 7 | 3.246 | 3.249 | 7 | 0 | 7 | 0 | 423 | 0 | 0 |
| 2019-Par4n | 0 | 2 | 0.013 | 0.364 | 2 | 0 | 2 | 0 | 428 | 2 | 0 |
| veriT+raSAT+Redlog | 0 | 0 | 2400.0 | 2400.0 | 0 | 0 | 0 | 2 | 428 | 26 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2020-CVC4n | 0 | 381 | 1164.874 | 1143.801 | 381 | 298 | 83 | 49 | 0 | 38 | 0 |
| z3n | 0 | 369 | 1722.104 | 1713.058 | 369 | 279 | 90 | 61 | 0 | 61 | 0 |
| 2019-CVC4n | 0 | 364 | 612.777 | 612.697 | 364 | 292 | 72 | 30 | 36 | 19 | 0 |
| cvc5 - fixedn | 0 | 354 | 1390.8 | 1383.579 | 354 | 278 | 76 | 76 | 0 | 49 | 0 |
| cvc5 | 0 | 354 | 1396.295 | 1383.704 | 354 | 278 | 76 | 76 | 0 | 49 | 0 |
| MathSAT5n | 0 | 335 | 1632.647 | 1632.79 | 335 | 270 | 65 | 95 | 0 | 57 | 0 |
| Yices2 | 0 | 285 | 1046.612 | 1047.164 | 285 | 221 | 64 | 42 | 103 | 42 | 0 |
| 2019-Par4n | 0 | 18 | 440.449 | 330.655 | 18 | 16 | 2 | 9 | 403 | 9 | 0 |
| 2019-MathSAT-defaultn | 0 | 9 | 3.687 | 3.69 | 9 | 2 | 7 | 0 | 421 | 0 | 0 |
| veriT+raSAT+Redlog | 0 | 1 | 624.008 | 624.011 | 1 | 1 | 0 | 26 | 403 | 26 | 0 |
n Non-competing.
Abstained: Total of benchmarks in logics in this division that solver chose to abstain from. For SAT/UNSAT scores, this column also includes benchmarks not known to be SAT/UNSAT.