papers/lux-symbolic-execution-halmos/sections/06-smt-solvers-the-engine-under-the-hood.tex

\section{SMT Solvers: The Engine Under the Hood}


\subsection{What Is SMT}

Satisfiability Modulo Theories (SMT) extends Boolean satisfiability (SAT) with
domain-specific theories: bitvectors, arrays, integers, reals. An SMT solver determines
whether a logical formula has a satisfying assignment.

For EVM symbolic execution, the relevant theories are:
\begin{itemize}[nosep]
  \item \textbf{QF\_BV}: Quantifier-free bitvectors (256-bit arithmetic).
  \item \textbf{QF\_ABV}: Arrays of bitvectors (storage, memory).
\end{itemize}

\subsection{Z3 and the DPLL(T) Architecture}

Z3, the default solver for Halmos, uses the DPLL(T) architecture:
\begin{enumerate}[nosep]
  \item A SAT solver handles the Boolean structure.
  \item Theory solvers handle domain-specific reasoning (bitvector arithmetic, array axioms).
  \item The SAT solver and theory solvers communicate: when the SAT solver proposes an
    assignment, the theory solver checks consistency.
\end{enumerate}

\subsection{Solver Timeouts}

Some path constraints are too complex for the solver to decide within a reasonable time.
Halmos reports these as ``timeout'' rather than ``verified'' or ``violated.'' A timeout
is neither a proof nor a counterexample---it means the analysis is incomplete.

Strategies for reducing solver timeouts:
\begin{itemize}[nosep]
  \item Simplify the contract (smaller functions, fewer state variables).
  \item Add \texttt{vm.assume} to eliminate irrelevant paths.
  \item Reduce loop unrolling bounds.
  \item Use \texttt{--solver-timeout-assertion} to increase the timeout.
\end{itemize}

%% ============================================================