The International Satisfiability Modulo Theories (SMT) Competition.
Competition results for the Equality+NonLinearArith (AUFDTNIRA, UFDTNIA, UFDTNIRA, AUFNIA, AUFNIRA, UFNIA) division in the Single Query Track.
Page generated on 2020-01-29 22:04:58 +0000
Benchmarks: 6376 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 |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 3716 | 3013136.001 | 3087261.738 | 3716 | 571 | 3145 | 2660 | 2472 | 0 |
| 2019-Par4n | 0 | 3099 | 5534932.089 | 2901244.368 | 3099 | 596 | 2503 | 2237 | 2235 | 2 |
| Vampire | 0 | 2828 | 9175583.367 | 8691884.056 | 2828 | 0 | 2828 | 3548 | 3548 | 0 |
| z3n | 0 | 2243 | 2468102.346 | 2471904.052 | 2243 | 514 | 1729 | 3096 | 1713 | 8 |
| Alt-Ergo | 0 | 1727 | 7299972.858 | 6687087.274 | 1727 | 0 | 1727 | 4649 | 2625 | 145 |
| 2018-Vampiren | 0 | 1660 | 8585229.707 | 8224243.678 | 1660 | 0 | 1660 | 3376 | 3376 | 0 |
| UltimateEliminator+MathSAT | 0 | 651 | 541479.635 | 530296.379 | 651 | 508 | 143 | 5725 | 319 | 0 |
| 2019-Vampiren | 0 | 1 | 0.116 | 0.116 | 1 | 0 | 1 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 3716 | 3013136.001 | 3087261.738 | 3716 | 571 | 3145 | 2660 | 2472 | 0 |
| Vampire | 0 | 3184 | 16878254.997 | 4290199.709 | 3184 | 0 | 3184 | 3192 | 3192 | 0 |
| 2019-Par4n | 0 | 3099 | 5538592.989 | 2801649.588 | 3099 | 596 | 2503 | 2237 | 2235 | 2 |
| z3n | 0 | 2243 | 2468102.346 | 2471904.052 | 2243 | 514 | 1729 | 3096 | 1713 | 8 |
| Alt-Ergo | 0 | 1750 | 12070500.898 | 3751632.117 | 1750 | 0 | 1750 | 4626 | 2567 | 145 |
| UltimateEliminator+MathSAT | 0 | 651 | 717842.865 | 400703.649 | 651 | 508 | 143 | 5725 | 319 | 0 |
| 2019-Vampiren | 0 | 1 | 0.116 | 0.116 | 1 | 0 | 1 | 0 | 0 | 0 |
| 2018-Vampiren | 1 | 2555 | 15096437.337 | 3799086.155 | 2555 | 0 | 2555 | 2481 | 2480 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2019-Par4n | 0 | 596 | 50733.722 | 25643.787 | 596 | 596 | 0 | 4740 | 2235 | 2 |
| CVC4 | 0 | 571 | 47112.485 | 47248.312 | 571 | 571 | 0 | 5805 | 2472 | 0 |
| z3n | 0 | 514 | 93120.682 | 93110.303 | 514 | 514 | 0 | 4825 | 1713 | 8 |
| UltimateEliminator+MathSAT | 0 | 508 | 38411.034 | 37654.36 | 508 | 508 | 0 | 5868 | 319 | 0 |
| 2019-Vampiren | 0 | 0 | 0.0 | 0.0 | 0 | 0 | 0 | 1 | 0 | 0 |
| Alt-Ergo | 0 | 0 | 245674.923 | 125349.054 | 0 | 0 | 0 | 6376 | 2567 | 145 |
| Vampire | 0 | 0 | 2865775.28 | 727196.48 | 0 | 0 | 0 | 6376 | 3192 | 0 |
| 2018-Vampiren | 1 | 41 | 2838745.43 | 714395.195 | 41 | 0 | 41 | 4995 | 2480 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 3185 | 1293704.4 | 1356798.491 | 3185 | 40 | 3145 | 3191 | 2472 | 0 |
| Vampire | 0 | 3184 | 7378805.247 | 1881793.439 | 3184 | 0 | 3184 | 3192 | 3192 | 0 |
| 2018-Vampiren | 0 | 2555 | 6736409.527 | 1695754.205 | 2555 | 0 | 2555 | 2481 | 2480 | 0 |
| 2019-Par4n | 0 | 2544 | 2104213.489 | 1067137.125 | 2544 | 41 | 2503 | 2792 | 2235 | 2 |
| z3n | 0 | 1766 | 1190027.041 | 1190934.513 | 1766 | 37 | 1729 | 3573 | 1713 | 8 |
| Alt-Ergo | 0 | 1750 | 7596955.183 | 2469491.989 | 1750 | 0 | 1750 | 4626 | 2567 | 145 |
| UltimateEliminator+MathSAT | 0 | 180 | 637428.9 | 322190.183 | 180 | 37 | 143 | 6196 | 319 | 0 |
| 2019-Vampiren | 0 | 1 | 0.116 | 0.116 | 1 | 0 | 1 | 0 | 0 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| CVC4 | 0 | 3180 | 76249.076 | 76220.539 | 3180 | 513 | 2667 | 3196 | 3071 | 0 |
| 2019-Par4n | 0 | 2619 | 70273.99 | 67986.356 | 2619 | 555 | 2064 | 2717 | 2715 | 2 |
| z3n | 0 | 2134 | 72362.771 | 72295.641 | 2134 | 491 | 1643 | 3205 | 2810 | 8 |
| Vampire | 0 | 1685 | 124560.602 | 116311.321 | 1685 | 0 | 1685 | 4691 | 4691 | 0 |
| Alt-Ergo | 0 | 1575 | 91350.738 | 85975.894 | 1575 | 0 | 1575 | 4801 | 3343 | 145 |
| 2018-Vampiren | 0 | 1185 | 98863.665 | 94174.303 | 1185 | 0 | 1185 | 3851 | 3851 | 0 |
| UltimateEliminator+MathSAT | 0 | 650 | 29019.755 | 22497.86 | 650 | 507 | 143 | 5726 | 334 | 0 |
| 2019-Vampiren | 0 | 1 | 0.116 | 0.116 | 1 | 0 | 1 | 0 | 0 | 0 |
n Non-competing.