diff --git a/src/util/expr.cpp b/src/util/expr.cpp
index a990ec357d2..d952acd87c8 100644
--- a/src/util/expr.cpp
+++ b/src/util/expr.cpp
@@ -9,19 +9,19 @@ Author: Daniel Kroening, kroening@kroening.com
 /// \file
 /// Expression Representation
 
+#include "arith_tools.h"
 #include "expr.h"
-#include <cassert>
-#include <stack>
-#include "string2int.h"
-#include "mp_arith.h"
+#include "expr_iterator.h"
 #include "fixedbv.h"
 #include "ieee_float.h"
 #include "invariant.h"
-#include "expr_iterator.h"
+#include "mp_arith.h"
 #include "rational.h"
 #include "rational_tools.h"
-#include "arith_tools.h"
 #include "std_expr.h"
+#include "string2int.h"
+
+#include <stack>
 
 void exprt::move_to_operands(exprt &expr)
 {
@@ -157,71 +157,6 @@ void exprt::make_false()
   set(ID_value, ID_false);
 }
 
-void exprt::negate()
-{
-  const irep_idt &type_id=type().id();
-
-  if(type_id==ID_bool)
-    make_not();
-  else
-  {
-    if(is_constant())
-    {
-      const irep_idt &value=get(ID_value);
-
-      if(type_id==ID_integer)
-      {
-        set(ID_value, integer2string(-string2integer(id2string(value))));
-      }
-      else if(type_id==ID_unsignedbv)
-      {
-        mp_integer int_value=binary2integer(id2string(value), false);
-        typet _type=type();
-        *this=from_integer(-int_value, _type);
-      }
-      else if(type_id==ID_signedbv)
-      {
-        mp_integer int_value=binary2integer(id2string(value), true);
-        typet _type=type();
-        *this=from_integer(-int_value, _type);
-      }
-      else if(type_id==ID_fixedbv)
-      {
-        fixedbvt fixedbv_value=fixedbvt(to_constant_expr(*this));
-        fixedbv_value.negate();
-        *this=fixedbv_value.to_expr();
-      }
-      else if(type_id==ID_floatbv)
-      {
-        ieee_floatt ieee_float_value=ieee_floatt(to_constant_expr(*this));
-        ieee_float_value.negate();
-        *this=ieee_float_value.to_expr();
-      }
-      else
-      {
-        make_nil();
-        UNREACHABLE;
-      }
-    }
-    else
-    {
-      if(id()==ID_unary_minus)
-      {
-        exprt tmp;
-        DATA_INVARIANT(operands().size()==1,
-                       "Unary minus must have one operand");
-        tmp.swap(op0());
-        swap(tmp);
-      }
-      else
-      {
-        unary_minus_exprt tmp(*this);
-        swap(tmp);
-      }
-    }
-  }
-}
-
 bool exprt::is_boolean() const
 {
   return type().id()==ID_bool;
@@ -312,151 +247,6 @@ bool exprt::is_one() const
   return false;
 }
 
