The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the QF_UFIDL division in the Single Query Track.
Page generated on 2020-07-04 11:46:59 +0000
Benchmarks: 300 Time Limit: 1200 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Yices2 | Yices2 | Yices2 | Yices2 | Yices2 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 298 | 3107.252 | 3106.588 | 298 | 73 | 225 | 2 | 2 | 0 | |
| Yices2-fixedn | 0 | 298 | 3122.561 | 3123.247 | 298 | 73 | 225 | 2 | 2 | 0 | |
| Yices2 | 0 | 298 | 3125.209 | 3125.736 | 298 | 73 | 225 | 2 | 2 | 0 | |
| z3n | 0 | 298 | 4189.782 | 4185.917 | 298 | 73 | 225 | 2 | 2 | 0 | |
| SMTInterpol-fixedn | 0 | 284 | 31141.602 | 29274.155 | 284 | 73 | 211 | 16 | 16 | 0 | |
| SMTInterpol | 0 | 284 | 31185.149 | 29161.75 | 284 | 73 | 211 | 16 | 16 | 0 | |
| MathSAT5n | 0 | 283 | 27266.965 | 27250.609 | 283 | 73 | 210 | 17 | 17 | 0 | |
| veriT | 0 | 275 | 32446.764 | 32451.847 | 275 | 73 | 202 | 25 | 21 | 0 | |
| CVC4 | 0 | 270 | 50143.226 | 50117.145 | 270 | 73 | 197 | 30 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 298 | 3107.392 | 3106.528 | 298 | 73 | 225 | 2 | 2 | 0 | |
| Yices2-fixedn | 0 | 298 | 3122.661 | 3123.147 | 298 | 73 | 225 | 2 | 2 | 0 | |
| Yices2 | 0 | 298 | 3125.409 | 3125.686 | 298 | 73 | 225 | 2 | 2 | 0 | |
| z3n | 0 | 298 | 4189.852 | 4185.847 | 298 | 73 | 225 | 2 | 2 | 0 | |
| SMTInterpol | 0 | 284 | 31185.149 | 29161.75 | 284 | 73 | 211 | 16 | 16 | 0 | |
| SMTInterpol-fixedn | 0 | 284 | 31141.602 | 29274.155 | 284 | 73 | 211 | 16 | 16 | 0 | |
| MathSAT5n | 0 | 283 | 27269.975 | 27249.679 | 283 | 73 | 210 | 17 | 17 | 0 | |
| veriT | 0 | 275 | 32449.884 | 32450.977 | 275 | 73 | 202 | 25 | 21 | 0 | |
| CVC4 | 0 | 270 | 50147.566 | 50115.955 | 270 | 73 | 197 | 30 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 73 | 3.783 | 3.984 | 73 | 73 | 0 | 227 | 2 | 0 |
| Yices2 | 0 | 73 | 4.427 | 4.556 | 73 | 73 | 0 | 227 | 2 | 0 |
| Yices2-fixedn | 0 | 73 | 4.464 | 4.744 | 73 | 73 | 0 | 227 | 2 | 0 |
| veriT | 0 | 73 | 11.5 | 11.487 | 73 | 73 | 0 | 227 | 21 | 0 |
| MathSAT5n | 0 | 73 | 29.795 | 29.801 | 73 | 73 | 0 | 227 | 17 | 0 |
| z3n | 0 | 73 | 106.461 | 102.176 | 73 | 73 | 0 | 227 | 2 | 0 |
| SMTInterpol | 0 | 73 | 306.005 | 106.869 | 73 | 73 | 0 | 227 | 16 | 0 |
| SMTInterpol-fixedn | 0 | 73 | 312.403 | 110.327 | 73 | 73 | 0 | 227 | 16 | 0 |
| CVC4 | 0 | 73 | 752.308 | 752.342 | 73 | 73 | 0 | 227 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 225 | 3103.609 | 3102.544 | 225 | 0 | 225 | 75 | 2 | 0 |
| Yices2-fixedn | 0 | 225 | 3118.197 | 3118.403 | 225 | 0 | 225 | 75 | 2 | 0 |
| Yices2 | 0 | 225 | 3120.981 | 3121.129 | 225 | 0 | 225 | 75 | 2 | 0 |
| z3n | 0 | 225 | 4083.391 | 4083.672 | 225 | 0 | 225 | 75 | 2 | 0 |
| SMTInterpol | 0 | 211 | 30879.143 | 29054.881 | 211 | 0 | 211 | 89 | 16 | 0 |
| SMTInterpol-fixedn | 0 | 211 | 30829.199 | 29163.828 | 211 | 0 | 211 | 89 | 16 | 0 |
| MathSAT5n | 0 | 210 | 27240.18 | 27219.878 | 210 | 0 | 210 | 90 | 17 | 0 |
| veriT | 0 | 202 | 32438.384 | 32439.49 | 202 | 0 | 202 | 98 | 21 | 0 |
| CVC4 | 0 | 197 | 49395.257 | 49363.613 | 197 | 0 | 197 | 103 | 30 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Yices 2.6.2n | 0 | 293 | 336.242 | 335.345 | 293 | 73 | 220 | 7 | 7 | 0 | |
| Yices2 | 0 | 293 | 343.059 | 343.314 | 293 | 73 | 220 | 7 | 7 | 0 | |
| Yices2-fixedn | 0 | 293 | 343.011 | 343.435 | 293 | 73 | 220 | 7 | 7 | 0 | |
| z3n | 0 | 290 | 596.367 | 592.123 | 290 | 73 | 217 | 10 | 10 | 0 | |
| SMTInterpol | 0 | 258 | 3488.77 | 1982.211 | 258 | 73 | 185 | 42 | 42 | 0 | |
| SMTInterpol-fixedn | 0 | 258 | 3390.075 | 1989.102 | 258 | 73 | 185 | 42 | 42 | 0 | |
| veriT | 0 | 256 | 1383.431 | 1383.416 | 256 | 73 | 183 | 44 | 44 | 0 | |
| MathSAT5n | 0 | 256 | 1742.391 | 1720.819 | 256 | 73 | 183 | 44 | 44 | 0 | |
| CVC4 | 0 | 205 | 2800.046 | 2798.523 | 205 | 72 | 133 | 95 | 95 | 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.