diff --git a/src/cbmc/cbmc_parse_options.cpp b/src/cbmc/cbmc_parse_options.cpp
index 35a5002572d..73255cfeb63 100644
--- a/src/cbmc/cbmc_parse_options.cpp
+++ b/src/cbmc/cbmc_parse_options.cpp
@@ -39,6 +39,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_skip.h>
 #include <goto-programs/show_goto_functions.h>
 
+#include <goto-symex/rewrite_union.h>
+#include <goto-symex/adjust_float_expressions.h>
+
 #include <goto-instrument/full_slicer.h>
 #include <goto-instrument/nondet_static.h>
 #include <goto-instrument/cover.h>
@@ -891,10 +894,13 @@ bool cbmc_parse_optionst::process_goto_program(
     remove_returns(symbol_table, goto_functions);
     remove_vector(symbol_table, goto_functions);
     remove_complex(symbol_table, goto_functions);
+    rewrite_union(goto_functions, ns);
 
     // add generic checks
     status() << "Generic Property Instrumentation" << eom;
     goto_check(ns, options, goto_functions);
+    // checks don't know about adjusted float expressions
+    adjust_float_expressions(goto_functions, ns);
 
     // ignore default/user-specified initialization
     // of variables with static lifetime
diff --git a/src/goto-programs/remove_complex.cpp b/src/goto-programs/remove_complex.cpp
index 553a70dab50..ed5e916f9f3 100644
--- a/src/goto-programs/remove_complex.cpp
+++ b/src/goto-programs/remove_complex.cpp
@@ -12,9 +12,6 @@ Date:   September 2014
 
 #include "remove_complex.h"
 
-void remove_complex(typet &);
-void remove_complex(exprt &);
-
 /*******************************************************************\
 
 Function: complex_member
@@ -27,7 +24,7 @@ Function: complex_member
 
 \*******************************************************************/
 
-exprt complex_member(const exprt &expr, irep_idt id)
+static exprt complex_member(const exprt &expr, irep_idt id)
 {
   if(expr.id()==ID_struct && expr.operands().size()==2)
   {
@@ -50,6 +47,90 @@ exprt complex_member(const exprt &expr, irep_idt id)
 
 /*******************************************************************\
 
+Function: have_to_remove_complex
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static bool have_to_remove_complex(const typet &type);
+
+static bool have_to_remove_complex(const exprt &expr)
+{
+  if(expr.id()==ID_typecast &&
+     to_typecast_expr(expr).op().type().id()==ID_complex &&
+     expr.type().id()!=ID_complex)
+    return true;
+
+  if(expr.type().id()==ID_complex)
+  {
+    if(expr.id()==ID_plus || expr.id()==ID_minus ||
+       expr.id()==ID_mult || expr.id()==ID_div)
+      return true;
+    else if(expr.id()==ID_unary_minus)
+      return true;
+    else if(expr.id()==ID_complex)
+      return true;
+    else if(expr.id()==ID_typecast)
+      return true;
+  }
+
+  if(expr.id()==ID_complex_real)
+    return true;
+  else if(expr.id()==ID_complex_imag)
+    return true;
+
+  if(have_to_remove_complex(expr.type()))
+     return true;
+
+  forall_operands(it, expr)
+    if(have_to_remove_complex(*it))
+      return true;
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: have_to_remove_complex
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static bool have_to_remove_complex(const typet &type)
+{
+  if(type.id()==ID_struct || type.id()==ID_union)
+  {
+    const struct_union_typet &struct_union_type=
+      to_struct_union_type(type);
+    for(struct_union_typet::componentst::const_iterator
+        it=struct_union_type.components().begin();
+        it!=struct_union_type.components().end();
+        it++)
+      if(have_to_remove_complex(it->type()))
+        return true;
+  }
+  else if(type.id()==ID_pointer ||
+          type.id()==ID_vector ||
+          type.id()==ID_array)
+    return have_to_remove_complex(type.subtype());
+  else if(type.id()==ID_complex)
+    return true;
+
+  return false;
+}
+
+/*******************************************************************\
+
 Function: remove_complex
 
 Inputs:
@@ -60,8 +141,13 @@ Purpose: removes complex data type
 
 \*******************************************************************/
 
-void remove_complex(exprt &expr)
+static void remove_complex(typet &);
+
+static void remove_complex(exprt &expr)
 {
+  if(!have_to_remove_complex(expr))
+    return;
+
   if(expr.id()==ID_typecast)
   {
     assert(expr.operands().size()==1);
@@ -200,8 +286,11 @@ Purpose: removes complex data type
 
 \*******************************************************************/
 
-void remove_complex(typet &type)
+static void remove_complex(typet &type)
 {
+  if(!have_to_remove_complex(type))
+    return;
+
   if(type.id()==ID_struct || type.id()==ID_union)
   {
     struct_union_typet &struct_union_type=
@@ -250,7 +339,7 @@ Purpose: removes complex data type
 
 \*******************************************************************/
 
-void remove_complex(symbolt &symbol)
+static void remove_complex(symbolt &symbol)
 {
   remove_complex(symbol.value);
   remove_complex(symbol.type);
@@ -286,7 +375,8 @@ Purpose: removes complex data type
 
 \*******************************************************************/
 
-void remove_complex(goto_functionst::goto_functiont &goto_function)
+static void remove_complex(
+  goto_functionst::goto_functiont &goto_function)
 {
   remove_complex(goto_function.type);
 
@@ -309,7 +399,7 @@ Purpose: removes complex data type
 
 \*******************************************************************/
 
-void remove_complex(goto_functionst &goto_functions)
+static void remove_complex(goto_functionst &goto_functions)
 {
   Forall_goto_functions(it, goto_functions)
     remove_complex(it->second);
diff --git a/src/goto-programs/remove_vector.cpp b/src/goto-programs/remove_vector.cpp
index 90df83ca43b..f7b63e42d4f 100644
--- a/src/goto-programs/remove_vector.cpp
+++ b/src/goto-programs/remove_vector.cpp
@@ -12,8 +12,80 @@ Date:   September 2014
 
 #include "remove_vector.h"
 
-void remove_vector(typet &);
-void remove_vector(exprt &);
+/*******************************************************************\
+
+Function: have_to_remove_vector
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+static bool have_to_remove_vector(const typet &type);
+
+static bool have_to_remove_vector(const exprt &expr)
+{
+  if(expr.type().id()==ID_vector)
+  {
+    if(expr.id()==ID_plus || expr.id()==ID_minus ||
+       expr.id()==ID_mult || expr.id()==ID_div ||
+       expr.id()==ID_mod  || expr.id()==ID_bitxor ||
+       expr.id()==ID_bitand || expr.id()==ID_bitor)
+      return true;
+    else if(expr.id()==ID_unary_minus || expr.id()==ID_bitnot)
+      return true;
+    else if(expr.id()==ID_vector)
+      return true;
+  }
+
+  if(have_to_remove_vector(expr.type()))
+    return true;
+
+  forall_operands(it, expr)
+    if(have_to_remove_vector(*it))
+      return true;
+
+  return false;
+}
+
+/*******************************************************************\
+
+Function: have_to_remove_vector
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+static bool have_to_remove_vector(const typet &type)
+{
+  if(type.id()==ID_struct || type.id()==ID_union)
+  {
+    const struct_union_typet &struct_union_type=
+      to_struct_union_type(type);
+
+    for(struct_union_typet::componentst::const_iterator
+        it=struct_union_type.components().begin();
+        it!=struct_union_type.components().end();
+        it++)
+      if(have_to_remove_vector(it->type()))
+        return true;
+  }
+  else if(type.id()==ID_pointer ||
+          type.id()==ID_complex ||
+          type.id()==ID_array)
+    return have_to_remove_vector(type.subtype());
+  else if(type.id()==ID_vector)
+    return true;
+
+  return false;
+}
 
 /*******************************************************************\
 
@@ -27,8 +99,13 @@ Purpose: removes vector data type
 
 \*******************************************************************/
 
-void remove_vector(exprt &expr)
+static void remove_vector(typet &);
+
+static void remove_vector(exprt &expr)
 {
+  if(!have_to_remove_vector(expr))
+    return;
+
   Forall_operands(it, expr)
     remove_vector(*it);
 
@@ -109,8 +186,11 @@ Purpose: removes vector data type
 
 \*******************************************************************/
 
-void remove_vector(typet &type)
+static void remove_vector(typet &type)
 {
+  if(!have_to_remove_vector(type))
+    return;
+
   if(type.id()==ID_struct || type.id()==ID_union)
   {
     struct_union_typet &struct_union_type=
@@ -155,7 +235,7 @@ Purpose: removes vector data type
 
 \*******************************************************************/
 
-void remove_vector(symbolt &symbol)
+static void remove_vector(symbolt &symbol)
 {
   remove_vector(symbol.value);
   remove_vector(symbol.type);
@@ -173,7 +253,7 @@ Purpose: removes vector data type
 
 \*******************************************************************/
 
-void remove_vector(symbol_tablet &symbol_table)
+static void remove_vector(symbol_tablet &symbol_table)
 {
   Forall_symbols(it, symbol_table.symbols)
     remove_vector(it->second);
@@ -214,7 +294,7 @@ Purpose: removes vector data type
 
 \*******************************************************************/
 
-void remove_vector(goto_functionst &goto_functions)
+static void remove_vector(goto_functionst &goto_functions)
 {
   Forall_goto_functions(it, goto_functions)
     remove_vector(it->second);
diff --git a/src/goto-symex/adjust_float_expressions.cpp b/src/goto-symex/adjust_float_expressions.cpp
index 94048db8e5f..46dee137447 100644
--- a/src/goto-symex/adjust_float_expressions.cpp
+++ b/src/goto-symex/adjust_float_expressions.cpp
@@ -13,10 +13,79 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/ieee_float.h>
 #include <util/arith_tools.h>
 
+#include <goto-programs/goto_model.h>
+
 #include "adjust_float_expressions.h"
 
 /*******************************************************************\
 
+Function: have_to_adjust_float_expressions
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static bool have_to_adjust_float_expressions(
+  const exprt &expr,
+  const namespacet &ns)
+{
+  if(expr.id()==ID_floatbv_plus ||
+     expr.id()==ID_floatbv_minus ||
+     expr.id()==ID_floatbv_mult ||
+     expr.id()==ID_floatbv_div ||
+     expr.id()==ID_floatbv_div ||
+     expr.id()==ID_floatbv_rem ||
+     expr.id()==ID_floatbv_typecast)
+    return false;
+
+  const typet &type=ns.follow(expr.type());
+
+  if(type.id()==ID_floatbv ||
+     (type.id()==ID_complex &&
+      ns.follow(type.subtype()).id()==ID_floatbv))
+  {
+    if(expr.id()==ID_plus || expr.id()==ID_minus ||
+       expr.id()==ID_mult || expr.id()==ID_div ||
+       expr.id()==ID_rem)
+      return true;
+  }
+
+  if(expr.id()==ID_typecast)
+  {
+    const typecast_exprt &typecast_expr=to_typecast_expr(expr);
+
+    const typet &src_type=typecast_expr.op().type();
+    const typet &dest_type=typecast_expr.type();
+
+    if(dest_type.id()==ID_floatbv &&
+       src_type.id()==ID_floatbv)
+      return true;
+    else if(dest_type.id()==ID_floatbv &&
+            (src_type.id()==ID_c_bool ||
+             src_type.id()==ID_signedbv ||
+             src_type.id()==ID_unsignedbv ||
+             src_type.id()==ID_c_enum_tag))
+      return true;
+    else if((dest_type.id()==ID_signedbv ||
+             dest_type.id()==ID_unsignedbv ||
+             dest_type.id()==ID_c_enum_tag) &&
+             src_type.id()==ID_floatbv)
+      return true;
+  }
+
+  forall_operands(it, expr)
+    if(have_to_adjust_float_expressions(*it, ns))
+      return true;
+
+  return false;
+}
+
+/*******************************************************************\
+
 Function: adjust_float_expressions
 
   Inputs:
@@ -32,6 +101,9 @@ void adjust_float_expressions(
   exprt &expr,
   const namespacet &ns)
 {
+  if(!have_to_adjust_float_expressions(expr, ns))
+    return;
+
   Forall_operands(it, expr)
     adjust_float_expressions(*it, ns);
 
@@ -126,3 +198,64 @@ void adjust_float_expressions(
     }
   }
 }
+
+/*******************************************************************\
+
+Function: adjust_float_expressions
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+static void adjust_float_expressions(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns)
+{
+  Forall_goto_program_instructions(it, goto_function.body)
+  {
+    adjust_float_expressions(it->code, ns);
+    adjust_float_expressions(it->guard, ns);
+  }
+}
+
+/*******************************************************************\
+
+Function: adjust_float_expressions
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void adjust_float_expressions(
+  goto_functionst &goto_functions,
+  const namespacet &ns)
+{
+  Forall_goto_functions(it, goto_functions)
+    adjust_float_expressions(it->second, ns);
+}
+
+/*******************************************************************\
+
+Function: adjust_float_expressions
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void adjust_float_expressions(goto_modelt &goto_model)
+{
+  namespacet ns(goto_model.symbol_table);
+  adjust_float_expressions(goto_model.goto_functions, ns);
+}
diff --git a/src/goto-symex/adjust_float_expressions.h b/src/goto-symex/adjust_float_expressions.h
index c8c87260996..f8547c59fa8 100644
--- a/src/goto-symex/adjust_float_expressions.h
+++ b/src/goto-symex/adjust_float_expressions.h
@@ -9,11 +9,18 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
 #define CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
 
-#include <util/expr.h>
-#include <util/namespace.h>
+class exprt;
+class namespacet;
+class goto_functionst;
+class goto_modelt;
 
 void adjust_float_expressions(
   exprt &expr,
   const namespacet &ns);
 
+void adjust_float_expressions(
+  goto_functionst &goto_functions,
+  const namespacet &ns);
+void adjust_float_expressions(goto_modelt &goto_model);
+
 #endif // CPROVER_GOTO_SYMEX_ADJUST_FLOAT_EXPRESSIONS_H
diff --git a/src/goto-symex/rewrite_union.cpp b/src/goto-symex/rewrite_union.cpp
index 26b9282dfdf..420d03e6a63 100644
--- a/src/goto-symex/rewrite_union.cpp
+++ b/src/goto-symex/rewrite_union.cpp
@@ -11,12 +11,48 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/expr_util.h>
 #include <util/byte_operators.h>
 
+#include <goto-programs/goto_model.h>
+
 #include <ansi-c/c_types.h>
 
 #include "rewrite_union.h"
 
 /*******************************************************************\
 
+Function: have_to_rewrite_union
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static bool have_to_rewrite_union(
+  const exprt &expr,
+  const namespacet &ns)
+{
+  if(expr.id()==ID_member)
+  {
+    const exprt &op=to_member_expr(expr).struct_op();
+    const typet &op_type=ns.follow(op.type());
+
+    if(op_type.id()==ID_union)
+      return true;
+  }
+  else if(expr.id()==ID_union)
+    return true;
+
+  forall_operands(it, expr)
+    if(have_to_rewrite_union(*it, ns))
+      return true;
+
+  return false;
+}
+
+/*******************************************************************\
+
 Function: rewrite_union
 
   Inputs:
@@ -32,6 +68,9 @@ void rewrite_union(
   exprt &expr,
   const namespacet &ns)
 {
+  if(!have_to_rewrite_union(expr, ns))
+    return;
+
   Forall_operands(it, expr)
     rewrite_union(*it, ns);
 
@@ -57,3 +96,64 @@ void rewrite_union(
     expr=tmp;
   }
 }
+
+/*******************************************************************\
+
+Function: rewrite_union
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+static void rewrite_union(
+  goto_functionst::goto_functiont &goto_function,
+  const namespacet &ns)
+{
+  Forall_goto_program_instructions(it, goto_function.body)
+  {
+    rewrite_union(it->code, ns);
+    rewrite_union(it->guard, ns);
+  }
+}
+
+/*******************************************************************\
+
+Function: rewrite_union
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void rewrite_union(
+  goto_functionst &goto_functions,
+  const namespacet &ns)
+{
+  Forall_goto_functions(it, goto_functions)
+    rewrite_union(it->second, ns);
+}
+
+/*******************************************************************\
+
+Function: rewrite_union
+
+Inputs:
+
+Outputs:
+
+Purpose:
+
+\*******************************************************************/
+
+void rewrite_union(goto_modelt &goto_model)
+{
+  namespacet ns(goto_model.symbol_table);
+  rewrite_union(goto_model.goto_functions, ns);
+}
diff --git a/src/goto-symex/rewrite_union.h b/src/goto-symex/rewrite_union.h
index 8f406960bc2..7215e0bf0a4 100644
--- a/src/goto-symex/rewrite_union.h
+++ b/src/goto-symex/rewrite_union.h
@@ -9,11 +9,20 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_GOTO_SYMEX_REWRITE_UNION_H
 #define CPROVER_GOTO_SYMEX_REWRITE_UNION_H
 
-#include <util/expr.h>
-#include <util/namespace.h>
+#include <goto-programs/goto_functions.h>
+
+class exprt;
+class namespacet;
+class goto_functionst;
+class goto_modelt;
 
 void rewrite_union(
   exprt &expr,
   const namespacet &ns);
 
+void rewrite_union(
+  goto_functionst &goto_functions,
+  const namespacet &ns);
+void rewrite_union(goto_modelt &goto_model);
+
 #endif // CPROVER_GOTO_SYMEX_REWRITE_UNION_H
diff --git a/src/goto-symex/symex_clean_expr.cpp b/src/goto-symex/symex_clean_expr.cpp
index 338854922b3..807c24d872a 100644
--- a/src/goto-symex/symex_clean_expr.cpp
+++ b/src/goto-symex/symex_clean_expr.cpp
@@ -13,8 +13,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <ansi-c/c_types.h>
 
-#include "adjust_float_expressions.h"
-#include "rewrite_union.h"
 #include "goto_symex.h"
 
 /*******************************************************************\
@@ -199,9 +197,7 @@ void goto_symext::clean_expr(
   statet &state,
   const bool write)
 {
-  rewrite_union(expr, ns);
   replace_nondet(expr);
   dereference(expr, state, write);
   replace_array_equal(expr);
-  adjust_float_expressions(expr, ns);
 }
diff --git a/src/path-symex/path_symex_state_read.cpp b/src/path-symex/path_symex_state_read.cpp
index 33aab3c5fc5..72fbc683f1c 100644
--- a/src/path-symex/path_symex_state_read.cpp
+++ b/src/path-symex/path_symex_state_read.cpp
@@ -11,9 +11,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <pointer-analysis/dereference.h>
 
-#include <goto-symex/adjust_float_expressions.h>
-#include <goto-symex/rewrite_union.h>
-
 #include "path_symex_state.h"
 
 //#define DEBUG
@@ -41,21 +38,13 @@ exprt path_symex_statet::read(const exprt &src, bool propagate)
   //std::cout << "path_symex_statet::read " << src.pretty() << std::endl;
   #endif
 
-  // This has five phases!
-  // 1. Floating-point expression adjustment (rounding mode)
-  // 2. Rewrite unions into byte operators
-  // 3. Dereferencing, including propagation of pointers.
-  // 4. Rewriting to SSA symbols
-  // 5. Simplifier
-
-  exprt tmp1=src;
-  adjust_float_expressions(tmp1, var_map.ns);
-
-  exprt tmp2=tmp1;
-  rewrite_union(tmp2, var_map.ns);
+  // This has three phases!
+  // 1. Dereferencing, including propagation of pointers.
+  // 2. Rewriting to SSA symbols
+  // 3. Simplifier
 
   // we force propagation for dereferencing
-  exprt tmp3=dereference_rec(tmp2, true);
+  exprt tmp3=dereference_rec(src, true);
 
   exprt tmp4=instantiate_rec(tmp3, propagate);
 
diff --git a/src/symex/symex_parse_options.cpp b/src/symex/symex_parse_options.cpp
index 7a9227e6f58..575dcb833bb 100644
--- a/src/symex/symex_parse_options.cpp
+++ b/src/symex/symex_parse_options.cpp
@@ -33,6 +33,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <goto-programs/remove_vector.h>
 #include <goto-programs/remove_virtual_functions.h>
 
+#include <goto-symex/rewrite_union.h>
+#include <goto-symex/adjust_float_expressions.h>
+
 #include <goto-instrument/cover.h>
 
 #include <langapi/mode.h>
@@ -359,6 +362,8 @@ bool symex_parse_optionst::process_goto_program(const optionst &options)
     remove_complex(goto_model);
     remove_vector(goto_model);
     remove_virtual_functions(goto_model);
+    rewrite_union(goto_model);
+    adjust_float_expressions(goto_model);
 
     // recalculate numbers, etc.
     goto_model.goto_functions.update();