diff --git a/src/util/fixedbv.cpp b/src/util/fixedbv.cpp
index 02b441badb4..2d4202b412f 100644
--- a/src/util/fixedbv.cpp
+++ b/src/util/fixedbv.cpp
@@ -106,6 +106,18 @@ fixedbvt &fixedbvt::operator*=(const fixedbvt &o)
   return *this;
 }
 
+fixedbvt &fixedbvt::operator+=(const fixedbvt &o)
+{
+  v += o.v;
+  return *this;
+}
+
+fixedbvt &fixedbvt::operator-=(const fixedbvt &o)
+{
+  v -= o.v;
+  return *this;
+}
+
 fixedbvt &fixedbvt::operator/=(const fixedbvt &o)
 {
   v*=power(2, o.spec.get_fraction_bits());
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index de7c9a539fd..5762ad31dff 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -70,12 +70,16 @@ static bool sum_expr(
 
   const irep_idt &type_id=dest.type().id();
 
-  if(type_id==ID_integer || type_id==ID_natural)
+  if(
+    type_id == ID_integer || type_id == ID_natural ||
+    type_id == ID_unsignedbv || type_id == ID_signedbv)
   {
-    dest.set_value(integer2string(
-      string2integer(id2string(dest.get_value()))+
-      string2integer(id2string(expr.get_value()))));
-    return false;
+    mp_integer a, b;
+    if(!to_integer(dest, a) && !to_integer(expr, b))
+    {
+      dest = from_integer(a + b, dest.type());
+      return false;
+    }
   }
   else if(type_id==ID_rational)
   {
@@ -86,26 +90,17 @@ static bool sum_expr(
       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()));
+    fixedbvt f(dest);
+    f += fixedbvt(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));
+    ieee_floatt f(dest);
+    f += ieee_floatt(expr);
     dest=f.to_expr();
     return false;
   }
@@ -124,12 +119,16 @@ static bool mul_expr(
 
   const irep_idt &type_id=dest.type().id();
 
-  if(type_id==ID_integer || type_id==ID_natural)
+  if(
+    type_id == ID_integer || type_id == ID_natural ||
+    type_id == ID_unsignedbv || type_id == ID_signedbv)
   {
-    dest.set_value(integer2string(
-      string2integer(id2string(dest.get_value()))*
-      string2integer(id2string(expr.get_value()))));
-    return false;
+    mp_integer a, b;
+    if(!to_integer(dest, a) && !to_integer(expr, b))
+    {
+      dest = from_integer(a * b, dest.type());
+      return false;
+    }
   }
   else if(type_id==ID_rational)
   {
@@ -140,15 +139,6 @@ static bool mul_expr(
       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));