diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 109273237b3..53f1cdcb44e 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -110,7 +110,8 @@ bool boolbvt::literal(
   throw "found no literal for expression";
 }
 
-const bvt &boolbvt::convert_bv(const exprt &expr)
+const bvt &
+boolbvt::convert_bv(const exprt &expr, optionalt<std::size_t> expected_width)
 {
   // check cache first
   std::pair<bv_cachet::iterator, bool> cache_result=
@@ -123,18 +124,27 @@ const bvt &boolbvt::convert_bv(const exprt &expr)
   // Iterators into hash_maps supposedly stay stable
   // even though we are inserting more elements recursively.
 
-  cache_result.first->second=convert_bitvector(expr);
+  const bvt &bv = convert_bitvector(expr);
+
+  INVARIANT_WITH_DIAGNOSTICS(
+    !expected_width || bv.size() == *expected_width,
+    "bitvector width shall match the indicated expected width",
+    expr.find_source_location(),
+    irep_pretty_diagnosticst(expr));
+
+  cache_result.first->second = bv;
 
   // check
   forall_literals(it, cache_result.first->second)
   {
     if(freeze_all && !it->is_constant())
       prop.set_frozen(*it);
-    if(it->var_no()==literalt::unused_var_no())
-    {
-      error() << "unused_var_no: " << expr.pretty() << eom;
-      assert(false);
-    }
+
+    INVARIANT_WITH_DIAGNOSTICS(
+      it->var_no() != literalt::unused_var_no(),
+      "variable number must be different from the unused variable number",
+      expr.find_source_location(),
+      irep_pretty_diagnosticst(expr));
   }
 
   return cache_result.first->second;
@@ -231,7 +241,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_floatbv_typecast)
     return convert_floatbv_typecast(to_floatbv_typecast_expr(expr));
   else if(expr.id()==ID_concatenation)
-    return convert_concatenation(expr);
+    return convert_concatenation(to_concatenation_expr(expr));
   else if(expr.id()==ID_replication)
     return convert_replication(to_replication_expr(expr));
   else if(expr.id()==ID_extractbits)
@@ -273,7 +283,7 @@ bvt boolbvt::convert_bitvector(const exprt &expr)
   else if(expr.id()==ID_vector)
     return convert_vector(expr);
   else if(expr.id()==ID_complex)
-    return convert_complex(expr);
+    return convert_complex(to_complex_expr(expr));
   else if(expr.id()==ID_complex_real)
     return convert_complex_real(to_complex_real_expr(expr));
   else if(expr.id()==ID_complex_imag)
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index d1f8d3ed9d3..c51f3a3803b 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -14,9 +14,10 @@ Author: Daniel Kroening, kroening@kroening.com
 // convert expression to boolean formula
 //
 
-#include <util/mp_arith.h>
-#include <util/expr.h>
 #include <util/byte_operators.h>
+#include <util/expr.h>
+#include <util/mp_arith.h>
+#include <util/optional.h>
 
 #include "bv_utils.h"
 #include "boolbv_width.h"
@@ -43,7 +44,10 @@ class boolbvt:public arrayst
   {
   }
 
-  virtual const bvt &convert_bv(const exprt &expr); // check cache
+  virtual const bvt &convert_bv( // check cache
+    const exprt &expr,
+    const optionalt<std::size_t> expected_width = nullopt);
+
   virtual bvt convert_bitvector(const exprt &expr); // no cache
 
   // overloading
@@ -139,7 +143,7 @@ class boolbvt:public arrayst
   virtual bvt convert_struct(const struct_exprt &expr);
   virtual bvt convert_array(const exprt &expr);
   virtual bvt convert_vector(const exprt &expr);
-  virtual bvt convert_complex(const exprt &expr);
+  virtual bvt convert_complex(const complex_exprt &expr);
   virtual bvt convert_complex_real(const complex_real_exprt &expr);
   virtual bvt convert_complex_imag(const complex_imag_exprt &expr);
   virtual bvt convert_lambda(const exprt &expr);
