The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the FPArith (BVFP, FP, BVFPLRA, FPLRA) division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 1422 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| CVC4 | CVC4 | CVC4 | CVC4 | CVC4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 994 | 289976.665 | 289960.674 | 994 | 194 | 800 | 216 | 148 | 31 |
| CVC4 | 0 | 900 | 383937.209 | 384009.537 | 900 | 225 | 675 | 522 | 311 | 0 |
| z3n | 0 | 806 | 224884.475 | 224889.586 | 806 | 24 | 782 | 180 | 163 | 0 |
| UltimateEliminator+MathSAT | 0 | 179 | 6600.698 | 4544.681 | 179 | 34 | 145 | 1243 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 994 | 289976.665 | 289960.674 | 994 | 194 | 800 | 216 | 148 | 31 |
| CVC4 | 0 | 900 | 383937.209 | 384009.537 | 900 | 225 | 675 | 522 | 311 | 0 |
| z3n | 0 | 806 | 224884.475 | 224889.586 | 806 | 24 | 782 | 180 | 163 | 0 |
| UltimateEliminator+MathSAT | 0 | 179 | 6600.698 | 4544.681 | 179 | 34 | 145 | 1243 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 225 | 56206.882 | 56214.603 | 225 | 225 | 0 | 1197 | 311 | 0 |
| 2019-Z3n | 0 | 194 | 23865.882 | 23869.13 | 194 | 194 | 0 | 1016 | 148 | 31 |
| UltimateEliminator+MathSAT | 0 | 34 | 1118.363 | 763.841 | 34 | 34 | 0 | 1388 | 1 | 0 |
| z3n | 0 | 24 | 2180.377 | 2180.528 | 24 | 24 | 0 | 962 | 163 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 800 | 86936.605 | 86950.925 | 800 | 0 | 800 | 410 | 148 | 31 |
| z3n | 0 | 782 | 91771.227 | 91751.248 | 782 | 0 | 782 | 204 | 163 | 0 |
| CVC4 | 0 | 675 | 109319.42 | 109335.703 | 675 | 0 | 675 | 747 | 311 | 0 |
| UltimateEliminator+MathSAT | 0 | 145 | 2923.163 | 2031.258 | 145 | 0 | 145 | 1277 | 1 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Z3n | 0 | 843 | 10008.261 | 10005.422 | 843 | 164 | 679 | 367 | 305 | 31 |
| CVC4 | 0 | 831 | 10309.155 | 10303.754 | 831 | 223 | 608 | 591 | 380 | 0 |
| z3n | 0 | 699 | 7794.006 | 7783.352 | 699 | 21 | 678 | 287 | 272 | 0 |
| UltimateEliminator+MathSAT | 0 | 179 | 4859.918 | 3368.631 | 179 | 34 | 145 | 1243 | 1 | 0 |
n Non-competing.