We consider the problem of solving floating-point constraints
  obtained from software verification. We present UppSAT --- an new
  implementation of a systematic approximation refinement framework as
  an abstract SMT solver.  Provided with an approximation and a
  decision procedure (implemented in an off-the-shelf SMT solver),
  UppSAT yields an approximating SMT solver.  Additionally, UppSAT
  includes a library of predefined approximation components which can
  be combined and extended to define new encodings, orderings and
  solving strategies. We propose that UppSAT can be used as a sandbox
  for easy and flexible exploration of new approximations. To
  substantiate this, we explore encodings of floating-point arithmetic
  into reduced precision floating-point arithmetic, real-arithmetic,
  and fixed-point arithmetic (encoded into the theory of bit-vectors
  in practice). In an experimental evaluation we compare the
  advantages and disadvantages of approximating solvers obtained by
  combining various encodings and decision procedures.