The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the Arith (LRA, LIA, NIA, NRA) division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 1212 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1084 | 140408.359 | 140404.258 | 1084 | 432 | 652 | 128 | 87 | 0 |
| CVC4 | 0 | 1012 | 258209.202 | 259372.984 | 1012 | 402 | 610 | 200 | 195 | 0 |
| 2019-Z3n | 0 | 975 | 185468.901 | 185482.975 | 975 | 422 | 553 | 127 | 127 | 0 |
| 2019-Par4n | 0 | 845 | 149406.065 | 74818.614 | 845 | 313 | 532 | 50 | 50 | 0 |
| UltimateEliminator+MathSAT | 0 | 627 | 459268.949 | 437317.465 | 627 | 235 | 392 | 585 | 341 | 0 |
| SMTInterpol-fixedn | 0 | 213 | 95597.407 | 91451.116 | 213 | 16 | 197 | 889 | 65 | 0 |
| SMTInterpol | 0 | 213 | 95601.616 | 91447.967 | 213 | 16 | 197 | 889 | 65 | 0 |
| veriT | 0 | 45 | 170553.838 | 170089.592 | 45 | 0 | 45 | 255 | 105 | 0 |
| veriT+viten | 0 | 42 | 220797.256 | 220816.258 | 42 | 0 | 42 | 258 | 168 | 8 |
| 2018-Z3n | 0 | 16 | 391.879 | 391.914 | 16 | 12 | 4 | 1 | 0 | 0 |
| Vampire | 4 | 462 | 1857869.414 | 1809918.953 | 462 | 1 | 461 | 750 | 746 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 1084 | 140408.359 | 140404.258 | 1084 | 432 | 652 | 128 | 87 | 0 |
| CVC4 | 0 | 1012 | 258209.202 | 259372.984 | 1012 | 402 | 610 | 200 | 195 | 0 |
| 2019-Z3n | 0 | 975 | 185468.901 | 185482.975 | 975 | 422 | 553 | 127 | 127 | 0 |
| 2019-Par4n | 0 | 845 | 149406.065 | 74818.614 | 845 | 313 | 532 | 50 | 50 | 0 |
| UltimateEliminator+MathSAT | 0 | 627 | 476015.379 | 422918.195 | 627 | 235 | 392 | 585 | 341 | 0 |
| SMTInterpol | 0 | 213 | 95601.616 | 91447.967 | 213 | 16 | 197 | 889 | 65 | 0 |
| SMTInterpol-fixedn | 0 | 213 | 95597.407 | 91451.116 | 213 | 16 | 197 | 889 | 65 | 0 |
| veriT | 0 | 45 | 170553.838 | 170089.592 | 45 | 0 | 45 | 255 | 105 | 0 |
| veriT+viten | 0 | 42 | 220797.256 | 220816.258 | 42 | 0 | 42 | 258 | 168 | 8 |
| 2018-Z3n | 0 | 16 | 391.879 | 391.914 | 16 | 12 | 4 | 1 | 0 | 0 |
| Vampire | 6 | 467 | 3553095.344 | 913781.74 | 467 | 1 | 466 | 745 | 739 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 432 | 34334.404 | 34330.385 | 432 | 432 | 0 | 780 | 87 | 0 |
| 2019-Z3n | 0 | 422 | 34868.459 | 34872.138 | 422 | 422 | 0 | 680 | 127 | 0 |
| CVC4 | 0 | 402 | 77022.884 | 77488.05 | 402 | 402 | 0 | 810 | 195 | 0 |
| 2019-Par4n | 0 | 313 | 32806.068 | 16444.541 | 313 | 313 | 0 | 582 | 50 | 0 |
| UltimateEliminator+MathSAT | 0 | 235 | 220968.974 | 183120.373 | 235 | 235 | 0 | 977 | 341 | 0 |
| SMTInterpol | 0 | 16 | 74646.443 | 71817.352 | 16 | 16 | 0 | 1086 | 65 | 0 |
| SMTInterpol-fixedn | 0 | 16 | 74691.9 | 71830.072 | 16 | 16 | 0 | 1086 | 65 | 0 |
| 2018-Z3n | 0 | 12 | 0.673 | 0.674 | 12 | 12 | 0 | 5 | 0 | 0 |
| veriT | 0 | 0 | 105667.331 | 105449.594 | 0 | 0 | 0 | 300 | 105 | 0 |
| veriT+viten | 0 | 0 | 117603.473 | 117611.953 | 0 | 0 | 0 | 300 | 168 | 8 |
| Vampire | 6 | 2 | 2122164.513 | 543661.731 | 2 | 1 | 1 | 1210 | 739 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 653 | 86875.245 | 86873.045 | 653 | 1 | 652 | 559 | 87 | 0 |
| CVC4 | 0 | 610 | 163217.207 | 163884.363 | 610 | 0 | 610 | 602 | 195 | 0 |
| 2019-Z3n | 0 | 553 | 132601.822 | 132609.977 | 553 | 0 | 553 | 549 | 127 | 0 |
| 2019-Par4n | 0 | 532 | 87826.437 | 43973.093 | 532 | 0 | 532 | 363 | 50 | 0 |
| Vampire | 0 | 466 | 1360323.521 | 351971.209 | 466 | 0 | 466 | 746 | 739 | 0 |
| UltimateEliminator+MathSAT | 0 | 392 | 240196.61 | 225389.996 | 392 | 0 | 392 | 820 | 341 | 0 |
| SMTInterpol-fixedn | 0 | 197 | 20863.892 | 19606.651 | 197 | 0 | 197 | 905 | 65 | 0 |
| SMTInterpol | 0 | 197 | 20917.871 | 19616.141 | 197 | 0 | 197 | 905 | 65 | 0 |
| veriT | 0 | 45 | 62838.431 | 62591.444 | 45 | 0 | 45 | 255 | 105 | 0 |
| veriT+viten | 0 | 42 | 99594.463 | 99604.242 | 42 | 0 | 42 | 258 | 168 | 8 |
| 2018-Z3n | 0 | 4 | 391.206 | 391.24 | 4 | 0 | 4 | 13 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| z3n | 0 | 979 | 6019.48 | 6002.699 | 979 | 405 | 574 | 233 | 195 | 0 |
| CVC4 | 0 | 946 | 6588.61 | 6588.401 | 946 | 373 | 573 | 266 | 264 | 0 |
| 2019-Z3n | 0 | 872 | 6896.161 | 6889.1 | 872 | 394 | 478 | 230 | 230 | 0 |
| 2019-Par4n | 0 | 778 | 4147.175 | 3522.815 | 778 | 290 | 488 | 117 | 117 | 0 |
| UltimateEliminator+MathSAT | 0 | 577 | 13550.495 | 11942.763 | 577 | 224 | 353 | 635 | 397 | 0 |
| Vampire | 0 | 347 | 21638.189 | 21058.735 | 347 | 1 | 346 | 865 | 865 | 0 |
| SMTInterpol-fixedn | 0 | 213 | 4724.396 | 3441.129 | 213 | 16 | 197 | 889 | 101 | 0 |
| SMTInterpol | 0 | 213 | 4734.598 | 3446.287 | 213 | 16 | 197 | 889 | 101 | 0 |
| veriT | 0 | 43 | 4278.429 | 4278.227 | 43 | 0 | 43 | 257 | 178 | 0 |
| veriT+viten | 0 | 42 | 4232.396 | 4232.568 | 42 | 0 | 42 | 258 | 168 | 8 |
| 2018-Z3n | 0 | 16 | 25.433 | 25.434 | 16 | 12 | 4 | 1 | 1 | 0 |
n Non-competing.