The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_NRA logic in the Single Query Track.
Page generated on 2021-07-18 17:29:06 +0000
Benchmarks: 2766 Time Limit: 1200 seconds Memory Limit: 60 GB
| 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 | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2481 | 399669.202 | 361574.005 | 2481 | 1164 | 1317 | 285 | 222 | 63 |
| cvc5 | 0 | 2424 | 457936.711 | 494015.508 | 2424 | 1135 | 1289 | 342 | 342 | 0 |
| Yices2 | 0 | 2207 | 706374.673 | 706393.693 | 2207 | 1033 | 1174 | 559 | 559 | 0 |
| z3n | 0 | 2141 | 711254.639 | 711998.222 | 2141 | 1089 | 1052 | 625 | 491 | 0 |
| SMT-RAT-MCSAT | 0 | 2002 | 940921.825 | 940887.411 | 2002 | 988 | 1014 | 764 | 728 | 13 |
| veriT+raSAT+Redlog | 0 | 1772 | 1213198.016 | 1213004.782 | 1772 | 816 | 956 | 994 | 994 | 0 |
| MathSAT5n | 0 | 1587 | 1449265.144 | 1449789.714 | 1587 | 465 | 1122 | 1179 | 1179 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2509 | 422005.372 | 346718.112 | 2509 | 1187 | 1322 | 257 | 194 | 63 |
| cvc5 | 0 | 2424 | 493909.782 | 493999.278 | 2424 | 1135 | 1289 | 342 | 342 | 0 |
| Yices2 | 0 | 2207 | 706438.053 | 706374.713 | 2207 | 1033 | 1174 | 559 | 559 | 0 |
| z3n | 0 | 2141 | 711686.449 | 711977.232 | 2141 | 1089 | 1052 | 625 | 491 | 0 |
| SMT-RAT-MCSAT | 0 | 2002 | 940988.825 | 940862.621 | 2002 | 988 | 1014 | 764 | 728 | 13 |
| veriT+raSAT+Redlog | 0 | 1772 | 1213262.826 | 1212982.462 | 1772 | 816 | 956 | 994 | 994 | 0 |
| MathSAT5n | 0 | 1587 | 1449868.014 | 1449737.364 | 1587 | 465 | 1122 | 1179 | 1179 | 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 | 1187 | 210403.901 | 159926.424 | 1187 | 1187 | 0 | 112 | 1467 | 194 | 63 |
| cvc5 | 0 | 1135 | 231251.989 | 231249.259 | 1135 | 1135 | 0 | 164 | 1467 | 342 | 0 |
| z3n | 0 | 1089 | 239100.604 | 239080.55 | 1089 | 1089 | 0 | 210 | 1467 | 491 | 0 |
| Yices2 | 0 | 1033 | 331488.834 | 331477.018 | 1033 | 1033 | 0 | 266 | 1467 | 559 | 0 |
| SMT-RAT-MCSAT | 0 | 988 | 372472.063 | 372388.666 | 988 | 988 | 0 | 311 | 1467 | 728 | 13 |
| veriT+raSAT+Redlog | 0 | 816 | 594180.479 | 594005.819 | 816 | 816 | 0 | 483 | 1467 | 994 | 0 |
| MathSAT5n | 0 | 465 | 1016302.714 | 1016229.61 | 465 | 465 | 0 | 834 | 1467 | 1179 | 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 | 1322 | 58001.471 | 33191.688 | 1322 | 0 | 1322 | 17 | 1427 | 194 | 63 |
| cvc5 | 0 | 1289 | 109057.793 | 109150.019 | 1289 | 0 | 1289 | 50 | 1427 | 342 | 0 |
| Yices2 | 0 | 1174 | 221349.219 | 221297.694 | 1174 | 0 | 1174 | 165 | 1427 | 559 | 0 |
| MathSAT5n | 0 | 1122 | 279965.3 | 279907.754 | 1122 | 0 | 1122 | 217 | 1427 | 1179 | 0 |
| z3n | 0 | 1052 | 324583.113 | 324893.284 | 1052 | 0 | 1052 | 287 | 1427 | 491 | 0 |
| SMT-RAT-MCSAT | 0 | 1014 | 415673.261 | 415630.351 | 1014 | 0 | 1014 | 325 | 1427 | 728 | 13 |
| veriT+raSAT+Redlog | 0 | 956 | 465482.346 | 465376.642 | 956 | 0 | 956 | 383 | 1427 | 994 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2346 | 17304.634 | 12642.772 | 2346 | 1112 | 1234 | 420 | 357 | 63 |
| cvc5 | 0 | 2199 | 16580.25 | 16556.889 | 2199 | 1048 | 1151 | 567 | 567 | 0 |
| Yices2 | 0 | 2060 | 18191.296 | 18166.571 | 2060 | 982 | 1078 | 706 | 706 | 0 |
| z3n | 0 | 2048 | 21152.217 | 21090.43 | 2048 | 1050 | 998 | 718 | 709 | 0 |
| SMT-RAT-MCSAT | 0 | 1823 | 25484.508 | 25422.957 | 1823 | 946 | 877 | 943 | 930 | 13 |
| veriT+raSAT+Redlog | 0 | 1710 | 26415.128 | 26370.697 | 1710 | 779 | 931 | 1056 | 1056 | 0 |
| MathSAT5n | 0 | 1425 | 35121.409 | 35084.276 | 1425 | 407 | 1018 | 1341 | 1341 | 0 |
n Non-competing.
N/A: Benchmarks not known to be SAT/UNSAT, respectively.