diff --git a/src/solvers/flattening/arrays.cpp b/src/solvers/flattening/arrays.cpp
index b48f4c65647..f3cd3805432 100644
--- a/src/solvers/flattening/arrays.cpp
+++ b/src/solvers/flattening/arrays.cpp
@@ -34,7 +34,7 @@ void arrayst::record_array_index(const index_exprt &index)
   // we are not allowed to put the index directly in the
   //   entry for the root of the equivalence class
   //   because this map is accessed during building the error trace
-  std::size_t number=arrays.number(index.array());
+  const std::size_t number = arrays.number(index.array());
   index_map[number].insert(index.index());
   update_indices.insert(number);
 }
@@ -45,14 +45,9 @@ literalt arrayst::record_array_equality(
   const exprt &op0=equality.op0();
   const exprt &op1=equality.op1();
 
-  // check types
-  if(!base_type_eq(op0.type(), op1.type(), ns))
-  {
-    prop.error() << equality.pretty() << messaget::eom;
-    DATA_INVARIANT(
-      false,
-      "record_array_equality got equality without matching types");
-  }
+  DATA_INVARIANT(
+    base_type_eq(op0.type(), op1.type(), ns),
+    "record_array_equality should get matching types");
 
   DATA_INVARIANT(
     ns.follow(op0.type()).id()==ID_array,
@@ -62,7 +57,7 @@ literalt arrayst::record_array_equality(
 
   array_equalities.back().f1=op0;
   array_equalities.back().f2=op1;
-  array_equalities.back().l=SUB::equality(op0, op1);
+  array_equalities.back().l = baset::equality(op0, op1);
 
   arrays.make_union(op0, op1);
   collect_arrays(op0);
diff --git a/src/solvers/flattening/arrays.h b/src/solvers/flattening/arrays.h
index a5434c3e48f..760bc86e549 100644
--- a/src/solvers/flattening/arrays.h
+++ b/src/solvers/flattening/arrays.h
@@ -27,17 +27,18 @@ class update_exprt;
 
 class arrayst:public equalityt
 {
+private:
+  typedef equalityt baset;
+
 public:
   arrayst(const namespacet &_ns, propt &_prop);
 
   void post_process() override
   {
     post_process_arrays();
-    SUB::post_process();
+    baset::post_process();
   }
 
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef equalityt SUB;
 
   literalt record_array_equality(const equal_exprt &expr);
   void record_array_index(const index_exprt &expr);
diff --git a/src/solvers/flattening/boolbv.cpp b/src/solvers/flattening/boolbv.cpp
index 219e372afcf..6a628259c25 100644
--- a/src/solvers/flattening/boolbv.cpp
+++ b/src/solvers/flattening/boolbv.cpp
@@ -29,15 +29,13 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <solvers/floatbv/float_utils.h>
 #include <solvers/lowering/expr_lowering.h>
 
-bool boolbvt::literal(
-  const exprt &expr,
-  const std::size_t bit,
-  literalt &dest) const
+optionalt<literalt>
+boolbvt::literal(const exprt &expr, const std::size_t bit) const
 {
   if(expr.type().id()==ID_bool)
   {
     assert(bit==0);
-    return prop_conv_solvert::literal(expr, dest);
+    return prop_conv_solvert::literal(expr);
   }
   else
   {
@@ -50,16 +48,15 @@ bool boolbvt::literal(
         map.mapping.find(identifier);
 
       if(it_m==map.mapping.end())
-        return true;
+        return {};
 
       const boolbv_mapt::map_entryt &map_entry=it_m->second;
 
       assert(bit<map_entry.literal_map.size());
       if(!map_entry.literal_map[bit].is_set)
-        return true;
+        return {};
 
-      dest=map_entry.literal_map[bit].l;
-      return false;
+      return map_entry.literal_map[bit].l;
     }
     else if(expr.id()==ID_index)
     {
@@ -76,7 +73,7 @@ bool boolbvt::literal(
 
       std::size_t offset=integer2unsigned(index*element_width);
 
-      return literal(index_expr.array(), bit+offset, dest);
+      return literal(index_expr.array(), bit + offset);
     }
     else if(expr.id()==ID_member)
     {
@@ -96,7 +93,7 @@ bool boolbvt::literal(
         const typet &subtype=it->type();
 
         if(it->get_name()==component_name)
-          return literal(expr.op0(), bit+offset, dest);
+          return literal(expr.op0(), bit + offset);
 
         std::size_t element_width=boolbv_width(subtype);
 
@@ -564,7 +561,7 @@ literalt boolbvt::convert_rest(const exprt &expr)
       return const_literal(true);
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }
 
 bool boolbvt::boolbv_set_equality_to_true(const equal_exprt &expr)
@@ -605,7 +602,7 @@ void boolbvt::set_to(const exprt &expr, bool value)
   const auto equal_expr = expr_try_dynamic_cast<equal_exprt>(expr);
   if(value && equal_expr && !boolbv_set_equality_to_true(*equal_expr))
     return;
-  SUB::set_to(expr, value);
+  baset::set_to(expr, value);
 }
 
 exprt boolbvt::make_bv_expr(const typet &type, const bvt &bv)
@@ -640,17 +637,9 @@ bool boolbvt::is_unbounded_array(const typet &type) const
   if(unbounded_array==unbounded_arrayt::U_ALL)
     return true;
 
-  const exprt &size=to_array_type(type).size();
-
-  mp_integer s;
-  if(to_integer(size, s))
-    return true;
-
-  if(unbounded_array==unbounded_arrayt::U_AUTO)
-    if(s>MAX_FLATTENED_ARRAY_SIZE)
-      return true;
-
-  return false;
+  const auto s = numeric_cast<mp_integer>(to_array_type(type).size());
+  return !s.has_value() || (unbounded_array == unbounded_arrayt::U_AUTO &&
+                            *s > MAX_FLATTENED_ARRAY_SIZE);
 }
 
 void boolbvt::print_assignment(std::ostream &out) const
diff --git a/src/solvers/flattening/boolbv.h b/src/solvers/flattening/boolbv.h
index 429a5aa4b37..193ba9ebf0e 100644
--- a/src/solvers/flattening/boolbv.h
+++ b/src/solvers/flattening/boolbv.h
@@ -53,7 +53,7 @@ class boolbvt:public arrayst
 
   void clear_cache() override
   {
-    SUB::clear_cache();
+    baset::clear_cache();
     bv_cache.clear();
   }
 
@@ -61,14 +61,11 @@ class boolbvt:public arrayst
   {
     post_process_quantifiers();
     functions.post_process();
-    SUB::post_process();
+    baset::post_process();
   }
 
   // get literals for variables/expressions, if available
-  virtual bool literal(
-    const exprt &expr,
-    std::size_t bit,
-    literalt &literal) const;
+  virtual optionalt<literalt> literal(const exprt &expr, std::size_t bit) const;
 
   using arrayst::literal;
 
@@ -103,7 +100,7 @@ class boolbvt:public arrayst
   virtual bool boolbv_set_equality_to_true(const equal_exprt &expr);
 
   // NOLINTNEXTLINE(readability/identifiers)
-  typedef arrayst SUB;
+  typedef arrayst baset;
 
   void conversion_failed(const exprt &expr, bvt &bv)
   {
diff --git a/src/solvers/flattening/boolbv_add_sub.cpp b/src/solvers/flattening/boolbv_add_sub.cpp
index 3656b33384a..484c927260b 100644
--- a/src/solvers/flattening/boolbv_add_sub.cpp
+++ b/src/solvers/flattening/boolbv_add_sub.cpp
@@ -26,39 +26,30 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
      type.id()!=ID_vector)
     return conversion_failed(expr);
 
-  std::size_t width=boolbv_width(type);
-
+  const std::size_t width = boolbv_width(type);
   if(width==0)
     return conversion_failed(expr);
 
   const exprt::operandst &operands=expr.operands();
 
-  if(operands.empty())
-    throw "operator "+expr.id_string()+" takes at least one operand";
-
+  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";
-
-  bool subtract=(expr.id()==ID_minus ||
-                 expr.id()=="no-overflow-minus");
-
-  bool no_overflow=(expr.id()=="no-overflow-plus" ||
-                    expr.id()=="no-overflow-minus");
+  const typet arithmetic_type =
+    (type.id() == ID_vector || type.id() == ID_complex)
+      ? ns.follow(type.subtype())
+      : type;
 
-  typet arithmetic_type=
-    (type.id()==ID_vector || type.id()==ID_complex)?
-      ns.follow(type.subtype()):type;
-
-  bv_utilst::representationt rep=
-    (arithmetic_type.id()==ID_signedbv ||
-     arithmetic_type.id()==ID_fixedbv)?bv_utilst::representationt::SIGNED:
-                                       bv_utilst::representationt::UNSIGNED;
+  const bv_utilst::representationt rep =
+    (arithmetic_type.id() == ID_signedbv || arithmetic_type.id() == ID_fixedbv)
+      ? bv_utilst::representationt::SIGNED
+      : bv_utilst::representationt::UNSIGNED;
 
   for(exprt::operandst::const_iterator
       it=operands.begin()+1;
@@ -75,13 +66,12 @@ bvt boolbvt::convert_add_sub(const exprt &expr)
     if(type.id()==ID_vector || type.id()==ID_complex)
     {
       const typet &subtype=ns.follow(type.subtype());
+      const std::size_t sub_width = boolbv_width(subtype);
+      INVARIANT(
+        sub_width != 0 && width % sub_width == 0,
+        "convert_add_sub: unexpected vector operand width");
 
-      std::size_t sub_width=boolbv_width(subtype);
-
-      if(sub_width==0 || width%sub_width!=0)
-        throw "convert_add_sub: unexpected vector operand width";
-
-      std::size_t size=width/sub_width;
+      const std::size_t size = width / sub_width;
       bv.resize(width);
 
       for(std::size_t i=0; i<size; i++)
diff --git a/src/solvers/flattening/boolbv_array.cpp b/src/solvers/flattening/boolbv_array.cpp
index b96639a6d40..25083271da2 100644
--- a/src/solvers/flattening/boolbv_array.cpp
+++ b/src/solvers/flattening/boolbv_array.cpp
@@ -6,39 +6,30 @@ Author: Daniel Kroening, kroening@kroening.com
 
 \*******************************************************************/
 
-
 #include "boolbv.h"
 
 bvt boolbvt::convert_array(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.type().id()==ID_array)
   {
-    assert(expr.has_operands());
+    INVARIANT(expr.has_operands(), "array should have operands");
     const exprt::operandst &operands=expr.operands();
-    assert(!operands.empty());
-    std::size_t op_width=width/operands.size();
-
+    const std::size_t op_width = width / operands.size();
     bvt bv;
     bv.reserve(width);
 
-    forall_expr(it, operands)
+    for(const exprt &op : operands)
     {
-      const bvt &tmp=convert_bv(*it);
-
-      if(tmp.size()!=op_width)
-        throw "convert_array: unexpected operand width";
-
-      forall_literals(it2, tmp)
-        bv.push_back(*it2);
+      const bvt &tmp = convert_bv(op);
+      CHECK_RETURN(tmp.size() == op_width);
+      bv.insert(bv.end(), tmp.begin(), tmp.end());
     }
 
     return bv;
   }
-
   return conversion_failed(expr);
 }
diff --git a/src/solvers/flattening/boolbv_array_of.cpp b/src/solvers/flattening/boolbv_array_of.cpp
index 2c01f095638..ea9455c3b99 100644
--- a/src/solvers/flattening/boolbv_array_of.cpp
+++ b/src/solvers/flattening/boolbv_array_of.cpp
@@ -13,16 +13,11 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_array_of(const array_of_exprt &expr)
 {
-  if(expr.type().id()!=ID_array)
-    throw "array_of must be array-typed";
-
   const array_typet &array_type=to_array_type(expr.type());
-
   if(is_unbounded_array(array_type))
     return conversion_failed(expr);
 
-  std::size_t width=boolbv_width(array_type);
-
+  const std::size_t width = boolbv_width(array_type);
   if(width==0)
   {
     // A zero-length array is acceptable;
@@ -34,29 +29,25 @@ bvt boolbvt::convert_array_of(const array_of_exprt &expr)
   }
 
   const exprt &array_size=array_type.size();
+  const auto size = numeric_cast<mp_integer>(array_size);
 
-  mp_integer size;
-
-  if(to_integer(array_size, size))
+  if(!size)
     return conversion_failed(expr);
 
   const bvt &tmp=convert_bv(expr.op0());
 
   bvt bv;
   bv.resize(width);
-
-  if(size*tmp.size()!=width)
-    throw "convert_array_of: unexpected operand width";
+  CHECK_RETURN(*size * tmp.size() == width);
 
   std::size_t offset=0;
-
   for(mp_integer i=0; i<size; i=i+1)
   {
     for(std::size_t j=0; j<tmp.size(); j++, offset++)
       bv[offset]=tmp[j];
   }
 
-  assert(offset==bv.size());
+  INVARIANT(offset == bv.size(), "final offset should correspond to size");
 
   return bv;
 }
diff --git a/src/solvers/flattening/boolbv_bv_rel.cpp b/src/solvers/flattening/boolbv_bv_rel.cpp
index 86140972cd2..31cd26de75d 100644
--- a/src/solvers/flattening/boolbv_bv_rel.cpp
+++ b/src/solvers/flattening/boolbv_bv_rel.cpp
@@ -46,7 +46,7 @@ literalt boolbvt::convert_bv_rel(const exprt &expr)
         else if(rel==ID_gt)
           return float_utils.relation(bv0, float_utilst::relt::GT, bv1);
         else
-          return SUB::convert_rest(expr);
+          return baset::convert_rest(expr);
       }
       else if((op0.type().id()==ID_range &&
                op1.type()==op0.type()) ||
@@ -109,5 +109,5 @@ literalt boolbvt::convert_bv_rel(const exprt &expr)
     }
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }
diff --git a/src/solvers/flattening/boolbv_extractbit.cpp b/src/solvers/flattening/boolbv_extractbit.cpp
index a2da9cc3352..ec6e3084ffc 100644
--- a/src/solvers/flattening/boolbv_extractbit.cpp
+++ b/src/solvers/flattening/boolbv_extractbit.cpp
@@ -50,7 +50,7 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     std::size_t width_op1=boolbv_width(operands[1].type());
 
     if(width_op0==0 || width_op1==0)
-      return SUB::convert_rest(expr);
+      return baset::convert_rest(expr);
 
     std::size_t index_width = std::max(address_bits(width_op0), width_op1);
     unsignedbv_typet index_type(index_width);
@@ -90,5 +90,5 @@ literalt boolbvt::convert_extractbit(const extractbit_exprt &expr)
     }
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }
diff --git a/src/solvers/flattening/boolbv_get.cpp b/src/solvers/flattening/boolbv_get.cpp
index 71d94d02f8a..62be8cf1942 100644
--- a/src/solvers/flattening/boolbv_get.cpp
+++ b/src/solvers/flattening/boolbv_get.cpp
@@ -62,7 +62,7 @@ exprt boolbvt::get(const exprt &expr) const
     }
   }
 
-  return SUB::get(expr);
+  return baset::get(expr);
 }
 
 exprt boolbvt::bv_get_rec(
diff --git a/src/solvers/flattening/boolbv_ieee_float_rel.cpp b/src/solvers/flattening/boolbv_ieee_float_rel.cpp
index 87c86572e0d..60518d21a54 100644
--- a/src/solvers/flattening/boolbv_ieee_float_rel.cpp
+++ b/src/solvers/flattening/boolbv_ieee_float_rel.cpp
@@ -40,9 +40,9 @@ literalt boolbvt::convert_ieee_float_rel(const exprt &expr)
       else if(rel==ID_ieee_float_notequal)
         return !float_utils.relation(bv0, float_utilst::relt::EQ, bv1);
       else
-        return SUB::convert_rest(expr);
+        return baset::convert_rest(expr);
     }
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index ca66fb2c697..0263837f464 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -8,6 +8,7 @@ Author: Daniel Kroening, kroening@kroening.com
 
 #include "boolbv.h"
 
