diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index 4e94f865ac8..8ea42d94cec 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -99,10 +99,14 @@ void rw_range_sett::get_objects_complex_imag(
 {
   const exprt &op = expr.op();
 
-  range_spect sub_size =
-    to_range_spect(pointer_offset_bits(op.type().subtype(), ns));
-  assert(sub_size>0);
-  range_spect offset = range_start == -1 ? 0 : sub_size;
+  auto subtype_bits = pointer_offset_bits(op.type().subtype(), ns);
+  CHECK_RETURN(subtype_bits.has_value());
+
+  range_spect sub_size = to_range_spect(*subtype_bits);
+  CHECK_RETURN(sub_size > 0);
+
+  range_spect offset=
+    (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
 
   get_objects_rec(mode, op, range_start + offset, size);
 }
@@ -173,8 +177,9 @@ void rw_range_sett::get_objects_shift(
 {
   const exprt simp_distance=simplify_expr(shift.distance(), ns);
 
-  range_spect src_size=
-    to_range_spect(pointer_offset_bits(shift.op().type(), ns));
+  auto op_bits = pointer_offset_bits(shift.op().type(), ns);
+
+  range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
 
   mp_integer dist;
   if(range_start==-1 ||
@@ -230,15 +235,18 @@ void rw_range_sett::get_objects_member(
 
   const struct_typet &struct_type=to_struct_type(type);
 
-  range_spect offset=
-    to_range_spect(
-      member_offset_bits(
-        struct_type,
-        expr.get_component_name(),
-        ns));
+  auto offset_bits =
+    member_offset_bits(struct_type, expr.get_component_name(), ns);
 
-  if(offset!=-1)
-    offset+=range_start;
+  range_spect offset;
+
+  if(offset_bits.has_value())
+  {
+    offset = to_range_spect(*offset_bits);
+    offset += range_start;
+  }
+  else
+    offset = -1;
 
   get_objects_rec(mode, expr.struct_op(), offset, size);
 }
@@ -259,15 +267,17 @@ void rw_range_sett::get_objects_index(
   {
     const vector_typet &vector_type=to_vector_type(type);
 
-    sub_size=
-      to_range_spect(pointer_offset_bits(vector_type.subtype(), ns));
+    auto subtype_bits = pointer_offset_bits(vector_type.subtype(), ns);
+
+    sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
   }
   else if(type.id()==ID_array)
   {
     const array_typet &array_type=to_array_type(type);
 
-    sub_size=
-      to_range_spect(pointer_offset_bits(array_type.subtype(), ns));
+    auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
+
+    sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
   }
   else
     return;
@@ -302,10 +312,13 @@ void rw_range_sett::get_objects_array(
   const array_typet &array_type=
     to_array_type(ns.follow(expr.type()));
 
-  range_spect sub_size=
-    to_range_spect(pointer_offset_bits(array_type.subtype(), ns));
+  auto subtype_bits = pointer_offset_bits(array_type.subtype(), ns);
+
+  range_spect sub_size;
 
-  if(sub_size==-1)
+  if(subtype_bits.has_value())
+    sub_size = to_range_spect(*subtype_bits);
+  else
   {
     forall_operands(it, expr)
       get_objects_rec(mode, *it, 0, -1);
@@ -342,8 +355,10 @@ void rw_range_sett::get_objects_struct(
   const struct_typet &struct_type=
     to_struct_type(ns.follow(expr.type()));
 
-  range_spect full_size=
-    to_range_spect(pointer_offset_bits(struct_type, ns));
+  auto struct_bits = pointer_offset_bits(struct_type, ns);
+
+  range_spect full_size =
+    struct_bits.has_value() ? to_range_spect(*struct_bits) : -1;
 
   range_spect offset=0;
   range_spect full_r_s=range_start==-1 ? 0 : range_start;
@@ -351,8 +366,9 @@ void rw_range_sett::get_objects_struct(
 
   forall_operands(it, expr)
   {
-    range_spect sub_size=
-      to_range_spect(pointer_offset_bits(it->type(), ns));
+    auto it_bits = pointer_offset_bits(it->type(), ns);
+
+    range_spect sub_size = it_bits.has_value() ? to_range_spect(*it_bits) : -1;
 
     if(offset==-1)
     {
@@ -401,8 +417,9 @@ void rw_range_sett::get_objects_typecast(
 {
   const exprt &op=tc.op();
 
-  range_spect new_size=
-    to_range_spect(pointer_offset_bits(op.type(), ns));
+  auto op_bits = pointer_offset_bits(op.type(), ns);
+
+  range_spect new_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
 
   if(range_start==-1)
     new_size=-1;
@@ -537,8 +554,11 @@ void rw_range_sett::get_objects_rec(
   {
     const symbol_exprt &symbol=to_symbol_expr(expr);
     const irep_idt identifier=symbol.get_identifier();
-    range_spect full_size=
-      to_range_spect(pointer_offset_bits(symbol.type(), ns));
+
+    auto symbol_bits = pointer_offset_bits(symbol.type(), ns);
+
+    range_spect full_size =
+      symbol_bits.has_value() ? to_range_spect(*symbol_bits) : -1;
 
     if(full_size==0 ||
        (full_size>0 && range_start>=full_size))
@@ -584,8 +604,10 @@ void rw_range_sett::get_objects_rec(
 
 void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr)
 {
-  range_spect size=
-    to_range_spect(pointer_offset_bits(expr.type(), ns));
+  auto expr_bits = pointer_offset_bits(expr.type(), ns);
+
+  range_spect size = expr_bits.has_value() ? to_range_spect(*expr_bits) : -1;
+
   get_objects_rec(mode, expr, 0, size);
 }
 
@@ -614,16 +636,24 @@ void rw_range_set_value_sett::get_objects_dereference(
   exprt object=deref;
   dereference(target, object, ns, value_sets);
 
-  range_spect new_size=
-    to_range_spect(pointer_offset_bits(object.type(), ns));
+  auto type_bits = pointer_offset_bits(object.type(), ns);
 
-  if(range_start==-1 || new_size<=range_start)
-    new_size=-1;
-  else
+  range_spect new_size;
+
+  if(type_bits.has_value())
   {
-    new_size-=range_start;
-    new_size=std::min(size, new_size);
+    new_size = to_range_spect(*type_bits);
+
+    if(range_start == -1 || new_size <= range_start)
+      new_size = -1;
+    else
+    {
+      new_size -= range_start;
+      new_size = std::min(size, new_size);
+    }
   }
+  else
+    new_size = -1;
 
   // value_set_dereferencet::build_reference_to will turn *p into
   // DYNAMIC_OBJECT(p) ? *p : invalid_objectN
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index fad39334e0b..2d2bc3b1dee 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -210,9 +210,11 @@ void rd_range_domaint::transform_function_call(
       if(identifier.empty())
         continue;
 
-      range_spect size=
-        to_range_spect(pointer_offset_bits(param.type(), ns));
-      gen(from, identifier, 0, size);
+      auto param_bits = pointer_offset_bits(param.type(), ns);
+      if(param_bits.has_value())
+        gen(from, identifier, 0, to_range_spect(*param_bits));
+      else
+        gen(from, identifier, 0, -1);
     }
   }
   else
diff --git a/src/ansi-c/expr2c.cpp b/src/ansi-c/expr2c.cpp
index 58f70ddc0e9..6ffbc25ce7b 100644
--- a/src/ansi-c/expr2c.cpp
+++ b/src/ansi-c/expr2c.cpp
@@ -3617,9 +3617,9 @@ std::string expr2ct::convert_with_precedence(
   else if(src.id()==ID_bswap)
     return convert_function(
       src,
-      "__builtin_bswap"+
-      integer2string(pointer_offset_bits(src.op0().type(), ns)),
-      precedence=16);
+      "__builtin_bswap" +
+        integer2string(*pointer_offset_bits(src.op0().type(), ns)),
+      precedence = 16);
 
   else if(src.id()==ID_isnormal)
     return convert_function(src, "isnormal", precedence=16);
diff --git a/src/ansi-c/padding.cpp b/src/ansi-c/padding.cpp
index d1d6e76f9fa..a3adef091c6 100644
--- a/src/ansi-c/padding.cpp
+++ b/src/ansi-c/padding.cpp
@@ -70,7 +70,7 @@ mp_integer alignment(const typet &type, const namespacet &ns)
           type.id()==ID_c_bool ||
           type.id()==ID_pointer)
   {
-    result=pointer_offset_size(type, ns);
+    result = *pointer_offset_size(type, ns);
   }
   else if(type.id()==ID_c_enum)
     result=alignment(type.subtype(), ns);
@@ -229,9 +229,9 @@ static void add_padding_msvc(struct_typet &type, const namespacet &ns)
       else
       {
         // keep track of offset
-        const mp_integer size = pointer_offset_size(it->type(), ns);
-        if(size >= 1)
-          offset += size;
+        const auto size = pointer_offset_size(it->type(), ns);
+        if(size.has_value() && *size >= 1)
+          offset += *size;
       }
     }
   }
@@ -375,10 +375,10 @@ static void add_padding_gcc(struct_typet &type, const namespacet &ns)
       }
     }
 
-    mp_integer size=pointer_offset_size(it_type, ns);
+    auto size = pointer_offset_size(it_type, ns);
 
-    if(size!=-1)
-      offset+=size;
+    if(size.has_value())
+      offset += *size;
   }
 
   // any explicit alignment for the struct?
@@ -435,9 +435,9 @@ void add_padding(union_typet &type, const namespacet &ns)
   // check per component, and ignore those without fixed size
   for(const auto &c : type.components())
   {
-    mp_integer s=pointer_offset_bits(c.type(), ns);
-    if(s>0)
-      size_bits=std::max(size_bits, s);
+    auto s = pointer_offset_bits(c.type(), ns);
+    if(s.has_value())
+      size_bits = std::max(size_bits, *s);
   }
 
   // Is the union packed?
diff --git a/src/ansi-c/type2name.cpp b/src/ansi-c/type2name.cpp
index 2bef9136b00..57b23492753 100644
--- a/src/ansi-c/type2name.cpp
+++ b/src/ansi-c/type2name.cpp
@@ -86,9 +86,9 @@ static std::string pointer_offset_bits_as_string(
   const typet &type,
   const namespacet &ns)
 {
-  mp_integer bits = pointer_offset_bits(type, ns);
-  CHECK_RETURN(bits != -1);
-  return integer2string(bits);
+  auto bits = pointer_offset_bits(type, ns);
+  CHECK_RETURN(bits.has_value());
+  return integer2string(*bits);
 }
 
 static bool parent_is_sym_check=false;
diff --git a/src/goto-instrument/alignment_checks.cpp b/src/goto-instrument/alignment_checks.cpp
index bb0ac407bc6..30076e833f9 100644
--- a/src/goto-instrument/alignment_checks.cpp
+++ b/src/goto-instrument/alignment_checks.cpp
@@ -51,12 +51,12 @@ void print_struct_alignment_problems(
         {
           const typet &it_type = it_next->type();
           const namespacet ns(symbol_table);
-          mp_integer size = pointer_offset_size(it_type, ns);
+          auto size = pointer_offset_size(it_type, ns);
 
-          if(size < 0)
+          if(!size.has_value())
             throw "type of unknown size:\n" + it_type.pretty();
 
-          cumulated_length += size;
+          cumulated_length += *size;
           // [it_mem;it_next] cannot be covered by an instruction
           if(cumulated_length > config.ansi_c.memory_operand_size)
           {
@@ -92,13 +92,13 @@ void print_struct_alignment_problems(
       #if 0
       const namespacet ns(symbol_table);
       const array_typet array=to_array_type(symbol_pair.second.type);
-      const mp_integer size=
+      const auto size=
         pointer_offset_size(array.subtype(), ns);
 
-      if(size<0)
+      if(!size.has_value())
         throw "type of unknown size:\n"+it_type.pretty();
 
-      if(2*integer2long(size)<=config.ansi_c.memory_operand_size)
+      if(2*integer2long(*size)<=config.ansi_c.memory_operand_size)
       {
         out << "\nWARNING: "
             << "declaration of an array at "
diff --git a/src/goto-instrument/count_eloc.cpp b/src/goto-instrument/count_eloc.cpp
index 56552f9ce19..f7626e0e15e 100644
--- a/src/goto-instrument/count_eloc.cpp
+++ b/src/goto-instrument/count_eloc.cpp
@@ -191,9 +191,9 @@ void print_global_state_size(const goto_modelt &goto_model)
       continue;
     }
 
-    const mp_integer bits = pointer_offset_bits(symbol.type, ns);
-    if(bits > 0)
-      total_size += bits;
+    const auto bits = pointer_offset_bits(symbol.type, ns);
+    if(bits.has_value() && bits.value() > 0)
+      total_size += bits.value();
   }
 
   std::cout << "Total size of global objects: " << total_size << " bits\n";
diff --git a/src/goto-programs/interpreter_evaluate.cpp b/src/goto-programs/interpreter_evaluate.cpp
index 71349a5734b..f1a60299323 100644
--- a/src/goto-programs/interpreter_evaluate.cpp
+++ b/src/goto-programs/interpreter_evaluate.cpp
@@ -161,18 +161,18 @@ bool interpretert::byte_offset_to_memory_offset(
 
     for(const auto &comp : st.components())
     {
-      const mp_integer comp_offset = member_offset(st, comp.get_name(), ns);
+      const auto comp_offset = member_offset(st, comp.get_name(), ns);
 
-      const mp_integer component_byte_size =
-        pointer_offset_size(comp.type(), ns);
-      if(component_byte_size<0)
+      const auto component_byte_size = pointer_offset_size(comp.type(), ns);
+
+      if(!comp_offset.has_value() && !component_byte_size.has_value())
         return true;
 
-      if(comp_offset + component_byte_size > offset)
+      if(*comp_offset + *component_byte_size > offset)
       {
         mp_integer subtype_result;
-        bool ret=byte_offset_to_memory_offset(
-          comp.type(), offset - comp_offset, subtype_result);
+        bool ret = byte_offset_to_memory_offset(
+          comp.type(), offset - *comp_offset, subtype_result);
         result=previous_member_offsets+subtype_result;
         return ret;
       }
@@ -190,25 +190,30 @@ bool interpretert::byte_offset_to_memory_offset(
   else if(source_type.id()==ID_array)
   {
     const auto &at=to_array_type(source_type);
+
     mp_vectort array_size_vec;
     evaluate(at.size(), array_size_vec);
+
     if(array_size_vec.size()!=1)
       return true;
+
     mp_integer array_size=array_size_vec[0];
-    mp_integer elem_size_bytes=pointer_offset_size(at.subtype(), ns);
-    if(elem_size_bytes<=0)
+    auto elem_size_bytes = pointer_offset_size(at.subtype(), ns);
+    if(!elem_size_bytes.has_value() || *elem_size_bytes == 0)
       return true;
+
     mp_integer elem_size_leaves;
     if(count_type_leaves(at.subtype(), elem_size_leaves))
       return true;
-    mp_integer this_idx=offset/elem_size_bytes;
+
+    mp_integer this_idx = offset / (*elem_size_bytes);
     if(this_idx>=array_size_vec[0])
       return true;
+
     mp_integer subtype_result;
-    bool ret=byte_offset_to_memory_offset(
-      at.subtype(),
-      offset%elem_size_bytes,
-      subtype_result);
+    bool ret = byte_offset_to_memory_offset(
+      at.subtype(), offset % (*elem_size_bytes), subtype_result);
+
     result=subtype_result+(elem_size_leaves*this_idx);
     return ret;
   }
@@ -246,7 +251,10 @@ bool interpretert::memory_offset_to_byte_offset(
         mp_integer subtype_result;
         bool ret=memory_offset_to_byte_offset(
           comp.type(), cell_offset, subtype_result);
-        result = member_offset(st, comp.get_name(), ns) + subtype_result;
+        const auto member_offset_result =
+          member_offset(st, comp.get_name(), ns);
+        CHECK_RETURN(member_offset_result.has_value());
+        result = member_offset_result.value() + subtype_result;
         return ret;
       }
       else
@@ -260,26 +268,31 @@ bool interpretert::memory_offset_to_byte_offset(
   else if(source_type.id()==ID_array)
   {
     const auto &at=to_array_type(source_type);
+
     mp_vectort array_size_vec;
     evaluate(at.size(), array_size_vec);
     if(array_size_vec.size()!=1)
       return true;
-    mp_integer elem_size=pointer_offset_size(at.subtype(), ns);
-    if(elem_size==-1)
+
+    auto elem_size = pointer_offset_size(at.subtype(), ns);
+    if(!elem_size.has_value())
       return true;
+
     mp_integer elem_count;
     if(count_type_leaves(at.subtype(), elem_count))
       return true;
+
     mp_integer this_idx=full_cell_offset/elem_count;
     if(this_idx>=array_size_vec[0])
       return true;
+
     mp_integer subtype_result;
     bool ret=
       memory_offset_to_byte_offset(
         at.subtype(),
         full_cell_offset%elem_count,
         subtype_result);
-    result=subtype_result+(elem_size*this_idx);
+    result = subtype_result + ((*elem_size) * this_idx);
     return ret;
   }
   else
diff --git a/src/goto-programs/vcd_goto_trace.cpp b/src/goto-programs/vcd_goto_trace.cpp
index 3f6d1ec778b..976b1e38733 100644
--- a/src/goto-programs/vcd_goto_trace.cpp
+++ b/src/goto-programs/vcd_goto_trace.cpp
@@ -61,12 +61,12 @@ std::string as_vcd_binary(
 
   // build "xxx"
 
-  const mp_integer width = pointer_offset_bits(type, ns);
+  const auto width = pointer_offset_bits(type, ns);
 
-  if(width>=0)
-    return std::string(integer2size_t(width), 'x');
-
-  return "";
+  if(width.has_value())
+    return std::string(integer2size_t(*width), 'x');
+  else
+    return "";
 }
 
 void output_vcd(
@@ -97,11 +97,12 @@ void output_vcd(
 
         const auto number=n.number(identifier);
 
-        const mp_integer width = pointer_offset_bits(type, ns);
+        const auto width = pointer_offset_bits(type, ns);
 
-        if(width>=1)
-          out << "$var reg " << width << " V" << number << " "
-              << identifier << " $end" << "\n";
+        if(width.has_value() && (*width) >= 1)
+          out << "$var reg " << (*width) << " V" << number << " " << identifier
+              << " $end"
+              << "\n";
       }
     }
   }
diff --git a/src/goto-symex/symex_assign.cpp b/src/goto-symex/symex_assign.cpp
index 3000679c73f..86543f5a9ce 100644
--- a/src/goto-symex/symex_assign.cpp
+++ b/src/goto-symex/symex_assign.cpp
@@ -272,7 +272,9 @@ void goto_symext::symex_assign_symbol(
     log.debug(),
     [this, &ssa_lhs](messaget::mstreamt &mstream) {
       mstream << "Assignment to " << ssa_lhs.get_identifier()
-              << " [" << pointer_offset_bits(ssa_lhs.type(), ns) << " bits]"
+              << " ["
+              << pointer_offset_bits(ssa_lhs.type(), ns).value_or(0)
+              << " bits]"
               << messaget::eom;
     });
 
diff --git a/src/goto-symex/symex_builtin_functions.cpp b/src/goto-symex/symex_builtin_functions.cpp
index f67d37febf2..b168c0f6d7d 100644
--- a/src/goto-symex/symex_builtin_functions.cpp
+++ b/src/goto-symex/symex_builtin_functions.cpp
@@ -77,10 +77,10 @@ void goto_symext::symex_allocate(
       if(tmp_type.is_not_nil())
       {
         // Did the size get multiplied?
-        mp_integer elem_size=pointer_offset_size(tmp_type, ns);
+        auto elem_size = pointer_offset_size(tmp_type, ns);
         mp_integer alloc_size;
 
-        if(elem_size<0)
+        if(!elem_size.has_value() || *elem_size==0)
         {
         }
         else if(to_integer(tmp_size, alloc_size) &&
@@ -102,13 +102,13 @@ void goto_symext::symex_allocate(
         }
         else
         {
-          if(alloc_size==elem_size)
+          if(alloc_size == *elem_size)
             object_type=tmp_type;
           else
           {
-            mp_integer elements=alloc_size/elem_size;
+            mp_integer elements = alloc_size / (*elem_size);
 
-            if(elements*elem_size==alloc_size)
+            if(elements * (*elem_size) == alloc_size)
               object_type=array_typet(
                 tmp_type, from_integer(elements, tmp_size.type()));
           }
diff --git a/src/goto-symex/symex_dereference.cpp b/src/goto-symex/symex_dereference.cpp
index 94e32e8a75d..b7cc65310e9 100644
--- a/src/goto-symex/symex_dereference.cpp
+++ b/src/goto-symex/symex_dereference.cpp
@@ -196,8 +196,9 @@ exprt goto_symext::address_arithmetic(
     if(expr.id()==ID_symbol &&
        expr.get_bool(ID_C_SSA_symbol))
     {
-      offset=compute_pointer_offset(expr, ns);
-      PRECONDITION(offset >= 0);
+      auto offset_opt = compute_pointer_offset(expr, ns);
+      PRECONDITION(offset_opt.has_value());
+      offset = *offset_opt;
     }
 
     if(offset>0)
diff --git a/src/goto-symex/symex_goto.cpp b/src/goto-symex/symex_goto.cpp
index 3d4426325e1..3e038e21840 100644
--- a/src/goto-symex/symex_goto.cpp
+++ b/src/goto-symex/symex_goto.cpp
@@ -255,7 +255,7 @@ void goto_symext::symex_goto(statet &state)
         log.debug(),
         [this, &new_lhs](messaget::mstreamt &mstream) {
           mstream << "Assignment to " << new_lhs.get_identifier()
-                  << " [" << pointer_offset_bits(new_lhs.type(), ns) << " bits]"
+                  << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
                   << messaget::eom;
         });
 
@@ -489,7 +489,7 @@ void goto_symext::phi_function(
       log.debug(),
       [this, &new_lhs](messaget::mstreamt &mstream) {
         mstream << "Assignment to " << new_lhs.get_identifier()
-                << " [" << pointer_offset_bits(new_lhs.type(), ns) << " bits]"
+                << " [" << pointer_offset_bits(new_lhs.type(), ns).value_or(0) << " bits]"
                 << messaget::eom;
       });
 
diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 12e931ab3e2..ea91de3e959 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -283,18 +283,18 @@ bool value_sett::eval_pointer_offset(
       else
       {
         const exprt &object=object_numbering[it->first];
-        mp_integer ptr_offset=compute_pointer_offset(object, ns);
+        auto ptr_offset = compute_pointer_offset(object, ns);
 
-        if(ptr_offset<0)
+        if(!ptr_offset.has_value())
           return false;
 
-        ptr_offset += *it->second;
+        *ptr_offset += *it->second;
 
-        if(mod && ptr_offset!=previous_offset)
+        if(mod && *ptr_offset != previous_offset)
           return false;
 
-        new_expr=from_integer(ptr_offset, expr.type());
-        previous_offset=ptr_offset;
+        new_expr = from_integer(*ptr_offset, expr.type());
+        previous_offset = *ptr_offset;
         mod=true;
       }
 
@@ -623,15 +623,15 @@ void value_sett::get_value_set_rec(
         if(pointer_sub_type.id()==ID_empty)
           pointer_sub_type=char_type();
 
-        mp_integer size=pointer_offset_size(pointer_sub_type, ns);
+        auto size = pointer_offset_size(pointer_sub_type, ns);
 
-        if(size<=0)
+        if(!size.has_value() || (*size) == 0)
         {
           i_is_set=false;
         }
         else
         {
-          i*=size;
+          i *= *size;
 
           if(expr.id()==ID_minus)
             i.negate();
@@ -890,11 +890,13 @@ void value_sett::get_value_set_rec(
       {
         const irep_idt &name = c.get_name();
 
-        mp_integer comp_offset=member_offset(struct_type, name, ns);
+        auto comp_offset = member_offset(struct_type, name, ns);
 
-        if(comp_offset>op1_offset)
+        if(!comp_offset.has_value())
+          continue;
+        else if(*comp_offset > op1_offset)
           break;
-        else if(comp_offset!=op1_offset)
+        else if(*comp_offset != op1_offset)
           continue;
 
         found=true;
@@ -1066,12 +1068,12 @@ void value_sett::get_reference_set_rec(
         }
         else if(!to_integer(offset, i) && o)
         {
-          mp_integer size=pointer_offset_size(array_type.subtype(), ns);
+          auto size = pointer_offset_size(array_type.subtype(), ns);
 
-          if(size<=0)
+          if(!size.has_value() || *size == 0)
             o.reset();
           else
-            *o = i * size;
+            *o = i * (*size);
         }
         else
           o.reset();
diff --git a/src/pointer-analysis/value_set_dereference.cpp b/src/pointer-analysis/value_set_dereference.cpp
index e5deb0bc696..d66c3d8a58c 100644
--- a/src/pointer-analysis/value_set_dereference.cpp
+++ b/src/pointer-analysis/value_set_dereference.cpp
@@ -346,6 +346,7 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
         symbol_expr,
         pointer_offset(pointer_expr),
         ns.follow(memory_symbol.type).subtype());
+
       result.value=index_expr;
     }
     else if(dereference_type_compare(
@@ -435,23 +436,21 @@ value_set_dereferencet::valuet value_set_dereferencet::build_reference_to(
       exprt adjusted_offset;
 
       // are we doing a byte?
-      mp_integer element_size =
-        pointer_offset_size(root_object_type.subtype(), ns);
+      auto element_size = pointer_offset_size(root_object_type.subtype(), ns);
 
-      if(element_size==1)
-      {
-        // no need to adjust offset
-        adjusted_offset=offset;
-      }
-      else if(element_size<=0)
+      if(!element_size.has_value() || *element_size == 0)
       {
         throw "unknown or invalid type size of:\n" +
           root_object_type.subtype().pretty();
       }
+      else if(*element_size == 1)
+      {
+        // no need to adjust offset
+        adjusted_offset = offset;
+      }
       else
       {
-        exprt element_size_expr=
-          from_integer(element_size, offset.type());
+        exprt element_size_expr = from_integer(*element_size, offset.type());
 
         adjusted_offset=binary_exprt(
           offset, ID_div, element_size_expr, offset.type());
@@ -593,11 +592,16 @@ bool value_set_dereferencet::memory_model_bytes(
 
   // See if we have an array of bytes already,
   // and we want something byte-sized.
-  if(ns.follow(from_type).id()==ID_array &&
-     pointer_offset_size(ns.follow(from_type).subtype(), ns)==1 &&
-     pointer_offset_size(to_type, ns)==1 &&
-     is_a_bv_type(ns.follow(from_type).subtype()) &&
-     is_a_bv_type(to_type))
+  auto from_type_subtype_size =
+    pointer_offset_size(ns.follow(from_type).subtype(), ns);
+
+  auto to_type_size = pointer_offset_size(to_type, ns);
+
+  if(
+    ns.follow(from_type).id() == ID_array &&
+    from_type_subtype_size.has_value() && *from_type_subtype_size == 1 &&
+    to_type_size.has_value() && *to_type_size == 1 &&
+    is_a_bv_type(ns.follow(from_type).subtype()) && is_a_bv_type(to_type))
   {
     // yes, can use 'index'
     result=index_exprt(value, offset, ns.follow(from_type).subtype());
diff --git a/src/solvers/flattening/boolbv_byte_extract.cpp b/src/solvers/flattening/boolbv_byte_extract.cpp
index 4a5eab0c3d8..973cfd3dce0 100644
--- a/src/solvers/flattening/boolbv_byte_extract.cpp
+++ b/src/solvers/flattening/boolbv_byte_extract.cpp
@@ -76,11 +76,14 @@ bvt boolbvt::convert_byte_extract(const byte_extract_exprt &expr)
 
   // see if the byte number is constant and within bounds, else work from the
   // root object
-  const mp_integer op_bytes = pointer_offset_size(expr.op().type(), ns);
+  const auto op_bytes_opt = pointer_offset_size(expr.op().type(), ns);
   auto index = numeric_cast<mp_integer>(expr.offset());
+
   if(
-    (!index.has_value() || (*index < 0 || *index >= op_bytes)) &&
-    (expr.op().id() == ID_member || expr.op().id() == ID_index ||
+    (!index.has_value() || !op_bytes_opt.has_value() ||
+     *index < 0 || *index >= *op_bytes_opt) &&
+    (expr.op().id() == ID_member ||
+     expr.op().id() == ID_index ||
      expr.op().id() == ID_byte_extract_big_endian ||
      expr.op().id() == ID_byte_extract_little_endian))
   {
diff --git a/src/solvers/flattening/boolbv_index.cpp b/src/solvers/flattening/boolbv_index.cpp
index f9bf25e6a3a..43ab3616fd5 100644
--- a/src/solvers/flattening/boolbv_index.cpp
+++ b/src/solvers/flattening/boolbv_index.cpp
@@ -335,11 +335,13 @@ bvt boolbvt::convert_index(
     o.build(array, ns);
     CHECK_RETURN(o.offset().id() != ID_unknown);
 
-    const mp_integer subtype_bytes =
+    const auto subtype_bytes_opt =
       pointer_offset_size(array_type.subtype(), ns);
+    CHECK_RETURN(subtype_bytes_opt.has_value());
+
     exprt new_offset = simplify_expr(
       plus_exprt(
-        o.offset(), from_integer(index * subtype_bytes, o.offset().type())),
+        o.offset(), from_integer(index * (*subtype_bytes_opt), o.offset().type())),
       ns);
 
     byte_extract_exprt be(
diff --git a/src/solvers/flattening/bv_pointers.cpp b/src/solvers/flattening/bv_pointers.cpp
index 16d46de9ad5..05411fa6bd2 100644
--- a/src/solvers/flattening/bv_pointers.cpp
+++ b/src/solvers/flattening/bv_pointers.cpp
@@ -136,11 +136,10 @@ bool bv_pointerst::convert_address_of_rec(
       UNREACHABLE;
 
     // get size
-    mp_integer size=
-      pointer_offset_size(array_type.subtype(), ns);
-    DATA_INVARIANT(size>0, "array subtype expected to have non-zero size");
+    auto size = pointer_offset_size(array_type.subtype(), ns);
+    CHECK_RETURN(size.has_value() && *size > 0);
 
-    offset_arithmetic(bv, size, index);
+    offset_arithmetic(bv, *size, index);
     CHECK_RETURN(bv.size()==bits);
     return false;
   }
@@ -171,13 +170,12 @@ bool bv_pointerst::convert_address_of_rec(
 
     if(struct_op_type.id()==ID_struct)
     {
-      mp_integer offset=member_offset(
-        to_struct_type(struct_op_type),
-        member_expr.get_component_name(), ns);
-      DATA_INVARIANT(offset>=0, "member offset expected to be positive");
+      auto offset = member_offset(
+        to_struct_type(struct_op_type), member_expr.get_component_name(), ns);
+      CHECK_RETURN(offset.has_value());
 
       // add offset
-      offset_arithmetic(bv, offset);
+      offset_arithmetic(bv, *offset);
     }
     else
     {
@@ -344,8 +342,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
         }
         else
         {
-          size = pointer_offset_size(pointer_sub_type, ns);
-          CHECK_RETURN(size > 0);
+          auto size_opt = pointer_offset_size(pointer_sub_type, ns);
+          CHECK_RETURN(size_opt.has_value() && *size_opt > 0);
+          size = *size_opt;
         }
       }
     }
@@ -426,8 +425,9 @@ bvt bv_pointerst::convert_pointer_type(const exprt &expr)
     }
     else
     {
-      element_size = pointer_offset_size(pointer_sub_type, ns);
-      DATA_INVARIANT(element_size > 0, "object size expected to be positive");
+      auto element_size_opt = pointer_offset_size(pointer_sub_type, ns);
+      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+      element_size = *element_size_opt;
     }
 
     offset_arithmetic(bv, element_size, neg_op1);
@@ -504,14 +504,14 @@ bvt bv_pointerst::convert_bitvector(const exprt &expr)
     }
     else
     {
-      element_size = pointer_offset_size(pointer_sub_type, ns);
-      DATA_INVARIANT(element_size > 0, "object size expected to be positive");
+      auto element_size_opt = pointer_offset_size(pointer_sub_type, ns);
+      CHECK_RETURN(element_size_opt.has_value() && *element_size_opt > 0);
+      element_size = *element_size_opt;
     }
 
-    if(element_size!=1)
+    if(element_size != 1)
     {
-      bvt element_size_bv=
-        bv_utils.build_constant(element_size, bv.size());
+      bvt element_size_bv = bv_utils.build_constant(element_size, bv.size());
       bv=bv_utils.divider(
         bv, element_size_bv, bv_utilst::representationt::SIGNED);
     }
diff --git a/src/solvers/flattening/flatten_byte_operators.cpp b/src/solvers/flattening/flatten_byte_operators.cpp
index e6639810fb5..febb2527a85 100644
--- a/src/solvers/flattening/flatten_byte_operators.cpp
+++ b/src/solvers/flattening/flatten_byte_operators.cpp
@@ -48,7 +48,9 @@ static exprt unpack_rec(
     const array_typet &array_type=to_array_type(type);
     const typet &subtype=array_type.subtype();
 
-    mp_integer element_width=pointer_offset_bits(subtype, ns);
+    auto element_width = pointer_offset_bits(subtype, ns);
+    CHECK_RETURN(element_width.has_value());
+
     // this probably doesn't really matter
     #if 0
     INVARIANT(
@@ -62,7 +64,7 @@ static exprt unpack_rec(
       irep_pretty_diagnosticst(type));
     #endif
 
-    if(!unpack_byte_array && element_width==8)
+    if(!unpack_byte_array && *element_width == 8)
       return src;
 
     mp_integer num_elements;
@@ -100,12 +102,14 @@ static exprt unpack_rec(
 
     for(const auto &comp : components)
     {
-      mp_integer element_width=pointer_offset_bits(comp.type(), ns);
+      auto element_width = pointer_offset_bits(comp.type(), ns);
 
       // the next member would be misaligned, abort
-      if(element_width<=0 || element_width%8!=0)
+      if(
+        !element_width.has_value() || *element_width == 0 ||
+        *element_width % 8 != 0)
       {
-        throw non_byte_alignedt(struct_type, comp, element_width);
+        throw non_byte_alignedt(struct_type, comp, *element_width);
       }
 
       member_exprt member(src, comp.get_name(), comp.type());
@@ -119,8 +123,12 @@ static exprt unpack_rec(
   {
     // a basic type; we turn that into extractbits while considering
     // endianness
-    mp_integer bits=pointer_offset_bits(type, ns);
-    if(bits<0)
+    auto bits_opt = pointer_offset_bits(type, ns);
+    mp_integer bits;
+
+    if(bits_opt.has_value())
+      bits = *bits_opt;
+    else
     {
       if(to_integer(max_bytes, bits))
       {
@@ -228,12 +236,13 @@ exprt flatten_byte_extract(
     const array_typet &array_type=to_array_type(type);
     const typet &subtype=array_type.subtype();
 
-    mp_integer element_width=pointer_offset_bits(subtype, ns);
+    auto element_width = pointer_offset_bits(subtype, ns);
     mp_integer num_elements;
     // TODO: consider ways of dealing with arrays of unknown subtype
     // size or with a subtype size that does not fit byte boundaries
-    if(element_width>0 && element_width%8==0 &&
-       to_integer(array_type.size(), num_elements))
+    if(
+      element_width.has_value() && *element_width >= 1 &&
+      *element_width % 8 == 0 && to_integer(array_type.size(), num_elements))
     {
       array_exprt array(array_type);
 
@@ -241,7 +250,7 @@ exprt flatten_byte_extract(
       {
         plus_exprt new_offset(
           unpacked.offset(),
-          from_integer(i*element_width, unpacked.offset().type()));
+          from_integer(i * (*element_width), unpacked.offset().type()));
 
         byte_extract_exprt tmp(unpacked);
         tmp.type()=subtype;
@@ -263,10 +272,12 @@ exprt flatten_byte_extract(
 
     for(const auto &comp : components)
     {
-      mp_integer element_width=pointer_offset_bits(comp.type(), ns);
+      auto element_width = pointer_offset_bits(comp.type(), ns);
 
       // the next member would be misaligned, abort
-      if(element_width<=0 || element_width%8!=0)
+      if(
+        !element_width.has_value() || *element_width == 0 ||
+        *element_width % 8 != 0)
       {
         failed=true;
         break;
@@ -295,14 +306,17 @@ exprt flatten_byte_extract(
   const array_typet &array_type=to_array_type(root.type());
   const typet &subtype=array_type.subtype();
 
-  DATA_INVARIANT(pointer_offset_bits(subtype, ns)==8,
-                 "offset bits are byte aligned");
+  auto subtype_bits = pointer_offset_bits(subtype, ns);
 
-  mp_integer size_bits=pointer_offset_bits(unpacked.type(), ns);
-  if(size_bits<0)
+  DATA_INVARIANT(
+    subtype_bits.has_value() && *subtype_bits == 8,
+    "offset bits are byte aligned");
+
+  auto size_bits = pointer_offset_bits(unpacked.type(), ns);
+  if(!size_bits.has_value())
   {
-    mp_integer op0_bits=pointer_offset_bits(unpacked.op().type(), ns);
-    if(op0_bits<0)
+    auto op0_bits = pointer_offset_bits(unpacked.op().type(), ns);
+    if(op0_bits.has_value())
     {
       throw non_const_byte_extraction_sizet(unpacked);
     }
@@ -310,8 +324,8 @@ exprt flatten_byte_extract(
       size_bits=op0_bits;
   }
 
-  mp_integer num_elements=
-    size_bits/8+((size_bits%8==0)?0:1);
+  mp_integer num_elements =
+    (*size_bits) / 8 + (((*size_bits) % 8 == 0) ? 0 : 1);
 
   const typet &offset_type=ns.follow(offset.type());
 
@@ -346,14 +360,16 @@ exprt flatten_byte_update(
   const namespacet &ns,
   bool negative_offset)
 {
-  mp_integer element_size = pointer_offset_size(src.value().type(), ns);
+  const auto element_size_opt = pointer_offset_size(src.value().type(), ns);
 
   INVARIANT_WITH_DIAGNOSTICS(
-    element_size >= 0,
+    element_size_opt.has_value(),
     "size of type in bytes must be known",
     irep_pretty_diagnosticst(src));
 
-  const typet &t = ns.follow(src.op().type());
+  const mp_integer &element_size = *element_size_opt;
+
+  const typet &t=ns.follow(src.op0().type());
 
   if(t.id()==ID_array)
   {
@@ -367,12 +383,14 @@ exprt flatten_byte_update(
        subtype.id()==ID_c_bool ||
        subtype.id()==ID_pointer)
     {
-      mp_integer sub_size=pointer_offset_size(subtype, ns);
+      auto sub_size_opt = pointer_offset_size(subtype, ns);
 
       INVARIANT(
-        sub_size >= 0,
+        sub_size_opt.has_value(),
         "bit width (rounded to full bytes) of subtype must be known");
 
+      const mp_integer &sub_size = *sub_size_opt;
+
       // byte array?
       if(sub_size==1)
       {
@@ -534,9 +552,9 @@ exprt flatten_byte_update(
           t.id()==ID_pointer)
   {
     // do a shift, mask and OR
-    mp_integer type_width=pointer_offset_bits(t, ns);
-    CHECK_RETURN(type_width > 0);
-    std::size_t width=integer2size_t(type_width);
+    const auto type_width = pointer_offset_bits(t, ns);
+    CHECK_RETURN(type_width.has_value() && *type_width > 0);
+    const std::size_t width = integer2size_t(*type_width);
 
     INVARIANT(
       element_size * 8 <= width,
diff --git a/src/solvers/flattening/pointer_logic.cpp b/src/solvers/flattening/pointer_logic.cpp
index e8addc209f1..5a4184793e8 100644
--- a/src/solvers/flattening/pointer_logic.cpp
+++ b/src/solvers/flattening/pointer_logic.cpp
@@ -110,14 +110,13 @@ exprt pointer_logict::object_rec(
 {
   if(src.type().id()==ID_array)
   {
-    mp_integer size=
-      pointer_offset_size(src.type().subtype(), ns);
+    auto size = pointer_offset_size(src.type().subtype(), ns);
 
-    if(size<=0)
+    if(!size.has_value() || *size == 0)
       return src;
 
-    mp_integer index=offset/size;
-    mp_integer rest=offset%size;
+    mp_integer index = offset / (*size);
+    mp_integer rest = offset % (*size);
     if(rest<0)
       rest=-rest;
 
@@ -146,9 +145,10 @@ exprt pointer_logict::object_rec(
 
       const typet &subtype=c.type();
 
-      mp_integer sub_size=pointer_offset_size(subtype, ns);
-      CHECK_RETURN(sub_size > 0);
-      mp_integer new_offset=current_offset+sub_size;
+      const auto sub_size = pointer_offset_size(subtype, ns);
+      CHECK_RETURN(sub_size.has_value() && *sub_size != 0);
+
+      mp_integer new_offset = current_offset + *sub_size;
 
       if(new_offset>offset)
       {
diff --git a/src/solvers/lowering/popcount.cpp b/src/solvers/lowering/popcount.cpp
index 3a6e6fd5b2d..c4205798ca6 100644
--- a/src/solvers/lowering/popcount.cpp
+++ b/src/solvers/lowering/popcount.cpp
@@ -26,12 +26,12 @@ exprt lower_popcount(const popcount_exprt &expr, const namespacet &ns)
 
   // make sure the operand width is a power of two
   exprt x = expr.op();
-  const mp_integer x_width = pointer_offset_bits(x.type(), ns);
-  CHECK_RETURN(x_width > 0);
-  const std::size_t bits = address_bits(x_width);
+  const auto x_width = pointer_offset_bits(x.type(), ns);
+  CHECK_RETURN(x_width.has_value() && *x_width >= 1);
+  const std::size_t bits = address_bits(*x_width);
   const std::size_t new_width = integer2size_t(power(2, bits));
   const bool need_typecast =
-    new_width > x_width || x.type().id() != ID_unsignedbv;
+    new_width > *x_width || x.type().id() != ID_unsignedbv;
   if(need_typecast)
     x.make_typecast(unsignedbv_typet(new_width));
 
diff --git a/src/solvers/smt2/smt2_conv.cpp b/src/solvers/smt2/smt2_conv.cpp
index 1d172e6a83c..078894e2d4b 100644
--- a/src/solvers/smt2/smt2_conv.cpp
+++ b/src/solvers/smt2/smt2_conv.cpp
@@ -562,15 +562,15 @@ void smt2_convt::convert_address_of_rec(
 
     const irep_idt &component_name = member_expr.get_component_name();
 
-    mp_integer offset = member_offset(struct_type, component_name, ns);
-    CHECK_RETURN(offset >= 0);
+    const auto offset = member_offset(struct_type, component_name, ns);
+    CHECK_RETURN(offset.has_value() && *offset >= 0);
 
     unsignedbv_typet index_type(boolbv_width(result_type));
 
     // pointer arithmetic
     out << "(bvadd ";
     convert_address_of_rec(struct_op, result_type);
-    convert_expr(from_integer(offset, index_type));
+    convert_expr(from_integer(*offset, index_type));
     out << ")"; // bvadd
   }
   else if(expr.id()==ID_if)
@@ -3033,18 +3033,18 @@ void smt2_convt::convert_plus(const plus_exprt &expr)
         p.type().id() == ID_pointer,
         "one of the operands should have pointer type");
 
-      mp_integer element_size = pointer_offset_size(expr.type().subtype(), ns);
-      CHECK_RETURN(element_size > 0);
+      const auto element_size = pointer_offset_size(expr.type().subtype(), ns);
+      CHECK_RETURN(element_size.has_value() && *element_size >= 1);
 
       out << "(bvadd ";
       convert_expr(p);
       out << " ";
 
-      if(element_size >= 2)
+      if(*element_size >= 2)
       {
         out << "(bvmul ";
         convert_expr(i);
-        out << " (_ bv" << element_size << " " << boolbv_width(expr.type())
+        out << " (_ bv" << *element_size << " " << boolbv_width(expr.type())
             << "))";
       }
       else
@@ -3212,12 +3212,11 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
     if(expr.op0().type().id()==ID_pointer &&
        expr.op1().type().id()==ID_pointer)
     {
-      // Pointer difference.
-      mp_integer element_size=
-        pointer_offset_size(expr.op0().type().subtype(), ns);
-      CHECK_RETURN(element_size > 0);
+      // Pointer difference
+      auto element_size = pointer_offset_size(expr.op0().type().subtype(), ns);
+      CHECK_RETURN(element_size.has_value() && *element_size >= 1);
 
-      if(element_size>=2)
+      if(*element_size >= 2)
         out << "(bvsdiv ";
 
       INVARIANT(
@@ -3231,9 +3230,9 @@ void smt2_convt::convert_minus(const minus_exprt &expr)
       convert_expr(expr.op1());
       out << ")";
 
-      if(element_size>=2)
-        out << " (_ bv" << element_size
-            << " " << boolbv_width(expr.type()) << "))";
+      if(*element_size >= 2)
+        out << " (_ bv" << *element_size << " " << boolbv_width(expr.type())
+            << "))";
     }
     else
     {
@@ -3853,12 +3852,13 @@ void smt2_convt::convert_member(const member_exprt &expr)
     {
       // we extract
       std::size_t member_width=boolbv_width(expr.type());
-      mp_integer member_offset=::member_offset(struct_type, name, ns);
+      const auto member_offset = ::member_offset(struct_type, name, ns);
+
       CHECK_RETURN_WITH_DIAGNOSTICS(
-        member_offset != -1, "failed to get struct member offset");
+        member_offset.has_value(), "failed to get struct member offset");
 
-      out << "((_ extract " << (member_offset*8+member_width-1)
-          << " " << member_offset*8 << ") ";
+      out << "((_ extract " << ((*member_offset) * 8 + member_width - 1) << " "
+          << (*member_offset) * 8 << ") ";
       convert_expr(struct_op);
       out << ")";
     }
diff --git a/src/util/endianness_map.cpp b/src/util/endianness_map.cpp
index 12d9a3f488b..be9f5907a9c 100644
--- a/src/util/endianness_map.cpp
+++ b/src/util/endianness_map.cpp
@@ -37,11 +37,12 @@ void endianness_mapt::build(const typet &src, bool little_endian)
 
 void endianness_mapt::build_little_endian(const typet &src)
 {
-  mp_integer s=pointer_offset_bits(src, ns); // error is -1
-  if(s<=0)
+  auto s = pointer_offset_bits(src, ns);
+
+  if(!s.has_value())
     return;
 
-  std::size_t new_size=map.size()+integer2size_t(s);
+  std::size_t new_size = map.size() + integer2size_t(*s);
   map.reserve(new_size);
 
   for(std::size_t i=map.size(); i<new_size; ++i)
@@ -62,10 +63,10 @@ void endianness_mapt::build_big_endian(const typet &src)
           src.id()==ID_c_bit_field)
   {
     // these do get re-ordered!
-    mp_integer bits=pointer_offset_bits(src, ns); // error is -1
-    CHECK_RETURN(bits>=0);
+    auto bits = pointer_offset_bits(src, ns); // error is -1
+    CHECK_RETURN(bits.has_value());
 
-    size_t bits_int=integer2size_t(bits), base=map.size();
+    size_t bits_int = integer2size_t(*bits), base = map.size();
 
     for(size_t bit=0; bit<bits_int; bit++)
     {
@@ -115,11 +116,12 @@ void endianness_mapt::build_big_endian(const typet &src)
   {
     // everything else (unions in particular)
     // is treated like a byte-array
-    mp_integer s=pointer_offset_bits(src, ns); // error is -1
-    if(s<=0)
+    auto s = pointer_offset_bits(src, ns); // error is -1
+
+    if(!s.has_value())
       return;
 
-    std::size_t new_size=map.size()+integer2size_t(s);
+    std::size_t new_size = map.size() + integer2size_t(*s);
     map.reserve(new_size);
 
     for(std::size_t i=map.size(); i<new_size; ++i)
diff --git a/src/util/expr_initializer.cpp b/src/util/expr_initializer.cpp
index 75f8b89b053..35ce2144dd1 100644
--- a/src/util/expr_initializer.cpp
+++ b/src/util/expr_initializer.cpp
@@ -254,13 +254,13 @@ exprt expr_initializert<nondet>::expr_initializer_rec(
       if(c.type().id() == ID_code)
         continue;
 
-      mp_integer bits = pointer_offset_bits(c.type(), ns);
+      auto bits = pointer_offset_bits(c.type(), ns);
 
-      if(bits>component_size)
+      if(bits.has_value() && *bits > component_size)
       {
         component = c;
         found=true;
-        component_size=bits;
+        component_size = *bits;
       }
     }
 
diff --git a/src/util/pointer_offset_size.cpp b/src/util/pointer_offset_size.cpp
index 5133481fff4..61666197150 100644
--- a/src/util/pointer_offset_size.cpp
+++ b/src/util/pointer_offset_size.cpp
@@ -47,17 +47,20 @@ member_offset_iterator &member_offset_iterator::operator++()
       DATA_INVARIANT(
         bit_field_bits == 0, "padding ensures offset at byte boundaries");
       const typet &subtype=comp.type();
-      mp_integer sub_size=pointer_offset_size(subtype, ns);
-      if(sub_size==-1)
+
+      auto sub_size = pointer_offset_size(subtype, ns);
+
+      if(!sub_size.has_value())
         current.second=-1; // give up
-      else current.second+=sub_size;
+      else
+        current.second += *sub_size;
     }
   }
   ++current.first;
   return *this;
 }
 
-mp_integer member_offset(
+optionalt<mp_integer> member_offset(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns)
@@ -77,7 +80,7 @@ mp_integer member_offset(
   return offsets->second;
 }
 
-mp_integer member_offset_bits(
+optionalt<mp_integer> member_offset_bits(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns)
@@ -88,38 +91,38 @@ mp_integer member_offset_bits(
   for(const auto &comp : components)
   {
     if(comp.get_name()==member)
-      break;
+      return offset;
 
-    mp_integer member_bits=pointer_offset_bits(comp.type(), ns);
-    if(member_bits==-1)
-      return member_bits;
+    auto member_bits = pointer_offset_bits(comp.type(), ns);
+    if(!member_bits.has_value())
+      return {};
 
-    offset+=member_bits;
+    offset += *member_bits;
   }
 
-  return offset;
+  return {};
 }
 
 /// Compute the size of a type in bytes, rounding up to full bytes
-mp_integer pointer_offset_size(
-  const typet &type,
-  const namespacet &ns)
+optionalt<mp_integer>
+pointer_offset_size(const typet &type, const namespacet &ns)
 {
-  mp_integer bits=pointer_offset_bits(type, ns);
-  if(bits==-1)
-    return -1;
-  return (bits+7)/8;
+  auto bits = pointer_offset_bits(type, ns);
+
+  if(bits.has_value())
+    return (*bits + 7) / 8;
+  else
+    return {};
 }
 
-mp_integer pointer_offset_bits(
-  const typet &type,
-  const namespacet &ns)
+optionalt<mp_integer>
+pointer_offset_bits(const typet &type, const namespacet &ns)
 {
   if(type.id()==ID_array)
   {
-    mp_integer sub=pointer_offset_bits(type.subtype(), ns);
-    if(sub<0)
-      return -1;
+    auto sub = pointer_offset_bits(type.subtype(), ns);
+    if(!sub.has_value())
+      return {};
 
     // get size
     const exprt &size=to_array_type(type).size();
@@ -128,15 +131,15 @@ mp_integer pointer_offset_bits(
     mp_integer i;
 
     if(to_integer(size, i))
-      return -1; // we cannot distinguish the elements
+      return {}; // we cannot distinguish the elements
 
-    return sub*i;
+    return (*sub) * i;
   }
   else if(type.id()==ID_vector)
   {
-    mp_integer sub=pointer_offset_bits(type.subtype(), ns);
-    if(sub<0)
-      return -1;
+    auto sub = pointer_offset_bits(type.subtype(), ns);
+    if(!sub.has_value())
+      return {};
 
     // get size
     const exprt &size=to_vector_type(type).size();
@@ -145,17 +148,18 @@ mp_integer pointer_offset_bits(
     mp_integer i;
 
     if(to_integer(size, i))
-      return -1; // we cannot distinguish the elements
+      return {}; // we cannot distinguish the elements
 
-    return sub*i;
+    return (*sub) * i;
   }
   else if(type.id()==ID_complex)
   {
-    mp_integer sub=pointer_offset_bits(type.subtype(), ns);
-    if(sub<0)
-      return -1;
+    auto sub = pointer_offset_bits(type.subtype(), ns);
 
-    return sub*2;
+    if(sub.has_value())
+      return (*sub) * 2;
+    else
+      return {};
   }
   else if(type.id()==ID_struct)
   {
@@ -165,10 +169,12 @@ mp_integer pointer_offset_bits(
     for(const auto &c : struct_type.components())
     {
       const typet &subtype = c.type();
-      mp_integer sub_size=pointer_offset_bits(subtype, ns);
-      if(sub_size==-1)
-        return -1;
-      result+=sub_size;
+      auto sub_size = pointer_offset_bits(subtype, ns);
+
+      if(!sub_size.has_value())
+        return {};
+
+      result += *sub_size;
     }
 
     return result;
@@ -183,11 +189,13 @@ mp_integer pointer_offset_bits(
     for(const auto &c : union_type.components())
     {
       const typet &subtype = c.type();
-      mp_integer sub_size=pointer_offset_bits(subtype, ns);
-      if(sub_size==-1)
-        return -1;
-      if(sub_size>result)
-        result=sub_size;
+      auto sub_size = pointer_offset_bits(subtype, ns);
+
+      if(!sub_size.has_value())
+        return {};
+
+      if(*sub_size > result)
+        result = *sub_size;
     }
 
     return result;
@@ -200,11 +208,11 @@ mp_integer pointer_offset_bits(
           type.id()==ID_c_bool ||
           type.id()==ID_c_bit_field)
   {
-    return to_bitvector_type(type).get_width();
+    return mp_integer(to_bitvector_type(type).get_width());
   }
   else if(type.id()==ID_c_enum)
   {
-    return to_bitvector_type(type.subtype()).get_width();
+    return mp_integer(to_bitvector_type(type.subtype()).get_width());
   }
   else if(type.id()==ID_c_enum_tag)
   {
@@ -212,15 +220,15 @@ mp_integer pointer_offset_bits(
   }
   else if(type.id()==ID_bool)
   {
-    return 1;
+    return mp_integer(1);
   }
   else if(type.id()==ID_pointer)
   {
     // the following is an MS extension
     if(type.get_bool(ID_C_ptr32))
-      return 32;
+      return mp_integer(32);
 
-    return to_bitvector_type(type).get_width();
+    return mp_integer(to_bitvector_type(type).get_width());
   }
   else if(type.id() == ID_symbol_type)
   {
@@ -236,14 +244,14 @@ mp_integer pointer_offset_bits(
   }
   else if(type.id()==ID_code)
   {
-    return 0;
+    return mp_integer(0);
   }
   else if(type.id()==ID_string)
   {
-    return 32;
+    return mp_integer(32);
   }
   else
-    return -1;
+    return {};
 }
 
 exprt member_offset_expr(
@@ -404,9 +412,9 @@ exprt size_of_expr(
       const typet &subtype = c.type();
       exprt sub_size;
 
-      mp_integer sub_bits=pointer_offset_bits(subtype, ns);
+      auto sub_bits = pointer_offset_bits(subtype, ns);
 
-      if(sub_bits==-1)
+      if(!sub_bits.has_value())
       {
         max_bytes=-1;
 
@@ -416,7 +424,7 @@ exprt size_of_expr(
       }
       else
       {
-        mp_integer sub_bytes=(sub_bits+7)/8;
+        mp_integer sub_bytes = (*sub_bits + 7) / 8;
 
         if(max_bytes>=0)
         {
@@ -507,9 +515,8 @@ exprt size_of_expr(
     return nil_exprt();
 }
 
-mp_integer compute_pointer_offset(
-  const exprt &expr,
-  const namespacet &ns)
+optionalt<mp_integer>
+compute_pointer_offset(const exprt &expr, const namespacet &ns)
 {
   if(expr.id()==ID_symbol)
   {
@@ -517,7 +524,7 @@ mp_integer compute_pointer_offset(
       return compute_pointer_offset(
         to_ssa_expr(expr).get_original_expr(), ns);
     else
-      return 0;
+      return mp_integer(0);
   }
   else if(expr.id()==ID_index)
   {
@@ -527,17 +534,18 @@ mp_integer compute_pointer_offset(
       array_type.id()==ID_array,
       "index into array expected, found "+array_type.id_string());
 
-    mp_integer o=compute_pointer_offset(index_expr.array(), ns);
+    auto o = compute_pointer_offset(index_expr.array(), ns);
 
-    if(o!=-1)
+    if(o.has_value())
     {
-      mp_integer sub_size=
-        pointer_offset_size(array_type.subtype(), ns);
+      auto sub_size = pointer_offset_size(array_type.subtype(), ns);
 
       mp_integer i;
 
-      if(sub_size>0 && !to_integer(index_expr.index(), i))
-        return o+i*sub_size;
+      if(
+        sub_size.has_value() && *sub_size > 0 &&
+        !to_integer(index_expr.index(), i))
+        return (*o) + i * (*sub_size);
     }
 
     // don't know
@@ -548,21 +556,24 @@ mp_integer compute_pointer_offset(
     const exprt &op=member_expr.struct_op();
     const struct_union_typet &type=to_struct_union_type(ns.follow(op.type()));
 
-    mp_integer o=compute_pointer_offset(op, ns);
+    auto o = compute_pointer_offset(op, ns);
 
-    if(o!=-1)
+    if(o.has_value())
     {
       if(type.id()==ID_union)
-        return o;
+        return *o;
 
-      return o+member_offset(
+      auto member_offset = ::member_offset(
         to_struct_type(type), member_expr.get_component_name(), ns);
+
+      if(member_offset.has_value())
+        return *o + *member_offset;
     }
   }
   else if(expr.id()==ID_string_constant)
-    return 0;
+    return mp_integer(0);
 
-  return -1; // don't know
+  return {}; // don't know
 }
 
 exprt build_sizeof_expr(
@@ -575,7 +586,11 @@ exprt build_sizeof_expr(
   mp_integer type_size=-1, val=-1;
 
   if(type.is_not_nil())
-    type_size=pointer_offset_size(type, ns);
+  {
+    auto tmp = pointer_offset_size(type, ns);
+    if(tmp.has_value())
+      type_size = *tmp;
+  }
 
   if(type_size<0 ||
      to_integer(expr, val) ||
@@ -585,10 +600,11 @@ exprt build_sizeof_expr(
 
   const typet t(size_type());
   DATA_INVARIANT(
-    address_bits(val+1)<=pointer_offset_bits(t, ns),
+    address_bits(val + 1) <= *pointer_offset_bits(t, ns),
     "sizeof value does not fit size_type");
 
   mp_integer remainder=0;
+
   if(type_size!=0)
   {
     remainder=val%type_size;
@@ -654,13 +670,19 @@ bool get_subexpression_at_offset(
     // A cell of the array might be, or contain, the subexpression
     // we're looking for.
     const auto &at=to_array_type(source_type);
-    mp_integer elem_size=pointer_offset_size(at.subtype(), ns);
-    if(elem_size==-1)
+
+    auto elem_size = pointer_offset_size(at.subtype(), ns);
+
+    if(!elem_size.has_value())
       return false;
-    mp_integer cellidx=offset/elem_size;
+
+    mp_integer cellidx = offset / (*elem_size);
+
     if(cellidx < 0 || !cellidx.is_long())
       return false;
-    offset=offset%elem_size;
+
+    offset = offset % (*elem_size);
+
     result=index_exprt(result, from_integer(cellidx, unsignedbv_typet(64)));
     return get_subexpression_at_offset(result, offset, target_type, ns);
   }
@@ -675,7 +697,9 @@ bool get_subexpression_at_offset(
   const namespacet &ns)
 {
   mp_integer offset_const;
+
   if(to_integer(offset, offset_const))
     return false;
-  return get_subexpression_at_offset(result, offset_const, target_type, ns);
+  else
+    return get_subexpression_at_offset(result, offset_const, target_type, ns);
 }
diff --git a/src/util/pointer_offset_size.h b/src/util/pointer_offset_size.h
index 0bdd67f85d3..ef4cbef4f1a 100644
--- a/src/util/pointer_offset_size.h
+++ b/src/util/pointer_offset_size.h
@@ -12,8 +12,9 @@ Author: Daniel Kroening, kroening@kroening.com
 #ifndef CPROVER_UTIL_POINTER_OFFSET_SIZE_H
 #define CPROVER_UTIL_POINTER_OFFSET_SIZE_H
 
-#include "mp_arith.h"
 #include "irep.h"
+#include "mp_arith.h"
+#include "optional.h"
 
 class exprt;
 class namespacet;
@@ -22,7 +23,7 @@ class typet;
 class member_exprt;
 class constant_exprt;
 
-// these return -1 on failure
+// these return 'nullopt' on failure
 
 // NOLINTNEXTLINE(readability/identifiers)
 class member_offset_iterator
@@ -40,27 +41,24 @@ class member_offset_iterator
   const refst* operator->() const { return &current; }
 };
 
-mp_integer member_offset(
+optionalt<mp_integer> member_offset(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns);
 
-mp_integer member_offset_bits(
+optionalt<mp_integer> member_offset_bits(
   const struct_typet &type,
   const irep_idt &member,
   const namespacet &ns);
 
-mp_integer pointer_offset_size(
-  const typet &type,
-  const namespacet &ns);
+optionalt<mp_integer>
+pointer_offset_size(const typet &type, const namespacet &ns);
 
-mp_integer pointer_offset_bits(
-  const typet &type,
-  const namespacet &ns);
+optionalt<mp_integer>
+pointer_offset_bits(const typet &type, const namespacet &ns);
 
-mp_integer compute_pointer_offset(
-  const exprt &expr,
-  const namespacet &ns);
+optionalt<mp_integer>
+compute_pointer_offset(const exprt &expr, const namespacet &ns);
 
 // these return 'nil' on failure
 
diff --git a/src/util/simplify_expr.cpp b/src/util/simplify_expr.cpp
index 2d9ecf36523..4a06c1d03c7 100644
--- a/src/util/simplify_expr.cpp
+++ b/src/util/simplify_expr.cpp
@@ -321,15 +321,16 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
       (expr.op0().op0().is_constant() &&
        to_constant_expr(expr.op0().op0()).get_value()==ID_NULL)))
   {
-    mp_integer sub_size=pointer_offset_size(op_type.subtype(), ns);
-    if(sub_size!=-1)
+    auto sub_size = pointer_offset_size(op_type.subtype(), ns);
+    if(sub_size.has_value())
     {
       // void*
-      if(sub_size==0 || sub_size==1)
+      if(*sub_size == 0 || *sub_size == 1)
         expr.op0()=typecast_exprt(expr.op0().op1(), size_type());
       else
-        expr.op0()=mult_exprt(from_integer(sub_size, size_type()),
-                              typecast_exprt(expr.op0().op1(), size_type()));
+        expr.op0() = mult_exprt(
+          from_integer(*sub_size, size_type()),
+          typecast_exprt(expr.op0().op1(), size_type()));
 
       simplify_rec(expr.op0());
       simplify_typecast(expr); // rec. call
@@ -392,9 +393,9 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
      op_type.id()==ID_pointer &&
      expr.op0().id()==ID_plus)
   {
-    const mp_integer step=pointer_offset_size(op_type.subtype(), ns);
+    const auto step = pointer_offset_size(op_type.subtype(), ns);
 
-    if(step>0)
+    if(step.has_value() && *step != 0)
     {
       const typet size_t_type(size_type());
       expr.op0().type()=size_t_type;
@@ -408,8 +409,8 @@ bool simplify_exprt::simplify_typecast(exprt &expr)
         else
         {
           op.make_typecast(size_t_type);
-          if(step>1)
-            op=mult_exprt(from_integer(step, size_t_type), op);
+          if(*step > 1)
+            op = mult_exprt(from_integer(*step, size_t_type), op);
         }
       }
 
@@ -1482,7 +1483,9 @@ exprt simplify_exprt::bits2expr(
   // bits start at lowest memory address
   const typet &type=ns.follow(_type);
 
-  if(pointer_offset_bits(type, ns)!=bits.size())
+  auto type_bits = pointer_offset_bits(type, ns);
+
+  if(!type_bits.has_value() || *type_bits != bits.size())
     return nil_exprt();
 
   if(type.id()==ID_unsignedbv ||
@@ -1539,20 +1542,21 @@ exprt simplify_exprt::bits2expr(
     mp_integer m_offset_bits=0;
     for(const auto &component : components)
     {
-      mp_integer m_size=pointer_offset_bits(component.type(), ns);
-      CHECK_RETURN(m_size >= 0);
+      const auto m_size = pointer_offset_bits(component.type(), ns);
+      CHECK_RETURN(m_size.has_value() && *m_size>=0);
 
       std::string comp_bits=
         std::string(
           bits,
           integer2size_t(m_offset_bits),
-          integer2size_t(m_size));
+          integer2size_t(*m_size));
+
       exprt comp=bits2expr(comp_bits, component.type(), little_endian);
       if(comp.is_nil())
         return nil_exprt();
       result.move_to_operands(comp);
 
-      m_offset_bits+=m_size;
+      m_offset_bits += *m_size;
     }
 
     return result;
@@ -1566,9 +1570,10 @@ exprt simplify_exprt::bits2expr(
       UNREACHABLE;
     std::size_t n_el=integer2size_t(size);
 
-    std::size_t el_size=
-      integer2size_t(pointer_offset_bits(type.subtype(), ns));
-    CHECK_RETURN(el_size > 0);
+    const auto el_size_opt = pointer_offset_bits(type.subtype(), ns);
+    CHECK_RETURN(el_size_opt.has_value() && *el_size_opt > 0);
+
+    const std::size_t el_size = integer2size_t(*el_size_opt);
 
     array_exprt result(array_type);
     result.reserve_operands(n_el);
@@ -1663,7 +1668,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     return false;
   }
 
-  const mp_integer el_size=pointer_offset_bits(expr.type(), ns);
+  const auto el_size = pointer_offset_bits(expr.type(), ns);
 
   // byte_extract(byte_extract(root, offset1), offset2) =>
   // byte_extract(root, offset1+offset2)
@@ -1695,8 +1700,9 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 
       return false;
     }
-    else if(el_size>=0 &&
-            el_size<=pointer_offset_bits(expr.op().op2().type(), ns))
+    else if(
+      el_size.has_value() &&
+      *el_size <= pointer_offset_bits(expr.op().op2().type(), ns))
     {
       expr.op()=expr.op().op2();
       expr.offset()=from_integer(0, expr.offset().type());
@@ -1727,7 +1733,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 
   // no proper simplification for expr.type()==void
   // or types of unknown size
-  if(el_size<=0)
+  if(!el_size.has_value() || *el_size == 0)
     return true;
 
   if(expr.op().id()==ID_array_of &&
@@ -1745,14 +1751,11 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     DATA_INVARIANT(!const_bits.empty(), "bit representation must be non-empty");
 
     // double the string until we have sufficiently many bits
-    while(mp_integer(const_bits.size())<offset*8+el_size)
+    while(mp_integer(const_bits.size()) < offset * 8 + *el_size)
       const_bits+=const_bits;
 
-    std::string el_bits=
-      std::string(
-        const_bits,
-        integer2size_t(offset*8),
-        integer2size_t(el_size));
+    std::string el_bits = std::string(
+      const_bits, integer2size_t(offset * 8), integer2size_t(*el_size));
 
     exprt tmp=
       bits2expr(
@@ -1768,9 +1771,9 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
   }
 
   // in some cases we even handle non-const array_of
-  if(expr.op().id()==ID_array_of &&
-     (offset*8)%el_size==0 &&
-     el_size<=pointer_offset_bits(expr.op().op0().type(), ns))
+  if(
+    expr.op().id() == ID_array_of && (offset * 8) % (*el_size) == 0 &&
+    *el_size <= pointer_offset_bits(expr.op().op0().type(), ns))
   {
     expr.op()=index_exprt(expr.op(), expr.offset());
     expr.offset()=from_integer(0, expr.offset().type());
@@ -1786,13 +1789,13 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
   // exact match of length only - otherwise we might lose bits of
   // flexible array members at the end of a struct
   if(bits.has_value() &&
-     mp_integer(bits->size())==el_size+offset*8)
+     mp_integer(bits->size()) == el_size.value() + offset * 8)
   {
     std::string bits_cut=
       std::string(
         bits.value(),
         integer2size_t(offset*8),
-        integer2size_t(el_size));
+        integer2size_t(el_size.value()));
 
     exprt tmp=
       bits2expr(
@@ -1824,11 +1827,12 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
         op_type_ptr->id()==ID_array;
         op_type_ptr=&(ns.follow(*op_type_ptr).subtype()))
     {
-      DATA_INVARIANT(el_size > 0, "arrays must not have zero-sized objects");
+      DATA_INVARIANT(*el_size > 0, "arrays must not have zero-sized objects");
       DATA_INVARIANT(
-        el_size % 8 == 0,
+        (*el_size) % 8 == 0,
         "array elements have a size in bits which is a multiple of bytes");
-      mp_integer el_bytes=el_size/8;
+
+      mp_integer el_bytes = (*el_size) / 8;
 
       if(base_type_eq(expr.type(), op_type_ptr->subtype(), ns) ||
          (expr.type().id()==ID_pointer &&
@@ -1854,12 +1858,12 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
       }
       else
       {
-        mp_integer sub_size=pointer_offset_size(op_type_ptr->subtype(), ns);
+        auto sub_size = pointer_offset_size(op_type_ptr->subtype(), ns);
 
-        if(sub_size>0)
+        if(sub_size.has_value() && *sub_size > 0)
         {
-          mp_integer index=offset/sub_size;
-          offset%=sub_size;
+          mp_integer index = offset / (*sub_size);
+          offset %= (*sub_size);
 
           result=
             index_exprt(
@@ -1879,14 +1883,13 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
     mp_integer m_offset_bits=0;
     for(const auto &component : components)
     {
-      mp_integer m_size=
-        pointer_offset_bits(component.type(), ns);
-      if(m_size<=0)
+      auto m_size = pointer_offset_bits(component.type(), ns);
+      if(!m_size.has_value() || *m_size <= 0)
         break;
 
-      if(offset*8==m_offset_bits &&
-         el_size==m_size &&
-         base_type_eq(expr.type(), component.type(), ns))
+      if(
+        offset * 8 == m_offset_bits && *el_size == *m_size &&
+        base_type_eq(expr.type(), component.type(), ns))
       {
         member_exprt member(expr.op(), component.get_name(), component.type());
         simplify_member(member);
@@ -1894,9 +1897,10 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
 
         return false;
       }
-      else if(offset*8>=m_offset_bits &&
-              offset*8+el_size<=m_offset_bits+m_size &&
-              m_offset_bits%8==0)
+      else if(
+        offset * 8 >= m_offset_bits &&
+        offset * 8 + *el_size <= m_offset_bits + *m_size &&
+        m_offset_bits % 8 == 0)
       {
         expr.op()=
           member_exprt(expr.op(), component.get_name(), component.type());
@@ -1908,7 +1912,7 @@ bool simplify_exprt::simplify_byte_extract(byte_extract_exprt &expr)
         return false;
       }
 
-      m_offset_bits+=m_size;
+      m_offset_bits += *m_size;
     }
   }
 
@@ -1930,14 +1934,13 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
   const exprt &root=expr.op();
   const exprt &offset=expr.offset();
   const exprt &value=expr.value();
-  const mp_integer val_size=pointer_offset_bits(value.type(), ns);
-  const mp_integer root_size=pointer_offset_bits(root.type(), ns);
+  const auto val_size = pointer_offset_bits(value.type(), ns);
+  const auto root_size = pointer_offset_bits(root.type(), ns);
 
   // byte update of full object is byte_extract(new value)
-  if(offset.is_zero() &&
-     val_size>0 &&
-     root_size>0 &&
-     val_size>=root_size)
+  if(
+    offset.is_zero() && val_size.has_value() && *val_size > 0 &&
+    root_size.has_value() && *root_size > 0 && *val_size >= *root_size)
   {
     byte_extract_exprt be(
       expr.id()==ID_byte_update_little_endian ?
@@ -1993,10 +1996,10 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
         else
         {
           // new offset = offset + component offset
-          mp_integer i=member_offset(struct_type, component_name, ns);
-          if(i!=-1)
+          auto i = member_offset(struct_type, component_name, ns);
+          if(i.has_value())
           {
-            exprt compo_offset = from_integer(i, offset.type());
+            exprt compo_offset = from_integer(*i, offset.type());
             plus_exprt new_offset(offset, compo_offset);
             simplify_node(new_offset);
             exprt new_value(with.op2());
@@ -2009,11 +2012,11 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
       }
       else if(tp.id()==ID_array)
       {
-        mp_integer i=pointer_offset_size(tp.subtype(), ns);
-        if(i!=-1)
+        auto i = pointer_offset_size(tp.subtype(), ns);
+        if(i.has_value())
         {
           const exprt &index=with.where();
-          mult_exprt index_offset(index, from_integer(i, index.type()));
+          mult_exprt index_offset(index, from_integer(*i, index.type()));
           simplify_node(index_offset);
 
           // index_offset may need a typecast
@@ -2044,7 +2047,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
   const typet &op_type=ns.follow(root.type());
 
   // size must be known
-  if(val_size<=0)
+  if(!val_size.has_value() || *val_size == 0)
     return true;
 
   // Are we updating (parts of) a struct? Do individual member updates
@@ -2054,8 +2057,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
     exprt result_expr;
     result_expr.make_nil();
 
-    mp_integer update_size=
-      pointer_offset_size(value.type(), ns);
+    auto update_size = pointer_offset_size(value.type(), ns);
 
     const struct_typet &struct_type=
       to_struct_type(op_type);
@@ -2064,27 +2066,36 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
 
     for(const auto &component : components)
     {
-      mp_integer m_offset=
-        member_offset(struct_type, component.get_name(), ns);
-      mp_integer m_size_bits=pointer_offset_bits(component.type(), ns);
-      mp_integer m_size_bytes=m_size_bits/8;
+      auto m_offset = member_offset(struct_type, component.get_name(), ns);
+
+      auto m_size_bits = pointer_offset_bits(component.type(), ns);
+
+      // can we determine the current offset?
+      if(!m_offset.has_value())
+      {
+        result_expr.make_nil();
+        break;
+      }
 
-      // can we determine the current offset, and is it a byte-sized
-      // member?
-      if(m_offset<0 ||
-         m_size_bits<=0 ||
-         m_size_bits%8!=0)
+      // is it a byte-sized member?
+      if(!m_size_bits.has_value() || *m_size_bits == 0 || (*m_size_bits) % 8 != 0)
       {
         result_expr.make_nil();
         break;
       }
+
+      mp_integer m_size_bytes = (*m_size_bits) / 8;
+
       // is that member part of the update?
-      else if(m_offset+m_size_bytes<=offset_int)
+      if(*m_offset + m_size_bytes <= offset_int)
         continue;
       // are we done updating?
-      else if(update_size>0 &&
-              m_offset>=offset_int+update_size)
+      else if(
+        update_size.has_value() && *update_size > 0 &&
+        *m_offset >= offset_int + *update_size)
+      {
         break;
+      }
 
       if(result_expr.is_nil())
         result_expr=expr.op();
@@ -2094,21 +2105,22 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
       result_expr=with_exprt(result_expr, member_name, nil_exprt());
 
       // are we updating on member boundaries?
-      if(m_offset<offset_int ||
-         (m_offset==offset_int &&
-          update_size>0 &&
-          m_size_bytes>update_size))
+      if(
+        m_offset < offset_int ||
+        (m_offset == offset_int && update_size.has_value() &&
+         *update_size > 0 && m_size_bytes > *update_size))
       {
         byte_update_exprt v(
           ID_byte_update_little_endian,
           member_exprt(root, component.get_name(), component.type()),
-          from_integer(offset_int-m_offset, offset.type()),
+          from_integer(offset_int - *m_offset, offset.type()),
           value);
 
         to_with_expr(result_expr).new_value().swap(v);
       }
-      else if(update_size>0 &&
-              m_offset+m_size_bytes>offset_int+update_size)
+      else if(
+        update_size.has_value() && *update_size > 0 &&
+        *m_offset + m_size_bytes > offset_int + *update_size)
       {
         // we don't handle this for the moment
         result_expr.make_nil();
@@ -2119,7 +2131,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
         byte_extract_exprt v(
           ID_byte_extract_little_endian,
           value,
-          from_integer(m_offset-offset_int, offset.type()),
+          from_integer(*m_offset - offset_int, offset.type()),
           component.type());
 
         to_with_expr(result_expr).new_value().swap(v);
@@ -2147,24 +2159,28 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
   // byte_extract
   if(root.id()==ID_array)
   {
-    mp_integer el_size=pointer_offset_bits(op_type.subtype(), ns);
-    if(el_size<=0 || el_size%8!=0 || val_size%8!=0)
+    auto el_size = pointer_offset_bits(op_type.subtype(), ns);
+
+    if(!el_size.has_value() || *el_size == 0 ||
+       (*el_size) % 8 != 0 || (*val_size) % 8 != 0)
+    {
       return true;
+    }
 
     exprt result=root;
 
     mp_integer m_offset_bits=0, val_offset=0;
     Forall_operands(it, result)
     {
-      if(offset_int*8+val_size<=m_offset_bits)
+      if(offset_int * 8 + (*val_size) <= m_offset_bits)
         break;
 
-      if(offset_int*8<m_offset_bits+el_size)
+      if(offset_int * 8 < m_offset_bits + *el_size)
       {
-        mp_integer bytes_req=(m_offset_bits+el_size)/8-offset_int;
+        mp_integer bytes_req = (m_offset_bits + *el_size) / 8 - offset_int;
         bytes_req-=val_offset;
-        if(val_offset+bytes_req>val_size/8)
-          bytes_req=val_size/8-val_offset;
+        if(val_offset + bytes_req > (*val_size) / 8)
+          bytes_req = (*val_size) / 8 - val_offset;
 
         byte_extract_exprt new_val(
           byte_extract_id(),
@@ -2184,7 +2200,7 @@ bool simplify_exprt::simplify_byte_update(byte_update_exprt &expr)
         val_offset+=bytes_req;
       }
 
-      m_offset_bits+=el_size;
+      m_offset_bits += *el_size;
     }
 
     expr.swap(result);
diff --git a/src/util/simplify_expr_array.cpp b/src/util/simplify_expr_array.cpp
index db64a51b243..d3ae282ab57 100644
--- a/src/util/simplify_expr_array.cpp
+++ b/src/util/simplify_expr_array.cpp
@@ -190,12 +190,12 @@ bool simplify_exprt::simplify_index(exprt &expr)
       // This rewrites byte_extract(s, o, array_type)[i]
       // to byte_extract(s, o+offset, sub_type)
 
-      mp_integer sub_size=pointer_offset_size(array_type.subtype(), ns);
-      if(sub_size==-1)
+      auto sub_size = pointer_offset_size(array_type.subtype(), ns);
+      if(!sub_size.has_value())
         return true;
 
       // add offset to index
-      mult_exprt offset(from_integer(sub_size, array.op1().type()), index);
+      mult_exprt offset(from_integer(*sub_size, array.op1().type()), index);
       plus_exprt final_offset(array.op1(), offset);
       simplify_node(final_offset);
 
diff --git a/src/util/simplify_expr_int.cpp b/src/util/simplify_expr_int.cpp
index 312a15bb352..a11b8b8c84b 100644
--- a/src/util/simplify_expr_int.cpp
+++ b/src/util/simplify_expr_int.cpp
@@ -1117,9 +1117,12 @@ bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr)
   if(to_integer(expr.lower(), end))
     return true;
 
-  const mp_integer width = pointer_offset_bits(op0_type, ns);
+  const auto width = pointer_offset_bits(op0_type, ns);
 
-  if(start < 0 || start >= width || end < 0 || end >= width)
+  if(!width.has_value())
+    return true;
+
+  if(start < 0 || start >= (*width) || end < 0 || end >= (*width))
     return true;
 
   DATA_INVARIANT(
@@ -1130,15 +1133,13 @@ bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr)
   {
     const irep_idt &value = to_constant_expr(expr.src()).get_value();
 
-    if(value.size()!=width)
+    if(value.size() != *width)
       return true;
 
     std::string svalue=id2string(value);
 
-    std::string extracted_value =
-      svalue.substr(
-        integer2size_t(width - start - 1),
-        integer2size_t(start - end + 1));
+    std::string extracted_value = svalue.substr(
+      integer2size_t(*width - start - 1), integer2size_t(start - end + 1));
 
     constant_exprt result(extracted_value, expr.type());
     expr.swap(result);
@@ -1149,16 +1150,16 @@ bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr)
   {
     // the most-significant bit comes first in an concatenation_exprt, hence we
     // count down
-    mp_integer offset = width;
+    mp_integer offset = *width;
 
     forall_operands(it, expr.src())
     {
-      mp_integer op_width = pointer_offset_bits(it->type(), ns);
+      auto op_width = pointer_offset_bits(it->type(), ns);
 
-      if(op_width <= 0)
+      if(!op_width.has_value() || *op_width <= 0)
         return true;
 
-      if(start + 1 == offset && end + op_width == offset)
+      if(start + 1 == offset && end + *op_width == offset)
       {
         exprt tmp = *it;
         if(tmp.type() != expr.type())
@@ -1168,7 +1169,7 @@ bool simplify_exprt::simplify_extractbits(extractbits_exprt &expr)
         return false;
       }
 
-      offset -= op_width;
+      offset -= *op_width;
     }
   }
 
diff --git a/src/util/simplify_expr_pointer.cpp b/src/util/simplify_expr_pointer.cpp
index b183c81890b..1e894acfad1 100644
--- a/src/util/simplify_expr_pointer.cpp
+++ b/src/util/simplify_expr_pointer.cpp
@@ -68,21 +68,25 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
       if(is_dereference_integer_object(expr.op0(), address))
       {
         // push index into address
+        auto step_size = pointer_offset_size(expr.type(), ns);
 
-        mp_integer step_size, index;
+        if(step_size.has_value())
+        {
+          mp_integer index;
 
-        step_size=pointer_offset_size(expr.type(), ns);
+          if(!to_integer(expr.op1(), index))
+          {
+            pointer_typet pointer_type =
+              to_pointer_type(to_dereference_expr(expr.op0()).pointer().type());
+            pointer_type.subtype() = expr.type();
 
-        if(!to_integer(expr.op1(), index) &&
-           step_size!=-1)
-        {
-          pointer_typet pointer_type=
-            to_pointer_type(to_dereference_expr(expr.op0()).pointer().type());
-          pointer_type.subtype()=expr.type();
-          typecast_exprt typecast_expr(
-            from_integer(step_size*index+address, index_type()), pointer_type);
-          expr = dereference_exprt(typecast_expr, expr.type());
-          result=true;
+            typecast_exprt typecast_expr(
+              from_integer((*step_size) * index + address, index_type()),
+              pointer_type);
+
+            expr = dereference_exprt(typecast_expr, expr.type());
+            result = true;
+          }
         }
       }
 
@@ -109,14 +113,14 @@ bool simplify_exprt::simplify_address_of_arg(exprt &expr)
         {
           const struct_typet &struct_type=to_struct_type(op_type);
           const irep_idt &member=to_member_expr(expr).get_component_name();
-          mp_integer offset=member_offset(struct_type, member, ns);
-          if(offset!=-1)
+          auto offset = member_offset(struct_type, member, ns);
+          if(offset.has_value())
           {
             pointer_typet pointer_type=
               to_pointer_type(to_dereference_expr(expr.op0()).pointer().type());
             pointer_type.subtype()=expr.type();
             typecast_exprt typecast_expr(
-              from_integer(address+offset, index_type()), pointer_type);
+              from_integer(address + *offset, index_type()), pointer_type);
             expr = dereference_exprt(typecast_expr, expr.type());
             result=true;
           }
@@ -231,11 +235,11 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     if(ptr.operands().size()!=1)
       return true;
 
-    mp_integer offset=compute_pointer_offset(ptr.op0(), ns);
+    auto offset = compute_pointer_offset(ptr.op0(), ns);
 
-    if(offset!=-1)
+    if(offset.has_value())
     {
-      expr=from_integer(offset, expr.type());
+      expr = from_integer(*offset, expr.type());
       return false;
     }
   }
@@ -335,10 +339,9 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
     if(pointer_sub_type.id()==ID_empty)
       pointer_sub_type=char_type();
 
-    mp_integer element_size=
-      pointer_offset_size(pointer_sub_type, ns);
+    auto element_size = pointer_offset_size(pointer_sub_type, ns);
 
-    if(element_size<0)
+    if(!element_size.has_value())
       return true;
 
     // this might change the type of the pointer!
@@ -357,8 +360,7 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
 
     simplify_node(sum);
 
-    exprt size_expr=
-      from_integer(element_size, expr.type());
+    exprt size_expr = from_integer(*element_size, expr.type());
 
     binary_exprt product(sum, ID_mult, size_expr, expr.type());
 
@@ -393,8 +395,8 @@ bool simplify_exprt::simplify_pointer_offset(exprt &expr)
         return true;
 
       // The constant address consists of OBJECT-ID || OFFSET.
-      mp_integer offset_bits=
-        pointer_offset_bits(ptr.type(), ns)-config.bv_encoding.object_bits;
+      mp_integer offset_bits =
+        *pointer_offset_bits(ptr.type(), ns) - config.bv_encoding.object_bits;
       number%=power(2, offset_bits);
 
       expr=from_integer(number, expr.type());
diff --git a/src/util/simplify_expr_struct.cpp b/src/util/simplify_expr_struct.cpp
index 02ab9558042..cb0b6eb5242 100644
--- a/src/util/simplify_expr_struct.cpp
+++ b/src/util/simplify_expr_struct.cpp
@@ -156,12 +156,12 @@ bool simplify_exprt::simplify_member(exprt &expr)
         return true;
 
       // add member offset to index
-      mp_integer offset_int=member_offset(struct_type, component_name, ns);
-      if(offset_int==-1)
+      auto offset_int = member_offset(struct_type, component_name, ns);
+      if(!offset_int.has_value())
         return true;
 
       const exprt &struct_offset=op.op1();
-      exprt member_offset=from_integer(offset_int, struct_offset.type());
+      exprt member_offset = from_integer(*offset_int, struct_offset.type());
       plus_exprt final_offset(struct_offset, member_offset);
       simplify_node(final_offset);
 
@@ -203,12 +203,11 @@ bool simplify_exprt::simplify_member(exprt &expr)
     }
 
     // need to convert!
-    mp_integer target_size=
-      pointer_offset_size(expr.type(), ns);
+    auto target_size = pointer_offset_size(expr.type(), ns);
 
-    if(target_size!=-1)
+    if(target_size.has_value())
     {
-      mp_integer target_bits=target_size*8;
+      mp_integer target_bits = target_size.value() * 8;
       const auto bits=expr2bits(op, true);
 
       if(bits.has_value() &&