The International Satisfiability Modulo Theories (SMT) Competition.
The following solvers have been submitted to SMT-COMP 2024 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 | Contributors | Archive | System description |
|---|---|---|---|---|---|---|---|---|---|
| Algaroba | X | Amar Shah, Federico Mora, Sanjit Seshia | Archive | System description | |||||
| Amaya | X | Vojtěch Havlena, Michal Hečko, Lukáš Holík, Ondřej Lengál | Archive | System description | |||||
| Bitwuzla | X | X | X | X | Aina Niemetz, Mathias Preiner | Archive | System description | ||
| COLIBRI | X | Bruno Marre, François Bobot, Christophe Junke | Archive | System description | |||||
| cvc5 | X | X | X | X | Leni Aniva, Haniel Barbosa, Clark Barrett, Hanna Lachnitt, Daniel Larraz, Abdalrhman Mohamed, Mudathir Mohamed, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Amalee Wilson, Yoni Zohar | Archive | System description | ||
| cvc5-cloud | X | Amalee Wilson, Clark Barrett | Archive | System description | |||||
| iProver v3.9 | X | Konstantin Korovin | Archive | System description | |||||
| OpenSMT | X | X | X | X | Tomáš Kolárik, Martin Blicha | Archive | System description | ||
| OSTRICH | X | Matthew Hague, Denghang Hu, Anthony W. Lin, Oliver Markgraf, Philipp Rümmer, Zhilin Wu | Archive | System description | |||||
| plat-smt | X | X | X | X | David Ewert | Archive | System description | ||
| SMT-RAT | X | X | Jasper Nalbach, Valentin Promies, Erika Ábrahám | Archive | System description | ||||
| SMTInterpol | X | X | X | X | 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 | X | Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud Asadzadeh | Archive | System description | ||||
| STP | X | X | X | Vijay Ganesh, Trevor Hansen, Mate Soos, Dan Liew, Ryan Govostes, Andrew V. Jones | Archive | System description | |||
| STP-Parti-Bitwuzla | X | X | Mengyu Zhao, Jinkun Lin, Shaowei Cai | Archive | System description | ||||
| Yices2 | X | X | X | X | Bruno Dutertre, Aman Goel, Stéphane Graham-Lengrand, Thomas Hader, Ahmed Irfan, Dejan Jovanovic, Ian A Mason | Archive | System description | ||
| YicesQS | X | Stéphane Graham-Lengrand | Archive | System description | |||||
| Z3-alpha | X | Zhengyang John Lu, Paul Sarnighausen-Cahn, Stefan Siemer, Florin Manea, Vijay Ganesh | Archive | System description | |||||
| Z3-Noodler | X | Vojtěch Havlena, Juraj Síč, David Chocholatý, Lukáš Holík, Ondřej Lengál | Archive | System description | |||||
| Z3-Parti-Z3++ | X | X | Mengyu Zhao, Shaowei Cai | Archive | System description |