SMT solver for bit-vectors and arrays

 Boolector is an efficient SMT solver for the quantifier-free theory of
 bit-vectors in combination with the quantifier-free extensional theory of
 arrays.