Blbej přetok

formula to the propositional logic (\emph{bit-blasting}) and use an

efficient \sat solver to decide its satisfiability. Therefore, the

efficiency of most of the bit-vector \smt solvers is tightly connected

to the efficiency of the \sat solvers. Plenty of solvers supporting

the quantifier-free bit-vector formulas exist: Beaver~\cite{Beaver},

to the efficiency of the \sat solvers. Plenty of solvers for the

quantifier-free bit-vector formulas exist: Beaver~\cite{Beaver},

Boolector~\cite{Boolector}, CVC4~\cite{CVC4}, MathSAT5~\cite{MathSAT},

OpenSMT~\cite{OpenSMT}, Sonolar~\cite{Sonolar}, Spear~\cite{Spear},

STP~\cite{STP}, UCLID~\cite{LS04}, Yices~\cite{Yices}, and