Le projet smt2d est un outil de vérification de formules mathématiques et d'analyse de contraintes logiques. Il permet de traiter des problèmes de satisfiabilité modulo théories (SMT) en utilisant la logique first-order avec équations et inégalités.