diff --git a/jbmc/src/java_bytecode/assignments_from_json.cpp b/jbmc/src/java_bytecode/assignments_from_json.cpp
index d4e3f6e7308..dee711f00e6 100644
--- a/jbmc/src/java_bytecode/assignments_from_json.cpp
+++ b/jbmc/src/java_bytecode/assignments_from_json.cpp
@@ -358,13 +358,13 @@ assign_primitive_from_json(const exprt &expr, const jsont &json)
   }
   else if(expr.type() == java_double_type())
   {
-    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
+    ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_double(std::stod(json.value));
     result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }
   else if(expr.type() == java_float_type())
   {
-    ieee_floatt ieee_float(to_floatbv_type(expr.type()));
+    ieee_float_valuet ieee_float(to_floatbv_type(expr.type()));
     ieee_float.from_float(std::stof(json.value));
     result.add(code_frontend_assignt{expr, ieee_float.to_expr()});
   }
diff --git a/jbmc/src/java_bytecode/expr2java.cpp b/jbmc/src/java_bytecode/expr2java.cpp
index 376b331a573..67d3f33fdd0 100644
--- a/jbmc/src/java_bytecode/expr2java.cpp
+++ b/jbmc/src/java_bytecode/expr2java.cpp
@@ -230,7 +230,7 @@ std::string expr2javat::convert_constant(
           (src.type()==java_double_type()))
   {
     // This converts NaNs to the canonical NaN
-    const ieee_floatt ieee_repr(to_constant_expr(src));
+    const ieee_float_valuet ieee_repr(to_constant_expr(src));
     if(ieee_repr.is_double())
       return floating_point_to_java_string(ieee_repr.to_double());
     return floating_point_to_java_string(ieee_repr.to_float());
diff --git a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
index 1bae680fa5d..8d3c23d50f3 100644
--- a/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_convert_method.cpp
@@ -2181,16 +2181,19 @@ exprt::operandst &java_bytecode_convert_methodt::convert_const(
       is_float ? ieee_float_spect::single_precision()
                : ieee_float_spect::double_precision());
 
-    ieee_floatt value(spec);
     if(arg0.type().id() != ID_floatbv)
     {
+      // conversion from integer to float may need rounding
+      auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
       const mp_integer number = numeric_cast_v<mp_integer>(arg0);
+      ieee_floatt value(spec, rm);
       value.from_integer(number);
+      results[0] = value.to_expr();
     }
     else
-      value.from_expr(arg0);
-
-    results[0] = value.to_expr();
+    {
+      results[0] = ieee_float_valuet{arg0}.to_expr();
+    }
   }
   else
   {
diff --git a/jbmc/src/java_bytecode/java_bytecode_parser.cpp b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
index ccf9375e717..e036b06bdc4 100644
--- a/jbmc/src/java_bytecode/java_bytecode_parser.cpp
+++ b/jbmc/src/java_bytecode/java_bytecode_parser.cpp
@@ -782,7 +782,7 @@ void java_bytecode_parsert::rconstant_pool()
 
       case CONSTANT_Float:
       {
-        ieee_floatt value(ieee_float_spect::single_precision());
+        ieee_float_valuet value(ieee_float_spect::single_precision());
         value.unpack(entry.number);
         entry.expr = value.to_expr();
       }
@@ -794,7 +794,7 @@ void java_bytecode_parsert::rconstant_pool()
 
       case CONSTANT_Double:
       {
-        ieee_floatt value(ieee_float_spect::double_precision());
+        ieee_float_valuet value(ieee_float_spect::double_precision());
         value.unpack(entry.number);
         entry.expr = value.to_expr();
       }
diff --git a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
index 7a3f10d403f..18106895546 100644
--- a/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
+++ b/jbmc/src/java_bytecode/java_string_library_preprocess.cpp
@@ -938,7 +938,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
 
   // Expression representing 0.0
   const ieee_float_spect float_spec{to_floatbv_type(params[0].type())};
-  ieee_floatt zero_float(float_spec);
+  ieee_float_valuet zero_float(float_spec);
   zero_float.from_float(0.0);
   const constant_exprt zero = zero_float.to_expr();
 
@@ -996,7 +996,7 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   string_expr_list.push_back(zero_string);
 
   // Case of -0.0
-  ieee_floatt minus_zero_float(float_spec);
+  ieee_float_valuet minus_zero_float(float_spec);
   minus_zero_float.from_float(-0.0f);
   condition_list.push_back(equal_exprt(arg, minus_zero_float.to_expr()));
   const refined_string_exprt minus_zero_string =
@@ -1004,8 +1004,9 @@ code_blockt java_string_library_preprocesst::make_float_to_string_code(
   string_expr_list.push_back(minus_zero_string);
 
   // Case of simple notation
-  ieee_floatt bound_inf_float(float_spec);
-  ieee_floatt bound_sup_float(float_spec);
+  auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+  ieee_floatt bound_inf_float(float_spec, rm);
+  ieee_floatt bound_sup_float(float_spec, rm);
   bound_inf_float.from_float(1e-3f);
   bound_sup_float.from_float(1e7f);
   bound_inf_float.change_spec(float_spec);
diff --git a/src/analyses/interval_domain.cpp b/src/analyses/interval_domain.cpp
index 4594a4d2e94..ed1fb8acd1f 100644
--- a/src/analyses/interval_domain.cpp
+++ b/src/analyses/interval_domain.cpp
@@ -288,7 +288,7 @@ void interval_domaint::assume_rec(
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {
-      ieee_floatt tmp(to_constant_expr(rhs));
+      ieee_float_valuet tmp(to_constant_expr(rhs));
       if(id==ID_lt)
         tmp.decrement();
       ieee_float_intervalt &fi=float_map[lhs_identifier];
@@ -313,7 +313,7 @@ void interval_domaint::assume_rec(
     }
     else if(is_float(lhs.type()) && is_float(rhs.type()))
     {
-      ieee_floatt tmp(to_constant_expr(lhs));
+      ieee_float_valuet tmp(to_constant_expr(lhs));
       if(id==ID_lt)
         tmp.increment();
       ieee_float_intervalt &fi=float_map[rhs_identifier];
diff --git a/src/analyses/interval_domain.h b/src/analyses/interval_domain.h
index e6a21f76d18..31638097c4a 100644
--- a/src/analyses/interval_domain.h
+++ b/src/analyses/interval_domain.h
@@ -18,7 +18,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "ai_domain.h"
 
-typedef interval_templatet<ieee_floatt> ieee_float_intervalt;
+typedef interval_templatet<ieee_float_valuet> ieee_float_intervalt;
 
 class interval_domaint:public ai_domain_baset
 {
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 07003ead306..6a390a2100f 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -1912,7 +1912,7 @@ std::string expr2ct::convert_constant(
   }
   else if(type.id()==ID_floatbv)
   {
-    dest=ieee_floatt(to_constant_expr(src)).to_ansi_c_string();
+    dest = ieee_float_valuet(to_constant_expr(src)).to_ansi_c_string();
 
     if(!dest.empty() && isdigit(dest[dest.size() - 1]))
     {
diff --git a/src/ansi-c/goto-conversion/goto_check_c.cpp b/src/ansi-c/goto-conversion/goto_check_c.cpp
index aadac285968..6ff092e2555 100644
--- a/src/ansi-c/goto-conversion/goto_check_c.cpp
+++ b/src/ansi-c/goto-conversion/goto_check_c.cpp
@@ -761,12 +761,13 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
       else if(old_type.id() == ID_floatbv) // float -> signed
       {
         // Note that the fractional part is truncated!
-        ieee_floatt upper(to_floatbv_type(old_type));
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt upper(to_floatbv_type(old_type), rm);
         upper.from_integer(power(2, new_width - 1));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());
 
-        ieee_floatt lower(to_floatbv_type(old_type));
+        ieee_floatt lower(to_floatbv_type(old_type), rm);
         lower.from_integer(-power(2, new_width - 1) - 1);
         const binary_relation_exprt no_overflow_lower(
           op, ID_gt, lower.to_expr());
@@ -844,12 +845,13 @@ void goto_check_ct::conversion_check(const exprt &expr, const guardt &guard)
       else if(old_type.id() == ID_floatbv) // float -> unsigned
       {
         // Note that the fractional part is truncated!
-        ieee_floatt upper(to_floatbv_type(old_type));
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt upper(to_floatbv_type(old_type), rm);
         upper.from_integer(power(2, new_width));
         const binary_relation_exprt no_overflow_upper(
           op, ID_lt, upper.to_expr());
 
-        ieee_floatt lower(to_floatbv_type(old_type));
+        ieee_floatt lower(to_floatbv_type(old_type), rm);
         lower.from_integer(-1);
         const binary_relation_exprt no_overflow_lower(
           op, ID_gt, lower.to_expr());
@@ -1295,8 +1297,8 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
     // -inf + +inf = NaN and +inf + -inf = NaN,
     // i.e., signs differ
     ieee_float_spect spec = ieee_float_spect(to_floatbv_type(plus_expr.type()));
-    exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
-    exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
+    exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
+    exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
 
     isnan = or_exprt(
       and_exprt(
@@ -1315,8 +1317,8 @@ void goto_check_ct::nan_check(const exprt &expr, const guardt &guard)
 
     ieee_float_spect spec =
       ieee_float_spect(to_floatbv_type(minus_expr.type()));
-    exprt plus_inf = ieee_floatt::plus_infinity(spec).to_expr();
-    exprt minus_inf = ieee_floatt::minus_infinity(spec).to_expr();
+    exprt plus_inf = ieee_float_valuet::plus_infinity(spec).to_expr();
+    exprt minus_inf = ieee_float_valuet::minus_infinity(spec).to_expr();
 
     isnan = or_exprt(
       and_exprt(
diff --git a/src/ansi-c/literals/convert_float_literal.cpp b/src/ansi-c/literals/convert_float_literal.cpp
index 283a852c074..46040693dbe 100644
--- a/src/ansi-c/literals/convert_float_literal.cpp
+++ b/src/ansi-c/literals/convert_float_literal.cpp
@@ -71,7 +71,9 @@ exprt convert_float_literal(const std::string &src)
     // but these aren't handled anywhere
   }
 
-  ieee_floatt a(type);
+  // This may require rounding.
+  auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+  ieee_floatt a(type, rm);
 
   if(parsed_float.exponent_base==10)
     a.from_base10(parsed_float.significand, parsed_float.exponent);
diff --git a/src/goto-instrument/goto_program2code.cpp b/src/goto-instrument/goto_program2code.cpp
index 6f18202d305..87edc71b678 100644
--- a/src/goto-instrument/goto_program2code.cpp
+++ b/src/goto-instrument/goto_program2code.cpp
@@ -1923,7 +1923,7 @@ void goto_program2codet::cleanup_expr(exprt &expr, bool no_typecast)
   {
     if(expr.type().id()==ID_floatbv)
     {
-      const ieee_floatt f(to_constant_expr(expr));
+      const ieee_float_valuet f(to_constant_expr(expr));
       if(f.is_NaN() || f.is_infinity())
         system_headers.insert("math.h");
     }
diff --git a/src/goto-programs/interpreter.cpp b/src/goto-programs/interpreter.cpp
index 3104f1d9de8..8ad54ddbf2d 100644
--- a/src/goto-programs/interpreter.cpp
+++ b/src/goto-programs/interpreter.cpp
@@ -576,7 +576,7 @@ exprt interpretert::get_value(
   }
   else if(type.id() == ID_floatbv)
   {
-    ieee_floatt f(to_floatbv_type(type));
+    ieee_float_valuet f(to_floatbv_type(type));
     f.unpack(rhs[numeric_cast_v<std::size_t>(offset)]);
     return f.to_expr();
   }
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 3cda7db79d0..72707e3692f 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -364,7 +364,7 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
     }
     else if(expr.type().id()==ID_floatbv)
     {
-      ieee_floatt f;
+      ieee_float_valuet f;
       f.from_expr(to_constant_expr(expr));
       return {f.pack()};
     }
@@ -731,8 +731,9 @@ interpretert::mp_vectort interpretert::evaluate(const exprt &expr)
         }
         else if(expr.type().id()==ID_floatbv)
         {
-          ieee_floatt f1(to_floatbv_type(expr.type()));
-          ieee_floatt f2(to_floatbv_type(op.type()));
+          auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+          ieee_floatt f1(to_floatbv_type(expr.type()), rm);
+          ieee_floatt f2(to_floatbv_type(op.type()), rm);
           f1.unpack(result);
           f2.unpack(tmp.front());
           f1*=f2;
diff --git a/src/goto-programs/json_expr.cpp b/src/goto-programs/json_expr.cpp
index 16139131b90..6331ebe2f6a 100644
--- a/src/goto-programs/json_expr.cpp
+++ b/src/goto-programs/json_expr.cpp
@@ -276,7 +276,7 @@ json_objectt json(const exprt &expr, const namespacet &ns, const irep_idt &mode)
         json_numbert(std::to_string(to_bitvector_type(type).get_width()));
       result["binary"] = json_stringt(binary(constant_expr));
       result["data"] =
-        json_stringt(ieee_floatt(constant_expr).to_ansi_c_string());
+        json_stringt(ieee_float_valuet(constant_expr).to_ansi_c_string());
     }
     else if(type.id() == ID_pointer)
     {
diff --git a/src/goto-programs/xml_expr.cpp b/src/goto-programs/xml_expr.cpp
index a07ce2cbe21..2cf54e5261f 100644
--- a/src/goto-programs/xml_expr.cpp
+++ b/src/goto-programs/xml_expr.cpp
@@ -212,7 +212,7 @@ xmlt xml(const exprt &expr, const namespacet &ns)
       result.set_attribute("width", width);
       result.set_attribute(
         "binary", integer2binary(bvrep2integer(value, width, false), width));
-      result.data = ieee_floatt(constant_expr).to_ansi_c_string();
+      result.data = ieee_float_valuet(constant_expr).to_ansi_c_string();
     }
     else if(type.id() == ID_pointer)
     {
diff --git a/src/solvers/floatbv/float_bv.cpp b/src/solvers/floatbv/float_bv.cpp
index 162f1e8cd0a..9450694fb43 100644
--- a/src/solvers/floatbv/float_bv.cpp
+++ b/src/solvers/floatbv/float_bv.cpp
@@ -240,7 +240,7 @@ exprt float_bvt::is_zero(const exprt &src)
 
   constant_exprt mask(integer2bvrep(v, width), src.type());
 
-  ieee_floatt z(type);
+  ieee_float_valuet z(type);
   z.make_zero();
 
   return equal_exprt(bitand_exprt(src, mask), z.to_expr());
diff --git a/src/solvers/floatbv/float_utils.cpp b/src/solvers/floatbv/float_utils.cpp
index 13706f06bd5..dc94a842226 100644
--- a/src/solvers/floatbv/float_utils.cpp
+++ b/src/solvers/floatbv/float_utils.cpp
@@ -136,7 +136,7 @@ bvt float_utilst::to_integer(
   return result;
 }
 
-bvt float_utilst::build_constant(const ieee_floatt &src)
+bvt float_utilst::build_constant(const ieee_float_valuet &src)
 {
   unbiased_floatt result;
 
@@ -1268,14 +1268,14 @@ bvt float_utilst::pack(const biased_floatt &src)
   return result;
 }
 
-ieee_floatt float_utilst::get(const bvt &src) const
+ieee_float_valuet float_utilst::get(const bvt &src) const
 {
   mp_integer int_value=0;
 
   for(std::size_t i=0; i<src.size(); i++)
     int_value+=power(2, i)*prop.l_get(src[i]).is_true();
 
-  ieee_floatt result;
+  ieee_float_valuet result;
   result.spec=spec;
   result.unpack(int_value);
 
diff --git a/src/solvers/floatbv/float_utils.h b/src/solvers/floatbv/float_utils.h
index 989c8d53377..875555c9120 100644
--- a/src/solvers/floatbv/float_utils.h
+++ b/src/solvers/floatbv/float_utils.h
@@ -87,7 +87,7 @@ class float_utilst
 
   ieee_float_spect spec;
 
-  bvt build_constant(const ieee_floatt &);
+  bvt build_constant(const ieee_float_valuet &);
 
   static inline literalt sign_bit(const bvt &src)
   {
@@ -139,7 +139,7 @@ class float_utilst
   literalt relation(const bvt &src1, relt rel, const bvt &src2);
 
   // constants
-  ieee_floatt get(const bvt &) const;
+  ieee_float_valuet get(const bvt &) const;
 
   // helpers
   literalt exponent_all_ones(const bvt &);
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index dba907efd9d..3aeb9598181 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -476,7 +476,8 @@ constant_exprt smt2_convt::parse_literal(
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::plus_infinity(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::plus_infinity(ieee_float_spect(s - 1, e))
+      .to_expr();
   }
   else if(src.get_sub().size()==4 &&
           src.get_sub()[0].id()=="_" &&
@@ -484,7 +485,8 @@ constant_exprt smt2_convt::parse_literal(
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::minus_infinity(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::minus_infinity(ieee_float_spect(s - 1, e))
+      .to_expr();
   }
   else if(src.get_sub().size()==4 &&
           src.get_sub()[0].id()=="_" &&
@@ -492,7 +494,7 @@ constant_exprt smt2_convt::parse_literal(
   {
     std::size_t e = unsafe_string2size_t(src.get_sub()[2].id_string());
     std::size_t s = unsafe_string2size_t(src.get_sub()[3].id_string());
-    return ieee_floatt::NaN(ieee_float_spect(s - 1, e)).to_expr();
+    return ieee_float_valuet::NaN(ieee_float_spect(s - 1, e)).to_expr();
   }
 
   if(type.id()==ID_signedbv ||
@@ -3445,7 +3447,7 @@ void smt2_convt::convert_constant(const constant_exprt &expr)
          significands including the hidden bit.  Thus some encoding
          is needed to get to IEEE-754 style representations. */
 
-      ieee_floatt v=ieee_floatt(expr);
+      ieee_float_valuet v = ieee_float_valuet(expr);
       size_t e=floatbv_type.get_e();
       size_t f=floatbv_type.get_f()+1;
 
diff --git a/src/solvers/smt2/smt2_format.cpp b/src/solvers/smt2/smt2_format.cpp
index 551f58f073c..a4771c632fe 100644
--- a/src/solvers/smt2/smt2_format.cpp
+++ b/src/solvers/smt2/smt2_format.cpp
@@ -93,7 +93,7 @@ std::ostream &smt2_format_rec(std::ostream &out, const exprt &expr)
     }
     else if(expr_type.id() == ID_floatbv)
     {
-      const ieee_floatt v = ieee_floatt(constant_expr);
+      const ieee_float_valuet v = ieee_float_valuet(constant_expr);
       const size_t e = v.spec.e;
       const size_t f = v.spec.f + 1; // SMT-LIB counts the hidden bit
 
diff --git a/src/solvers/strings/string_constraint_generator_float.cpp b/src/solvers/strings/string_constraint_generator_float.cpp
index ecc5e044b79..e33c5794a51 100644
--- a/src/solvers/strings/string_constraint_generator_float.cpp
+++ b/src/solvers/strings/string_constraint_generator_float.cpp
@@ -77,7 +77,7 @@ exprt get_significand(
 /// \return an expression representing this floating point
 exprt constant_float(const double f, const ieee_float_spect &float_spec)
 {
-  ieee_floatt fl(float_spec);
+  ieee_float_valuet fl(float_spec);
   if(float_spec == ieee_float_spect::single_precision())
     fl.from_float(f);
   else if(float_spec == ieee_float_spect::double_precision())
diff --git a/src/statement-list/converters/convert_real_literal.cpp b/src/statement-list/converters/convert_real_literal.cpp
index 555da5efe11..3d6d5f3d12e 100644
--- a/src/statement-list/converters/convert_real_literal.cpp
+++ b/src/statement-list/converters/convert_real_literal.cpp
@@ -18,7 +18,7 @@ Author: Matthias Weiss, matthias.weiss@diffblue.com
 
 constant_exprt convert_real_literal(const std::string &src)
 {
-  ieee_floatt real{get_real_type()};
+  ieee_float_valuet real{get_real_type()};
   real.from_float(std::stof(src));
   return real.to_expr();
 }
diff --git a/src/statement-list/statement_list_parse_tree_io.cpp b/src/statement-list/statement_list_parse_tree_io.cpp
index 82e6171814f..91dee4ec54b 100644
--- a/src/statement-list/statement_list_parse_tree_io.cpp
+++ b/src/statement-list/statement_list_parse_tree_io.cpp
@@ -31,7 +31,7 @@ static void output_constant(std::ostream &os, const constant_exprt &constant)
     os << ivalue;
   else if(can_cast_type<floatbv_typet>(constant.type()))
   {
-    ieee_floatt real{get_real_type()};
+    ieee_float_valuet real{get_real_type()};
     real.from_expr(constant);
     os << real.to_float();
   }
diff --git a/src/util/arith_tools.cpp b/src/util/arith_tools.cpp
index 73dc989bf99..7d40b77b60d 100644
--- a/src/util/arith_tools.cpp
+++ b/src/util/arith_tools.cpp
@@ -171,7 +171,9 @@ constant_exprt from_integer(
   }
   else if(type_id==ID_floatbv)
   {
-    ieee_floatt ieee_float(to_floatbv_type(type));
+    ieee_floatt ieee_float(
+      to_floatbv_type(type), ieee_floatt::rounding_modet::ROUND_TO_EVEN);
+    // always rounds to zero
     ieee_float.from_integer(int_value);
     return ieee_float.to_expr();
   }
diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index bb9c814a496..a3d0776b07a 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -75,7 +75,7 @@ bool exprt::is_zero() const
     }
     else if(type_id==ID_floatbv)
     {
-      if(ieee_floatt(constant)==0)
+      if(ieee_float_valuet(constant) == 0)
         return true;
     }
     else if(type_id==ID_pointer)
@@ -131,7 +131,7 @@ bool exprt::is_one() const
     }
     else if(type_id==ID_floatbv)
     {
-      if(ieee_floatt(constant_expr) == 1)
+      if(ieee_float_valuet(constant_expr) == 1)
         return true;
     }
   }
diff --git a/src/util/format_constant.cpp b/src/util/format_constant.cpp
index 6fa62c898fb..39f94e3f832 100644
--- a/src/util/format_constant.cpp
+++ b/src/util/format_constant.cpp
@@ -36,7 +36,7 @@ std::string format_constantt::operator()(const exprt &expr)
     }
     else if(expr.type().id()==ID_floatbv)
     {
-      return ieee_floatt(to_constant_expr(expr)).format(*this);
+      return ieee_float_valuet(to_constant_expr(expr)).format(*this);
     }
   }
   else if(expr.id()==ID_string_constant)
diff --git a/src/util/format_expr.cpp b/src/util/format_expr.cpp
index eb32bf90351..55118640c91 100644
--- a/src/util/format_expr.cpp
+++ b/src/util/format_expr.cpp
@@ -207,7 +207,7 @@ static std::ostream &format_rec(std::ostream &os, const constant_exprt &src)
   else if(type == ID_string)
     return os << '"' << escape(id2string(src.get_value())) << '"';
   else if(type == ID_floatbv)
-    return os << ieee_floatt(src);
+    return os << ieee_float_valuet(src);
   else if(type == ID_pointer)
   {
     if(src.is_null_pointer())
diff --git a/src/util/ieee_float.cpp b/src/util/ieee_float.cpp
index 050e51d03f9..a4874830994 100644
--- a/src/util/ieee_float.cpp
+++ b/src/util/ieee_float.cpp
@@ -57,17 +57,12 @@ void ieee_float_spect::from_type(const floatbv_typet &type)
     e=e-1; // no hidden bit
 }
 
-constant_exprt ieee_floatt::rounding_mode_expr(rounding_modet rm)
-{
-  return floatbv_rounding_mode(static_cast<unsigned>(rm));
-}
-
-void ieee_floatt::print(std::ostream &out) const
+void ieee_float_valuet::print(std::ostream &out) const
 {
   out << to_ansi_c_string();
 }
 
-std::string ieee_floatt::format(const format_spect &format_spec) const
+std::string ieee_float_valuet::format(const format_spect &format_spec) const
 {
   std::string result;
 
@@ -127,7 +122,7 @@ std::string ieee_floatt::format(const format_spect &format_spec) const
   return result;
 }
 
-mp_integer ieee_floatt::base10_digits(const mp_integer &src)
+mp_integer ieee_float_valuet::base10_digits(const mp_integer &src)
 {
   PRECONDITION(src >= 0);
   mp_integer tmp=src;
@@ -136,7 +131,7 @@ mp_integer ieee_floatt::base10_digits(const mp_integer &src)
   return result;
 }
 
-std::string ieee_floatt::to_string_decimal(std::size_t precision) const
+std::string ieee_float_valuet::to_string_decimal(std::size_t precision) const
 {
   std::string result;
 
@@ -230,7 +225,7 @@ std::string ieee_floatt::to_string_decimal(std::size_t precision) const
 
 /// format as [-]d.ddde+-d Note that printf always produces at least two digits
 /// for the exponent.
-std::string ieee_floatt::to_string_scientific(std::size_t precision) const
+std::string ieee_float_valuet::to_string_scientific(std::size_t precision) const
 {
   std::string result;
 
@@ -317,7 +312,7 @@ std::string ieee_floatt::to_string_scientific(std::size_t precision) const
   return result;
 }
 
-void ieee_floatt::unpack(const mp_integer &i)
+void ieee_float_valuet::unpack(const mp_integer &i)
 {
   PRECONDITION(spec.f != 0);
   PRECONDITION(spec.e != 0);
@@ -367,12 +362,12 @@ void ieee_floatt::unpack(const mp_integer &i)
   }
 }
 
-bool ieee_floatt::is_normal() const
+bool ieee_float_valuet::is_normal() const
 {
   return fraction>=power(2, spec.f);
 }
 
-mp_integer ieee_floatt::pack() const
+mp_integer ieee_float_valuet::pack() const
 {
   mp_integer result=0;
 
@@ -410,7 +405,7 @@ mp_integer ieee_floatt::pack() const
   return result;
 }
 
-void ieee_floatt::extract_base2(
+void ieee_float_valuet::extract_base2(
   mp_integer &_fraction,
   mp_integer &_exponent) const
 {
@@ -434,7 +429,7 @@ void ieee_floatt::extract_base2(
   }
 }
 
-void ieee_floatt::extract_base10(
+void ieee_float_valuet::extract_base10(
   mp_integer &_fraction,
   mp_integer &_exponent) const
 {
@@ -470,19 +465,97 @@ void ieee_floatt::extract_base10(
   }
 }
 
-ieee_floatt ieee_floatt::one(const ieee_float_spect &spec)
+ieee_float_valuet ieee_float_valuet::one(const ieee_float_spect &spec)
 {
-  ieee_floatt result{spec};
+  ieee_float_valuet result{spec};
   result.exponent = 0;
   result.fraction = power(2, result.spec.f);
   return result;
 }
 
-ieee_floatt ieee_floatt::one(const floatbv_typet &type)
+ieee_float_valuet ieee_float_valuet::one(const floatbv_typet &type)
 {
   return one(ieee_float_spect{type});
 }
 
+/// Note that calling from_double -> to_double can return different bit patterns
+/// for NaN.
+double ieee_float_valuet::to_double() const
+{
+  PRECONDITION(spec == ieee_float_spect::double_precision());
+  union
+  {
+    double f;
+    uint64_t i;
+  } a;
+
+  if(infinity_flag)
+  {
+    if(sign_flag)
+      return -std::numeric_limits<double>::infinity();
+    else
+      return std::numeric_limits<double>::infinity();
+  }
+
+  if(NaN_flag)
+  {
+    if(sign_flag)
+      return -std::numeric_limits<double>::quiet_NaN();
+    else
+      return std::numeric_limits<double>::quiet_NaN();
+  }
+
+  mp_integer i = pack();
+  CHECK_RETURN(i.is_ulong());
+  CHECK_RETURN(i <= std::numeric_limits<std::uint64_t>::max());
+
+  a.i = i.to_ulong();
+  return a.f;
+}
+
+/// Note that calling from_float -> to_float can return different bit patterns
+/// for NaN.
+float ieee_float_valuet::to_float() const
+{
+  // if false - ieee_floatt::to_float not supported on this architecture
+  static_assert(
+    std::numeric_limits<float>::is_iec559,
+    "this requires the float layout is according to the IEC 559/IEEE 754 "
+    "standard");
+  static_assert(
+    sizeof(float) == sizeof(uint32_t), "a 32 bit float type is required");
+
+  union
+  {
+    float f;
+    uint32_t i;
+  } a;
+
+  if(infinity_flag)
+  {
+    if(sign_flag)
+      return -std::numeric_limits<float>::infinity();
+    else
+      return std::numeric_limits<float>::infinity();
+  }
+
+  if(NaN_flag)
+  {
+    if(sign_flag)
+      return -std::numeric_limits<float>::quiet_NaN();
+    else
+      return std::numeric_limits<float>::quiet_NaN();
+  }
+
+  a.i = numeric_cast_v<uint32_t>(pack());
+  return a.f;
+}
+
+constant_exprt ieee_floatt::rounding_mode_expr(rounding_modet rm)
+{
+  return floatbv_rounding_mode(static_cast<unsigned>(rm));
+}
+
 void ieee_floatt::build(
   const mp_integer &_fraction,
   const mp_integer &_exponent)
@@ -496,6 +569,196 @@ void ieee_floatt::build(
   align();
 }
 
+constant_exprt ieee_float_valuet::to_expr() const
+{
+  return constant_exprt(integer2bvrep(pack(), spec.width()), spec.to_type());
+}
+
+bool ieee_float_valuet::operator<(const ieee_float_valuet &other) const
+{
+  PRECONDITION(other.spec == spec);
+
+  if(NaN_flag || other.NaN_flag)
+    return false;
+
+  // check both zero?
+  if(is_zero() && other.is_zero())
+    return false;
+
+  // one of them zero?
+  if(is_zero())
+    return !other.sign_flag;
+  else if(other.is_zero())
+    return sign_flag;
+
+  // check sign
+  if(sign_flag != other.sign_flag)
+    return sign_flag;
+
+  // handle infinity
+  if(infinity_flag)
+  {
+    if(other.infinity_flag)
+      return false;
+    else
+      return sign_flag;
+  }
+  else if(other.infinity_flag)
+    return !sign_flag;
+
+  // check exponent
+  if(exponent != other.exponent)
+  {
+    if(sign_flag) // both negative
+      return exponent > other.exponent;
+    else
+      return exponent < other.exponent;
+  }
+
+  // check significand
+  if(sign_flag) // both negative
+    return fraction > other.fraction;
+  else
+    return fraction < other.fraction;
+}
+
+bool ieee_float_valuet::operator<=(const ieee_float_valuet &other) const
+{
+  PRECONDITION(other.spec == spec);
+
+  if(NaN_flag || other.NaN_flag)
+    return false;
+
+  // check zero
+  if(is_zero() && other.is_zero())
+    return true;
+
+  // handle infinity
+  if(infinity_flag && other.infinity_flag && sign_flag == other.sign_flag)
+    return true;
+
+  if(
+    !infinity_flag && !other.infinity_flag && sign_flag == other.sign_flag &&
+    exponent == other.exponent && fraction == other.fraction)
+    return true;
+
+  return *this < other;
+}
+
+bool ieee_float_valuet::operator>(const ieee_float_valuet &other) const
+{
+  return other < *this;
+}
+
+bool ieee_float_valuet::operator>=(const ieee_float_valuet &other) const
+{
+  return other <= *this;
+}
+
+bool ieee_float_valuet::operator==(const ieee_float_valuet &other) const
+{
+  PRECONDITION(other.spec == spec);
+
+  // packed equality!
+  if(NaN_flag && other.NaN_flag)
+    return true;
+  else if(NaN_flag || other.NaN_flag)
+    return false;
+
+  if(infinity_flag && other.infinity_flag && sign_flag == other.sign_flag)
+    return true;
+  else if(infinity_flag || other.infinity_flag)
+    return false;
+
+  // if(a.is_zero() && b.is_zero()) return true;
+
+  return exponent == other.exponent && fraction == other.fraction &&
+         sign_flag == other.sign_flag;
+}
+
+bool ieee_float_valuet::ieee_equal(const ieee_float_valuet &other) const
+{
+  PRECONDITION(other.spec == spec);
+
+  if(NaN_flag || other.NaN_flag)
+    return false;
+  if(is_zero() && other.is_zero())
+    return true;
+  PRECONDITION(spec == other.spec);
+  return *this == other;
+}
+
+bool ieee_float_valuet::operator==(int i) const
+{
+  auto rm = ieee_floatt::rounding_modet::ROUND_TO_ZERO;
+  ieee_floatt other(spec, rm);
+  other.from_integer(i);
+  return *this == other;
+}
+
+bool ieee_float_valuet::operator!=(const ieee_float_valuet &other) const
+{
+  return !(*this == other);
+}
+
+bool ieee_float_valuet::ieee_not_equal(const ieee_float_valuet &other) const
+{
+  PRECONDITION(other.spec == spec);
+
+  if(NaN_flag || other.NaN_flag)
+    return true; // !!!
+  if(is_zero() && other.is_zero())
+    return false;
+  PRECONDITION(spec == other.spec);
+  return *this != other;
+}
+
+/// Sets *this to the next representable number closer to plus infinity (greater
+/// = true) or minus infinity (greater = false).
+void ieee_float_valuet::next_representable(bool greater)
+{
+  if(is_NaN())
+    return;
+
+  bool old_sign = get_sign();
+
+  if(is_zero())
+  {
+    unpack(1);
+    set_sign(!greater);
+
+    return;
+  }
+
+  if(is_infinity())
+  {
+    if(get_sign() == greater)
+    {
+      make_fltmax();
+      set_sign(old_sign);
+    }
+    return;
+  }
+
+  bool dir;
+  if(greater)
+    dir = !get_sign();
+  else
+    dir = get_sign();
+
+  set_sign(false);
+
+  mp_integer old = pack();
+  if(dir)
+    ++old;
+  else
+    --old;
+
+  unpack(old);
+
+  // sign change impossible (zero case caught earlier)
+  set_sign(old_sign);
+}
 /// compute f * (10^e)
 void ieee_floatt::from_base10(
   const mp_integer &_fraction,
@@ -595,7 +858,7 @@ void ieee_floatt::align()
   if(biased_exponent>=spec.max_exponent())
   {
     // we need to consider the rounding mode here
-    switch(rounding_mode)
+    switch(rounding_mode())
     {
     case UNKNOWN:
     case NONDETERMINISTIC:
@@ -671,7 +934,7 @@ void ieee_floatt::divide_and_round(
 
   if(remainder!=0)
   {
-    switch(rounding_mode)
+    switch(rounding_mode())
     {
     case ROUND_TO_EVEN:
       {
@@ -713,11 +976,6 @@ void ieee_floatt::divide_and_round(
   }
 }
 
-constant_exprt ieee_floatt::to_expr() const
-{
-  return constant_exprt(integer2bvrep(pack(), spec.width()), spec.to_type());
-}
-
 ieee_floatt &ieee_floatt::operator/=(const ieee_floatt &other)
 {
   PRECONDITION(other.spec.f == spec.f);
@@ -861,7 +1119,7 @@ ieee_floatt &ieee_floatt::operator+=(const ieee_floatt &other)
       return *this;
     else
     {
-      if(rounding_mode==ROUND_TO_MINUS_INF)
+      if(rounding_mode()==ROUND_TO_MINUS_INF)
       {
         set_sign(true);
         return *this;
@@ -902,7 +1160,7 @@ ieee_floatt &ieee_floatt::operator+=(const ieee_floatt &other)
   // there is some set of rules to get the sign
   if(fraction==0)
   {
-    if(rounding_mode==ROUND_TO_MINUS_INF)
+    if(rounding_mode()==ROUND_TO_MINUS_INF)
       sign_flag=true;
     else
       sign_flag=false;
@@ -926,149 +1184,6 @@ ieee_floatt &ieee_floatt::operator-=(const ieee_floatt &other)
   return (*this)+=_other;
 }
 
-bool ieee_floatt::operator<(const ieee_floatt &other) const
-{
-  PRECONDITION(other.spec == spec);
-
-  if(NaN_flag || other.NaN_flag)
-    return false;
-
-  // check both zero?
-  if(is_zero() && other.is_zero())
-    return false;
-
-  // one of them zero?
-  if(is_zero())
-    return !other.sign_flag;
-  else if(other.is_zero())
-    return sign_flag;
-
-  // check sign
-  if(sign_flag!=other.sign_flag)
-    return sign_flag;
-
-  // handle infinity
-  if(infinity_flag)
-  {
-    if(other.infinity_flag)
-      return false;
-    else
-      return sign_flag;
-  }
-  else if(other.infinity_flag)
-    return !sign_flag;
-
-  // check exponent
-  if(exponent!=other.exponent)
-  {
-    if(sign_flag) // both negative
-      return exponent>other.exponent;
-    else
-      return exponent<other.exponent;
-  }
-
-  // check significand
-  if(sign_flag) // both negative
-    return fraction>other.fraction;
-  else
-    return fraction<other.fraction;
-}
-
-bool ieee_floatt::operator<=(const ieee_floatt &other) const
-{
-  PRECONDITION(other.spec == spec);
-
-  if(NaN_flag || other.NaN_flag)
-    return false;
-
-  // check zero
-  if(is_zero() && other.is_zero())
-    return true;
-
-  // handle infinity
-  if(infinity_flag && other.infinity_flag &&
-     sign_flag==other.sign_flag)
-    return true;
-
-  if(!infinity_flag && !other.infinity_flag &&
-     sign_flag==other.sign_flag &&
-     exponent==other.exponent &&
-     fraction==other.fraction)
-    return true;
-
-  return *this<other;
-}
-
-bool ieee_floatt::operator>(const ieee_floatt &other) const
-{
-  return other<*this;
-}
-
-bool ieee_floatt::operator>=(const ieee_floatt &other) const
-{
-  return other<=*this;
-}
-
-bool ieee_floatt::operator==(const ieee_floatt &other) const
-{
-  PRECONDITION(other.spec == spec);
-
-  // packed equality!
-  if(NaN_flag && other.NaN_flag)
-    return true;
-  else if(NaN_flag || other.NaN_flag)
-    return false;
-
-  if(infinity_flag && other.infinity_flag &&
-     sign_flag==other.sign_flag)
-    return true;
-  else if(infinity_flag || other.infinity_flag)
-    return false;
-
-  // if(a.is_zero() && b.is_zero()) return true;
-
-  return
-    exponent==other.exponent &&
-    fraction==other.fraction &&
-    sign_flag==other.sign_flag;
-}
-
-bool ieee_floatt::ieee_equal(const ieee_floatt &other) const
-{
-  PRECONDITION(other.spec == spec);
-
-  if(NaN_flag || other.NaN_flag)
-    return false;
-  if(is_zero() && other.is_zero())
-    return true;
-  PRECONDITION(spec == other.spec);
-  return *this==other;
-}
-
-bool ieee_floatt::operator==(int i) const
-{
-  ieee_floatt other(spec);
-  other.from_integer(i);
-  return *this==other;
-}
-
-bool ieee_floatt::operator!=(const ieee_floatt &other) const
-{
-  return !(*this==other);
-}
-
-bool ieee_floatt::ieee_not_equal(const ieee_floatt &other) const
-{
-  PRECONDITION(other.spec == spec);
-
-  if(NaN_flag || other.NaN_flag)
-    return true; // !!!
-  if(is_zero() && other.is_zero())
-    return false;
-  PRECONDITION(spec == other.spec);
-  return *this!=other;
-}
-
 void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
 {
   mp_integer _exponent=exponent-spec.f;
@@ -1088,7 +1203,7 @@ void ieee_floatt::change_spec(const ieee_float_spect &dest_spec)
     build(_fraction, _exponent);
 }
 
-void ieee_floatt::from_expr(const constant_exprt &expr)
+void ieee_float_valuet::from_expr(const constant_exprt &expr)
 {
   spec=ieee_float_spect(to_floatbv_type(expr.type()));
   unpack(bvrep2integer(expr.get_value(), spec.width(), false));
@@ -1115,7 +1230,7 @@ mp_integer ieee_floatt::to_integer() const
   return result;
 }
 
-void ieee_floatt::from_double(const double d)
+void ieee_float_valuet::from_double(const double d)
 {
   spec.f=52;
   spec.e=11;
@@ -1139,7 +1254,7 @@ void ieee_floatt::from_double(const double d)
   unpack(u.i);
 }
 
-void ieee_floatt::from_float(const float f)
+void ieee_float_valuet::from_float(const float f)
 {
   spec.f=23;
   spec.e=8;
@@ -1163,7 +1278,7 @@ void ieee_floatt::from_float(const float f)
   unpack(u.i);
 }
 
-void ieee_floatt::make_NaN()
+void ieee_float_valuet::make_NaN()
 {
   NaN_flag=true;
   // sign=false;
@@ -1172,19 +1287,19 @@ void ieee_floatt::make_NaN()
   infinity_flag=false;
 }
 
-void ieee_floatt::make_fltmax()
+void ieee_float_valuet::make_fltmax()
 {
   mp_integer bit_pattern=
     power(2, spec.e+spec.f)-1-power(2, spec.f);
   unpack(bit_pattern);
 }
 
-void ieee_floatt::make_fltmin()
+void ieee_float_valuet::make_fltmin()
 {
   unpack(power(2, spec.f));
 }
 
-void ieee_floatt::make_plus_infinity()
+void ieee_float_valuet::make_plus_infinity()
 {
   NaN_flag=false;
   sign_flag=false;
@@ -1193,130 +1308,18 @@ void ieee_floatt::make_plus_infinity()
   infinity_flag=true;
 }
 
-void ieee_floatt::make_minus_infinity()
+void ieee_float_valuet::make_minus_infinity()
 {
   make_plus_infinity();
   sign_flag=true;
 }
 
-bool ieee_floatt::is_double() const
+bool ieee_float_valuet::is_double() const
 {
   return spec.f==52 && spec.e==11;
 }
 
-bool ieee_floatt::is_float() const
+bool ieee_float_valuet::is_float() const
 {
   return spec.f==23 && spec.e==8;
 }
-
-/// Note that calling from_double -> to_double can return different bit patterns
-/// for NaN.
-double ieee_floatt::to_double() const
-{
-  PRECONDITION(spec == ieee_float_spect::double_precision());
-  union { double f; uint64_t i; } a;
-
-  if(infinity_flag)
-  {
-    if(sign_flag)
-      return -std::numeric_limits<double>::infinity();
-    else
-      return std::numeric_limits<double>::infinity();
-  }
-
-  if(NaN_flag)
-  {
-    if(sign_flag)
-      return -std::numeric_limits<double>::quiet_NaN();
-    else
-      return std::numeric_limits<double>::quiet_NaN();
-  }
-
-  mp_integer i=pack();
-  CHECK_RETURN(i.is_ulong());
-  CHECK_RETURN(i <= std::numeric_limits<std::uint64_t>::max());
-
-  a.i=i.to_ulong();
-  return a.f;
-}
-
-/// Note that calling from_float -> to_float can return different bit patterns
-/// for NaN.
-float ieee_floatt::to_float() const
-{
-  // if false - ieee_floatt::to_float not supported on this architecture
-  static_assert(
-    std::numeric_limits<float>::is_iec559,
-    "this requires the float layout is according to the IEC 559/IEEE 754 "
-    "standard");
-  static_assert(
-    sizeof(float) == sizeof(uint32_t), "a 32 bit float type is required");
-
-  union { float f; uint32_t i; } a;
-
-  if(infinity_flag)
-  {
-    if(sign_flag)
-      return -std::numeric_limits<float>::infinity();
-    else
-      return std::numeric_limits<float>::infinity();
-  }
-
-  if(NaN_flag)
-  {
-    if(sign_flag)
-      return -std::numeric_limits<float>::quiet_NaN();
-    else
-      return std::numeric_limits<float>::quiet_NaN();
-  }
-
-  a.i = numeric_cast_v<uint32_t>(pack());
-  return a.f;
-}
-
-/// Sets *this to the next representable number closer to plus infinity (greater
-/// = true) or minus infinity (greater = false).
-void ieee_floatt::next_representable(bool greater)
-{
-  if(is_NaN())
-    return;
-
-  bool old_sign=get_sign();
-
-  if(is_zero())
-  {
-    unpack(1);
-    set_sign(!greater);
-
-    return;
-  }
-
-  if(is_infinity())
-  {
-    if(get_sign()==greater)
-    {
-      make_fltmax();
-      set_sign(old_sign);
-    }
-    return;
-  }
-
-  bool dir;
-  if(greater)
-    dir=!get_sign();
-  else
-    dir=get_sign();
-
-  set_sign(false);
-
-  mp_integer old=pack();
-  if(dir)
-    ++old;
-  else
-    --old;
-
-  unpack(old);
-
-  // sign change impossible (zero case caught earlier)
-  set_sign(old_sign);
-}
diff --git a/src/util/ieee_float.h b/src/util/ieee_float.h
index 8f1696291b9..927998c2ec6 100644
--- a/src/util/ieee_float.h
+++ b/src/util/ieee_float.h
@@ -112,28 +112,14 @@ class ieee_float_spect
   }
 };
 
-class ieee_floatt
+/// An IEEE 754 floating-point value, including specificiation.
+class ieee_float_valuet
 {
 public:
-  // ROUND_TO_EVEN is also known as "round to nearest, ties to even", and
-  // is the IEEE default.
-  // The numbering below is what x86 uses in the control word and
-  // what is recommended in C11 5.2.4.2.2
-  enum rounding_modet
-  {
-    ROUND_TO_EVEN=0, ROUND_TO_MINUS_INF=1,
-    ROUND_TO_PLUS_INF=2,  ROUND_TO_ZERO=3,
-    UNKNOWN, NONDETERMINISTIC
-  };
-
-  // A helper to turn a rounding mode into a constant bitvector expression
-  static constant_exprt rounding_mode_expr(rounding_modet);
-
   ieee_float_spect spec;
 
-  explicit ieee_floatt(const ieee_float_spect &_spec)
+  explicit ieee_float_valuet(const ieee_float_spect &_spec)
     : spec(_spec),
-      rounding_mode(ROUND_TO_EVEN),
       sign_flag(false),
       exponent(0),
       fraction(0),
@@ -142,9 +128,8 @@ class ieee_floatt
   {
   }
 
-  ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
-    : spec(std::move(__spec)),
-      rounding_mode(__rounding_mode),
+  explicit ieee_float_valuet(const floatbv_typet &type)
+    : spec(ieee_float_spect(type)),
       sign_flag(false),
       exponent(0),
       fraction(0),
@@ -153,23 +138,13 @@ class ieee_floatt
   {
   }
 
-  explicit ieee_floatt(const floatbv_typet &type)
-    : spec(ieee_float_spect(type)),
-      rounding_mode(ROUND_TO_EVEN),
-      sign_flag(false),
-      exponent(0),
-      fraction(0),
-      NaN_flag(false),
-      infinity_flag(false)
+  explicit ieee_float_valuet(const constant_exprt &expr)
   {
+    from_expr(expr);
   }
 
-  explicit ieee_floatt(
-    const floatbv_typet &type,
-    rounding_modet __rounding_mode)
-    : spec(ieee_float_spect(type)),
-      rounding_mode(__rounding_mode),
-      sign_flag(false),
+  ieee_float_valuet()
+    : sign_flag(false),
       exponent(0),
       fraction(0),
       NaN_flag(false),
@@ -177,25 +152,6 @@ class ieee_floatt
   {
   }
 
-  ieee_floatt():
-    rounding_mode(ROUND_TO_EVEN),
-    sign_flag(false), exponent(0), fraction(0),
-    NaN_flag(false), infinity_flag(false)
-  {
-  }
-
-  explicit ieee_floatt(const constant_exprt &expr):
-    rounding_mode(ROUND_TO_EVEN)
-  {
-    from_expr(expr);
-  }
-
-  ieee_floatt(const constant_exprt &expr, rounding_modet __rounding_mode)
-    : rounding_mode(__rounding_mode)
-  {
-    from_expr(expr);
-  }
-
   void negate()
   {
     sign_flag=!sign_flag;
@@ -213,22 +169,22 @@ class ieee_floatt
     infinity_flag=false;
   }
 
-  static ieee_floatt zero(const floatbv_typet &type)
+  static ieee_float_valuet zero(const floatbv_typet &type)
   {
-    ieee_floatt result(type);
+    ieee_float_valuet result(type);
     result.make_zero();
     return result;
   }
 
-  static ieee_floatt zero(const ieee_float_spect &spec)
+  static ieee_float_valuet zero(const ieee_float_spect &spec)
   {
-    ieee_floatt result(spec);
+    ieee_float_valuet result(spec);
     result.make_zero();
     return result;
   }
 
-  static ieee_floatt one(const floatbv_typet &);
-  static ieee_floatt one(const ieee_float_spect &);
+  static ieee_float_valuet one(const floatbv_typet &);
+  static ieee_float_valuet one(const ieee_float_spect &);
 
   void make_NaN();
   void make_plus_infinity();
@@ -236,22 +192,42 @@ class ieee_floatt
   void make_fltmax(); // maximum representable finite floating-point number
   void make_fltmin(); // minimum normalized positive floating-point number
 
-  static ieee_floatt NaN(const ieee_float_spect &_spec)
-  { ieee_floatt c(_spec); c.make_NaN(); return c; }
+  static ieee_float_valuet NaN(const ieee_float_spect &_spec)
+  {
+    ieee_float_valuet c(_spec);
+    c.make_NaN();
+    return c;
+  }
 
-  static ieee_floatt plus_infinity(const ieee_float_spect &_spec)
-  { ieee_floatt c(_spec); c.make_plus_infinity(); return c; }
+  static ieee_float_valuet plus_infinity(const ieee_float_spect &_spec)
+  {
+    ieee_float_valuet c(_spec);
+    c.make_plus_infinity();
+    return c;
+  }
 
-  static ieee_floatt minus_infinity(const ieee_float_spect &_spec)
-  { ieee_floatt c(_spec); c.make_minus_infinity(); return c; }
+  static ieee_float_valuet minus_infinity(const ieee_float_spect &_spec)
+  {
+    ieee_float_valuet c(_spec);
+    c.make_minus_infinity();
+    return c;
+  }
 
   // maximum representable finite floating-point number
-  static ieee_floatt fltmax(const ieee_float_spect &_spec)
-  { ieee_floatt c(_spec); c.make_fltmax(); return c; }
+  static ieee_float_valuet fltmax(const ieee_float_spect &_spec)
+  {
+    ieee_float_valuet c(_spec);
+    c.make_fltmax();
+    return c;
+  }
 
   // minimum normalized positive floating-point number
-  static ieee_floatt fltmin(const ieee_float_spect &_spec)
-  { ieee_floatt c(_spec); c.make_fltmin(); return c; }
+  static ieee_float_valuet fltmin(const ieee_float_spect &_spec)
+  {
+    ieee_float_valuet c(_spec);
+    c.make_fltmin();
+    return c;
+  }
 
   // set to next representable number towards plus infinity
   void increment(bool distinguish_zero=false)
@@ -283,10 +259,7 @@ class ieee_floatt
   const mp_integer &get_exponent() const { return exponent; }
   const mp_integer &get_fraction() const { return fraction; }
 
-  // performs conversion to IEEE floating point format
-  void from_integer(const mp_integer &i);
-  void from_base10(const mp_integer &exp, const mp_integer &frac);
-  void build(const mp_integer &exp, const mp_integer &frac);
+  // Construct IEEE floating point value
   void unpack(const mp_integer &i);
   void from_double(const double d);
   void from_float(const float f);
@@ -302,9 +275,6 @@ class ieee_floatt
   void extract_base10(mp_integer &_exponent, mp_integer &_fraction) const;
   mp_integer to_integer() const; // this always rounds to zero
 
-  // conversions
-  void change_spec(const ieee_float_spect &dest_spec);
-
   // output
   void print(std::ostream &out) const;
 
@@ -321,34 +291,22 @@ class ieee_floatt
   constant_exprt to_expr() const;
   void from_expr(const constant_exprt &expr);
 
-  // the usual operators
-  ieee_floatt &operator/=(const ieee_floatt &other);
-  ieee_floatt &operator*=(const ieee_floatt &other);
-  ieee_floatt &operator+=(const ieee_floatt &other);
-  ieee_floatt &operator-=(const ieee_floatt &other);
-
-  bool operator<(const ieee_floatt &other) const;
-  bool operator<=(const ieee_floatt &other) const;
-  bool operator>(const ieee_floatt &other) const;
-  bool operator>=(const ieee_floatt &other) const;
+  bool operator<(const ieee_float_valuet &) const;
+  bool operator<=(const ieee_float_valuet &) const;
+  bool operator>(const ieee_float_valuet &) const;
+  bool operator>=(const ieee_float_valuet &) const;
 
   // warning: these do packed equality, not IEEE equality
   // e.g., NAN==NAN
-  bool operator==(const ieee_floatt &other) const;
-  bool operator!=(const ieee_floatt &other) const;
+  bool operator==(const ieee_float_valuet &) const;
+  bool operator!=(const ieee_float_valuet &) const;
   bool operator==(int i) const;
 
   // these do IEEE equality, i.e., NAN!=NAN
-  bool ieee_equal(const ieee_floatt &other) const;
-  bool ieee_not_equal(const ieee_floatt &other) const;
+  bool ieee_equal(const ieee_float_valuet &) const;
+  bool ieee_not_equal(const ieee_float_valuet &) const;
 
 protected:
-  void divide_and_round(mp_integer &dividend, const mp_integer &divisor);
-  void align();
-  void next_representable(bool greater);
-
-  rounding_modet rounding_mode;
-
   // we store the number unpacked
   bool sign_flag;
   mp_integer exponent; // this is unbiased
@@ -357,13 +315,85 @@ class ieee_floatt
 
   // number of digits of an integer >=1 in base 10
   static mp_integer base10_digits(const mp_integer &src);
+
+  void next_representable(bool greater);
 };
 
-inline std::ostream &operator<<(
-  std::ostream &out,
-  const ieee_floatt &f)
+inline std::ostream &operator<<(std::ostream &out, const ieee_float_valuet &f)
 {
   return out << f.to_ansi_c_string();
 }
 
+/// An IEEE 754 value plus a rounding mode,
+/// enabling operations with rounding on values.
+class ieee_floatt : public ieee_float_valuet
+{
+public:
+  // ROUND_TO_EVEN is also known as "round to nearest, ties to even", and
+  // is the IEEE default.
+  // The numbering below is what x86 uses in the control word and
+  // what is recommended in C11 5.2.4.2.2
+  enum rounding_modet
+  {
+    ROUND_TO_EVEN = 0,
+    ROUND_TO_MINUS_INF = 1,
+    ROUND_TO_PLUS_INF = 2,
+    ROUND_TO_ZERO = 3,
+    UNKNOWN,
+    NONDETERMINISTIC
+  };
+
+  rounding_modet rounding_mode() const
+  {
+    return _rounding_mode;
+  }
+
+  // A helper to turn a rounding mode into a constant bitvector expression
+  static constant_exprt rounding_mode_expr(rounding_modet);
+
+  ieee_floatt(ieee_float_spect __spec, rounding_modet __rounding_mode)
+    : ieee_float_valuet(__spec), _rounding_mode(__rounding_mode)
+  {
+  }
+
+  ieee_floatt(const floatbv_typet &type, rounding_modet __rounding_mode)
+    : ieee_float_valuet(type), _rounding_mode(__rounding_mode)
+  {
+  }
+
+  explicit ieee_floatt(
+    const constant_exprt &expr,
+    rounding_modet __rounding_mode)
+    : ieee_float_valuet(expr), _rounding_mode(__rounding_mode)
+  {
+  }
+
+  // performs conversion to IEEE floating point format,
+  // with rounding.
+  void from_integer(const mp_integer &i);
+  void from_base10(const mp_integer &exp, const mp_integer &frac);
+  void build(const mp_integer &exp, const mp_integer &frac);
+
+  // performs conversions from IEEE float-point format
+  // to something else
+  double to_double() const;
+  float to_float() const;
+  mp_integer to_integer() const; // this always rounds to zero
+
+  // conversions
+  void change_spec(const ieee_float_spect &dest_spec);
+
+  // the usual operators
+  ieee_floatt &operator/=(const ieee_floatt &other);
+  ieee_floatt &operator*=(const ieee_floatt &other);
+  ieee_floatt &operator+=(const ieee_floatt &other);
+  ieee_floatt &operator-=(const ieee_floatt &other);
+
+protected:
+  rounding_modet _rounding_mode;
+
+  void divide_and_round(mp_integer &dividend, const mp_integer &divisor);
+  void align();
+};
+
 #endif // CPROVER_UTIL_IEEE_FLOAT_H
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index c425602cbf5..1eaa54a4dea 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -70,7 +70,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_abs(const abs_exprt &expr)
 
     if(type.id()==ID_floatbv)
     {
-      ieee_floatt value(to_constant_expr(to_unary_expr(expr).op()));
+      ieee_float_valuet value(to_constant_expr(to_unary_expr(expr).op()));
       value.set_sign(false);
       return value.to_expr();
     }
@@ -104,7 +104,7 @@ simplify_exprt::resultt<> simplify_exprt::simplify_sign(const sign_exprt &expr)
 
     if(type.id()==ID_floatbv)
     {
-      ieee_floatt value(to_constant_expr(expr.op()));
+      ieee_float_valuet value(to_constant_expr(expr.op()));
       return make_boolean_expr(value.get_sign());
     }
     else if(type.id()==ID_signedbv ||
@@ -1179,7 +1179,8 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
         const floatbv_typet &f_expr_type=
           to_floatbv_type(expr_type);
 
-        ieee_floatt f(f_expr_type);
+        auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+        ieee_floatt f(f_expr_type, rm);
         f.from_integer(int_value);
 
         return f.to_expr();
@@ -1215,7 +1216,9 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
     }
     else if(op_type_id==ID_floatbv)
     {
-      ieee_floatt f(to_constant_expr(expr.op()));
+      ieee_floatt f(
+        to_constant_expr(expr.op()),
+        ieee_floatt::rounding_modet::ROUND_TO_EVEN);
 
       if(expr_type_id==ID_unsignedbv ||
          expr_type_id==ID_signedbv)
@@ -1233,7 +1236,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       {
         fixedbvt fixedbv;
         fixedbv.spec=fixedbv_spect(to_fixedbv_type(expr_type));
-        ieee_floatt factor(f.spec);
+        ieee_floatt factor(f.spec, ieee_floatt::rounding_modet::ROUND_TO_EVEN);
         factor.from_integer(power(2, fixedbv.spec.get_fraction_bits()));
         f*=factor;
         fixedbv.set_value(f.to_integer());
@@ -1267,7 +1270,7 @@ simplify_exprt::simplify_typecast(const typecast_exprt &expr)
       {
         const auto width = to_bv_type(op_type).get_width();
         const auto int_value = bvrep2integer(value, width, false);
-        ieee_floatt ieee_float{to_floatbv_type(expr_type)};
+        ieee_float_valuet ieee_float{to_floatbv_type(expr_type)};
         ieee_float.unpack(int_value);
         return ieee_float.to_expr();
       }
diff --git a/src/util/simplify_expr_floatbv.cpp b/src/util/simplify_expr_floatbv.cpp
index 1cce00bfa96..b70ccb9b689 100644
--- a/src/util/simplify_expr_floatbv.cpp
+++ b/src/util/simplify_expr_floatbv.cpp
@@ -26,7 +26,7 @@ simplify_exprt::simplify_isinf(const unary_exprt &expr)
 
   if(expr.op().is_constant())
   {
-    ieee_floatt value(to_constant_expr(expr.op()));
+    ieee_float_valuet value(to_constant_expr(expr.op()));
     return make_boolean_expr(value.is_infinity());
   }
 
@@ -40,7 +40,7 @@ simplify_exprt::simplify_isnan(const unary_exprt &expr)
 
   if(expr.op().is_constant())
   {
-    ieee_floatt value(to_constant_expr(expr.op()));
+    ieee_float_valuet value(to_constant_expr(expr.op()));
     return make_boolean_expr(value.is_NaN());
   }
 
@@ -54,7 +54,7 @@ simplify_exprt::simplify_isnormal(const unary_exprt &expr)
 
   if(expr.op().is_constant())
   {
-    ieee_floatt value(to_constant_expr(expr.op()));
+    ieee_float_valuet value(to_constant_expr(expr.op()));
     return make_boolean_expr(value.is_normal());
   }
 
@@ -73,7 +73,7 @@ bool simplify_exprt::simplify_abs(exprt &expr)
 
     if(type.id()==ID_floatbv)
     {
-      ieee_floatt value(to_constant_expr(expr.op0()));
+      ieee_float_valuet value(to_constant_expr(expr.op0()));
       value.set_sign(false);
       expr=value.to_expr();
       return false;
@@ -115,7 +115,7 @@ bool simplify_exprt::simplify_sign(exprt &expr)
 
     if(type.id()==ID_floatbv)
     {
-      ieee_floatt value(to_constant_expr(expr.op0()));
+      ieee_float_valuet value(to_constant_expr(expr.op0()));
       expr = make_boolean_expr(value.get_sign());
       return false;
     }
@@ -351,8 +351,8 @@ simplify_exprt::simplify_ieee_float_relation(const binary_relation_exprt &expr)
 
   if(expr.lhs().is_constant() && expr.rhs().is_constant())
   {
-    ieee_floatt f_lhs(to_constant_expr(expr.lhs()));
-    ieee_floatt f_rhs(to_constant_expr(expr.rhs()));
+    ieee_float_valuet f_lhs(to_constant_expr(expr.lhs()));
+    ieee_float_valuet f_rhs(to_constant_expr(expr.rhs()));
 
     if(expr.id()==ID_ieee_float_notequal)
       return make_boolean_expr(f_lhs.ieee_not_equal(f_rhs));
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 6cdb467e25b..97fb7242e1e 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -102,8 +102,9 @@ static bool sum_expr(
   }
   else if(type_id==ID_floatbv)
   {
-    ieee_floatt f(dest);
-    f += ieee_floatt(expr);
+    auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+    ieee_floatt f(dest, rm);
+    f += ieee_floatt(expr, rm);
     dest=f.to_expr();
     return false;
   }
@@ -151,8 +152,9 @@ static bool mul_expr(
   }
   else if(type_id==ID_floatbv)
   {
-    ieee_floatt f(to_constant_expr(dest));
-    f*=ieee_floatt(to_constant_expr(expr));
+    auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+    ieee_floatt f(to_constant_expr(dest), rm);
+    f *= ieee_floatt(to_constant_expr(expr), rm);
     dest=f.to_expr();
     return false;
   }
@@ -1302,7 +1304,7 @@ simplify_exprt::simplify_unary_minus(const unary_minus_exprt &expr)
     }
     else if(type_id==ID_floatbv)
     {
-      ieee_floatt f(constant_expr);
+      ieee_float_valuet f(constant_expr);
       f.negate();
       return f.to_expr();
     }
@@ -1494,8 +1496,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_both_constant(
   }
   else if(tmp0.type().id() == ID_floatbv)
   {
-    ieee_floatt f0(tmp0_const);
-    ieee_floatt f1(tmp1_const);
+    ieee_float_valuet f0(tmp0_const);
+    ieee_float_valuet f1(tmp1_const);
 
     if(expr.id() == ID_ge)
       return make_boolean_expr(f0 >= f1);
@@ -1889,7 +1891,8 @@ simplify_exprt::resultt<> simplify_exprt::simplify_inequality_rhs_is_constant(
     expr.op0().id() == ID_typecast && expr.op0().type().id() == ID_floatbv &&
     to_typecast_expr(expr.op0()).op().type().id() == ID_floatbv)
   {
-    ieee_floatt const_val(to_constant_expr(expr.op1()));
+    auto rm = ieee_floatt::rounding_modet::ROUND_TO_EVEN;
+    ieee_floatt const_val(to_constant_expr(expr.op1()), rm);
     ieee_floatt const_val_converted=const_val;
     const_val_converted.change_spec(ieee_float_spect(
       to_floatbv_type(to_typecast_expr(expr.op0()).op().type())));
diff --git a/unit/solvers/floatbv/float_utils.cpp b/unit/solvers/floatbv/float_utils.cpp
index b7cdcce9b6a..f545753720f 100644
--- a/unit/solvers/floatbv/float_utils.cpp
+++ b/unit/solvers/floatbv/float_utils.cpp
@@ -34,7 +34,7 @@ static float random_float(distt &dist, std::mt19937 &gen)
   return u.f;
 }
 
-static bool eq(const ieee_floatt &a, const ieee_floatt &b)
+static bool eq(const ieee_float_valuet &a, const ieee_float_valuet &b)
 {
   return (a.is_NaN() && b.is_NaN()) ||
          (a.is_infinity() && b.is_infinity() && a.get_sign() == b.get_sign()) ||
@@ -69,8 +69,8 @@ static float set_values(
   float_utilst &float_utils,
   float &f1,
   float &f2,
-  ieee_floatt &i1,
-  ieee_floatt &i2)
+  ieee_float_valuet &i1,
+  ieee_float_valuet &i2)
 {
   f1 = random_float(dist, gen);
   f2 = random_float(dist, gen);
@@ -86,8 +86,8 @@ static bvt compute(
   float_utilst &float_utils,
   const float &f2,
   float &f3,
-  const ieee_floatt &i1,
-  const ieee_floatt &i2)
+  const ieee_float_valuet &i1,
+  const ieee_float_valuet &i2)
 {
   const bvt b1 = float_utils.build_constant(i1);
   const bvt b2 = float_utils.build_constant(i2);
@@ -118,10 +118,10 @@ static bvt compute(
 
 static void print(
   unsigned i,
-  const ieee_floatt &i1,
-  const ieee_floatt &i2,
-  const ieee_floatt &i3,
-  const ieee_floatt &fres,
+  const ieee_float_valuet &i1,
+  const ieee_float_valuet &i2,
+  const ieee_float_valuet &i3,
+  const ieee_float_valuet &fres,
   const float &f1,
   const float &f2,
   const float &f3)
@@ -147,7 +147,7 @@ static void print(
 
 SCENARIO("float_utils", "[core][solvers][floatbv][float_utils]")
 {
-  ieee_floatt i1, i2, i3;
+  ieee_float_valuet i1, i2, i3;
   float f1, f2, f3;
 
   std::random_device rd;
@@ -171,7 +171,7 @@ SCENARIO("float_utils", "[core][solvers][floatbv][float_utils]")
         const satcheckt::resultt result = satcheck.prop_solve();
         REQUIRE(result == satcheckt::resultt::P_SATISFIABLE);
 
-        const ieee_floatt fres = float_utils.get(res);
+        const ieee_float_valuet fres = float_utils.get(res);
 
         if(!eq(fres, i3))
           print(i, i1, i2, i3, fres, f1, f2, f3);
@@ -184,7 +184,7 @@ SCENARIO("float_utils", "[core][solvers][floatbv][float_utils]")
 
 SCENARIO("float_approximation", "[core][solvers][floatbv][float_approximation]")
 {
-  ieee_floatt i1, i2, i3;
+  ieee_float_valuet i1, i2, i3;
   float f1, f2, f3;
 
   std::random_device rd;
@@ -208,7 +208,7 @@ SCENARIO("float_approximation", "[core][solvers][floatbv][float_approximation]")
         const satcheckt::resultt result = satcheck.prop_solve();
         REQUIRE(result == satcheckt::resultt::P_SATISFIABLE);
 
-        const ieee_floatt fres = float_utils.get(res);
+        const ieee_float_valuet fres = float_utils.get(res);
 
         if(!eq(fres, i3))
           print(i, i1, i2, i3, fres, f1, f2, f3);