diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 53f1cdcb44e..ea001385f9b 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -224,9 +224,8 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
           expr.id()=="no-overflow-plus" ||
           expr.id()=="no-overflow-minus")
     return convert_add_sub(expr);
-  else if(expr.id()==ID_mult ||
-          expr.id()=="no-overflow-mult")
-    return convert_mult(expr);
+  else if(expr.id() == ID_mult)
+    return convert_mult(to_mult_expr(expr));
   else if(expr.id()==ID_div)
     return convert_div(to_div_expr(expr));
   else if(expr.id()==ID_mod)
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index c51f3a3803b..ffcce81c9da 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -152,7 +152,7 @@ class boolbvt:public arrayst
   virtual bvt convert_union(const union_exprt &expr);
   virtual bvt convert_bv_typecast(const typecast_exprt &expr);
   virtual bvt convert_add_sub(const exprt &expr);
-  virtual bvt convert_mult(const exprt &expr);
+  virtual bvt convert_mult(const mult_exprt &expr);
   virtual bvt convert_div(const div_exprt &expr);
   virtual bvt convert_mod(const mod_exprt &expr);
   virtual bvt convert_floatbv_op(const exprt &expr);
diff --git a/src/solvers/flattening/boolbv_map.cpp b/src/solvers/flattening/boolbv_map.cpp
index fd12b81ebd7..ab90f63a873 100644
--- a/src/solvers/flattening/boolbv_map.cpp
+++ b/src/solvers/flattening/boolbv_map.cpp
@@ -67,7 +67,9 @@ boolbv_mapt::map_entryt &boolbv_mapt::get_map_entry(
     map_entry.literal_map.resize(map_entry.width);
   }
 
-  assert(map_entry.literal_map.size()==map_entry.width);
+  INVARIANT(
+    map_entry.literal_map.size() == map_entry.width,
+    "number of literals in the literal map shall equal the bitvector width");
 
   return map_entry;
 }
