SMT-COMP 2026

The International Satisfiability Modulo Theories (SMT) Competition.

GitHub

SMT-COMP 2026

Participants

The following solvers have been submitted to SMT-COMP 2026 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
BitwuzlaXXXX42Aina Niemetz, Mathias PreinerArchiveSystem description
Bitwuzla-BV_PartiX998244353Mengyu Zhao, Zhenghang Xu, Shaowei CaiArchiveSystem description
Bitwuzla-MachBVX1126300213Xiang Zhang, Shaohuang Chen, Mengyu Zhao, Shaowei CaiArchiveSystem description
Bitwuzla-SPFDX998244353Mengyu Zhao, Zhenghang Xu, Shaowei CaiArchiveSystem description
BitwuzllobX42Dominik Schreiber, Aina Niemetz, Mathias PreinerArchiveSystem description
bv_decideXX42Henrik 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-nokernelXX42Henrik 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
colibri2X72François Bobot, Hichem Rami Ait El Hara, Christophe JunkeArchiveSystem description
cvc5XXXX44Haniel Barbosa, Clark Barrett, Lydia Kondylidou, Hanna Lachnitt, Daniel Larraz, Abdalrhman Mohamed, Mudathir Mohamed, José Neto, Aina Niemetz, Alex Ozdemir, Mathias Preiner, Andrew Reynolds, Hans-Jörg Schurr, Cesare Tinelli, Yoni ZoharArchiveSystem description
cvc5-cvc5-xyzX66Xingyu Xie, Yingte Xu, Zhiyuan ZhangArchiveSystem description
NeuroSymX42Vishal Kumar Swain, Sangharatna Godboley, P. Radha Krishna, Avijit Das, Lucas CordeiroArchiveSystem description
OpenSMTXXXX987Tomáš Kolárik, Martin BlichaArchiveSystem description
OpenSMT (min-ucore)X367Tomáš Kolárik, Martin BlichaArchiveSystem description
OpenSMT-SMTSX6789Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud AsadzadehArchiveSystem description
OpenSMT-SMTS-seqX67891Tomáš Kolárik, Antti E. J. Hyvärinen, Seyedmasoud AsadzadehArchiveSystem description
OSTRICHX718582Matthew Hague, Denghang Hu, Anthony W. Lin, Oliver Markgraf, Philipp Ruemmer, Zhilin WuArchiveSystem description
plat-smtXXXX6536David EwertArchiveSystem description
QiuQiX0Zhendong Lei, Jianrong Yuan, Yue Zhang, Qiuchen Qian, Pinyan LuArchiveSystem description
QiuQiX0Zhendong Lei, Jianrong Yuan, Yue Zhang, Qiuchen Qian, Pinyan LuArchiveSystem description
RooleX22961Jan Onderka, Armin BiereArchiveSystem description
SametX3948761623Martin BlichaArchiveSystem description
SMT-RATXX29Jasper Nalbach, Valentin Promies, Erika ÁbrahámArchiveSystem description
SMTInterpolXXXX2570846495Max 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
UltimateEliminator+MathSATXXX0Max Barth, Daniel Dietsch, Matthias HeizmannArchiveSystem description
XolverX20260528Fuqi JiaArchiveSystem description
Yices2XXXXX37Bruno 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-alpha2X33John Lu, Avik Kumar, Piyush Jha, Arie Gurfinkel, Vijay GaneshArchiveSystem description
z3-BooledASSXXXX2026Umut KorkmazArchiveSystem description
Z3-GEXX42Shuming Shi, Wenbo Wei, Zhengfeng Yang, Jianlin WangArchiveSystem description
Z3-NoodlerX24305Vojtěch Havlena, Juraj Síč, David Chocholatý, Lukáš Holík, Ondřej Lengál, Michal HečkoArchiveSystem description
z3-parallelX0Ilana Shapiro, Nikolaj BjørnerArchiveSystem description
Z3-siriX42BingZhe Zhou, HanNan Wang, Yuan Yao, Taolue Chen, Feng Xu, Xiaoxing MaArchiveSystem description
Z3-Z3++X19970530Bohan Li, Shihao Jiao, Jun WuArchiveSystem description
Bitwuzla-0-9-1 nX42Aina Niemetz, Mathias PreinerArchiveSystem description
bitwuzla-dandelion nX421Runzhou Li, Peison YaoArchiveSystem description
bitwuzla-dandelion-base nX421Aina Niemetz, Mathias PreinerArchiveSystem description
Bitwuzla-MachBV-base nX42Aina Niemetz, Mathias PreinerArchiveSystem description
cvc5-cvc5-xyz-base nX66All cvc5 ContributorsArchiveSystem description
OpenSMT-SMTS-base nX67893Tomáš Kolárik, Martin BlichaArchiveSystem description
OpenSMT-SMTS-seq-base nX67893Tomáš Kolárik, Martin BlichaArchiveSystem description
Z3-alpha2-base nX33Nikolaj Bjørner et al.ArchiveSystem description
Z3-alpha2-debug nX33John Lu, Avik Kumar, Piyush Jha, Arie Gurfinkel, Vijay GaneshArchiveSystem description
z3-BooledASS-base nXXXXNikolaj Bjørner, Leonardo de MouraArchiveSystem description
Z3-GEX-base nX33Nikolaj Bjørner et al.ArchiveSystem description
Z3-Noodler-base nX928343Nikolaj Bjørner et al.ArchiveSystem description
Z3-siri-base nX33Nikolaj Bjørner et al.ArchiveSystem description
Z3-Z3++-base nXNikolaj BjørnerArchiveSystem description

n Non-competing.

The opening value of the NYSE Composite Index on 2026-06-12 was 23412.89, resulting in a competition seed of 2341289 + 20389785 = 22731074.