diff --git a/src/util/bv_arithmetic.cpp b/src/util/bv_arithmetic.cpp
index 88d4cff5702..cb452fba194 100644
--- a/src/util/bv_arithmetic.cpp
+++ b/src/util/bv_arithmetic.cpp
@@ -82,7 +82,7 @@ mp_integer bv_arithmetict::pack() const
   return value+power(2, spec.width);
 }
 
-exprt bv_arithmetict::to_expr() const
+constant_exprt bv_arithmetict::to_expr() const
 {
   return constant_exprt(integer2bvrep(value, spec.width), spec.to_type());
 }
@@ -180,10 +180,8 @@ void bv_arithmetict::change_spec(const bv_spect &dest_spec)
   adjust();
 }
 
-void bv_arithmetict::from_expr(const exprt &expr)
+void bv_arithmetict::from_expr(const constant_exprt &expr)
 {
-  PRECONDITION(expr.is_constant());
   spec=bv_spect(expr.type());
-  value = bvrep2integer(
-    to_constant_expr(expr).get_value(), spec.width, spec.is_signed);
+  value = bvrep2integer(expr.get_value(), spec.width, spec.is_signed);
 }
diff --git a/src/util/bv_arithmetic.h b/src/util/bv_arithmetic.h
index 3774344d18f..bb0e52abe06 100644
--- a/src/util/bv_arithmetic.h
+++ b/src/util/bv_arithmetic.h
@@ -15,6 +15,7 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "mp_arith.h"
 #include "format_spec.h"
 
+class constant_exprt;
 class exprt;
 class typet;
 
@@ -60,7 +61,7 @@ class bv_arithmetict
   {
   }
 
-  explicit bv_arithmetict(const exprt &expr)
+  explicit bv_arithmetict(const constant_exprt &expr)
   {
     from_expr(expr);
   }
@@ -91,8 +92,8 @@ class bv_arithmetict
   std::string format(const format_spect &format_spec) const;
 
   // expressions
-  exprt to_expr() const;
-  void from_expr(const exprt &expr);
+  constant_exprt to_expr() const;
+  void from_expr(const constant_exprt &expr);
 
   bv_arithmetict &operator/=(const bv_arithmetict &other);
   bv_arithmetict &operator*=(const bv_arithmetict &other);