Solving SMT formulas involving the theory of floating-pointing arithmetic (FPA) can be encountered in several domains including symbolic execution and program synthesis. Unfortunately, SMT solvers which support FPA often struggle trying to satisfy ...