صدق‌پذیری در پیمانه نظریات
حل‌کننده‌ها

جدول زیر بعضی از ویژگی‌های چند تا از حل کننده‌های SMT موجود را خلاصه‌بندی نموده‌است. ستون «SMT-LIB» نشان‌دهنده سازگاری با زبان SMT-LIB است؛ بیشتر سامانه‌هایی را که با 'yes' نشان‌گذاری کرده‌ایم، فقط از نسخه‌های قدیمی SMT-LIB پشتیبانی می‌کنند، یا اینکه فقط پشتیبانی جزئی از زبان دارند. ستون «CVC» نشان‌دهنده پشتیبانی از زبان CVC است. ستون «DIMACS» نشان‌دهنده پشتیبانی از قالب DIMACS است.
این پروژه‌ها نه فقط از نظر ویژگی و کارایی با هم فرق دارند، بلکه از نظر زیست‌پذیری انجمن اطراف شان، علاقه پیشرونده به پروژه و توانمندی مشارکت مستندات، تعمیرها، تست‌ها و ارتقا با هم تفاوت دارند.
| بن‌سازه> Name | بن‌سازه> OS | بن‌سازه> License | ویژگی‌ها> SMT-LIB | ویژگی‌ها> CVC | ویژگی‌ها> DIMACS | ویژگی‌ها> Built-in theories | ویژگی‌ها> API | ویژگی‌ها> SMT-COMP  | یادداشت‌ها>  |
| --- | --- | --- | --- | --- | --- | --- | --- | --- | --- |
| ABsolver | Linux | CPL | v1.2 | نه | آری | linear arithmetic, non-linear arithmetic | C++ | no | DPLL-based |
| Alt-Ergo | Linux,  Mac OS , Windows | CeCILL-C (roughly equivalent to LGPL) | partial v1.2 and v2.0 | نه | نه | empty theory, linear integer and rational arithmetic, non-linear arithmetic, polymorphic arrays, enumerated datatypes, AC symbols, bitvectors, record datatypes, quantifiers | OCaml | ۲۰۰۸ | Polymorphic first-order input language à la ML, SAT-solver based, combines Shostak-like and Nelson-Oppen like approaches for reasoning modulo theories |
| Barcelogic | Linux | Proprietary | v1.2 |  |  | empty theory, difference logic | C++ | ۲۰۰۹ | DPLL-based, congruence closure |
| Beaver | Linux, Windows | BSD | v1.2 | نه | نه | bitvectors | OCaml | ۲۰۰۹ | SAT-solver based |
| Boolector | Linux | MIT | v1.2 | نه | نه | bitvectors, arrays | C | ۲۰۰۹ | SAT-solver based |
| CVC3 | Linux | BSD | v1.2 | آری |  | empty theory, linear arithmetic, arrays, tuples, types, records, bitvectors, quantifiers | C/C++ | ۲۰۱۰ | proof output to HOL |
| CVC4 | Linux,  Mac OS , Windows, FreeBSD | BSD | آری | آری |  | rational and integer linear arithmetic, arrays, tuples, records, inductive data types, bitvectors, strings, and equality over uninterpreted function symbols | C++ | ۲۰۱۰ | version 1.5 released July 2017 |
| Decision Procedure Toolkit (DPT) | Linux | Apache | نه |  |  |  | OCaml | no | DPLL-based |
| iSAT | Linux | Proprietary | نه |  |  | non-linear arithmetic |  | no | DPLL-based |
| MathSAT | Linux,  Mac OS , Windows | Proprietary | آری |  | آری | empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays | C/C++, Python, Java | ۲۰۱۰ | DPLL-based |
| MiniSmt | Linux | LGPL | partial v2.0 |  |  | non-linear arithmetic |  | ۲۰۱۰ | SAT-solver based, Yices-based |
| Norn |  |  |  |  |  |  |  |  | SMT solver for string constraints |
: 
| OpenCog | Linux | AGPL | نه | نه | نه | probabilistic logic, arithmetic. relational models | C++, Scheme, Python | no | subgraph isomorphism |
| OpenSMT | Linux,  Mac OS , Windows | GPLv3 | partial v2.0 |  | آری | empty theory, differences, linear arithmetic, bitvectors | C++ | ۲۰۱۱ | lazy SMT Solver |
| raSAT | Linux | GPLv3 | v2.0 |  |  | real and integer nonlinear arithmetic |  | ۲۰۱۴، ۲۰۱۵ | extension of the Interval Constraint Propagation with Testing and the Intermediate Value Theorem |
| SatEEn |  ? | Proprietary | v1.2 |  |  | linear arithmetic, difference logic | none | ۲۰۰۹ |  |
| SMTInterpol | Linux,  Mac OS , Windows | LGPLv3 | v2.5 |  |  | uninterpreted functions, linear real arithmetic, and linear integer arithmetic | Java | ۲۰۱۲ | Focuses on generating high quality, compact interpolants. |
| SMCHR | Linux,  Mac OS , Windows | GPLv3 | نه | نه | نه | linear arithmetic, nonlinear arithmetic, heaps | C | no | Can implement new theories using Constraint Handling Rules. |
| SMT-RAT | Linux,  Mac OS | MIT | v2.0 | نه | نه | linear arithmetic, nonlinear arithmetic | C++ | ۲۰۱۵ | Toolbox for strategic and parallel SMT solving consisting of a collection of SMT compliant implementations. |
| SONOLAR | Linux, Windows | Proprietary | partial v2.0 |  |  | bitvectors | C | ۲۰۱۰ | SAT-solver based |
| Spear | Linux,  Mac OS , Windows | Proprietary | v1.2 |  |  | bitvectors |  | ۲۰۰۸ |  |
| STP | Linux, OpenBSD, Windows,  Mac OS | MIT | partial v2.0 | آری | نه | bitvectors, arrays | C, C++, Python, OCaml, Java | ۲۰۱۱ | SAT-solver based |
| SWORD | Linux | Proprietary | v1.2 |  |  | bitvectors |  | ۲۰۰۹ |  |
| UCLID | Linux | BSD | نه | نه | نه | empty theory, linear arithmetic, bitvectors, and constrained lambda (arrays, memories, cache, etc.) |  | no | SAT-solver based, written in  Moscow ML . Input language is SMV model checker. Well-documented! |
| veriT | Linux, OS X | BSD | partial v2.0 |  |  | empty theory, rational and integer linear arithmetics, quantifiers, and equality over uninterpreted function symbols | C/C++ | ۲۰۱۰ | SAT-solver based |
| Yices | Linux,  Mac OS , Windows, FreeBSD | GPLv3 | v2.0 | نه | آری | rational and integer linear arithmetic, bitvectors, arrays, and equality over uninterpreted function symbols | C | ۲۰۱۴ | Source code is available online |
| Z3 Theorem Prover | Linux,  Mac OS , Windows, FreeBSD | MIT | v2.0 |  | آری | empty theory, linear arithmetic, nonlinear arithmetic, bitvectors, arrays, datatypes, quantifiers, strings | C/C++, .NET, OCaml, Python, Java, Haskell | ۲۰۱۱ | Source code is available online |