-bool exprt::sum(const exprt &expr)
-{
-  if(!is_constant() || !expr.is_constant())
-    return true;
-  if(type()!=expr.type())
-    return true;
-
-  const irep_idt &type_id=type().id();
-
-  if(type_id==ID_integer || type_id==ID_natural)
-  {
-    set(ID_value, integer2string(
-      string2integer(get_string(ID_value))+
-      string2integer(expr.get_string(ID_value))));
-    return false;
-  }
-  else if(type_id==ID_rational)
-  {
-    rationalt a, b;
-    if(!to_rational(*this, a) && !to_rational(expr, b))
-    {
-      exprt a_plus_b=from_rational(a+b);
-      set(ID_value, a_plus_b.get_string(ID_value));
-      return false;
-    }
-  }
-  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
-  {
-    set(ID_value, integer2binary(
-      binary2integer(get_string(ID_value), false)+
-      binary2integer(expr.get_string(ID_value), false),
-      unsafe_string2unsigned(type().get_string(ID_width))));
-    return false;
-  }
-  else if(type_id==ID_fixedbv)
-  {
-    set(ID_value, integer2binary(
-      binary2integer(get_string(ID_value), false)+
-      binary2integer(expr.get_string(ID_value), false),
-      unsafe_string2unsigned(type().get_string(ID_width))));
-    return false;
-  }
-  else if(type_id==ID_floatbv)
-  {
-    ieee_floatt f(to_constant_expr(*this));
-    f+=ieee_floatt(to_constant_expr(expr));
-    *this=f.to_expr();
-    return false;
-  }
-
-  return true;
-}
-
-bool exprt::mul(const exprt &expr)
-{
-  if(!is_constant() || !expr.is_constant())
-    return true;
-  if(type()!=expr.type())
-    return true;
-
-  const irep_idt &type_id=type().id();
-
-  if(type_id==ID_integer || type_id==ID_natural)
-  {
-    set(ID_value, integer2string(
-      string2integer(get_string(ID_value))*
-      string2integer(expr.get_string(ID_value))));
-    return false;
-  }
-  else if(type_id==ID_rational)
-  {
-    rationalt a, b;
-    if(!to_rational(*this, a) && !to_rational(expr, b))
-    {
-      exprt a_mul_b=from_rational(a*b);
-      set(ID_value, a_mul_b.get_string(ID_value));
-      return false;
-    }
-  }
-  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
-  {
-    // the following works for signed and unsigned integers
-    set(ID_value, integer2binary(
-      binary2integer(get_string(ID_value), false)*
-      binary2integer(expr.get_string(ID_value), false),
-      unsafe_string2unsigned(type().get_string(ID_width))));
-    return false;
-  }
-  else if(type_id==ID_fixedbv)
-  {
-    fixedbvt f(to_constant_expr(*this));
-    f*=fixedbvt(to_constant_expr(expr));
-    *this=f.to_expr();
-    return false;
-  }
-  else if(type_id==ID_floatbv)
-  {
-    ieee_floatt f(to_constant_expr(*this));
-    f*=ieee_floatt(to_constant_expr(expr));
-    *this=f.to_expr();
-    return false;
-  }
-
-  return true;
-}
-
-bool exprt::subtract(const exprt &expr)
-{
-  if(!is_constant() || !expr.is_constant())
-    return true;
-
-  if(type()!=expr.type())
-    return true;
-
-  const irep_idt &type_id=type().id();
-
-  if(type_id==ID_integer || type_id==ID_natural)
-  {
-    set(ID_value, integer2string(
-      string2integer(get_string(ID_value))-
-      string2integer(expr.get_string(ID_value))));
-    return false;
-  }
-  else if(type_id==ID_rational)
-  {
-    rationalt a, b;
-    if(!to_rational(*this, a) && !to_rational(expr, b))
-    {
-      exprt a_minus_b=from_rational(a-b);
-      set(ID_value, a_minus_b.get_string(ID_value));
-      return false;
-    }
-  }
-  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
-  {
-    set(ID_value, integer2binary(
-      binary2integer(get_string(ID_value), false)-
-      binary2integer(expr.get_string(ID_value), false),
-      unsafe_string2unsigned(type().get_string(ID_width))));
-    return false;
-  }
-
-  return true;
-}
-
 const source_locationt &exprt::find_source_location() const
 {
   const source_locationt &l=source_location();
diff --git a/src/util/expr.h b/src/util/expr.h
index c78bc9b2981..ba64a3ce220 100644
--- a/src/util/expr.h
+++ b/src/util/expr.h
@@ -113,11 +113,6 @@ class exprt:public irept
   void make_true();
   void make_false();
   void make_bool(bool value);
-  void negate();
-
-  bool sum(const exprt &expr);
-  bool mul(const exprt &expr);
-  bool subtract(const exprt &expr);
 
   bool is_constant() const;
   bool is_true() const;
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 89a40b97070..9e941f58083 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -10,18 +10,19 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <cassert>
 
+#include "arith_tools.h"
 #include "base_type.h"
-#include "rational.h"
-#include "expr.h"
-#include "namespace.h"
-#include "config.h"
 #include "bv_arithmetic.h"
-#include "std_expr.h"
+#include "config.h"
+#include "expr.h"
 #include "expr_util.h"
-#include "arith_tools.h"
 #include "fixedbv.h"
-#include "rational_tools.h"
 #include "ieee_float.h"
+#include "namespace.h"
+#include "rational.h"
+#include "rational_tools.h"
+#include "std_expr.h"
+#include "string2int.h"
 
 bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
 {
@@ -53,6 +54,114 @@ bool simplify_exprt::simplify_bswap(bswap_exprt &expr)
   return true;
 }
 
+//! produce a sum of two constant expressions of the same type
+//! \return 'false' iff this was successful
+static bool sum_expr(
+  constant_exprt &dest,
+  const constant_exprt &expr)
+{
+  if(dest.type()!=expr.type())
+    return true;
+
+  const irep_idt &type_id=dest.type().id();
+
+  if(type_id==ID_integer || type_id==ID_natural)
+  {
+    dest.set_value(integer2string(
+      string2integer(id2string(dest.get_value()))+
+      string2integer(id2string(expr.get_value()))));
+    return false;
+  }
+  else if(type_id==ID_rational)
+  {
+    rationalt a, b;
+    if(!to_rational(dest, a) && !to_rational(expr, b))
+    {
+      dest=from_rational(a+b);
+      return false;
+    }
+  }
+  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
+  {
+    dest.set_value(integer2binary(
+      binary2integer(id2string(dest.get_value()), false)+
+      binary2integer(id2string(expr.get_value()), false),
+      to_bitvector_type(dest.type()).get_width()));
+    return false;
+  }
+  else if(type_id==ID_fixedbv)
+  {
+    dest.set_value(integer2binary(
+      binary2integer(id2string(dest.get_value()), false)+
+      binary2integer(id2string(expr.get_value()), false),
+      to_bitvector_type(dest.type()).get_width()));
+    return false;
+  }
+  else if(type_id==ID_floatbv)
+  {
+    ieee_floatt f(to_constant_expr(dest));
+    f+=ieee_floatt(to_constant_expr(expr));
+    dest=f.to_expr();
+    return false;
+  }
+
+  return true;
+}
+
+//! produce a product of two expressions of the same type
+//! \return 'false' iff this was successful
+static bool mul_expr(
+  constant_exprt &dest,
+  const constant_exprt &expr)
+{
+  if(dest.type()!=expr.type())
+    return true;
+
+  const irep_idt &type_id=dest.type().id();
+
+  if(type_id==ID_integer || type_id==ID_natural)
+  {
+    dest.set_value(integer2string(
+      string2integer(id2string(dest.get_value()))*
+      string2integer(id2string(expr.get_value()))));
+    return false;
+  }
+  else if(type_id==ID_rational)
+  {
+    rationalt a, b;
+    if(!to_rational(dest, a) && !to_rational(expr, b))
+    {
+      dest=from_rational(a*b);
+      return false;
+    }
+  }
+  else if(type_id==ID_unsignedbv || type_id==ID_signedbv)
+  {
+    // the following works for signed and unsigned integers
+    dest.set_value(integer2binary(
+      binary2integer(id2string(dest.get_value()), false)*
+      binary2integer(id2string(expr.get_value()), false),
+      to_bitvector_type(dest.type()).get_width()));
+    return false;
+  }
+  else if(type_id==ID_fixedbv)
+  {
+    fixedbvt f(to_constant_expr(dest));
+    f*=fixedbvt(to_constant_expr(expr));
+    dest=f.to_expr();
+    return false;
+  }
+  else if(type_id==ID_floatbv)
+  {
+    ieee_floatt f(to_constant_expr(dest));
+    f*=ieee_floatt(to_constant_expr(expr));
+    dest=f.to_expr();
+    return false;
+  }
+
+  return true;
+}
+
 bool simplify_exprt::simplify_mult(exprt &expr)
 {
   // check to see if it is a number type
@@ -104,7 +213,7 @@ bool simplify_exprt::simplify_mult(exprt &expr)
       if(found)
       {
         // update the constant factor
-        if(!constant->mul(*it))
+        if(!mul_expr(to_constant_expr(*constant), to_constant_expr(*it)))
           do_erase=true;
       }
       else
@@ -356,7 +465,7 @@ bool simplify_exprt::simplify_plus(exprt &expr)
            it->is_constant() &&
            next->is_constant())
         {
-          it->sum(*next);
+          sum_expr(to_constant_expr(*it), to_constant_expr(*next));
           operands.erase(next);
         }
       }
@@ -408,7 +517,8 @@ bool simplify_exprt::simplify_plus(exprt &expr)
           }
           else
           {
-            if(!const_sum->sum(*it))
+            if(!sum_expr(to_constant_expr(*const_sum), 
+                         to_constant_expr(*it)))
             {
               *it=from_integer(0, it->type());
               assert(it->is_not_nil());