SMT-COMP 2025

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2025

Participants

The following solvers have been submitted to SMT-COMP 2025 or were entered as non-competing solvers by the organizers for comparison.

SolverSingle Query TrackIncremental TrackUnsat Core TrackModel Validation TrackCloud TrackParallel TrackSeedContributorsArchiveSystem description
AmayaX587087Vojtěch Havlena, Michal Hečko, Lukáš Holík, Ondřej LengálArchiveSystem description
BitwuzlaXXXXX42Aina Niemetz, Mathias PreinerArchiveSystem description
Bitwuzla-MachBVX1126300213Xiang Zhang, Shaohuang Chen, Mengyu Zhao, Shaowei CaiArchiveSystem description
bv_decideX42Henrik Böving, Siddharth Bhat, Alex Keizer, Luisa Cicolini, Leon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Josh Clune, Clark Barrett, Tobias GrosserArchiveSystem description
bv_decide-nokernelX42Henrik Böving, Siddharth Bhat, Alex Keizer, Luisa Cicolini, Leon Frenot, Abdalrhman Mohamed, Léo Stefanesco, Harun Khan, Josh Clune, Clark Barrett, Tobias GrosserArchiveSystem description
COLIBRIX0Bruno Marre, François Bobot, Christophe JunkeArchiveSystem description
colibri2X42François Bobot, Hichem Ait El Hara, Christophe JunkeArchiveSystem description
cvc5XXXX8465677983Haniel 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 ZoharArchiveSystem description
iProver v3.9.3XX139Konstantin KorovinArchiveSystem description
OpenSMTXXXX87Tomáš Kolárik, Martin BlichaArchiveSystem description
OpenSMT (min-ucore)X67Tomáš Kolárik, Martin BlichaArchiveSystem description
OSTRICHX718582Matthew Hague, Denghang Hu, Anthony W. Lin, Oliver Markgraf, Philipp Ruemmer, Zhilin WuArchiveSystem description
SMT-RATXX21Jasper Nalbach, Valentin Promies, Erika ÁbrahámArchiveSystem description
SMTInterpolXXXX2030142482Max 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 SchindlerArchiveSystem description
SMTSX89Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud AsadzadehArchiveSystem description
STP-Parti-BitwuzlaX998244353Mengyu Zhao, Zhenghang Xu, Jinkun Lin, Shaowei CaiArchiveSystem description
UltimateEliminator+MathSATXXX0Max Barth, Daniel Dietsch, Matthias HeizmannArchiveSystem description
Yices2XXXXX0Bruno Dutertre, Aman Goel, Stéphane Graham-Lengrand, Thomas Hader, Ahmed Irfan, Dejan Jovanovic, Enrico Lipparini, Ian A Mason, Karthik Nukala, Harald RuessArchiveSystem description
YicesQSX0Stéphane Graham-LengrandArchiveSystem description
Z3-alphaX33John Lu, Paul Sarnighausen-Cahn, Jiahao Chen, Florin Manea, Vijay GaneshArchiveSystem description
Z3-Inc-Z3++X19970530Bohan Li, Shaowei CaiArchiveSystem description
Z3-NoodlerX48655Vojtěch Havlena, Juraj Síč, David Chocholatý, Lukáš Holík, Ondřej Lengál, Michal HečkoArchiveSystem description
Z3-Noodler-MochaX13Shaoke Cui, Chuan Luo, Zhenwei Yang, Chunming HuArchiveSystem description
Z3-OwlX421Hanrui Zuo, Peisen YaoArchiveSystem description
Z3-Parti-Z3ppX998244353Mengyu Zhao, Shaowei CaiArchiveSystem description
z3siriX42BingZhe Zhou, HanNan WangArchiveSystem description
Bitwuzla nX42Aina Niemetz, Mathias PreinerArchiveSystem description
Bitwuzla nX42Aina Niemetz, Mathias PreinerArchiveSystem description
Bitwuzla-MachBV-base nXAina Niemetz, Mathias PreinerArchiveSystem description
SMTS (32 cores) nX89Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud AsadzadehArchiveSystem description
SMTS (64 cores) nX89Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud AsadzadehArchiveSystem description
STP-Parti-Bitwuzla nX998244353Mengyu Zhao, Zhenghang Xu, Jinkun Lin, Shaowei CaiArchiveSystem description
STP-Parti-Bitwuzla nX998244353Mengyu Zhao, Zhenghang Xu, Jinkun Lin, Shaowei CaiArchiveSystem description
STP-Parti-Bitwuzla nX998244353Mengyu Zhao, Zhenghang Xu, Jinkun Lin, Shaowei CaiArchiveSystem description
Z3-alpha-base nXNikolaj Bjørner et al.ArchiveSystem description
Z3-Inc-Z3++-base nXNikolaj BjørnerArchiveSystem description
Z3-Noodler-base nXNikolaj Bjørner et al.ArchiveSystem description
Z3-Noodler-Mocha-base nXVojtěch Havlena, Juraj Síč, David Chocholatý, Lukáš Holík, Ondřej Lengál, Michal HečkoArchiveSystem description
Z3-Owl-base nXNikolaj Bjørner et al.ArchiveSystem description
Z3-Parti-Z3pp nX998244353Mengyu Zhao, Shaowei CaiArchiveSystem description
Z3-Parti-Z3pp nX998244353Mengyu Zhao, Shaowei CaiArchiveSystem description
Z3-Parti-Z3pp nX998244353Mengyu Zhao, Shaowei CaiArchiveSystem description
z3siri-base nXNikolaj Bjørner et al.ArchiveSystem 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.