\myheading{SMT-specific} \leveldown{} \begin{itemize} \item Important website: \url{https://smt-lib.org/}. \item Theories: \url{https://smt-lib.org/logics.shtml}, \url{https://cs.nyu.edu/pipermail/smt-lib/2005/000046.html}. \item SMT-COMP mailing list: \url{https://cs.nyu.edu/mailman/listinfo/smt-comp}. \item SMT-LIB mailing list: \url{https://cs.nyu.edu/pipermail/smt-lib/}, \url{https://groups.google.com/forum/#!forum/smt-lib}. \item Since 2022, all SMT-related discussion is moved into: \url{https://smtlib.zulipchat.com/} \item SMT-LIB standard: \url{https://smt-lib.org/papers/smt-lib-reference-v2.6-r2017-07-18.pdf} \item David R. Cok -- The SMT-LIBv2 Language and Tools: A Tutorial: \url{http://smtlib.github.io/jSMTLIB/SMTLIBTutorial.pdf} \end{itemize} \myheading{Benchmarks} SAT/SMT is a young field (yet). Not much documentation exist. So I've found SMT benchmark collection as an invaluable source of information. Benchmarks are typically generated by a SMT applications, so you can get into better understanding, how SMT is used. \url{https://smt-lib.org/benchmarks.shtml} \levelup{}