The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_NonLinearRealArith division in the Single Query Track.
Page generated on 2022-08-10 11:17:45 +0000
Benchmarks: 2908 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | Z3++ | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3++-fixedn | 0 | 2641 | 379531.82 | 379433.129 | 2641 | 1340 | 1301 | 267 | 0 | 265 | 0 |
| 2019-Par4n | 0 | 2629 | 394912.029 | 356695.171 | 2629 | 1292 | 1337 | 279 | 0 | 221 | 58 |
| cvc5 | 0 | 2545 | 525901.735 | 526314.738 | 2545 | 1244 | 1301 | 363 | 0 | 363 | 0 |
| NRA-LS | 0 | 2488 | 550489.833 | 551413.565 | 2488 | 1198 | 1290 | 420 | 0 | 5 | 0 |
| Yices2 | 0 | 2341 | 702255.323 | 702324.97 | 2341 | 1150 | 1191 | 567 | 0 | 567 | 0 |
| z3-4.8.17n | 0 | 2275 | 666874.65 | 666955.286 | 2275 | 1229 | 1046 | 633 | 0 | 499 | 0 |
| SMT-RAT-MCSAT 22.06 | 0 | 2189 | 895361.649 | 895423.466 | 2189 | 1123 | 1066 | 719 | 0 | 674 | 21 |
| veriT+raSAT+Redlog | 0 | 1879 | 1206512.928 | 1206107.221 | 1879 | 905 | 974 | 1029 | 0 | 989 | 0 |
| MathSATn | 0 | 1544 | 1671561.013 | 1671677.835 | 1544 | 417 | 1127 | 1364 | 0 | 1364 | 0 |
| Z3++ | 6 | 2634 | 379866.348 | 379759.488 | 2634 | 1333 | 1301 | 274 | 0 | 264 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2650 | 412116.989 | 346590.821 | 2650 | 1310 | 1340 | 258 | 0 | 200 | 58 |
| Z3++-fixedn | 0 | 2641 | 379553.38 | 379423.299 | 2641 | 1340 | 1301 | 267 | 0 | 265 | 0 |
| cvc5 | 0 | 2545 | 526363.395 | 526298.488 | 2545 | 1244 | 1301 | 363 | 0 | 363 | 0 |
| NRA-LS | 0 | 2488 | 550607.043 | 551413.405 | 2488 | 1198 | 1290 | 420 | 0 | 5 | 0 |
| Yices2 | 0 | 2341 | 702330.553 | 702302.83 | 2341 | 1150 | 1191 | 567 | 0 | 567 | 0 |
| z3-4.8.17n | 0 | 2275 | 666962.06 | 666934.046 | 2275 | 1229 | 1046 | 633 | 0 | 499 | 0 |
| SMT-RAT-MCSAT 22.06 | 0 | 2189 | 895429.739 | 895399.226 | 2189 | 1123 | 1066 | 719 | 0 | 674 | 21 |
| veriT+raSAT+Redlog | 0 | 1879 | 1206582.328 | 1206082.811 | 1879 | 905 | 974 | 1029 | 0 | 989 | 0 |
| MathSATn | 0 | 1544 | 1671701.033 | 1671625.855 | 1544 | 417 | 1127 | 1364 | 0 | 1364 | 0 |
| Z3++ | 6 | 2634 | 379887.798 | 379749.928 | 2634 | 1333 | 1301 | 274 | 0 | 264 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Z3++-fixedn | 0 | 1340 | 138024.587 | 137945.426 | 1340 | 1340 | 0 | 90 | 1478 | 265 | 0 |
| Z3++ | 0 | 1333 | 139336.035 | 139236.716 | 1333 | 1333 | 0 | 97 | 1478 | 264 | 1 |
| 2019-Par4n | 0 | 1310 | 213683.539 | 169246.767 | 1310 | 1310 | 0 | 120 | 1478 | 200 | 58 |
| cvc5 | 0 | 1244 | 270666.703 | 270732.525 | 1244 | 1244 | 0 | 186 | 1478 | 363 | 0 |
| z3-4.8.17n | 0 | 1229 | 212691.942 | 212695.026 | 1229 | 1229 | 0 | 201 | 1478 | 499 | 0 |
| NRA-LS | 0 | 1198 | 306992.76 | 307433.823 | 1198 | 1198 | 0 | 232 | 1478 | 5 | 0 |
| Yices2 | 0 | 1150 | 343815.982 | 343799.517 | 1150 | 1150 | 0 | 280 | 1478 | 567 | 0 |
| SMT-RAT-MCSAT 22.06 | 0 | 1123 | 372615.186 | 372598.715 | 1123 | 1123 | 0 | 307 | 1478 | 674 | 21 |
| veriT+raSAT+Redlog | 0 | 905 | 598863.169 | 598592.935 | 905 | 905 | 0 | 525 | 1478 | 989 | 0 |
| MathSATn | 0 | 417 | 1228570.074 | 1228571.637 | 417 | 417 | 0 | 1013 | 1478 | 1364 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 1340 | 66433.45 | 45344.054 | 1340 | 0 | 1340 | 28 | 1540 | 200 | 58 |
| Z3++-fixedn | 0 | 1301 | 109996.301 | 109945.301 | 1301 | 0 | 1301 | 67 | 1540 | 265 | 0 |
| cvc5 | 0 | 1301 | 123696.692 | 123565.963 | 1301 | 0 | 1301 | 67 | 1540 | 363 | 0 |
| NRA-LS | 0 | 1290 | 114879.042 | 114971.712 | 1290 | 0 | 1290 | 78 | 1540 | 5 | 0 |
| Yices2 | 0 | 1191 | 226514.571 | 226503.313 | 1191 | 0 | 1191 | 177 | 1540 | 567 | 0 |
| MathSATn | 0 | 1127 | 311130.959 | 311054.219 | 1127 | 0 | 1127 | 241 | 1540 | 1364 | 0 |
| SMT-RAT-MCSAT 22.06 | 0 | 1066 | 393704.309 | 393689.791 | 1066 | 0 | 1066 | 302 | 1540 | 674 | 21 |
| z3-4.8.17n | 0 | 1046 | 329665.195 | 329633.389 | 1046 | 0 | 1046 | 322 | 1540 | 499 | 0 |
| veriT+raSAT+Redlog | 0 | 974 | 475719.159 | 475489.876 | 974 | 0 | 974 | 394 | 1540 | 989 | 0 |
| Z3++ | 6 | 1301 | 108760.907 | 108722.226 | 1301 | 0 | 1301 | 67 | 1540 | 264 | 1 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 2483 | 16782.933 | 12793.51 | 2483 | 1228 | 1255 | 425 | 0 | 367 | 58 |
| cvc5 | 0 | 2271 | 18421.749 | 18364.297 | 2271 | 1125 | 1146 | 637 | 0 | 637 | 0 |
| Z3++-fixedn | 0 | 2270 | 17686.372 | 17632.441 | 2270 | 1174 | 1096 | 638 | 0 | 638 | 0 |
| NRA-LS | 0 | 2258 | 19069.891 | 18991.231 | 2258 | 1084 | 1174 | 650 | 0 | 650 | 0 |
| Yices2 | 0 | 2239 | 17320.312 | 17289.707 | 2239 | 1117 | 1122 | 669 | 0 | 669 | 0 |
| z3-4.8.17n | 0 | 2215 | 19732.441 | 19693.745 | 2215 | 1200 | 1015 | 693 | 0 | 693 | 0 |
| SMT-RAT-MCSAT 22.06 | 0 | 1991 | 24874.127 | 24834.232 | 1991 | 1065 | 926 | 917 | 0 | 896 | 21 |
| veriT+raSAT+Redlog | 0 | 1799 | 26907.436 | 26854.311 | 1799 | 859 | 940 | 1109 | 0 | 1069 | 0 |
| MathSATn | 0 | 1388 | 39519.321 | 39474.876 | 1388 | 365 | 1023 | 1520 | 0 | 1520 | 0 |
| Z3++ | 6 | 2266 | 17647.393 | 17613.101 | 2266 | 1168 | 1098 | 642 | 0 | 635 | 1 |
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.