The International Satisfiability Modulo Theories (SMT) Competition.
The following solvers have been submitted to SMT-COMP 2025 or were entered as non-competing solvers by the organizers for comparison.
| Solver | Single Query Track | Incremental Track | Unsat Core Track | Model Validation Track | Cloud Track | Parallel Track | Seed | Contributors | Archive | System description |
|---|---|---|---|---|---|---|---|---|---|---|
| Amaya | X | 587087 | Vojtěch Havlena, Michal Hečko, Lukáš Holík, Ondřej Lengál | Archive | System description | |||||
| Bitwuzla | X | X | X | X | X | 42 | Aina Niemetz, Mathias Preiner | Archive | System description | |
| Bitwuzla-MachBV | X | 1126300213 | Xiang Zhang, Shaohuang Chen, Mengyu Zhao, Shaowei Cai | Archive | System description | |||||
| bv_decide | X | 42 | Henrik Böving, Siddharth Bhat, Alex Keizer, Luisa Cicolini, Leon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Josh Clune, Clark Barrett, Tobias Grosser | Archive | System description | |||||
| bv_decide-nokernel | X | 42 | Henrik Böving, Siddharth Bhat, Alex Keizer, Luisa Cicolini, Leon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Josh Clune, Clark Barrett, Tobias Grosser | Archive | System description | |||||
| COLIBRI | X | 0 | Bruno Marre, François Bobot, Christophe Junke | Archive | System description | |||||
| colibri2 | X | 42 | François Bobot, Hichem Ait El Hara, Christophe Junke | Archive | System description | |||||
| cvc5 | X | X | X | X | 8465677983 | Haniel Barbosa, Clark Barrett, Hanna Lachnitt, Daniel Larraz, Abdalrhman Mohamed, Mudathir Mohamed, José Neto, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Amalee Wilson, Yoni Zohar | Archive | System description | ||
| iProver v3.9.3 | X | X | 139 | Konstantin Korovin | Archive | System description | ||||
| OpenSMT | X | X | X | X | 87 | Tomáš Kolárik, Martin Blicha | Archive | System description | ||
| OpenSMT (min-ucore) | X | 67 | Tomáš Kolárik, Martin Blicha | Archive | System description | |||||
| OSTRICH | X | 718582 | Matthew Hague, Denghang Hu, Anthony W. Lin, Oliver Markgraf, Philipp Ruemmer, Zhilin Wu | Archive | System description | |||||
| SMT-RAT | X | X | 21 | Jasper Nalbach, Valentin Promies, Erika Ábrahám | Archive | System description | ||||
| SMTInterpol | X | X | X | X | 2030142482 | Max Barth, Leon Cacace, Jürgen Christ, Daniel Dietsch, Leonard Fichtner, Joanna Greulich, Elisabeth Henkel, Matthias Heizmann, Jochen Hoenicke, Moritz Mohr, Alexander Nutz, Markus Pomrehn, Pascal Raiola, Tanja Schindler | Archive | System description | ||
| SMTS | X | 89 | Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh | Archive | System description | |||||
| STP-Parti-Bitwuzla | X | 998244353 | Mengyu Zhao, Zhenghang Xu, Jinkun Lin, Shaowei Cai | Archive | System description | |||||
| UltimateEliminator+MathSAT | X | X | X | 0 | Max Barth, Daniel Dietsch, Matthias Heizmann | Archive | System description | |||
| Yices2 | X | X | X | X | X | 0 | Bruno Dutertre, Aman Goel, Stéphane Graham-Lengrand, Thomas Hader, Ahmed Irfan, Dejan Jovanovic, Enrico Lipparini, Ian A Mason, Karthik Nukala, Harald Ruess | Archive | System description | |
| YicesQS | X | 0 | Stéphane Graham-Lengrand | Archive | System description | |||||
| Z3-alpha | X | 33 | John Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Florin Manea, Vijay Ganesh | Archive | System description | |||||
| Z3-Inc-Z3++ | X | 19970530 | Bohan Li, Shaowei Cai | Archive | System description | |||||
| Z3-Noodler | X | 48655 | Vojtěch Havlena, Juraj Síč, David Chocholatý, Lukáš Holík, Ondřej Lengál, Michal Hečko | Archive | System description | |||||
| Z3-Noodler-Mocha | X | 13 | Shaoke Cui, Chuan Luo, Zhenwei Yang, Chunming Hu | Archive | System description | |||||
| Z3-Owl | X | 421 | Hanrui Zuo, Peisen Yao | Archive | System description | |||||
| Z3-Parti-Z3pp | X | 998244353 | Mengyu Zhao, Shaowei Cai | Archive | System description | |||||
| z3siri | X | 42 | BingZhe Zhou, HanNan Wang | Archive | System description | |||||
| Bitwuzla-32core n | X | 42 | Aina Niemetz, Mathias Preiner | Archive | System description | |||||
| Bitwuzla-64core n | X | 42 | Aina Niemetz, Mathias Preiner | Archive | System description | |||||
| Bitwuzla-MachBV-base n | X | Aina Niemetz, Mathias Preiner | Archive | System description | ||||||
| SMTS (32 cores) n | X | 89 | Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh | Archive | System description | |||||
| SMTS (64 cores) n | X | 89 | Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh | Archive | System description | |||||
| STP-Parti-Bitwuzla-16core n | X | 998244353 | Mengyu Zhao, Zhenghang Xu, Jinkun Lin, Shaowei Cai | Archive | System description | |||||
| STP-Parti-Bitwuzla-32core n | X | 998244353 | Mengyu Zhao, Zhenghang Xu, Jinkun Lin, Shaowei Cai | Archive | System description | |||||
| STP-Parti-Bitwuzla-64core n | X | 998244353 | Mengyu Zhao, Zhenghang Xu, Jinkun Lin, Shaowei Cai | Archive | System description | |||||
| Z3-alpha-base n | X | Nikolaj Bjørner et al. | Archive | System description | ||||||
| Z3-Inc-Z3++-base n | X | Nikolaj Bjørner | Archive | System description | ||||||
| Z3-Noodler-base n | X | Nikolaj Bjørner et al. | Archive | System description | ||||||
| Z3-Noodler-Mocha-base n | X | Vojtěch Havlena, Juraj Síč, David Chocholatý, Lukáš Holík, Ondřej Lengál, Michal Hečko | Archive | System description | ||||||
| Z3-Owl-base n | X | Nikolaj Bjørner et al. | Archive | System description | ||||||
| Z3-Parti-Z3pp-16core n | X | 998244353 | Mengyu Zhao, Shaowei Cai | Archive | System description | |||||
| Z3-Parti-Z3pp-32core n | X | 998244353 | Mengyu Zhao, Shaowei Cai | Archive | System description | |||||
| Z3-Parti-Z3pp-64core n | X | 998244353 | Mengyu Zhao, Shaowei Cai | Archive | System description | |||||
| z3siri-base n | X | Nikolaj Bjørner et al. | Archive | System description |
n Non-competing.
The opening value of the NYSE Composite Index on 2025-06-30 was 20338.41, resulting in a competition seed of 2033841 + 755033430 = 757067271.