The International Satisfiability Modulo Theories (SMT) Competition.
Home
Introduction
Benchmark Submission
Publications
SMT-LIB
Previous Editions
Competition results for the UFNIA division in the Single Query Track.
Page generated on 2019-07-23 17:56:09 +0000
Benchmarks: 5993 Time Limit: 2400 seconds Memory Limit: 60 GB
| Sequential Performance | Parallel Performance | SAT Performance (parallel) | UNSAT Performance (parallel) | 24s Performance (parallel) |
|---|---|---|---|---|
| Par4 | Par4 | Par4 | Par4 | Par4 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 3506 | 6230692.435 | 6103765.261 | 3506 | 455 | 3051 | 2487 | 2477 | 10 | |
| CVC4-SymBreakn | 0 | 3325 | 6613445.664 | 6891006.83 | 3325 | 453 | 2872 | 2668 | 2666 | 0 | |
| CVC4 | 0 | 3316 | 6542541.597 | 6844099.983 | 3316 | 455 | 2861 | 2677 | 2674 | 0 | |
| Z3n | 0 | 2496 | 6527302.798 | 6532235.778 | 2496 | 355 | 2141 | 3497 | 2466 | 12 | |
| 2018-Z3n | 0 | 2462 | 6566706.847 | 6571648.333 | 2462 | 347 | 2115 | 3531 | 2481 | 7 | |
| Vampire | 0 | 2352 | 9372892.581 | 8901045.119 | 2352 | 0 | 2352 | 3641 | 3641 | 0 | |
| 2018-Vampiren | 0 | 2137 | 9910677.307 | 9422860.859 | 2137 | 0 | 2137 | 3856 | 3856 | 0 | |
| Alt-Ergo | 0 | 1001 | 8314962.019 | 7558228.524 | 1001 | 0 | 1001 | 4992 | 2794 | 177 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 20 | 589384.757 | 583032.793 | 20 | 0 | 20 | 5973 | 236 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 550604.062 | 606084.406 | 0 | 0 | 0 | 5993 | 245 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Vampiren | 0 | 3774 | 16115465.297 | 7407890.407 | 3774 | 0 | 3774 | 2219 | 2219 | 0 | |
| Par4 | 0 | 3513 | 6234500.095 | 6097428.771 | 3513 | 455 | 3058 | 2480 | 2470 | 10 | |
| CVC4-SymBreakn | 0 | 3325 | 6857534.154 | 6890865.67 | 3325 | 453 | 2872 | 2668 | 2666 | 0 | |
| CVC4 | 0 | 3316 | 6828611.544 | 6843968.593 | 3316 | 455 | 2861 | 2677 | 2675 | 0 | |
| Vampire | 0 | 2510 | 10614412.931 | 8762318.366 | 2510 | 0 | 2510 | 3483 | 3483 | 0 | |
| Z3n | 0 | 2496 | 6528991.378 | 6532128.428 | 2496 | 355 | 2141 | 3497 | 2466 | 12 | |
| 2018-Z3n | 0 | 2462 | 6569187.697 | 6571543.013 | 2462 | 347 | 2115 | 3531 | 2481 | 7 | |
| Alt-Ergo | 0 | 1041 | 8881364.949 | 7084848.122 | 1041 | 0 | 1041 | 4952 | 2392 | 177 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 20 | 965056.527 | 507410.633 | 20 | 0 | 20 | 5973 | 128 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 985239.123 | 541737.776 | 0 | 0 | 0 | 5993 | 145 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 455 | 46158.86 | 32894.924 | 455 | 455 | 0 | 5538 | 2470 | 10 |
| CVC4 | 0 | 455 | 57428.932 | 58743.389 | 455 | 455 | 0 | 5538 | 2675 | 0 |
| CVC4-SymBreakn | 0 | 453 | 60083.228 | 61034.461 | 453 | 453 | 0 | 5540 | 2666 | 0 |
| Z3n | 0 | 355 | 242862.056 | 243021.43 | 355 | 355 | 0 | 5638 | 2466 | 12 |
| 2018-Z3n | 0 | 347 | 264897.996 | 264900.095 | 347 | 347 | 0 | 5646 | 2481 | 7 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 0 | 1581.293 | 1111.201 | 0 | 0 | 0 | 5993 | 128 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 8672.491 | 8213.296 | 0 | 0 | 0 | 5993 | 145 | 0 |
| Alt-Ergo | 0 | 0 | 174639.733 | 173527.261 | 0 | 0 | 0 | 5993 | 2392 | 177 |
| 2018-Vampiren | 0 | 0 | 1672812.85 | 1110405.91 | 0 | 0 | 0 | 5993 | 2219 | 0 |
| Vampire | 0 | 0 | 1154401.18 | 1111085.27 | 0 | 0 | 0 | 5993 | 3483 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|
| 2018-Vampiren | 0 | 3774 | 9647335.147 | 3059462.787 | 3774 | 0 | 3774 | 2219 | 2219 | 0 |
| Par4 | 0 | 3058 | 2948341.234 | 2824533.847 | 3058 | 0 | 3058 | 2935 | 2470 | 10 |
| CVC4-SymBreakn | 0 | 2872 | 3559368.223 | 3591740.131 | 2872 | 0 | 2872 | 3121 | 2666 | 0 |
| CVC4 | 0 | 2861 | 3532619.558 | 3546642.628 | 2861 | 0 | 2861 | 3132 | 2675 | 0 |
| Vampire | 0 | 2510 | 5953604.971 | 4411852.076 | 2510 | 0 | 2510 | 3483 | 3483 | 0 |
| Z3n | 0 | 2141 | 3636561.063 | 3637807.669 | 2141 | 0 | 2141 | 3852 | 2466 | 12 |
| 2018-Z3n | 0 | 2115 | 3651782.274 | 3652119.15 | 2115 | 0 | 2115 | 3878 | 2481 | 7 |
| Alt-Ergo | 0 | 1041 | 6583449.735 | 5039440.002 | 1041 | 0 | 1041 | 4952 | 2392 | 177 |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 20 | 958922.89 | 502894.916 | 20 | 0 | 20 | 5973 | 128 | 0 |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 955356.106 | 513608.027 | 0 | 0 | 0 | 5993 | 145 | 0 |
| Solver | Error Score | Correct Score | CPU Time Score | Wall Time Score | Solved | Solved SAT | Solved UNSAT | Unsolved | Abstained | Timeout | Memout |
|---|---|---|---|---|---|---|---|---|---|---|---|
| Par4 | 0 | 2907 | 80665.317 | 77643.12 | 2907 | 410 | 2497 | 3086 | 3076 | 10 | |
| CVC4 | 0 | 2430 | 90359.415 | 90311.8 | 2430 | 393 | 2037 | 3563 | 3562 | 0 | |
| CVC4-SymBreakn | 0 | 2398 | 91389.83 | 91344.793 | 2398 | 390 | 2008 | 3595 | 3594 | 0 | |
| Z3n | 0 | 2299 | 88961.382 | 88925.002 | 2299 | 329 | 1970 | 3694 | 3536 | 12 | |
| 2018-Z3n | 0 | 2245 | 89833.519 | 89811.581 | 2245 | 315 | 1930 | 3748 | 3585 | 7 | |
| 2018-Vampiren | 0 | 1521 | 116058.676 | 109689.503 | 1521 | 0 | 1521 | 4472 | 4472 | 0 | |
| Vampire | 0 | 1455 | 125364.932 | 113305.256 | 1455 | 0 | 1455 | 4538 | 4538 | 0 | |
| Alt-Ergo | 0 | 841 | 101444.895 | 95404.638 | 841 | 0 | 841 | 5152 | 3695 | 177 | |
| UltimateEliminator+MathSAT-5.5.4 | 0 | 20 | 25734.318 | 19991.943 | 20 | 0 | 20 | 5973 | 257 | 0 | |
| UltimateEliminator+Yices-2.6.1 | 0 | 0 | 25414.984 | 19702.56 | 0 | 0 | 0 | 5993 | 270 | 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.