@@ -89,15 +91,18 @@ void boolbv_mapt::get_literals(
 {
   map_entryt &map_entry=get_map_entry(identifier, type);
 
-  assert(literals.size()==width);
-  assert(map_entry.literal_map.size()==width);
+  PRECONDITION(literals.size() == width);
+  INVARIANT(
+    map_entry.literal_map.size() == width,
+    "number of literals in the literal map shall equal the bitvector width");
 
   Forall_literals(it, literals)
   {
     literalt &l=*it;
     const std::size_t bit=it-literals.begin();
 
-    assert(bit<map_entry.literal_map.size());
+    INVARIANT(
+      bit < map_entry.literal_map.size(), "bit index shall be within bounds");
     map_bitt &mb=map_entry.literal_map[bit];
 
     if(mb.is_set)
@@ -128,12 +133,15 @@ void boolbv_mapt::set_literals(
   forall_literals(it, literals)
   {
     const literalt &literal=*it;
-    const std::size_t bit=it-literals.begin();
 
-    assert(literal.is_constant() ||
-           literal.var_no()<prop.no_variables());
+    INVARIANT(
+      literal.is_constant() || literal.var_no() < prop.no_variables(),
+      "variable number of non-constant literals shall be within bounds");
+
+    const std::size_t bit = it - literals.begin();
 
-    assert(bit<map_entry.literal_map.size());
+    INVARIANT(
+      bit < map_entry.literal_map.size(), "bit index shall be within bounds");
     map_bitt &mb=map_entry.literal_map[bit];
 
     if(mb.is_set)
diff --git a/src/solvers/flattening/boolbv_member.cpp b/src/solvers/flattening/boolbv_member.cpp
index e6dbf1c0b5f..9c41aa3c37a 100644
--- a/src/solvers/flattening/boolbv_member.cpp
+++ b/src/solvers/flattening/boolbv_member.cpp
@@ -28,8 +28,12 @@ bvt boolbvt::convert_member(const member_exprt &expr)
                          from_integer(0, index_type()),
                          expr.type()));
   }
-  else if(struct_op_type.id()==ID_struct)
+  else
   {
+    INVARIANT(
+      struct_op_type.id() == ID_struct,
+      "member_exprt should denote access to a union or struct");
+
     const irep_idt &component_name=expr.get_component_name();
     const struct_typet::componentst &components=
       to_struct_type(struct_op_type).components();
@@ -43,22 +47,18 @@ bvt boolbvt::convert_member(const member_exprt &expr)
 
       if(c.get_name() == component_name)
       {
-        if(!base_type_eq(subtype, expr.type(), ns))
-        {
-          #if 0
-          std::cout << "DEBUG " << expr.pretty() << "\n";
-          #endif
-
-          error().source_location=expr.find_source_location();
-          error() << "member: component type does not match: "
-                  << subtype.pretty() << " vs. "
-                  << expr.type().pretty() << eom;
-          throw 0;
-        }
+        DATA_INVARIANT_WITH_DIAGNOSTICS(
+          base_type_eq(subtype, expr.type(), ns),
+          "struct component type shall match the member expression type",
+          subtype.pretty(),
+          expr.type().pretty());
 
         bvt bv;
         bv.resize(sub_width);
-        assert(offset+sub_width<=struct_bv.size());
+        INVARIANT(
+          offset + sub_width <= struct_bv.size(),
+          "bitvector part corresponding to struct element shall be contained "
+          "within the full struct bitvector");
 
         for(std::size_t i=0; i<sub_width; i++)
           bv[i]=struct_bv[offset+i];
@@ -69,15 +69,10 @@ bvt boolbvt::convert_member(const member_exprt &expr)
       offset+=sub_width;
     }
 
-    error().source_location=expr.find_source_location();
-    error() << "component " << component_name
-            << " not found in structure" << eom;
-    throw 0;
-  }
-  else
-  {
-    error().source_location=expr.find_source_location();
-    error() << "member takes struct or union operand" << eom;
-    throw 0;
+    INVARIANT_WITH_DIAGNOSTICS(
+      false,
+      "struct type shall contain component accessed by member expression",
+      expr.find_source_location(),
+      id2string(component_name));
   }
 }
diff --git a/src/solvers/flattening/boolbv_mod.cpp b/src/solvers/flattening/boolbv_mod.cpp
index 1692fbc6a2f..c4a846dba65 100644
--- a/src/solvers/flattening/boolbv_mod.cpp
+++ b/src/solvers/flattening/boolbv_mod.cpp
@@ -27,20 +27,22 @@ bvt boolbvt::convert_mod(const mod_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  if(expr.op0().type().id()!=expr.type().id() ||
-     expr.op1().type().id()!=expr.type().id())
-    throw "mod got mixed-type operands";
+  DATA_INVARIANT(
+    expr.op0().type().id() == expr.type().id(),
+    "type of the first operand of a modulo operation shall equal the "
+    "expression type");
+
+  DATA_INVARIANT(
+    expr.op1().type().id() == expr.type().id(),
+    "type of the second operand of a modulo operation shall equal the "
+    "expression type");
 
   bv_utilst::representationt rep=
     expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                   bv_utilst::representationt::UNSIGNED;
 
-  const bvt &op0=convert_bv(expr.op0());
-  const bvt &op1=convert_bv(expr.op1());
-
-  if(op0.size()!=width ||
-     op1.size()!=width)
-    throw "convert_mod: unexpected operand width";
+  const bvt &op0 = convert_bv(expr.op0(), width);
+  const bvt &op1 = convert_bv(expr.op1(), width);
 
   bvt res, rem;
 
diff --git a/src/solvers/flattening/boolbv_mult.cpp b/src/solvers/flattening/boolbv_mult.cpp
index 15803b7ead5..6c5fc553789 100644
--- a/src/solvers/flattening/boolbv_mult.cpp
+++ b/src/solvers/flattening/boolbv_mult.cpp
@@ -10,7 +10,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <util/std_types.h>
 
-bvt boolbvt::convert_mult(const exprt &expr)
+bvt boolbvt::convert_mult(const mult_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
@@ -21,22 +21,17 @@ bvt boolbvt::convert_mult(const exprt &expr)
   bv.resize(width);
 
   const exprt::operandst &operands=expr.operands();
-  if(operands.empty())
-    throw "mult without operands";
+  DATA_INVARIANT(!operands.empty(), "multiplication must have operands");
 
   const exprt &op0=expr.op0();
 
-  bool no_overflow=expr.id()=="no-overflow-mult";
+  DATA_INVARIANT(
+    op0.type() == expr.type(),
+    "multiplication operands should have same type as expression");
 
   if(expr.type().id()==ID_fixedbv)
   {
-    if(op0.type()!=expr.type())
-      throw "multiplication with mixed types";
-
-    bv=convert_bv(op0);
-
-    if(bv.size()!=width)
-      throw "convert_mult: unexpected operand width";
+    bv = convert_bv(op0, width);
 
     std::size_t fraction_bits=
       to_fixedbv_type(expr.type()).get_fraction_bits();
@@ -44,16 +39,14 @@ bvt boolbvt::convert_mult(const exprt &expr)
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
-      if(it->type()!=expr.type())
-        throw "multiplication with mixed types";
+      DATA_INVARIANT(
+        it->type() == expr.type(),
+        "multiplication operands should have same type as expression");
 
       // do a sign extension by fraction_bits bits
       bv=bv_utils.sign_extension(bv, bv.size()+fraction_bits);
 
-      bvt op=convert_bv(*it);
-
-      if(op.size()!=width)
-        throw "convert_mult: unexpected operand width";
+      bvt op = convert_bv(*it, width);
 
       op=bv_utils.sign_extension(op, bv.size());
 
@@ -68,33 +61,22 @@ bvt boolbvt::convert_mult(const exprt &expr)
   else if(expr.type().id()==ID_unsignedbv ||
           expr.type().id()==ID_signedbv)
   {
-    if(op0.type()!=expr.type())
-      throw "multiplication with mixed types";
-
     bv_utilst::representationt rep=
       expr.type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                     bv_utilst::representationt::UNSIGNED;
 
-    bv=convert_bv(op0);
-
-    if(bv.size()!=width)
-      throw "convert_mult: unexpected operand width";
+    bv = convert_bv(op0, width);
 
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
-      if(it->type()!=expr.type())
-        throw "multiplication with mixed types";
-
-      const bvt &op=convert_bv(*it);
+      DATA_INVARIANT(
+        it->type() == expr.type(),
+        "multiplication operands should have same type as expression");
 
-      if(op.size()!=width)
-        throw "convert_mult: unexpected operand width";
+      const bvt &op = convert_bv(*it, width);
 
-      if(no_overflow)
-        bv=bv_utils.multiplier_no_overflow(bv, op, rep);
-      else
-        bv=bv_utils.multiplier(bv, op, rep);
+      bv = bv_utils.multiplier(bv, op, rep);
     }
 
     return bv;
diff --git a/src/solvers/flattening/boolbv_not.cpp b/src/solvers/flattening/boolbv_not.cpp
index d57cb1e9dff..039707a1acb 100644
--- a/src/solvers/flattening/boolbv_not.cpp
+++ b/src/solvers/flattening/boolbv_not.cpp
@@ -12,9 +12,7 @@ Author: Daniel Kroening, kroening@kroening.com
 bvt boolbvt::convert_not(const not_exprt &expr)
 {
   const bvt &op_bv=convert_bv(expr.op());
-
-  if(op_bv.empty())
-    throw "not operator takes one non-empty operand";
+  CHECK_RETURN(!op_bv.empty());
 
   const typet &op_type=expr.op().type();
 
diff --git a/src/solvers/flattening/boolbv_onehot.cpp b/src/solvers/flattening/boolbv_onehot.cpp
index 168185e00f8..78d5a126d7b 100644
--- a/src/solvers/flattening/boolbv_onehot.cpp
+++ b/src/solvers/flattening/boolbv_onehot.cpp
@@ -11,6 +11,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 literalt boolbvt::convert_onehot(const unary_exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_onehot || expr.id() == ID_onehot0);
+
   bvt op=convert_bv(expr.op());
 
   literalt one_seen=const_literal(false);
@@ -25,8 +27,12 @@ literalt boolbvt::convert_onehot(const unary_exprt &expr)
 
   if(expr.id()==ID_onehot)
     return prop.land(one_seen, !more_than_one_seen);
-  else if(expr.id()==ID_onehot0)
-    return !more_than_one_seen;
   else
-    throw "unexpected onehot expression";
+  {
+    INVARIANT(
+      expr.id() == ID_onehot0,
+      "should be a onehot0 expression as other onehot expression kind has been "
+      "handled in other branch");
+    return !more_than_one_seen;
+  }
 }
diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp
index f7e4798f780..01e4672739d 100644
--- a/src/solvers/flattening/boolbv_overflow.cpp
+++ b/src/solvers/flattening/boolbv_overflow.cpp
@@ -19,8 +19,9 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   if(expr.id()==ID_overflow_plus ||
      expr.id()==ID_overflow_minus)
   {
-    if(operands.size()!=2)
-      throw "operator "+expr.id_string()+" takes two operands";
+    DATA_INVARIANT(
+      operands.size() == 2,
+      "expression " + expr.id_string() + " should have two operands");
 
     const bvt &bv0=convert_bv(operands[0]);
     const bvt &bv1=convert_bv(operands[1]);
@@ -38,27 +39,25 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   }
   else if(expr.id()==ID_overflow_mult)
   {
-    if(operands.size()!=2)
-      throw "operator "+expr.id_string()+" takes two operands";
+    DATA_INVARIANT(
+      operands.size() == 2,
+      "overflow_mult expression should have two operands");
 
     if(operands[0].type().id()!=ID_unsignedbv &&
        operands[0].type().id()!=ID_signedbv)
       return SUB::convert_rest(expr);
 
     bvt bv0=convert_bv(operands[0]);
-    bvt bv1=convert_bv(operands[1]);
-
-    if(bv0.size()!=bv1.size())
-      throw "operand size mismatch on overflow-*";
+    bvt bv1 = convert_bv(operands[1], bv0.size());
 
     bv_utilst::representationt rep=
       operands[0].type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
                                            bv_utilst::representationt::UNSIGNED;
 
-    if(operands[0].type()!=operands[1].type())
-      throw "operand type mismatch on overflow-*";
+    DATA_INVARIANT(
+      operands[0].type() == operands[1].type(),
+      "operands of overflow_mult expression shall have same type");
 
-    DATA_INVARIANT(bv0.size()==bv1.size(), "operands size mismatch");
     std::size_t old_size=bv0.size();
     std::size_t new_size=old_size*2;
 
@@ -97,8 +96,8 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   }
   else if(expr.id() == ID_overflow_shl)
   {
-    if(operands.size() != 2)
-      throw "operator " + expr.id_string() + " takes two operands";
+    DATA_INVARIANT(
+      operands.size() == 2, "overflow_shl expression should have two operands");
 
     const bvt &bv0=convert_bv(operands[0]);
     const bvt &bv1=convert_bv(operands[1]);
@@ -163,47 +162,14 @@ literalt boolbvt::convert_overflow(const exprt &expr)
   }
   else if(expr.id()==ID_overflow_unary_minus)
   {
-    if(operands.size()!=1)
-      throw "operator "+expr.id_string()+" takes one operand";
+    DATA_INVARIANT(
+      operands.size() == 1,
+      "overflow_unary_minus expression should have one operand");
 
     const bvt &bv=convert_bv(operands[0]);
 
     return bv_utils.overflow_negate(bv);
   }
-  else if(has_prefix(expr.id_string(), "overflow-typecast-"))
-  {
-    std::size_t bits=unsafe_string2unsigned(id2string(expr.id()).substr(18));
-
-    const exprt::operandst &operands=expr.operands();
-
-    if(operands.size()!=1)
-      throw "operator "+expr.id_string()+" takes one operand";
-
-    const exprt &op=operands[0];
-
-    const bvt &bv=convert_bv(op);
-
-    if(bits>=bv.size() || bits==0)
-      throw "overflow-typecast got wrong number of bits";
-
-    // signed or unsigned?
-    if(op.type().id()==ID_signedbv)
-    {
-      bvt tmp_bv;
-      for(std::size_t i=bits; i<bv.size(); i++)
-        tmp_bv.push_back(prop.lxor(bv[bits-1], bv[i]));
-
-      return prop.lor(tmp_bv);
-    }
-    else
-    {
-      bvt tmp_bv;
-      for(std::size_t i=bits; i<bv.size(); i++)
-        tmp_bv.push_back(bv[i]);
-
-      return prop.lor(tmp_bv);
-    }
-  }
 
   return SUB::convert_rest(expr);
 }
diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h
index b371a9feda8..29c265b3c42 100644
--- a/src/solvers/refinement/bv_refinement.h
+++ b/src/solvers/refinement/bv_refinement.h
@@ -51,7 +51,7 @@ class bv_refinementt:public bv_pointerst
   void post_process_arrays() override;
 
   // Refine arithmetic
-  bvt convert_mult(const exprt &expr) override;
+  bvt convert_mult(const mult_exprt &expr) override;
   bvt convert_div(const div_exprt &expr) override;
   bvt convert_mod(const mod_exprt &expr) override;
   bvt convert_floatbv_op(const exprt &expr) override;
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 86641b8ffa4..0dc3673be39 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -50,7 +50,7 @@ bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
   return bv;
 }
 
-bvt bv_refinementt::convert_mult(const exprt &expr)
+bvt bv_refinementt::convert_mult(const mult_exprt &expr)
 {
   if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
     return SUB::convert_mult(expr);
@@ -65,7 +65,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
   PRECONDITION(operands.size()>=2);
 
   if(operands.size()>2)
-    return convert_mult(make_binary(expr)); // make binary
+    return convert_mult(to_mult_expr(make_binary(expr))); // make binary
 
   // we keep multiplication by a constant for integers
   if(type.id()!=ID_floatbv)