diff --git a/lib/cbmc b/lib/cbmc
index fc4f7ca71..0fc8a492c 160000
--- a/lib/cbmc
+++ b/lib/cbmc
@@ -1 +1 @@
-Subproject commit fc4f7ca71ddcbd290cea0d9ac58b6cc6f6b79cb0
+Subproject commit 0fc8a492c86903e28e2c64d84f0db35cc98cbd8e
diff --git a/src/hw-cbmc/map_vars.cpp b/src/hw-cbmc/map_vars.cpp
index 69a5419d2..ced93bd94 100644
--- a/src/hw-cbmc/map_vars.cpp
+++ b/src/hw-cbmc/map_vars.cpp
@@ -243,8 +243,8 @@ bool map_varst::array_types_eq(
   
   namespacet ns(symbol_table);
 
-  const typet &s1 = ns.follow(type1.element_type());
-  const typet &s2 = ns.follow(type2.element_type());
+  const typet &s1 = type1.element_type();
+  const typet &s2 = type2.element_type();
 
   if(s1.id()==ID_array && s2.id()==ID_array)
     return array_types_eq(to_array_type(s1), to_array_type(s2), error_msg);
@@ -279,12 +279,6 @@ bool map_varst::check_types_rec(
 {
   namespacet ns(symbol_table);
 
-  if(type1.id()==ID_symbol)
-    return check_types_rec(ns.follow(type1), type2, error_msg);
-
-  if(type2.id()==ID_symbol)
-    return check_types_rec(type1, ns.follow(type2), error_msg);
-
   // type is the same?
   if(type1 == type2)
     return false;
@@ -357,8 +351,8 @@ void map_varst::add_constraint_rec(
 {
   namespacet ns(symbol_table);
 
-  const typet &t1=ns.follow(program_symbol.type());
-  const typet &t2=ns.follow(module_symbol.type());
+  const typet &t1 = program_symbol.type();
+  const typet &t2 = module_symbol.type();
 
   // check the type
   if(t1==t2)
@@ -426,7 +420,7 @@ const symbolt &map_varst::add_array(symbolt &symbol)
 {
   const namespacet ns(symbol_table);
 
-  const typet &full_type=ns.follow(symbol.type);
+  const typet &full_type = symbol.type;
 
   if(full_type.id()==ID_incomplete_array)
   {
@@ -514,7 +508,7 @@ void map_varst::map_var_rec(
   const irep_idt &prefix)
 {
   const namespacet ns(symbol_table);
-  const typet &expr_type=ns.follow(expr.type());
+  const typet &expr_type = expr.type();
   const struct_typet &struct_type=to_struct_type(expr_type);
   const struct_typet::componentst &components=struct_type.components();
 
@@ -534,9 +528,9 @@ void map_varst::map_var_rec(
       base_name=c_it->get_base_name();
     else
       base_name=name;
-    
-    bool module_instance=ns.follow(c_it->type()).id()==ID_struct;
-    
+
+    bool module_instance = c_it->type().id() == ID_struct;
+
     irep_idt full_name=id2string(prefix)+"."+id2string(base_name);
 
     const symbol_table_baset::symbolst::const_iterator sub_symbol_it =
@@ -603,8 +597,8 @@ void map_varst::map_var(
 
   const namespacet ns(symbol_table);
 
-  const typet &type1=ns.follow(program_symbol.type());
-  const typet &type2=ns.follow(module_symbol.type);
+  const typet &type1 = program_symbol.type();
+  const typet &type2 = module_symbol.type;
 
   std::string error_msg;
   if(check_types_rec(type1, type2, error_msg))
@@ -721,7 +715,7 @@ void map_varst::map_vars(const irep_idt &top_module)
     index_exprt expr(
       symbol_expr,
       timeframe_expr,
-      to_array_type(ns.follow(symbol_expr.type())).element_type());
+      to_array_type(symbol_expr.type()).element_type());
 
     top_level_inputs.clear();
 
@@ -733,7 +727,7 @@ void map_varst::map_vars(const irep_idt &top_module)
       const irep_idt &base_name = entry.second.base_name;
       symbolt &symbol = symbol_table.get_writeable_ref(entry.first);
       if (symbol.type.id() == ID_struct_tag)
-        symbol.type = ns.follow(symbol.type);
+        symbol.type = symbol.type;
       if (base_name == "next_timeframe" && symbol.type.id() == ID_code) {
         namespacet ns(symbol_table);
         add_next_timeframe(symbol, struct_symbol, top_level_inputs, ns);
diff --git a/src/hw-cbmc/next_timeframe.cpp b/src/hw-cbmc/next_timeframe.cpp
index b69a9822d..0dd072ff2 100644
--- a/src/hw-cbmc/next_timeframe.cpp
+++ b/src/hw-cbmc/next_timeframe.cpp
@@ -50,8 +50,7 @@ void add_next_timeframe(
   code_blockt block;
   block.add(assignment_increase);
 
-  const struct_typet &struct_type =
-      to_struct_type(ns.follow(struct_symbol.type));
+  const struct_typet &struct_type = to_struct_type(struct_symbol.type);
 
   // now assign the non-inputs in the module symbol
   const index_exprt index_expr(array_symbol.symbol_expr(),
diff --git a/src/hw-cbmc/set_inputs.cpp b/src/hw-cbmc/set_inputs.cpp
index d5e3de049..4038d6195 100644
--- a/src/hw-cbmc/set_inputs.cpp
+++ b/src/hw-cbmc/set_inputs.cpp
@@ -38,10 +38,9 @@ void add_set_inputs(
   const symbolt &struct_symbol=ns.lookup(struct_identifier);
   const symbolt &array_symbol=ns.lookup(id2string(struct_identifier)+"_array");
   const symbolt &timeframe_symbol=ns.lookup("hw-cbmc::timeframe");
-  
-  const struct_typet &struct_type=
-    to_struct_type(ns.follow(struct_symbol.type));
-  
+
+  const struct_typet &struct_type = to_struct_type(struct_symbol.type);
+
   // We now assume current input values to be equal,
   // with the goal of adding assumptions on inputs.
   const index_exprt index_expr(
diff --git a/src/trans-netlist/trans_trace.cpp b/src/trans-netlist/trans_trace.cpp
index b75d04582..c7543e449 100644
--- a/src/trans-netlist/trans_trace.cpp
+++ b/src/trans-netlist/trans_trace.cpp
@@ -387,14 +387,10 @@ static mp_integer vcd_width(
   const typet &type,
   const namespacet &ns)
 {
-  if(type.id()==ID_symbol)
-    return vcd_width(ns.follow(type), ns);
-  else if(type.id()==ID_unsignedbv ||
-          type.id()==ID_signedbv ||
-          type.id()==ID_bv ||
-          type.id()==ID_fixedbv ||
-          type.id()==ID_floatbv ||
-          type.id()==ID_pointer)
+  if(
+    type.id() == ID_unsignedbv || type.id() == ID_signedbv ||
+    type.id() == ID_bv || type.id() == ID_fixedbv || type.id() == ID_floatbv ||
+    type.id() == ID_pointer)
   {
     return to_bitvector_type(type).get_width();
   }
@@ -456,8 +452,8 @@ static std::string as_vcd_binary(
   const exprt &expr,
   const namespacet &ns)
 {
-  const typet &type=ns.follow(expr.type());
-  
+  const auto &type = expr.type();
+
   if(expr.id()==ID_constant)
   {
     if(
diff --git a/src/verilog/convert_literals.cpp b/src/verilog/convert_literals.cpp
index 1e03a4a7d..3780ef66f 100644
--- a/src/verilog/convert_literals.cpp
+++ b/src/verilog/convert_literals.cpp
@@ -103,7 +103,12 @@ constant_exprt convert_real_literal(const irep_idt &value)
   // adjust exponent
   exponent -= str_fraction_part.size();
 
-  ieee_floatt ieee_float{ieee_float_spect::double_precision()};
+  // IEEE 1800-2017 5.7.2 says that real literal constants
+  // are IEEE 754 double-precision, but doesn't specify
+  // how to round when converting decimals.
+  ieee_floatt ieee_float{
+    ieee_float_spect::double_precision(),
+    ieee_floatt::rounding_modet::ROUND_TO_EVEN};
 
   ieee_float.from_base10(significand, exponent);
 
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index dbeba3825..ea7a06633 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -1246,8 +1246,7 @@ expr2verilogt::convert_constant(const constant_exprt &src)
   {
     constant_exprt tmp = src;
     tmp.type() = ieee_float_spect::double_precision().to_type();
-    ieee_floatt ieee_float;
-    ieee_float.from_expr(tmp);
+    auto ieee_float = ieee_float_valuet{tmp};
     return {precedence, ieee_float.to_ansi_c_string()};
   }
   else if(type.id() == ID_string)