diff --git a/src/solvers/floatbv/float_approximation.cpp b/src/solvers/floatbv/float_approximation.cpp
index 63d2e372813..16384fdb435 100644
--- a/src/solvers/floatbv/float_approximation.cpp
+++ b/src/solvers/floatbv/float_approximation.cpp
@@ -48,7 +48,8 @@ void float_approximationt::normalization_shift(bvt &fraction, bvt &exponent)
     bv_utils.cond_implies_equal(shift, shifted_fraction, new_fraction);
 
     // build new exponent
-    bvt adjustment=bv_utils.build_constant(-i, exponent.size());
+    bvt adjustment =
+      bv_utils.build_constant(-static_cast<int>(i), exponent.size());
     bvt added_exponent=bv_utils.add(exponent, adjustment);
     bv_utils.cond_implies_equal(shift, added_exponent, new_exponent);
   }
diff --git a/unit/CMakeLists.txt b/unit/CMakeLists.txt
index 6def86d4887..036cc3ce4c4 100644
--- a/unit/CMakeLists.txt
+++ b/unit/CMakeLists.txt
@@ -7,7 +7,6 @@ list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/miniBDD.cpp
 
     # Don't build
-    ${CMAKE_CURRENT_SOURCE_DIR}/sharing_map.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/elf_reader.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/smt2_parser.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/json.cpp
@@ -15,7 +14,6 @@ list(REMOVE_ITEM sources
     ${CMAKE_CURRENT_SOURCE_DIR}/osx_fat_reader.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/wp.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/cpp_scanner.cpp
-    ${CMAKE_CURRENT_SOURCE_DIR}/float_utils.cpp
     ${CMAKE_CURRENT_SOURCE_DIR}/ieee_float.cpp
 
     # Will be built into a separate library and linked
diff --git a/unit/Makefile b/unit/Makefile
index a52eafa79b8..1e4dc900bdd 100644
--- a/unit/Makefile
+++ b/unit/Makefile
@@ -17,6 +17,7 @@ SRC += unit_tests.cpp \
        analyses/does_remove_const/is_type_at_least_as_const_as.cpp \
        goto-programs/goto_trace_output.cpp \
        path_strategies.cpp \
+       solvers/floatbv/float_utils.cpp \
        solvers/refinement/array_pool/array_pool.cpp \
        solvers/refinement/string_constraint_generator_valueof/calculate_max_string_length.cpp \
        solvers/refinement/string_constraint_generator_valueof/get_numeric_value_from_character.cpp \
diff --git a/unit/float_utils.cpp b/unit/float_utils.cpp
deleted file mode 100644
index d9280280c41..00000000000
--- a/unit/float_utils.cpp
+++ /dev/null
@@ -1,133 +0,0 @@
-#include <iostream>
-
-#include <solvers/sat/satcheck.h>
-#include <solvers/floatbv/float_utils.h>
-
-float random_float()
-{
-  unsigned u=random();
-  u=(u<<16)^random();
-  return *(float *)&u;
-}
-
-bool eq(const ieee_floatt &a, const ieee_floatt &b)
-{
-  if(a.is_NaN() && b.is_NaN()) return true;
-  if(a.is_infinity() && b.is_infinity() &&
-     a.get_sign()==b.get_sign()) return true;
-  return a==b;
-}
-
-std::string to_str(const bvt &bv)
-{
-  std::string result;
-  for(unsigned i=0; i<bv.size(); i++)
-  {
-    char ch;
-    if(bv[i]==const_literal(true))
-      ch='1';
-    else if(bv[i]==const_literal(false))
-      ch='0';
-    else
-      ch='?';
-    result=ch+result;
-  }
-  return result;
-}
-
-typedef enum { PLUS=0, MINUS=1, MULT=2, DIV=3 } binopt;
-const char *binopsyms[]={ " + ", " - ", " * ", " / " };
-
-int main()
-{
-  ieee_floatt i1, i2, i3;
-  bvt b1, b2, b3, res;
-  float f1, f2, f3;
-
-  for(unsigned i=0; i<200; i++)
-  {
-    if(i%20==0)
-      std::cout << "*********** " << i << std::endl;
-
-    satcheckt satcheck;
-    float_utilst float_utils(satcheck);
-
-    #if 0
-    f1=random_float();
-    f2=random_float();
-    i1.from_float(f1);
-    i2.from_float(f2);
-    float_utils.spec=i1.spec;
-    b1=float_utils.build_constant(i1);
-    b2=float_utils.build_constant(i2);
-    f3=f1;
-
-    int op=(binopt)i%3;
-    // op=PLUS;
-    #else
-    f1=-0.25;
-    f2=-2.5;
-    i1.from_float(f1);
-    i2.from_float(f2);
-    float_utils.spec=i1.spec;
-    b1=float_utils.build_constant(i1);
-    b2=float_utils.build_constant(i2);
-    f3=f1;
-
-    int op=DIV;
-    #endif
-
-    switch(op)
-    {
-    case PLUS:
-      f3+=f2;
-      res=float_utils.add(b1, b2);
-      break;
-
-    case MINUS:
-      f3-=f2;
-      res=float_utils.sub(b1, b2);
-      break;
-
-    case MULT:
-      f3*=f2;
-      res=float_utils.mul(b1, b2);
-      break;
-
-    case DIV:
-      f3/=f2;
-      res=float_utils.div(b1, b2);
-      break;
-
-    default:assert(0);
-    }
-
-    i3.from_float(f3);
-
-    satcheckt::resultt result=satcheck.prop_solve();
-    assert(result==satcheckt::P_SATISFIABLE);
-
-    ieee_floatt fres;
-    fres=float_utils.get(res);
-
-    if(!eq(fres, i3))
-    {
-      const char *opsym=binopsyms[op];
-      std::cout << i1 << opsym << i2 << " != " << fres << std::endl;
-      std::cout << f1 << opsym << f2 << " == " << f3 << std::endl;
-      std::cout << integer2binary(i1.get_exponent(), i1.spec.e) << " " <<
-                   integer2binary(i1.get_fraction(), i1.spec.f+1) << opsym <<
-                   integer2binary(i2.get_exponent(), i1.spec.e) << " " <<
-                   integer2binary(i2.get_fraction(), i1.spec.f+1) << " != " <<
-                   integer2binary(fres.get_exponent(), i1.spec.e) << " " <<
-                   integer2binary(fres.get_fraction(), i1.spec.f+1) << std::endl;
-      std::cout << integer2binary(i1.get_exponent(), i1.spec.e) << " " <<
-                   integer2binary(i1.get_fraction(), i1.spec.f+1) << opsym <<
-                   integer2binary(i2.get_exponent(), i1.spec.e) << " " <<
-                   integer2binary(i2.get_fraction(), i1.spec.f+1) << " == " <<
-                   integer2binary(i3.get_exponent(), i1.spec.e) << " " <<
-                   integer2binary(i3.get_fraction(), i1.spec.f+1) << std::endl;
-      std::cout << std::endl;
-    }
-  }
-}
diff --git a/unit/solvers/floatbv/float_utils.cpp b/unit/solvers/floatbv/float_utils.cpp
new file mode 100644
index 00000000000..fe82c3cbe7c
--- /dev/null
+++ b/unit/solvers/floatbv/float_utils.cpp
@@ -0,0 +1,219 @@
+/*******************************************************************\
+
+ Module: Unit tests for float utils and approximation
+
+ Author: Daniel Kroening
+
+\*******************************************************************/
+
+#include <testing-utils/catch.hpp>
+
+// for debug output in case of failure
+#include <iostream>
+#include <limits>
+#include <random>
+
+#include <solvers/floatbv/float_approximation.h>
+#include <solvers/floatbv/float_utils.h>
+#include <solvers/sat/satcheck.h>
+
+typedef std::uniform_int_distribution<unsigned> distt;
+
+static float random_float(distt &dist, std::mt19937 &gen)
+{
+  union
+  {
+    float f;
+    unsigned int i;
+  } u;
+
+  u.i = dist(gen);
+  u.i = (u.i << 16) ^ dist(gen);
+
+  return u.f;
+}
+
+static bool eq(const ieee_floatt &a, const ieee_floatt &b)
+{
+  return (a.is_NaN() && b.is_NaN()) ||
+         (a.is_infinity() && b.is_infinity() && a.get_sign() == b.get_sign()) ||
+         a == b;
+}
+
+#if 0
+static std::string to_str(const bvt &bv)
+{
+  std::string result;
+  for(unsigned i=0; i<bv.size(); i++)
+  {
+    char ch;
+    if(bv[i]==const_literal(true))
+      ch='1';
+    else if(bv[i]==const_literal(false))
+      ch='0';
+    else
+      ch='?';
+    result=ch+result;
+  }
+  return result;
+}
+#endif
+
+typedef enum { PLUS=0, MINUS=1, MULT=2, DIV=3 } binopt;
+const char *binopsyms[]={ " + ", " - ", " * ", " / " };
+
+static float set_values(
+  distt &dist,
+  std::mt19937 &gen,
+  float_utilst &float_utils,
+  float &f1,
+  float &f2,
+  ieee_floatt &i1,
+  ieee_floatt &i2)
+{
+  f1 = random_float(dist, gen);
+  f2 = random_float(dist, gen);
+  i1.from_float(f1);
+  i2.from_float(f2);
+  float_utils.spec = i1.spec;
+
+  return f1;
+}
+
+static bvt compute(
+  unsigned i,
+  float_utilst &float_utils,
+  const float &f2,
+  float &f3,
+  const ieee_floatt &i1,
+  const ieee_floatt &i2)
+{
+  const bvt b1 = float_utils.build_constant(i1);
+  const bvt b2 = float_utils.build_constant(i2);
+
+  const auto op = i % 3;
+
+  switch(op)
+  {
+  case PLUS:
+    f3 += f2;
+    return float_utils.add(b1, b2);
+
+  case MINUS:
+    f3 -= f2;
+    return float_utils.sub(b1, b2);
+
+  case MULT:
+    f3 *= f2;
+    return float_utils.mul(b1, b2);
+
+  case DIV:
+    f3 /= f2;
+    return float_utils.div(b1, b2);
+  }
+
+  return bvt();
+}
+
+static void print(
+  unsigned i,
+  const ieee_floatt &i1,
+  const ieee_floatt &i2,
+  const ieee_floatt &i3,
+  const ieee_floatt &fres,
+  const float &f1,
+  const float &f2,
+  const float &f3)
+{
+  const unsigned op = i % 3;
+  const char *opsym = binopsyms[op];
+
+  std::cout << i1 << opsym << i2 << " != " << fres << '\n';
+  std::cout << f1 << opsym << f2 << " == " << f3 << '\n';
+  std::cout << integer2binary(i1.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i1.get_fraction(), i1.spec.f + 1) << opsym
+            << integer2binary(i2.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i2.get_fraction(), i1.spec.f + 1) << " != "
+            << integer2binary(fres.get_exponent(), i1.spec.e) << " "
+            << integer2binary(fres.get_fraction(), i1.spec.f + 1) << '\n';
+  std::cout << integer2binary(i1.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i1.get_fraction(), i1.spec.f + 1) << opsym
+            << integer2binary(i2.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i2.get_fraction(), i1.spec.f + 1) << " == "
+            << integer2binary(i3.get_exponent(), i1.spec.e) << " "
+            << integer2binary(i3.get_fraction(), i1.spec.f + 1) << '\n';
+}
+
+SCENARIO("float_utils", "[core][solvers][floatbv][float_utils]")
+{
+  ieee_floatt i1, i2, i3;
+  float f1, f2, f3;
+
+  std::random_device rd;
+  std::mt19937 gen(rd());
+  distt dist(0, std::numeric_limits<unsigned>::max());
+
+  for(unsigned i = 0; i < 200; i++)
+  {
+    satcheckt satcheck;
+    float_utilst float_utils(satcheck);
+
+    GIVEN("Two random floating point numbers")
+    {
+      f3 = set_values(dist, gen, float_utils, f1, f2, i1, i2);
+      bvt res = compute(i, float_utils, f2, f3, i1, i2);
+
+      THEN("Machine execution yields the same result as symbolic computation")
+      {
+        i3.from_float(f3);
+
+        const satcheckt::resultt result = satcheck.prop_solve();
+        REQUIRE(result == satcheckt::resultt::P_SATISFIABLE);
+
+        const ieee_floatt fres = float_utils.get(res);
+
+        if(!eq(fres, i3))
+          print(i, i1, i2, i3, fres, f1, f2, f3);
+
+        REQUIRE(eq(fres, i3));
+      }
+    }
+  }
+}
+
+SCENARIO("float_approximation", "[core][solvers][floatbv][float_approximation]")
+{
+  ieee_floatt i1, i2, i3;
+  float f1, f2, f3;
+
+  std::random_device rd;
+  std::mt19937 gen(rd());
+  distt dist(0, std::numeric_limits<unsigned>::max());
+
+  for(unsigned i = 0; i < 200; i++)
+  {
+    satcheckt satcheck;
+    float_approximationt float_utils(satcheck);
+
+    GIVEN("Two random floating point numbers")
+    {
+      f3 = set_values(dist, gen, float_utils, f1, f2, i1, i2);
+      bvt res = compute(i, float_utils, f2, f3, i1, i2);
+
+      THEN("Machine execution yields the same result as symbolic computation")
+      {
+        i3.from_float(f3);
+
+        const satcheckt::resultt result = satcheck.prop_solve();
+        REQUIRE(result == satcheckt::resultt::P_SATISFIABLE);
+
+        const ieee_floatt fres = float_utils.get(res);
+
+        if(!eq(fres, i3))
+          print(i, i1, i2, i3, fres, f1, f2, f3);
+
+        REQUIRE(eq(fres, i3));
+      }
+    }
+  }
+}
diff --git a/unit/solvers/floatbv/module_dependencies.txt b/unit/solvers/floatbv/module_dependencies.txt
new file mode 100644
index 00000000000..1a7bba2910a
--- /dev/null
+++ b/unit/solvers/floatbv/module_dependencies.txt
@@ -0,0 +1,4 @@
+solvers/floatbv
+solvers/sat
+testing-utils
+util