SONOLAR, the Solver for non-linear Arithmetic, is an SMT-Solver that solves quantifier-free fixed-size bit-vector logic formulas. The solver supports the SMT-LIB format including the following logics: Bit vectors (QF_BV). Bit vectors with arrays (QF_ABV). IEEE 754 floating point operations including all rounding modes with arbitrary range and precision: The solver supports the symbols described in the SMT-LIB theory for floting point numbers. Since SMT-LIB logic names are yet to be defined for this theory, the logics QF_BV and QF_ABV have been extended by these symbols. SONOLAR uses bit-blasting to translate bitvector constraints to a Boolean formula and lets a SAT solver decide the satisfiability. For handling the extensional theory of arrays, the lemmas on demand approach described in [2] has been adopted. To this end a series of word-level simplification rules are applied to the input formula which is then converted to an And-Inverter Graph. After performing bit-level simplifications a Boolean CNF formula is generated and fed to a SAT solver. MiniSat 2.2.0 and Glucose 3.0 are used as SAT solvers [4, 1]. SONOLAR is currently used for automatic test data generation in the field of model-based testing and C/C++-unit testing