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 2023-07-06 16:04:54 +0000
Benchmarks: 478 Time Limit: 1200 seconds Memory Limit: 60 GB
Logics:| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| cvc5 | cvc5 | Yices2 | cvc5 | cvc5 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 374 | 12927.277 | 12909.548 | 374 | 273 | 101 | 104 | 0 | 104 | 0 |
| Yices2 | 0 | 370 | 8857.964 | 8812.164 | 370 | 288 | 82 | 108 | 0 | 108 | 0 |
| 2020-CVC4n | 0 | 354 | 9204.836 | 9206.092 | 354 | 263 | 91 | 124 | 0 | 99 | 0 |
| SMTInterpol | 0 | 179 | 2593.099 | 1600.994 | 179 | 142 | 37 | 299 | 0 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 374 | 12927.277 | 12909.548 | 374 | 273 | 101 | 104 | 0 | 104 | 0 |
| Yices2 | 0 | 370 | 8857.964 | 8812.164 | 370 | 288 | 82 | 108 | 0 | 108 | 0 |
| 2020-CVC4n | 0 | 354 | 9204.836 | 9206.092 | 354 | 263 | 91 | 124 | 0 | 99 | 0 |
| SMTInterpol | 0 | 179 | 2593.099 | 1600.994 | 179 | 142 | 37 | 299 | 0 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Yices2 | 0 | 288 | 8578.381 | 8579.502 | 288 | 288 | 0 | 24 | 166 | 108 | 0 |
| cvc5 | 0 | 273 | 10314.682 | 10305.245 | 273 | 273 | 0 | 39 | 166 | 104 | 0 |
| 2020-CVC4n | 0 | 263 | 6548.232 | 6549.118 | 263 | 263 | 0 | 49 | 166 | 99 | 0 |
| SMTInterpol | 0 | 142 | 1555.28 | 842.7 | 142 | 142 | 0 | 170 | 166 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 101 | 2612.595 | 2604.304 | 101 | 0 | 101 | 30 | 347 | 104 | 0 |
| 2020-CVC4n | 0 | 91 | 2656.604 | 2656.973 | 91 | 0 | 91 | 40 | 347 | 99 | 0 |
| Yices2 | 0 | 82 | 279.583 | 232.662 | 82 | 0 | 82 | 49 | 347 | 108 | 0 |
| SMTInterpol | 0 | 37 | 1037.82 | 758.293 | 37 | 0 | 37 | 94 | 347 | 10 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| cvc5 | 0 | 325 | 775.274 | 755.626 | 325 | 233 | 92 | 153 | 0 | 153 | 0 |
| 2020-CVC4n | 0 | 307 | 420.028 | 419.992 | 307 | 227 | 80 | 171 | 0 | 149 | 0 |
| Yices2 | 0 | 302 | 317.341 | 317.487 | 302 | 225 | 77 | 176 | 0 | 176 | 0 |
| SMTInterpol | 0 | 162 | 772.224 | 325.536 | 162 | 130 | 32 | 316 | 0 | 28 | 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.