\myheading{SMT-specific}

\leveldown{}

\begin{itemize}
\item Important website: \url{http://smtlib.cs.uiowa.edu/}.

\item Theories: \url{http://smtlib.cs.uiowa.edu/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 SMT-LIB standard: \url{http://smtlib.cs.uiowa.edu/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.

Using gitlab at \verb|uiowa.edu|\footnote{\url{https://clc-gitlab.cs.uiowa.edu:2443/explore/groups}}:

\begin{lstlisting}
sudo apt-get install git-lfs
git clone https://clc-gitlab.cs.uiowa.edu:2443/mpreiner/smt-lib-non-incremental.git
cd smt-lib-non-incremental
git submodule update --init
cd ..
git clone https://clc-gitlab.cs.uiowa.edu:2443/mpreiner/smt-lib-incremental.git
cd smt-lib-incremental
git submodule update --init
cd ..
\end{lstlisting}

Using starexec\footnote{\url{https://www.starexec.org/starexec/secure/explore/spaces.jsp?id=1}},
pick this:
\begin{itemize}
\item ``do you want to download the single space or the hierarchy?'' --- hierarchy
\item ``do you want to download the benchmarks and/or the solvers?'' --- solvers + benchmarks
\item ``do you want to store benchmarks/solvers in id directories?'' --- no
\end{itemize}

These benchmarks are used in
SMT-COMP competition\footnote{\url{https://smt-comp.github.io/}}.

\levelup{}