@@ -162,7 +166,7 @@ class boolbvt:public arrayst
   virtual bvt convert_bitwise(const exprt &expr);
   virtual bvt convert_unary_minus(const unary_exprt &expr);
   virtual bvt convert_abs(const abs_exprt &expr);
-  virtual bvt convert_concatenation(const exprt &expr);
+  virtual bvt convert_concatenation(const concatenation_exprt &expr);
   virtual bvt convert_replication(const replication_exprt &expr);
   virtual bvt convert_bv_literals(const exprt &expr);
   virtual bvt convert_constant(const constant_exprt &expr);
diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp
index 3656b33384a..764801efa53 100644
--- a/src/solvers/flattening/boolbv_add_sub.cpp
+++ b/src/solvers/flattening/boolbv_add_sub.cpp
@@ -15,6 +15,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_add_sub(const exprt &expr)
 {
+  PRECONDITION(
+    expr.id() == ID_plus || expr.id() == ID_minus ||
+    expr.id() == "no-overflow-plus" || expr.id() == "no-overflow-minus");
+
   const typet &type=ns.follow(expr.type());
 
   if(type.id()!=ID_unsignedbv &&
@@ -33,17 +37,15 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
   const exprt::operandst &operands=expr.operands();
 
-  if(operands.empty())
-    throw "operator "+expr.id_string()+" takes at least one operand";
+  DATA_INVARIANT(
+    !operands.empty(),
+    "operator " + expr.id_string() + " takes at least one operand");
 
   const exprt &op0=expr.op0();
   DATA_INVARIANT(
     op0.type() == type, "add/sub with mixed types:\n" + expr.pretty());
 
-  bvt bv=convert_bv(op0);
-
-  if(bv.size()!=width)
-    throw "convert_add_sub: unexpected operand 0 width";
+  bvt bv = convert_bv(op0, width);
 
   bool subtract=(expr.id()==ID_minus ||
                  expr.id()=="no-overflow-minus");
@@ -67,19 +69,16 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
     DATA_INVARIANT(
       it->type() == type, "add/sub with mixed types:\n" + expr.pretty());
 
-    const bvt &op=convert_bv(*it);
-
-    if(op.size()!=width)
-      throw "convert_add_sub: unexpected operand width";
+    const bvt &op = convert_bv(*it, width);
 
     if(type.id()==ID_vector || type.id()==ID_complex)
     {
-      const typet &subtype=ns.follow(type.subtype());
-
-      std::size_t sub_width=boolbv_width(subtype);
+      std::size_t sub_width = boolbv_width(type.subtype());
 
-      if(sub_width==0 || width%sub_width!=0)
-        throw "convert_add_sub: unexpected vector operand width";
+      INVARIANT(sub_width != 0, "vector elements shall have nonzero bit width");
+      INVARIANT(
+        width % sub_width == 0,
+        "total vector bit width shall be a multiple of the element bit width");
 
       std::size_t size=width/sub_width;
       bv.resize(width);
@@ -91,8 +90,9 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
         for(std::size_t j=0; j<tmp_op.size(); j++)
         {
-          assert(i*sub_width+j<op.size());
-          tmp_op[j]=op[i*sub_width+j];
+          const std::size_t index = i * sub_width + j;
+          INVARIANT(index < op.size(), "bit index shall be within bounds");
+          tmp_op[j] = op[index];
         }
 
         bvt tmp_result;
@@ -100,25 +100,29 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
 
         for(std::size_t j=0; j<tmp_result.size(); j++)
         {
-          assert(i*sub_width+j<bv.size());
-          tmp_result[j]=bv[i*sub_width+j];
+          const std::size_t index = i * sub_width + j;
+          INVARIANT(index < bv.size(), "bit index shall be within bounds");
+          tmp_result[j] = bv[index];
         }
 
         if(type.subtype().id()==ID_floatbv)
         {
           // needs to change due to rounding mode
-          float_utilst float_utils(prop, to_floatbv_type(subtype));
+          float_utilst float_utils(prop, to_floatbv_type(type.subtype()));
           tmp_result=float_utils.add_sub(tmp_result, tmp_op, subtract);
         }
         else
           tmp_result=bv_utils.add_sub(tmp_result, tmp_op, subtract);
 
-        assert(tmp_result.size()==sub_width);
+        INVARIANT(
+          tmp_result.size() == sub_width,
+          "applying the add/sub operation shall not change the bitwidth");
 
         for(std::size_t j=0; j<tmp_result.size(); j++)
         {
-          assert(i*sub_width+j<bv.size());
-          bv[i*sub_width+j]=tmp_result[j];
+          const std::size_t index = i * sub_width + j;
+          INVARIANT(index < bv.size(), "bit index shall be within bounds");
+          bv[index] = tmp_result[j];
         }
       }
     }
diff --git a/src/solvers/flattening/boolbv_array.cpp b/src/solvers/flattening/boolbv_array.cpp
index b96639a6d40..9bfd8c125a4 100644
--- a/src/solvers/flattening/boolbv_array.cpp
+++ b/src/solvers/flattening/boolbv_array.cpp
@@ -6,9 +6,10 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
+#include <util/invariant.h>
+
 bvt boolbvt::convert_array(const exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
@@ -18,9 +19,11 @@ bvt boolbvt::convert_array(const exprt &expr)
 
   if(expr.type().id()==ID_array)
   {
-    assert(expr.has_operands());
+    DATA_INVARIANT(
+      expr.has_operands(),
+      "the bit width being nonzero implies that the array has a nonzero size "
+      "in which case the array shall have operands");
     const exprt::operandst &operands=expr.operands();
-    assert(!operands.empty());
     std::size_t op_width=width/operands.size();
 
     bvt bv;
@@ -28,10 +31,7 @@ bvt boolbvt::convert_array(const exprt &expr)
 
     forall_expr(it, operands)
     {
-      const bvt &tmp=convert_bv(*it);
-
-      if(tmp.size()!=op_width)
-        throw "convert_array: unexpected operand width";
+      const bvt &tmp = convert_bv(*it, op_width);
 
       forall_literals(it2, tmp)
         bv.push_back(*it2);
diff --git a/src/solvers/flattening/boolbv_array_of.cpp b/src/solvers/flattening/boolbv_array_of.cpp
index 2c01f095638..055d6062833 100644
--- a/src/solvers/flattening/boolbv_array_of.cpp
+++ b/src/solvers/flattening/boolbv_array_of.cpp
@@ -9,12 +9,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 
 #include <util/arith_tools.h>
+#include <util/invariant.h>
 #include <util/std_types.h>
 
 bvt boolbvt::convert_array_of(const array_of_exprt &expr)
 {
-  if(expr.type().id()!=ID_array)
-    throw "array_of must be array-typed";
+  DATA_INVARIANT(
+    expr.type().id() == ID_array, "array_of expression shall have array type");
 
   const array_typet &array_type=to_array_type(expr.type());
 
@@ -42,21 +43,25 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
 
   const bvt &tmp=convert_bv(expr.op0());
 
+  INVARIANT(
+    size * tmp.size() == width,
+    "total array bit width shall equal the number of elements times the "
+    "element bit with");
+
   bvt bv;
   bv.resize(width);
 
-  if(size*tmp.size()!=width)
-    throw "convert_array_of: unexpected operand width";
-
-  std::size_t offset=0;
+  auto b_it = tmp.begin();
 
-  for(mp_integer i=0; i<size; i=i+1)
+  for(auto &b : bv)
   {
-    for(std::size_t j=0; j<tmp.size(); j++, offset++)
-      bv[offset]=tmp[j];
-  }
+    b = *b_it;
 
-  assert(offset==bv.size());
+    b_it++;
+
+    if(b_it == tmp.end())
+      b_it = tmp.begin();
+  }
 
   return bv;
 }
diff --git a/src/solvers/flattening/boolbv_bitwise.cpp b/src/solvers/flattening/boolbv_bitwise.cpp
index 33d4a1c2021..0daa959a560 100644
--- a/src/solvers/flattening/boolbv_bitwise.cpp
+++ b/src/solvers/flattening/boolbv_bitwise.cpp
@@ -19,8 +19,7 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
   {
     DATA_INVARIANT(expr.operands().size() == 1, "bitnot takes one operand");
     const exprt &op0=expr.op0();
-    const bvt &op_bv=convert_bv(op0);
-    CHECK_RETURN(op_bv.size() == width);
+    const bvt &op_bv = convert_bv(op0, width);
     return bv_utils.inverted(op_bv);
   }
   else if(expr.id()==ID_bitand || expr.id()==ID_bitor ||
@@ -33,8 +32,7 @@ bvt boolbvt::convert_bitwise(const exprt &expr)
 
     forall_operands(it, expr)
     {
-      const bvt &op=convert_bv(*it);
-      CHECK_RETURN(op.size() == width);
+      const bvt &op = convert_bv(*it, width);
 
       if(it==expr.operands().begin())
         bv=op;
diff --git a/src/solvers/flattening/boolbv_bswap.cpp b/src/solvers/flattening/boolbv_bswap.cpp
index e8f9c0ff52b..6f23ebb66d1 100644
--- a/src/solvers/flattening/boolbv_bswap.cpp
+++ b/src/solvers/flattening/boolbv_bswap.cpp
@@ -19,8 +19,7 @@ bvt boolbvt::convert_bswap(const bswap_exprt &expr)
   if(width % byte_bits != 0)
     return conversion_failed(expr);
 
-  bvt result = convert_bv(expr.op());
-  CHECK_RETURN(result.size() == width);
+  bvt result = convert_bv(expr.op(), width);
 
   std::size_t dest_base = width;
 
diff --git a/src/solvers/flattening/boolbv_byte_update.cpp b/src/solvers/flattening/boolbv_byte_update.cpp
index 3dab1a8544e..71b92334a99 100644
--- a/src/solvers/flattening/boolbv_byte_update.cpp
+++ b/src/solvers/flattening/boolbv_byte_update.cpp
@@ -9,19 +9,16 @@ Author: Daniel Kroening, kroening@kroening.com
 #include "boolbv.h"
 
 #include <iostream>
-#include <cassert>
 
 #include <util/arith_tools.h>
 #include <util/byte_operators.h>
+#include <util/invariant.h>
 
 #include "bv_endianness_map.h"
 
 bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
 {
-  if(expr.operands().size()!=3)
-    throw "byte_update takes three operands";
-
-  const exprt &op=expr.op0();
+  const exprt &op = expr.op();
   const exprt &offset_expr=expr.offset();
   const exprt &value=expr.value();
 
@@ -70,8 +67,11 @@ bvt boolbvt::convert_byte_update(const byte_update_exprt &expr)
           size_t index_op=map_op.map_bit(offset_i+i);
           size_t index_value=map_value.map_bit(i);
 
-          assert(index_op<bv.size());
-          assert(index_value<value_bv.size());
+          INVARIANT(
+            index_op < bv.size(), "bit vector index shall be within bounds");
+          INVARIANT(
+            index_value < value_bv.size(),
+            "bit vector index shall be within bounds");
 
           bv[index_op]=value_bv[index_value];
         }
diff --git a/src/solvers/flattening/boolbv_case.cpp b/src/solvers/flattening/boolbv_case.cpp
index 7e1d2280a32..fb031078c46 100644
--- a/src/solvers/flattening/boolbv_case.cpp
+++ b/src/solvers/flattening/boolbv_case.cpp
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_case(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_case);
+
   const std::vector<exprt> &operands=expr.operands();
 
   std::size_t width=boolbv_width(expr.type());
@@ -26,11 +28,11 @@ bvt boolbvt::convert_case(const exprt &expr)
   Forall_literals(it, bv)
     *it=prop.new_variable();
 
-  if(operands.size()<3)
-    throw "case takes at least three operands";
+  DATA_INVARIANT(
+    operands.size() >= 3, "case should have at least three operands");
 
-  if((operands.size()%2)!=1)
-    throw "number of case operands must be odd";
+  DATA_INVARIANT(
+    operands.size() % 2 == 1, "number of case operands should be odd");
 
   enum { FIRST, COMPARE, VALUE } what=FIRST;
   bvt compare_bv;
@@ -81,7 +83,7 @@ bvt boolbvt::convert_case(const exprt &expr)
       break;
 
     default:
-      assert(false);
+      UNREACHABLE;
     }
   }
 
diff --git a/src/solvers/flattening/boolbv_complex.cpp b/src/solvers/flattening/boolbv_complex.cpp
index daf931cd98d..1f541dec726 100644
--- a/src/solvers/flattening/boolbv_complex.cpp
+++ b/src/solvers/flattening/boolbv_complex.cpp
@@ -6,43 +6,36 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
-bvt boolbvt::convert_complex(const exprt &expr)
+#include <util/invariant.h>
+
+bvt boolbvt::convert_complex(const complex_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
   if(width==0)
     return conversion_failed(expr);
 
-  if(expr.type().id()==ID_complex)
-  {
-    const exprt::operandst &operands=expr.operands();
-
-    bvt bv;
-    bv.reserve(width);
+  DATA_INVARIANT(
+    expr.type().id() == ID_complex,
+    "complex expression shall have complex type");
 
-    if(operands.size()==2)
-    {
-      std::size_t op_width=width/operands.size();
+  bvt bv;
+  bv.reserve(width);
 
-      forall_expr(it, operands)
-      {
-        const bvt &tmp=convert_bv(*it);
+  const exprt::operandst &operands = expr.operands();
+  std::size_t op_width = width / operands.size();
 
-        if(tmp.size()!=op_width)
-          throw "convert_complex: unexpected operand width";
-
-        forall_literals(it2, tmp)
-          bv.push_back(*it2);
-      }
-    }
+  forall_expr(it, operands)
+  {
+    const bvt &tmp = convert_bv(*it, op_width);
 
-    return bv;
+    forall_literals(it2, tmp)
+      bv.push_back(*it2);
   }
 
-  return conversion_failed(expr);
+  return bv;
 }
 
 bvt boolbvt::convert_complex_real(const complex_real_exprt &expr)
@@ -52,9 +45,8 @@ bvt boolbvt::convert_complex_real(const complex_real_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  bvt bv = convert_bv(expr.op());
+  bvt bv = convert_bv(expr.op(), width * 2);
 
-  assert(bv.size()==width*2);
   bv.resize(width); // chop
 
   return bv;
@@ -67,9 +59,8 @@ bvt boolbvt::convert_complex_imag(const complex_imag_exprt &expr)
   if(width==0)
     return conversion_failed(expr);
 
-  bvt bv = convert_bv(expr.op());
+  bvt bv = convert_bv(expr.op(), width * 2);
 
-  assert(bv.size()==width*2);
   bv.erase(bv.begin(), bv.begin()+width);
 
   return bv;
diff --git a/src/solvers/flattening/boolbv_concatenation.cpp b/src/solvers/flattening/boolbv_concatenation.cpp
index 73a2a1b922b..7ed2331c652 100644
--- a/src/solvers/flattening/boolbv_concatenation.cpp
+++ b/src/solvers/flattening/boolbv_concatenation.cpp
@@ -6,10 +6,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
-bvt boolbvt::convert_concatenation(const exprt &expr)
+#include <util/invariant.h>
+
+bvt boolbvt::convert_concatenation(const concatenation_exprt &expr)
 {
   std::size_t width=boolbv_width(expr.type());
 
@@ -18,8 +19,8 @@ bvt boolbvt::convert_concatenation(const exprt &expr)
 
   const exprt::operandst &operands=expr.operands();
 
-  if(operands.empty())
-    throw "concatenation takes at least one operand";
+  DATA_INVARIANT(
+    !operands.empty(), "concatentation shall have at least one operand");
 
   std::size_t offset=width;
   bvt bv;
@@ -29,8 +30,9 @@ bvt boolbvt::convert_concatenation(const exprt &expr)
   {
     const bvt &op=convert_bv(*it);
 
-    if(op.size()>offset)
-      throw "concatenation operand width too big";
+    INVARIANT(
+      op.size() <= offset,
+      "concatentation operand must fit into the result bitvector");
 
     offset-=op.size();
 
@@ -38,8 +40,10 @@ bvt boolbvt::convert_concatenation(const exprt &expr)
       bv[offset+i]=op[i];
   }
 
-  if(offset!=0)
-    throw "concatenation operand width too small";
+  INVARIANT(
+    offset == 0,
+    "all bits in the result bitvector must have been filled up by the "
+    "concatentation operands");
 
   return bv;
 }
diff --git a/src/solvers/flattening/boolbv_cond.cpp b/src/solvers/flattening/boolbv_cond.cpp
index e6bb129b0d4..fe36739055b 100644
--- a/src/solvers/flattening/boolbv_cond.cpp
+++ b/src/solvers/flattening/boolbv_cond.cpp
@@ -12,6 +12,8 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_cond(const exprt &expr)
 {
+  PRECONDITION(expr.id() == ID_cond);
+
   const exprt::operandst &operands=expr.operands();
 
   std::size_t width=boolbv_width(expr.type());
@@ -22,11 +24,10 @@ bvt boolbvt::convert_cond(const exprt &expr)
   bvt bv;
   bv.resize(width);
 
-  if(operands.size()<2)
-    throw "cond takes at least two operands";
+  DATA_INVARIANT(operands.size() >= 2, "cond must have at least two operands");
 
-  if((operands.size()%2)!=0)
-    throw "number of cond operands must be even";
+  DATA_INVARIANT(
+    operands.size() % 2 == 0, "number of cond operands must be even");
 
   if(prop.has_set_to())
   {
@@ -49,13 +50,7 @@ bvt boolbvt::convert_cond(const exprt &expr)
       }
       else
       {
-        const bvt &op=convert_bv(*it);
-
-        DATA_INVARIANT(
-          bv.size() == op.size(),
-          std::string("size of value operand does not match:\n") +
-            "result size: " + std::to_string(bv.size()) +
-            "\noperand: " + std::to_string(op.size()) + '\n' + it->pretty());
+        const bvt &op = convert_bv(*it, bv.size());
 
         literalt value_literal=bv_utils.equal(bv, op);
 
@@ -70,16 +65,16 @@ bvt boolbvt::convert_cond(const exprt &expr)
     // functional version -- go backwards
     for(std::size_t i=expr.operands().size(); i!=0; i-=2)
     {
-      assert(i>=2);
+      INVARIANT(
+        i >= 2,
+        "since the number of operands is even if i is nonzero it must be "
+        "greater than two");
       const exprt &cond=expr.operands()[i-2];
       const exprt &value=expr.operands()[i-1];
 
       literalt cond_literal=convert(cond);
 
-      const bvt &op=convert_bv(value);
-
-      if(bv.size()!=op.size())
-        throw "unexpected operand size in convert_cond";
+      const bvt &op = convert_bv(value, bv.size());
 
       for(std::size_t i=0; i<bv.size(); i++)
         bv[i]=prop.lselect(cond_literal, op[i], bv[i]);
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 67abb9a73cb..16d46de9ad5 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -447,7 +447,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   }
   else if(expr.id()==ID_concatenation)
   {
-    return SUB::convert_concatenation(expr);
+    return SUB::convert_concatenation(to_concatenation_expr(expr));
   }
   else if(expr.id()==ID_byte_extract_little_endian ||
           expr.id()==ID_byte_extract_big_endian)
diff --git a/src/util/optional.h b/src/util/optional.h
index 92bcac4baf2..4fd2a1b0a17 100644
--- a/src/util/optional.h
+++ b/src/util/optional.h
@@ -36,4 +36,6 @@ using optionalt=nonstd::optional<T>; // NOLINT template typedef
 
 typedef nonstd::bad_optional_access bad_optional_accesst;
 
+using nonstd::nullopt;
+
 #endif // CPROVER_UTIL_OPTIONAL_H