+#include <algorithm>
 #include <cassert>
 
 #include <util/arith_tools.h>
@@ -15,33 +16,45 @@ Author: Daniel Kroening, kroening@kroening.com
 #include <util/simplify_expr.h>
 #include <util/std_expr.h>
 
+/// \param array: an array expression
+/// \return true if all elements are equal
+static bool is_uniform(const exprt &array)
+{
+  if(array.id() == ID_array_of)
+    return true;
+  if(array.id() == ID_constant || array.id() == ID_array)
+  {
+    return std::all_of(
+      array.operands().begin(),
+      array.operands().end(),
+      [&](const exprt &expr) { // NOLINT
+        return expr == array.op0();
+      });
+  }
+  return false;
+}
+
 bvt boolbvt::convert_index(const index_exprt &expr)
 {
   const exprt &array=expr.array();
   const exprt &index=expr.index();
-
   const typet &array_op_type=ns.follow(array.type());
-
   bvt bv;
 
   if(array_op_type.id()==ID_array)
   {
-    const array_typet &array_type=
-      to_array_type(array_op_type);
-
-    std::size_t width=boolbv_width(expr.type());
+    const array_typet &array_type = to_array_type(array_op_type);
+    const std::size_t width = boolbv_width(expr.type());
 
     if(width==0)
       return conversion_failed(expr);
 
     // see if the array size is constant
-
     if(is_unbounded_array(array_type))
     {
       // use array decision procedure
 
       // free variables
-
       bv.resize(width);
       for(std::size_t i=0; i<width; i++)
         bv[i]=prop.new_variable();
@@ -49,28 +62,23 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       record_array_index(expr);
 
       // record type if array is a symbol
-
       if(array.id()==ID_symbol)
         map.get_map_entry(
           to_symbol_expr(array).get_identifier(), array_type);
 
       // make sure we have the index in the cache
       convert_bv(index);
-
       return bv;
     }
 
     // Must have a finite size
-    mp_integer array_size;
-    if(to_integer(array_type.size(), array_size))
-      throw "failed to convert array size";
+    const auto array_size = numeric_cast_v<mp_integer>(array_type.size());
 
     // see if the index address is constant
     // many of these are compacted by simplify_expr
     // but variable location writes will block this
-    mp_integer index_value;
-    if(!to_integer(index, index_value))
-      return convert_index(array, index_value);
+    if(const auto index_value = numeric_cast<mp_integer>(index))
+      return convert_index(array, *index_value);
 
     // Special case : arrays of one thing (useful for constants)
     // TODO : merge with ACTUAL_ARRAY_HACK so that ranges of the same
@@ -78,52 +86,25 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     // this rather than as a series of individual options.
     #define UNIFORM_ARRAY_HACK
     #ifdef UNIFORM_ARRAY_HACK
-    bool is_uniform = false;
-
-    if(array.id()==ID_array_of)
-    {
-      is_uniform = true;
-    }
-    else if(array.id()==ID_constant || array.id()==ID_array)
-    {
-      bool found_exception = false;
-      forall_expr(it, array.operands())
-      {
-        if(*it != array.op0())
-        {
-          found_exception = true;
-          break;
-        }
-      }
-
-      if(!found_exception)
-        is_uniform = true;
-    }
-
-    if(is_uniform && prop.has_set_to())
+    if(is_uniform(array) && prop.has_set_to())
     {
       static int uniform_array_counter;  // Temporary hack
 
-      std::string identifier=
-        "__CPROVER_internal_uniform_array_"+
-        std::to_string(uniform_array_counter++);
+      const std::string identifier = "__CPROVER_internal_uniform_array_" +
+                                     std::to_string(uniform_array_counter++);
 
-      symbol_exprt result(identifier, expr.type());
+      const symbol_exprt result(identifier, expr.type());
       bv = convert_bv(result);
 
-      equal_exprt value_equality(result, array.op0());
+      const equal_exprt value_equality(result, array.op0());
 
-      binary_relation_exprt lower_bound(
+      const binary_relation_exprt lower_bound(
         from_integer(0, index.type()), ID_le, index);
-      binary_relation_exprt upper_bound(
+      const binary_relation_exprt upper_bound(
         index, ID_lt, from_integer(array_size, index.type()));
 
-      if(lower_bound.lhs().is_nil() ||
-         upper_bound.rhs().is_nil())
-        throw "number conversion failed (2)";
-
-      and_exprt range_condition(lower_bound, upper_bound);
-      implies_exprt implication(range_condition, value_equality);
+      const and_exprt range_condition(lower_bound, upper_bound);
+      const implies_exprt implication(range_condition, value_equality);
 
       // Simplify may remove the lower bound if the type
       // is correct.
@@ -147,42 +128,27 @@ bvt boolbvt::convert_index(const index_exprt &expr)
       // Symbol for output
       static int actual_array_counter;  // Temporary hack
 
-      std::string identifier=
-        "__CPROVER_internal_actual_array_"+
-        std::to_string(actual_array_counter++);
+      const std::string identifier = "__CPROVER_internal_actual_array_" +
+                                     std::to_string(actual_array_counter++);
 
-      symbol_exprt result(identifier, expr.type());
+      const symbol_exprt result(identifier, expr.type());
       bv = convert_bv(result);
 
-      // add implications
-
-      equal_exprt index_equality;
-      index_equality.lhs()=index; // index operand
-
-      equal_exprt value_equality;
-      value_equality.lhs()=result;
+      INVARIANT(
+        array_size <= array.operands().size(),
+        "size should not exceed number of operands");
 
 #ifdef COMPACT_EQUAL_CONST
       bv_utils.equal_const_register(convert_bv(index));  // Definitely
       bv_utils.equal_const_register(convert_bv(result)); // Maybe
 #endif
 
-      exprt::operandst::const_iterator it = array.operands().begin();
-
-      for(mp_integer i=0; i<array_size; i=i+1)
+      for(std::size_t i = 0; i < array_size; ++i)
       {
-        index_equality.rhs()=from_integer(i, index_equality.lhs().type());
-
-        if(index_equality.rhs().is_nil())
-          throw "number conversion failed (1)";
-
-        assert(it != array.operands().end());
-
-        value_equality.rhs()=*it++;
-
-        // Cache comparisons and equalities
-        prop.l_set_to_true(convert(implies_exprt(index_equality,
-                                                 value_equality)));
+        const equal_exprt index_equality(index, from_integer(i, index.type()));
+        const equal_exprt value_equality(result, array.operands()[i]);
+        prop.l_set_to_true(
+          convert(implies_exprt(index_equality, value_equality)));
       }
 
       return bv;
@@ -190,18 +156,14 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
 #endif
 
-
     // TODO : As with constant index, there is a trade-off
     // of when it is best to flatten the whole array and
     // when it is best to use the array theory and then use
     // one or more of the above encoding strategies.
 
     // get literals for the whole array
-
     const bvt &array_bv=convert_bv(array);
-
-    if(array_size*width!=array_bv.size())
-      throw "unexpected array size";
+    CHECK_RETURN(array_size * width == array_bv.size());
 
     // TODO: maybe a shifter-like construction would be better
     // Would be a lot more compact but propagate worse
@@ -209,15 +171,10 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     if(prop.has_set_to())
     {
       // free variables
-
       bv.resize(width);
       for(std::size_t i=0; i<width; i++)
         bv[i]=prop.new_variable();
 
-      // add implications
-
-      equal_exprt index_equality;
-      index_equality.lhs()=index; // index operand
 
 #ifdef COMPACT_EQUAL_CONST
       bv_utils.equal_const_register(convert_bv(index));  // Definitely
@@ -228,16 +185,12 @@ bvt boolbvt::convert_index(const index_exprt &expr)
 
       for(mp_integer i=0; i<array_size; i=i+1)
       {
-        index_equality.rhs()=from_integer(i, index_equality.lhs().type());
-
-        if(index_equality.rhs().is_nil())
-          throw "number conversion failed (1)";
-
+        const equal_exprt index_equality(index, from_integer(i, index.type()));
         mp_integer offset=i*width;
 
         for(std::size_t j=0; j<width; j++)
-          equal_bv[j]=prop.lequal(bv[j],
-                             array_bv[integer2size_t(offset+j)]);
+          equal_bv[j] =
+            prop.lequal(bv[j], array_bv[integer2size_t(offset + j)]);
 
         prop.l_set_to_true(
           prop.limplies(convert(index_equality), prop.land(equal_bv)));
@@ -246,34 +199,23 @@ bvt boolbvt::convert_index(const index_exprt &expr)
     else
     {
       bv.resize(width);
-
-      equal_exprt equality;
-      equality.lhs()=index; // index operand
+      const typet index_type = index.type();
+      INVARIANT(array_size > 0, "array size should be positive");
 
 #ifdef COMPACT_EQUAL_CONST
       bv_utils.equal_const_register(convert_bv(index));  // Definitely
 #endif
 
-      typet constant_type=index.type(); // type of index operand
-
-      assert(array_size>0);
-
-      for(mp_integer i=0; i<array_size; i=i+1)
+      for(mp_integer i = 0; i < array_size; ++i)
       {
-        equality.op1()=from_integer(i, constant_type);
-
-        literalt e=convert(equality);
-
-        mp_integer offset=i*width;
-
-        for(std::size_t j=0; j<width; j++)
+        const equal_exprt equality(index, from_integer(i, index_type));
+        const literalt e = convert(equality);
+        const mp_integer offset = i * width;
+        for(std::size_t j = 0; j < width; ++j)
         {
           literalt l=array_bv[integer2size_t(offset+j)];
-
-          if(i==0) // this initializes bv
-            bv[j]=l;
-          else
-            bv[j]=prop.lselect(e, l, bv[j]);
+          // for 0 only initializes bv
+          bv[j] = i == 0 ? l : prop.lselect(e, l, bv[j]);
         }
       }
     }
@@ -289,14 +231,10 @@ bvt boolbvt::convert_index(
   const exprt &array,
   const mp_integer &index)
 {
-  const array_typet &array_type=
-    to_array_type(ns.follow(array.type()));
-
-  std::size_t width=boolbv_width(array_type.subtype());
-
+  const array_typet &array_type = to_array_type(ns.follow(array.type()));
+  const std::size_t width = boolbv_width(array_type.subtype());
   if(width==0)
     return conversion_failed(array);
-
   bvt bv;
   bv.resize(width);
 
@@ -309,20 +247,15 @@ bvt boolbvt::convert_index(
   // the array (constant and variable indexes) and updated
   // versions of it.
 
-  const bvt &tmp=convert_bv(array); // recursive call
-
-  mp_integer offset=index*width;
-
-  if(offset>=0 &&
-     offset+width<=mp_integer(tmp.size()))
+  const bvt &tmp = convert_bv(array);
+  const mp_integer offset = index * width;
+  const bool in_bounds =
+    offset >= 0 && offset + width <= mp_integer(tmp.size());
+  if(in_bounds)
   {
-    // in bounds
-
     // The assertion below is disabled as we want to be able
     // to run CBMC without simplifier.
     // Expression simplification should remove these cases
-    // assert(array.id()!=ID_array_of &&
-    //       array.id()!=ID_array);
     // If not there are large improvements possible as above
 
     for(std::size_t i=0; i<width; i++)
@@ -339,19 +272,18 @@ bvt boolbvt::convert_index(
 
     const mp_integer subtype_bytes =
       pointer_offset_size(array_type.subtype(), ns);
-    exprt new_offset = simplify_expr(
+    const exprt new_offset = simplify_expr(
       plus_exprt(
         o.offset(), from_integer(index * subtype_bytes, o.offset().type())),
       ns);
 
-    byte_extract_exprt be(
+    const byte_extract_exprt be(
       byte_extract_id(), o.root_object(), new_offset, array_type.subtype());
 
     return convert_bv(be);
   }
   else
   {
-    // out of bounds
     for(std::size_t i=0; i<width; i++)
       bv[i]=prop.new_variable();
   }
diff --git a/src/solvers/flattening/boolbv_mult.cpp b/src/solvers/flattening/boolbv_mult.cpp
index 15803b7ead5..b4711ce7f0d 100644
--- a/src/solvers/flattening/boolbv_mult.cpp
+++ b/src/solvers/flattening/boolbv_mult.cpp
@@ -12,53 +12,40 @@ Author: Daniel Kroening, kroening@kroening.com
 
 bvt boolbvt::convert_mult(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);
-
   bvt bv;
   bv.resize(width);
 
   const exprt::operandst &operands=expr.operands();
-  if(operands.empty())
-    throw "mult without operands";
-
+  DATA_INVARIANT(!operands.empty(), "mult must have operands");
   const exprt &op0=expr.op0();
-
-  bool no_overflow=expr.id()=="no-overflow-mult";
+  const bool no_overflow = expr.id() == "no-overflow-mult";
 
   if(expr.type().id()==ID_fixedbv)
   {
-    if(op0.type()!=expr.type())
-      throw "multiplication with mixed types";
-
+    DATA_INVARIANT(op0.type() == expr.type(), "multiplication with mixed types");
     bv=convert_bv(op0);
 
-    if(bv.size()!=width)
-      throw "convert_mult: unexpected operand width";
-
-    std::size_t fraction_bits=
+    DATA_INVARIANT(bv.size() == width, "convert_mult: unexpected operand width");
+    const std::size_t fraction_bits =
       to_fixedbv_type(expr.type()).get_fraction_bits();
 
     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 should have uniform operand types");
 
       // 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";
-
+      INVARIANT(op.size() == width, "convert_mult: unexpected operand width");
       op=bv_utils.sign_extension(op, bv.size());
-
       bv=bv_utils.signed_multiplier(bv, op);
-
       // cut it down again
       bv.erase(bv.begin(), bv.begin()+fraction_bits);
     }
@@ -68,37 +55,25 @@ 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";
-
+    DATA_INVARIANT(
+      op0.type() == expr.type(), "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";
-
+    INVARIANT(bv.size() == width, "convert_mult: unexpected operand width");
     for(exprt::operandst::const_iterator it=operands.begin()+1;
         it!=operands.end(); it++)
     {
-      if(it->type()!=expr.type())
-        throw "multiplication with mixed types";
-
+      INVARIANT(it->type() == expr.type(), "multiplication with mixed types");
       const bvt &op=convert_bv(*it);
+      CHECK_RETURN(op.size() == width);
 
-      if(op.size()!=width)
-        throw "convert_mult: unexpected operand width";
-
-      if(no_overflow)
-        bv=bv_utils.multiplier_no_overflow(bv, op, rep);
-      else
-        bv=bv_utils.multiplier(bv, op, rep);
+      bv = no_overflow ? bv_utils.multiplier_no_overflow(bv, op, rep)
+                       : bv_utils.multiplier(bv, op, rep);
     }
-
     return bv;
   }
-
   return conversion_failed(expr);
 }
diff --git a/src/solvers/flattening/boolbv_overflow.cpp b/src/solvers/flattening/boolbv_overflow.cpp
index f7e4798f780..664adc400d7 100644
--- a/src/solvers/flattening/boolbv_overflow.cpp
+++ b/src/solvers/flattening/boolbv_overflow.cpp
@@ -26,7 +26,7 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     const bvt &bv1=convert_bv(operands[1]);
 
     if(bv0.size()!=bv1.size())
-      return SUB::convert_rest(expr);
+      return baset::convert_rest(expr);
 
     bv_utilst::representationt rep=
       expr.op0().type().id()==ID_signedbv?bv_utilst::representationt::SIGNED:
@@ -43,7 +43,7 @@ literalt boolbvt::convert_overflow(const exprt &expr)
 
     if(operands[0].type().id()!=ID_unsignedbv &&
        operands[0].type().id()!=ID_signedbv)
-      return SUB::convert_rest(expr);
+      return baset::convert_rest(expr);
 
     bvt bv0=convert_bv(operands[0]);
     bvt bv1=convert_bv(operands[1]);
@@ -205,5 +205,5 @@ literalt boolbvt::convert_overflow(const exprt &expr)
     }
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }
diff --git a/src/solvers/flattening/boolbv_quantifier.cpp b/src/solvers/flattening/boolbv_quantifier.cpp
index 23f8857f80d..0f85390abc3 100644
--- a/src/solvers/flattening/boolbv_quantifier.cpp
+++ b/src/solvers/flattening/boolbv_quantifier.cpp
@@ -205,7 +205,7 @@ literalt boolbvt::convert_quantifier(const exprt &src)
 {
   exprt expr(src);
   if(!instantiate_quantifier(expr, ns))
-    return SUB::convert_rest(src);
+    return baset::convert_rest(src);
 
   quantifiert quantifier;
   quantifier.expr=expr;
diff --git a/src/solvers/flattening/boolbv_typecast.cpp b/src/solvers/flattening/boolbv_typecast.cpp
index 724b59b6a78..45202b01a47 100644
--- a/src/solvers/flattening/boolbv_typecast.cpp
+++ b/src/solvers/flattening/boolbv_typecast.cpp
@@ -608,5 +608,5 @@ literalt boolbvt::convert_typecast(const typecast_exprt &expr)
   if(!bv.empty())
     return prop.lor(bv);
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index e899f386767..26cf6aadf56 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -83,7 +83,7 @@ literalt bv_pointerst::convert_rest(const exprt &expr)
     }
   }
 
-  return SUB::convert_rest(expr);
+  return baset::convert_rest(expr);
 }
 
 bv_pointerst::bv_pointerst(
@@ -283,15 +283,15 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   }
   else if(expr.id()==ID_if)
   {
-    return SUB::convert_if(to_if_expr(expr));
+    return baset::convert_if(to_if_expr(expr));
   }
   else if(expr.id()==ID_index)
   {
-    return SUB::convert_index(to_index_expr(expr));
+    return baset::convert_index(to_index_expr(expr));
   }
   else if(expr.id()==ID_member)
   {
-    return SUB::convert_member(to_member_expr(expr));
+    return baset::convert_member(to_member_expr(expr));
   }
   else if(expr.id()==ID_address_of)
   {
@@ -452,7 +452,7 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   else if(expr.id()==ID_lshr ||
           expr.id()==ID_shl)
   {
-    return SUB::convert_shift(to_shift_expr(expr));
+    return baset::convert_shift(to_shift_expr(expr));
   }
   else if(expr.id()==ID_bitand ||
           expr.id()==ID_bitor ||
@@ -462,12 +462,12 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
   }
   else if(expr.id()==ID_concatenation)
   {
-    return SUB::convert_concatenation(expr);
+    return baset::convert_concatenation(expr);
   }
   else if(expr.id()==ID_byte_extract_little_endian ||
           expr.id()==ID_byte_extract_big_endian)
   {
-    return SUB::convert_byte_extract(to_byte_extract_expr(expr));
+    return baset::convert_byte_extract(to_byte_extract_expr(expr));
   }
   else if(
     expr.id() == ID_byte_update_little_endian ||
@@ -601,7 +601,7 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     return bv_utils.zero_extension(op0, width);
   }
 
-  return SUB::convert_bitvector(expr);
+  return baset::convert_bitvector(expr);
 }
 
 exprt bv_pointerst::bv_get_rec(
@@ -611,7 +611,7 @@ exprt bv_pointerst::bv_get_rec(
   const typet &type) const
 {
   if(type.id()!=ID_pointer)
-    return SUB::bv_get_rec(bv, unknown, offset, type);
+    return baset::bv_get_rec(bv, unknown, offset, type);
 
   std::string value_addr, value_offset, value;
 
@@ -838,7 +838,7 @@ void bv_pointerst::do_postponed(
 void bv_pointerst::post_process()
 {
   // post-processing arrays may yield further objects, do this first
-  SUB::post_process();
+  baset::post_process();
 
   for(postponed_listt::const_iterator
       it=postponed_list.begin();
diff --git a/src/solvers/flattening/bv_pointers.h b/src/solvers/flattening/bv_pointers.h
index cd0cc8166ef..e903f9d82fa 100644
--- a/src/solvers/flattening/bv_pointers.h
+++ b/src/solvers/flattening/bv_pointers.h
@@ -16,6 +16,9 @@ Author: Daniel Kroening, kroening@kroening.com
 
 class bv_pointerst:public boolbvt
 {
+private:
+  typedef boolbvt baset;
+
 public:
   bv_pointerst(const namespacet &_ns, propt &_prop);
 
@@ -24,9 +27,6 @@ class bv_pointerst:public boolbvt
 protected:
   pointer_logict pointer_logic;
 
-  // NOLINTNEXTLINE(readability/identifiers)
-  typedef boolbvt SUB;
-
   unsigned object_bits, offset_bits, bits;
 
   void encode(std::size_t object, bvt &bv);
diff --git a/src/solvers/prop/prop_conv.cpp b/src/solvers/prop/prop_conv.cpp
index 0e929871f53..93cb937ce2b 100644
--- a/src/solvers/prop/prop_conv.cpp
+++ b/src/solvers/prop/prop_conv.cpp
@@ -33,24 +33,15 @@ void prop_convt::set_frozen(const bvt &bv)
       set_frozen(bit);
 }
 
-bool prop_conv_solvert::literal(const exprt &expr, literalt &dest) const
+optionalt<literalt> prop_conv_solvert::literal(const exprt &expr) const
 {
-  assert(expr.type().id()==ID_bool);
-
-  if(expr.id()==ID_symbol)
-  {
-    const irep_idt &identifier=
-      to_symbol_expr(expr).get_identifier();
-
-    symbolst::const_iterator result=symbols.find(identifier);
-
-    if(result==symbols.end())
-      return true;
-    dest=result->second;
-    return false;
-  }
-
-  throw "found no literal for expression";
+  PRECONDITION(expr.type().id() == ID_bool);
+  PRECONDITION(expr.id() == ID_symbol);
+  const irep_idt &identifier = to_symbol_expr(expr).get_identifier();
+  auto result = symbols.find(identifier);
+  if(result == symbols.end())
+    return {};
+  return result->second;
 }
 
 literalt prop_conv_solvert::get_literal(const irep_idt &identifier)
@@ -71,43 +62,27 @@ literalt prop_conv_solvert::get_literal(const irep_idt &identifier)
 }
 
 /// get a boolean value from counter example if not valid
-bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const
+optionalt<tvt> prop_conv_solvert::get_bool(const exprt &expr) const
 {
-  // trivial cases
-
   if(expr.is_true())
+    return tvt(true);
+  if(expr.is_false())
+    return tvt(false);
+  if(expr.id() == ID_symbol)
   {
-    value=tvt(true);
-    return false;
-  }
-  else if(expr.is_false())
-  {
-    value=tvt(false);
-    return false;
-  }
-  else if(expr.id()==ID_symbol)
-  {
-    symbolst::const_iterator result=
-      symbols.find(to_symbol_expr(expr).get_identifier());
-
+    const auto result = symbols.find(to_symbol_expr(expr).get_identifier());
     if(result==symbols.end())
-      return true;
-
-    value=prop.l_get(result->second);
-    return false;
+      return {};
+    return prop.l_get(result->second);
   }
-
-  // sub-expressions
-
   if(expr.id()==ID_not)
   {
     if(expr.type().id()==ID_bool &&
        expr.operands().size()==1)
     {
-      if(get_bool(expr.op0(), value))
-        return true;
-      value=!value;
-      return false;
+      if(auto result = get_bool(expr.op0()))
+        return !*result;
+      return {};
     }
   }
   else if(expr.id()==ID_and || expr.id()==ID_or)
@@ -115,48 +90,35 @@ bool prop_conv_solvert::get_bool(const exprt &expr, tvt &value) const
     if(expr.type().id()==ID_bool &&
        expr.operands().size()>=1)
     {
-      value=tvt(expr.id()==ID_and);
+      auto value = tvt(expr.id() == ID_and);
 
       forall_operands(it, expr)
       {
-        tvt tmp;
-        if(get_bool(*it, tmp))
-          return true;
-
+        auto tmp = get_bool(*it);
+        if(!tmp)
+          return {};
         if(expr.id()==ID_and)
         {
-          if(tmp.is_false())
-          {
-            value=tvt(false);
-            return false;
-          }
-
-          value=value && tmp;
+          if(tmp->is_false())
+            return tvt(false);
+          value = value && *tmp;
         }
         else // or
         {
-          if(tmp.is_true())
-          {
-            value=tvt(true);
-            return false;
-          }
-
-          value=value || tmp;
+          if(tmp->is_true())
+            return tvt(true);
+          value = value || *tmp;
         }
       }
-
-      return false;
+      return value;
     }
   }
 
   // check cache
-
-  cachet::const_iterator cache_result=cache.find(expr);
+  const auto cache_result = cache.find(expr);
   if(cache_result==cache.end())
-    return true;
-
-  value=prop.l_get(cache_result->second);
-  return false;
+    return {};
+  return prop.l_get(cache_result->second);
 }
 
 literalt prop_conv_solvert::convert(const exprt &expr)
@@ -337,29 +299,13 @@ literalt prop_conv_solvert::convert_rest(const exprt &expr)
 
 bool prop_conv_solvert::set_equality_to_true(const equal_exprt &expr)
 {
-  if(!equality_propagation)
+  if(!equality_propagation || expr.lhs().id() != ID_symbol)
     return true;
 
-  // optimization for constraint of the form
-  // new_variable = value
-
-  if(expr.lhs().id()==ID_symbol)
-  {
-    const irep_idt &identifier=
-      to_symbol_expr(expr.lhs()).get_identifier();
-
-    literalt tmp=convert(expr.rhs());
-
-    std::pair<symbolst::iterator, bool> result=
-      symbols.insert(std::pair<irep_idt, literalt>(identifier, tmp));
-
-    if(result.second)
-      return false; // ok, inserted!
-
-    // nah, already there
-  }
-
-  return true;
+  const irep_idt &identifier = to_symbol_expr(expr.lhs()).get_identifier();
+  const literalt tmp = convert(expr.rhs());
+  const bool inserted = symbols.emplace(identifier, tmp).second;
+  return !inserted;
 }
 
 void prop_conv_solvert::set_to(const exprt &expr, bool value)
@@ -484,16 +430,19 @@ decision_proceduret::resultt prop_conv_solvert::dec_solve()
 
 exprt prop_conv_solvert::get(const exprt &expr) const
 {
-  tvt value;
-
-  if(expr.type().id()==ID_bool &&
-     !get_bool(expr, value))
+  if(expr.type().id() == ID_bool)
   {
-    switch(value.get_value())
+    if(const auto value = get_bool(expr))
     {
-     case tvt::tv_enumt::TV_TRUE:  return true_exprt();
-     case tvt::tv_enumt::TV_FALSE: return false_exprt();
-     case tvt::tv_enumt::TV_UNKNOWN: return false_exprt(); // default
+      switch(value->get_value())
+      {
+      case tvt::tv_enumt::TV_TRUE:
+        return true_exprt();
+      case tvt::tv_enumt::TV_FALSE:
+        return false_exprt();
+      case tvt::tv_enumt::TV_UNKNOWN:
+        return false_exprt(); // default
+      }
     }
   }
 
diff --git a/src/solvers/prop/prop_conv.h b/src/solvers/prop/prop_conv.h
index 261771040a6..224d845dac0 100644
--- a/src/solvers/prop/prop_conv.h
+++ b/src/solvers/prop/prop_conv.h
@@ -106,7 +106,7 @@ class prop_conv_solvert:public prop_convt
   { return prop.has_is_in_conflict(); }
 
   // get literal for expression, if available
-  virtual bool literal(const exprt &expr, literalt &literal) const;
+  virtual optionalt<literalt> literal(const exprt &expr) const;
 
   bool use_cache = true;
   bool equality_propagation = true;
@@ -131,7 +131,7 @@ class prop_conv_solvert:public prop_convt
   bool post_processing_done = false;
 
   // get a _boolean_ value from counterexample if not valid
-  virtual bool get_bool(const exprt &expr, tvt &value) const;
+  virtual optionalt<tvt> get_bool(const exprt &expr) const;
 
   virtual literalt convert_rest(const exprt &expr);
   virtual literalt convert_bool(const exprt &expr);
diff --git a/src/solvers/refinement/bv_refinement.h b/src/solvers/refinement/bv_refinement.h
index 05b4c056d9b..6f16a5322f7 100644
--- a/src/solvers/refinement/bv_refinement.h
+++ b/src/solvers/refinement/bv_refinement.h
@@ -21,6 +21,7 @@ Author: Daniel Kroening, kroening@kroening.com
 class bv_refinementt:public bv_pointerst
 {
 private:
+  typedef bv_pointerst baset;
   struct configt
   {
     ui_message_handlert::uit ui=ui_message_handlert::uit::PLAIN;
diff --git a/src/solvers/refinement/refine_arithmetic.cpp b/src/solvers/refinement/refine_arithmetic.cpp
index 86641b8ffa4..e5106f0f021 100644
--- a/src/solvers/refinement/refine_arithmetic.cpp
+++ b/src/solvers/refinement/refine_arithmetic.cpp
@@ -39,11 +39,11 @@ void bv_refinementt::approximationt::add_under_assumption(literalt l)
 bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
 {
   if(!config_.refine_arithmetic)
-    return SUB::convert_floatbv_op(expr);
+    return baset::convert_floatbv_op(expr);
 
   if(ns.follow(expr.type()).id()!=ID_floatbv ||
      expr.operands().size()!=3)
-    return SUB::convert_floatbv_op(expr);
+    return baset::convert_floatbv_op(expr);
 
   bvt bv;
   add_approximation(expr, bv);
@@ -53,7 +53,7 @@ bvt bv_refinementt::convert_floatbv_op(const exprt &expr)
 bvt bv_refinementt::convert_mult(const exprt &expr)
 {
   if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
-    return SUB::convert_mult(expr);
+    return baset::convert_mult(expr);
 
   // we catch any multiplication
   // unless it involves a constant
@@ -70,7 +70,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
   // we keep multiplication by a constant for integers
   if(type.id()!=ID_floatbv)
     if(operands[0].is_constant() || operands[1].is_constant())
-      return SUB::convert_mult(expr);
+      return baset::convert_mult(expr);
 
   bvt bv;
   approximationt &a=add_approximation(expr, bv);
@@ -101,7 +101,7 @@ bvt bv_refinementt::convert_mult(const exprt &expr)
 bvt bv_refinementt::convert_div(const div_exprt &expr)
 {
   if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
-    return SUB::convert_div(expr);
+    return baset::convert_div(expr);
 
   // we catch any division
   // unless it's integer division by a constant
@@ -109,7 +109,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr)
   PRECONDITION(expr.operands().size()==2);
 
   if(expr.op1().is_constant())
-    return SUB::convert_div(expr);
+    return baset::convert_div(expr);
 
   bvt bv;
   add_approximation(expr, bv);
@@ -119,7 +119,7 @@ bvt bv_refinementt::convert_div(const div_exprt &expr)
 bvt bv_refinementt::convert_mod(const mod_exprt &expr)
 {
   if(!config_.refine_arithmetic || expr.type().id()==ID_fixedbv)
-    return SUB::convert_mod(expr);
+    return baset::convert_mod(expr);
 
   // we catch any mod
   // unless it's integer + constant
@@ -127,7 +127,7 @@ bvt bv_refinementt::convert_mod(const mod_exprt &expr)
   PRECONDITION(expr.operands().size()==2);
 
   if(expr.op1().is_constant())
-    return SUB::convert_mod(expr);
+    return baset::convert_mod(expr);
 
   bvt bv;
   add_approximation(expr, bv);