diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index adc20b6144f..219e372afcf 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -253,7 +253,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
     return convert_bitvector(expr.op0());
   }
   else if(expr.id()==ID_abs)
-    return convert_abs(expr);
+    return convert_abs(to_abs_expr(expr));
   else if(expr.id() == ID_bswap)
     return convert_bswap(to_bswap_expr(expr));
   else if(expr.id()==ID_byte_extract_little_endian ||
@@ -433,13 +433,7 @@ bvt boolbvt::convert_function_application(
 
 literalt boolbvt::convert_rest(const exprt &expr)
 {
-  if(expr.type().id()!=ID_bool)
-  {
-    error() << "boolbvt::convert_rest got non-boolean operand: "
-            << expr.pretty() << eom;
-    throw 0;
-  }
-
+  PRECONDITION(expr.type().id() == ID_bool);
   const exprt::operandst &operands=expr.operands();
 
   if(expr.id()==ID_typecast)
@@ -451,9 +445,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
     return convert_verilog_case_equality(to_binary_relation_expr(expr));
   else if(expr.id()==ID_notequal)
   {
-    if(expr.operands().size()!=2)
-      throw "notequal expects two operands";
-
+    DATA_INVARIANT(expr.operands().size() == 2, "notequal expects two operands");
     return !convert_equality(equal_exprt(expr.op0(), expr.op1()));
   }
   else if(expr.id()==ID_ieee_float_equal ||
@@ -480,57 +472,37 @@ literalt boolbvt::convert_rest(const exprt &expr)
   else if(expr.id()==ID_index)
   {
     bvt bv=convert_index(to_index_expr(expr));
-
-    if(bv.size()!=1)
-      throw "convert_index returned non-bool bitvector";
-
+    CHECK_RETURN(bv.size() == 1);
     return bv[0];
   }
   else if(expr.id()==ID_member)
   {
     bvt bv=convert_member(to_member_expr(expr));
-
-    if(bv.size()!=1)
-      throw "convert_member returned non-bool bitvector";
-
+    CHECK_RETURN(bv.size() == 1);
     return bv[0];
   }
   else if(expr.id()==ID_case)
   {
     bvt bv=convert_case(expr);
-
-    if(bv.size()!=1)
-      throw "convert_case returned non-bool bitvector";
-
+    CHECK_RETURN(bv.size() == 1);
     return bv[0];
   }
   else if(expr.id()==ID_cond)
   {
     bvt bv=convert_cond(expr);
-
-    if(bv.size()!=1)
-      throw "convert_cond returned non-bool bitvector";
-
+    CHECK_RETURN(bv.size() == 1);
     return bv[0];
   }
   else if(expr.id()==ID_sign)
   {
-    if(expr.operands().size()!=1)
-      throw "sign expects one operand";
-
+    DATA_INVARIANT(expr.operands().size() == 1, "sign expects one operand");
     const bvt &bv=convert_bv(operands[0]);
-
-    if(bv.empty())
-      throw "sign operator takes one non-empty operand";
-
-    if(operands[0].type().id()==ID_signedbv)
+    CHECK_RETURN(!bv.empty());
+    const irep_idt type_id = operands[0].type().id();
+    if(type_id == ID_signedbv || type_id == ID_fixedbv || type_id == ID_floatbv)
       return bv[bv.size()-1];
-    else if(operands[0].type().id()==ID_unsignedbv)
+    if(type_id == ID_unsignedbv)
       return const_literal(false);
-    else if(operands[0].type().id()==ID_fixedbv)
-      return bv[bv.size()-1];
-    else if(operands[0].type().id()==ID_floatbv)
-      return bv[bv.size()-1];
   }
   else if(expr.id()==ID_reduction_or  || expr.id()==ID_reduction_and  ||
           expr.id()==ID_reduction_nor || expr.id()==ID_reduction_nand ||
@@ -542,9 +514,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
     return convert_overflow(expr);
   else if(expr.id()==ID_isnan)
   {
-    if(expr.operands().size()!=1)
-      throw "isnan expects one operand";
-
+    DATA_INVARIANT(expr.operands().size() == 1, "isnan expects one operand");
     const bvt &bv=convert_bv(operands[0]);
 
     if(expr.op0().type().id()==ID_floatbv)
@@ -552,16 +522,13 @@ literalt boolbvt::convert_rest(const exprt &expr)
       float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
       return float_utils.is_NaN(bv);
     }
-    else if(expr.op0().type().id()==ID_fixedbv)
+    else if(expr.op0().type().id() == ID_fixedbv)
       return const_literal(false);
   }
   else if(expr.id()==ID_isfinite)
   {
-    if(expr.operands().size()!=1)
-      throw "isfinite expects one operand";
-
+    DATA_INVARIANT(expr.operands().size() == 1, "isfinite expects one operand");
     const bvt &bv=convert_bv(operands[0]);
-
     if(expr.op0().type().id()==ID_floatbv)
     {
       float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
@@ -569,37 +536,31 @@ literalt boolbvt::convert_rest(const exprt &expr)
         !float_utils.is_infinity(bv),
         !float_utils.is_NaN(bv));
     }
-    else if(expr.op0().type().id()==ID_fixedbv)
+    else if(expr.op0().type().id() == ID_fixedbv)
       return const_literal(true);
   }
   else if(expr.id()==ID_isinf)
   {
-    if(expr.operands().size()!=1)
-      throw "isinf expects one operand";
-
+    DATA_INVARIANT(expr.operands().size() == 1, "isinf expects one operand");
     const bvt &bv=convert_bv(operands[0]);
-
     if(expr.op0().type().id()==ID_floatbv)
     {
       float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
       return float_utils.is_infinity(bv);
     }
-    else if(expr.op0().type().id()==ID_fixedbv)
+    else if(expr.op0().type().id() == ID_fixedbv)
       return const_literal(false);
   }
   else if(expr.id()==ID_isnormal)
   {
-    if(expr.operands().size()!=1)
-      throw "isnormal expects one operand";
-
-    const bvt &bv=convert_bv(operands[0]);
-
+    DATA_INVARIANT(expr.operands().size() == 1, "isnormal expects one operand");
     if(expr.op0().type().id()==ID_floatbv)
     {
+      const bvt &bv = convert_bv(operands[0]);
       float_utilst float_utils(prop, to_floatbv_type(expr.op0().type()));
       return float_utils.is_normal(bv);
     }
-    else if(expr.op0().type().id()==ID_fixedbv)
+    else if(expr.op0().type().id() == ID_fixedbv)
       return const_literal(true);
   }
 
@@ -699,17 +660,16 @@ void boolbvt::print_assignment(std::ostream &out) const
     out << pair.first << "=" << pair.second.get_value(prop) << '\n';
 }
 
-void boolbvt::build_offset_map(const struct_typet &src, offset_mapt &dest)
+boolbvt::offset_mapt boolbvt::build_offset_map(const struct_typet &src)
 {
-  const struct_typet::componentst &components=
-    src.components();
-
-  dest.resize(components.size());
-  std::size_t offset=0;
-  for(std::size_t i=0; i<components.size(); i++)
+  const struct_typet::componentst &components = src.components();
+  offset_mapt dest;
+  dest.reserve(components.size());
+  std::size_t offset = 0;
+  for(const auto &comp : components)
   {
-    std::size_t comp_width=boolbv_width(components[i].type());
-    dest[i]=offset;
-    offset+=comp_width;
+    dest.push_back(offset);
+    offset += boolbv_width(comp.type());
   }
+  return dest;
 }
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index f6e85baf83d..429a5aa4b37 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -163,7 +163,7 @@ class boolbvt:public arrayst
   virtual bvt convert_shift(const binary_exprt &expr);
   virtual bvt convert_bitwise(const exprt &expr);
   virtual bvt convert_unary_minus(const unary_exprt &expr);
-  virtual bvt convert_abs(const exprt &expr);
+  virtual bvt convert_abs(const abs_exprt &expr);
   virtual bvt convert_concatenation(const exprt &expr);
   virtual bvt convert_replication(const replication_exprt &expr);
   virtual bvt convert_bv_literals(const exprt &expr);
@@ -250,7 +250,7 @@ class boolbvt:public arrayst
   void post_process_quantifiers();
 
   typedef std::vector<std::size_t> offset_mapt;
-  void build_offset_map(const struct_typet &src, offset_mapt &dest);
+  offset_mapt build_offset_map(const struct_typet &src);
 
   // strings
   numbering<irep_idt> string_numbering;
diff --git a/src/solvers/flattening/boolbv_abs.cpp b/src/solvers/flattening/boolbv_abs.cpp
index 1caabde0fa4..e43451f282e 100644
--- a/src/solvers/flattening/boolbv_abs.cpp
+++ b/src/solvers/flattening/boolbv_abs.cpp
@@ -14,26 +14,19 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include <solvers/floatbv/float_utils.h>
 
-bvt boolbvt::convert_abs(const exprt &expr)
+bvt boolbvt::convert_abs(const abs_exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
+  const std::size_t width = boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  const exprt::operandst &operands=expr.operands();
+  const bvt &op_bv=convert_bv(expr.op());
 
-  if(operands.size()!=1)
-    throw "abs takes one operand";
-
-  const exprt &op0=expr.op0();
-
-  const bvt &op_bv=convert_bv(op0);
-
-  if(op0.type()!=expr.type())
+  if(expr.op().type()!=expr.type())
     return conversion_failed(expr);
 
-  bvtypet bvtype=get_bvtype(expr.type());
+  const bvtypet bvtype = get_bvtype(expr.type());
 
   if(bvtype==bvtypet::IS_FIXED ||
      bvtype==bvtypet::IS_SIGNED ||
diff --git a/src/solvers/flattening/boolbv_bitwise.cpp b/src/solvers/flattening/boolbv_bitwise.cpp
index 9eda6eafcd9..33d4a1c2021 100644
--- a/src/solvers/flattening/boolbv_bitwise.cpp
+++ b/src/solvers/flattening/boolbv_bitwise.cpp
@@ -11,23 +11,16 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_bitwise(const exprt &expr)
 {
-  std::size_t width=boolbv_width(expr.type());
-
+  const std::size_t width = boolbv_width(expr.type());
   if(width==0)
     return conversion_failed(expr);
 
   if(expr.id()==ID_bitnot)
   {
-    if(expr.operands().size()!=1)
-      throw "bitnot takes one operand";
-
+    DATA_INVARIANT(expr.operands().size() == 1, "bitnot takes one operand");
     const exprt &op0=expr.op0();
-
     const bvt &op_bv=convert_bv(op0);
-
-    if(op_bv.size()!=width)
-      throw "convert_bitwise: unexpected operand width";
-
+    CHECK_RETURN(op_bv.size() == width);
     return bv_utils.inverted(op_bv);
   }
   else if(expr.id()==ID_bitand || expr.id()==ID_bitor ||
@@ -41,9 +34,7 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
     forall_operands(it, expr)
     {
       const bvt &op=convert_bv(*it);
-
-      if(op.size()!=width)
-        throw "convert_bitwise: unexpected operand width";
+      CHECK_RETURN(op.size() == width);
 
       if(it==expr.operands().begin())
         bv=op;
@@ -64,7 +55,7 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
           else if(expr.id()==ID_bitxnor)
             bv[i]=prop.lequal(bv[i], op[i]);
           else
-            throw "unexpected operand";
+            UNIMPLEMENTED;
         }
       }
     }
@@ -72,5 +63,5 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
     return bv;
   }
 
-  throw "unexpected bitwise operand";
+  UNIMPLEMENTED;
 }
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index b489a9b1924..86fd36231f9 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -23,16 +23,15 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 {
-  assert(map.number_of_bits()==src.size());
-
+  PRECONDITION(map.number_of_bits() == src.size());
   bvt result;
-  result.resize(src.size(), const_literal(false));
+  result.reserve(src.size());
 
   for(std::size_t i=0; i<src.size(); i++)
   {
-    size_t mapped_index=map.map_bit(i);
-    assert(mapped_index<src.size());
-    result[i]=src[mapped_index];
+    const size_t mapped_index = map.map_bit(i);
+    CHECK_RETURN(mapped_index < src.size());
+    result.push_back(src[mapped_index]);
   }
 
   return result;
@@ -40,16 +39,12 @@ bvt map_bv(const bv_endianness_mapt &map, const bvt &src)
 
 bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 {
-  if(expr.operands().size()!=2)
-    throw "byte_extract takes two operands";
-
   // if we extract from an unbounded array, call the flattening code
   if(is_unbounded_array(expr.op().type()))
   {
     try
     {
-      exprt tmp = flatten_byte_extract(expr, ns);
-      return convert_bv(tmp);
+      return convert_bv(flatten_byte_extract(expr, ns));
     }
     catch(const flatten_byte_extract_exceptiont &byte_extract_flatten_exception)
     {
@@ -58,7 +53,7 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
     }
   }
 
-  std::size_t width=boolbv_width(expr.type());
+  const std::size_t width = boolbv_width(expr.type());
 
   // special treatment for bit-fields and big-endian:
   // we need byte granularity
@@ -105,22 +100,10 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
   const exprt &op=expr.op();
   const exprt &offset=expr.offset();
-
-  bool little_endian;
-
-  if(expr.id()==ID_byte_extract_little_endian)
-    little_endian=true;
-  else if(expr.id()==ID_byte_extract_big_endian)
-    little_endian=false;
-  else
-  {
-    little_endian=false;
-    assert(false);
-  }
+  const bool little_endian = expr.id() == ID_byte_extract_little_endian;
 
   // first do op0
-
-  bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
+  const bv_endianness_mapt op_map(op.type(), little_endian, ns, boolbv_width);
   const bvt op_bv=map_bv(op_map, convert_bv(op));
 
   // do result
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index ba5b70e52b8..ca66fb2c697 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -17,12 +17,6 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_index(const index_exprt &expr)
 {
-  if(expr.id()!=ID_index)
-    throw "expected index expression";
-
-  if(expr.operands().size()!=2)
-    throw "index takes two operands";
-
   const exprt &array=expr.array();
   const exprt &index=expr.index();
 
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index 838c8df84ac..724b59b6a78 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -530,10 +530,8 @@ bool boolbvt::type_conversion(
           op_struct.components();
 
         // build offset maps
-        offset_mapt op_offsets, dest_offsets;
-
-        build_offset_map(op_struct, op_offsets);
-        build_offset_map(dest_struct, dest_offsets);
+        const offset_mapt op_offsets = build_offset_map(op_struct);
+        const offset_mapt dest_offsets = build_offset_map(dest_struct);
 
         // build name map
         typedef std::map<irep_idt, std::size_t> op_mapt;