diff --git a/src/pointer-analysis/value_set.cpp b/src/pointer-analysis/value_set.cpp
index 18b6280eea8..b096016117d 100644
--- a/src/pointer-analysis/value_set.cpp
+++ b/src/pointer-analysis/value_set.cpp
@@ -75,24 +75,23 @@ value_sett::entryt &value_sett::get_entry(
 bool value_sett::insert(
   object_mapt &dest,
   object_numberingt::number_type n,
-  const objectt &object) const
+  const offsett &offset) const
 {
   auto entry=dest.read().find(n);
 
   if(entry==dest.read().end())
   {
     // new
-    dest.write()[n]=object;
+    dest.write()[n] = offset;
     return true;
   }
-  else if(!entry->second.offset_is_set)
+  else if(!entry->second)
     return false; // no change
-  else if(object.offset_is_set &&
-          entry->second.offset==object.offset)
+  else if(offset && *entry->second == *offset)
     return false; // no change
   else
   {
-    dest.write()[n].offset_is_set=false;
+    dest.write()[n].reset();
     return true;
   }
 }
@@ -155,8 +154,8 @@ void value_sett::output(
       {
         result="<"+from_expr(ns, identifier, o)+", ";
 
-        if(o_it->second.offset_is_set)
-          result+=integer2string(o_it->second.offset)+"";
+        if(o_it->second)
+          result += integer2string(*o_it->second) + "";
         else
           result+='*';
 
@@ -199,8 +198,8 @@ exprt value_sett::to_expr(const object_map_dt::value_type &it) const
 
   od.object()=object;
 
-  if(it.second.offset_is_set)
-    od.offset()=from_integer(it.second.offset, index_type());
+  if(it.second)
+    od.offset() = from_integer(*it.second, index_type());
 
   od.type()=od.object().type();
 
@@ -282,7 +281,7 @@ bool value_sett::eval_pointer_offset(
         it=object_map.begin();
         it!=object_map.end();
         it++)
-      if(!it->second.offset_is_set)
+      if(!it->second)
         return false;
       else
       {
@@ -292,7 +291,7 @@ bool value_sett::eval_pointer_offset(
         if(ptr_offset<0)
           return false;
 
-        ptr_offset+=it->second.offset;
+        ptr_offset += *it->second;
 
         if(mod && ptr_offset!=previous_offset)
           return false;
@@ -635,15 +634,15 @@ void value_sett::get_value_set_rec(
         it!=pointer_expr_set.read().end();
         it++)
     {
-      objectt object=it->second;
+      offsett offset = it->second;
 
       // adjust by offset
-      if(object.offset_is_set && i_is_set)
-        object.offset+=i;
+      if(offset && i_is_set)
+        *offset += i;
       else
-        object.offset_is_set=false;
+        offset.reset();
 
-      insert(dest, it->first, object);
+      insert(dest, it->first, offset);
     }
   }
   else if(expr.id()==ID_mult)
@@ -668,12 +667,12 @@ void value_sett::get_value_set_rec(
         it!=pointer_expr_set.read().end();
         it++)
     {
-      objectt object=it->second;
+      offsett offset = it->second;
 
       // kill any offset
-      object.offset_is_set=false;
+      offset.reset();
 
-      insert(dest, it->first, object);
+      insert(dest, it->first, offset);
     }
   }
   else if(expr.id()==ID_side_effect)
@@ -1002,24 +1001,23 @@ void value_sett::get_reference_set_rec(
         if(ns.follow(object.type())!=array_type)
           index_expr.make_typecast(array.type());
 
-        objectt o=a_it->second;
+        offsett o = a_it->second;
         mp_integer i;
 
         if(offset.is_zero())
         {
         }
-        else if(!to_integer(offset, i) &&
-                o.offset_is_set)
+        else if(!to_integer(offset, i) && o)
         {
           mp_integer size=pointer_offset_size(array_type.subtype(), ns);
 
           if(size<=0)
-            o.offset_is_set=false;
+            o.reset();
           else
-            o.offset=i*size;
+            *o = i * size;
         }
         else
-          o.offset_is_set=false;
+          o.reset();
 
         insert(dest, index_expr, o);
       }
@@ -1052,7 +1050,7 @@ void value_sett::get_reference_set_rec(
         insert(dest, exprt(ID_unknown, expr.type()));
       else
       {
-        objectt o=it->second;
+        offsett o = it->second;
 
         member_exprt member_expr(object, component_name, expr.type());
 
@@ -1282,7 +1280,7 @@ void value_sett::do_free(
         else
         {
           // adjust
-          objectt o=o_it->second;
+          offsett o = o_it->second;
           exprt tmp(object);
           to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
           insert(new_object_map, tmp, o);
diff --git a/src/pointer-analysis/value_set.h b/src/pointer-analysis/value_set.h
index 4ebc099bcce..1be4a60045e 100644
--- a/src/pointer-analysis/value_set.h
+++ b/src/pointer-analysis/value_set.h
@@ -61,54 +61,23 @@ class value_sett
   typedef irep_idt idt;
 
   /// Represents the offset into an object: either a unique integer offset,
-  /// or an unknown value, represented by `!offset_is_set`.
-  class objectt
+  /// or an unknown value, represented by `!offset`.
+  typedef optionalt<mp_integer> offsett;
+  bool offset_is_zero(const offsett &offset) const
   {
-  public:
-    /// Constructs an unknown offset
-    objectt():offset_is_set(false)
-    {
-    }
-
-    /// Constructs a known offset
-    explicit objectt(const mp_integer &_offset):
-      offset(_offset),
-      offset_is_set(true)
-    {
-    }
-
-    /// Offset into the target object. Ignored if `offset_is_set` is false.
-    mp_integer offset;
-
-    /// If true, `offset` gives a unique integer offset; if false, represents
-    /// an unknown offset.
-    bool offset_is_set;
-
-    bool offset_is_zero() const
-    { return offset_is_set && offset.is_zero(); }
-
-    bool operator==(const objectt &other) const
-    {
-      return
-        offset_is_set==other.offset_is_set &&
-        (!offset_is_set || offset==other.offset);
-    }
-    bool operator!=(const objectt &other) const
-    {
-      return !(*this==other);
-    }
-  };
+    return offset && offset->is_zero();
+  }
 
   /// Represents a set of expressions (`exprt` instances) with corresponding
-  /// offsets (`objectt` instances). This is the RHS set of a single row of
+  /// offsets (`offsett` instances). This is the RHS set of a single row of
   /// the enclosing `value_sett`, such as `{ null, dynamic_object1 }`.
-  /// The set is represented as a map from numbered `exprt`s to `objectt`
+  /// The set is represented as a map from numbered `exprt`s to `offsett`
   /// instead of a set of pairs to make lookup by `exprt` easier. All
   /// methods matching the interface of `std::map` forward those methods
   /// to the internal map.
   class object_map_dt
   {
-    typedef std::map<object_numberingt::number_type, objectt> data_typet;
+    typedef std::map<object_numberingt::number_type, offsett> data_typet;
     data_typet data;
 
   public:
@@ -135,9 +104,18 @@ class value_sett
     void erase(key_type i) { data.erase(i); }
     void erase(const_iterator it) { data.erase(it); }
 
-    objectt &operator[](key_type i) { return data[i]; }
-    objectt &at(key_type i) { return data.at(i); }
-    const objectt &at(key_type i) const { return data.at(i); }
+    offsett &operator[](key_type i)
+    {
+      return data[i];
+    }
+    offsett &at(key_type i)
+    {
+      return data.at(i);
+    }
+    const offsett &at(key_type i) const
+    {
+      return data.at(i);
+    }
 
     template <typename It>
     void insert(It b, It e) { data.insert(b, e); }
@@ -210,7 +188,7 @@ class value_sett
   /// \param src: expression to add
   bool insert(object_mapt &dest, const exprt &src) const
   {
-    return insert(dest, object_numbering.number(src), objectt());
+    return insert(dest, object_numbering.number(src), offsett());
   }
 
   /// Adds an expression to an object map, with known offset. If the
@@ -218,13 +196,13 @@ class value_sett
   /// with a differing offset its offset is marked unknown.
   /// \param dest: object map to update
   /// \param src: expression to add
-  /// \param offset: offset into `src`
+  /// \param offset_value: offset into `src`
   bool insert(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert(dest, object_numbering.number(src), objectt(offset));
+    return insert(dest, object_numbering.number(src), offsett(offset_value));
   }
 
   /// Adds a numbered expression and offset to an object map. If the
@@ -237,7 +215,7 @@ class value_sett
   bool insert(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const;
+    const offsett &offset) const;
 
   /// Adds an expression and offset to an object map. If the
   /// destination map has an existing entry for the same expression
@@ -245,9 +223,9 @@ class value_sett
   /// \param dest: object map to update
   /// \param expr: expression to add
   /// \param object: offset into `expr` (may be unknown).
-  bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
+  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert(dest, object_numbering.number(expr), object);
+    return insert(dest, object_numbering.number(expr), offset);
   }
 
   /// Represents a row of a `value_sett`. For example, this might represent
diff --git a/src/pointer-analysis/value_set_fi.cpp b/src/pointer-analysis/value_set_fi.cpp
index 7e661711c39..23ccd0c7dad 100644
--- a/src/pointer-analysis/value_set_fi.cpp
+++ b/src/pointer-analysis/value_set_fi.cpp
@@ -102,8 +102,8 @@ void value_set_fit::output(
       {
         result="<"+from_expr(ns, identifier, o)+", ";
 
-        if(o_it->second.offset_is_set)
-          result+=integer2string(o_it->second.offset)+"";
+        if(o_it->second)
+          result += integer2string(*o_it->second) + "";
         else
           result+='*';
 
@@ -197,13 +197,12 @@ void value_set_fit::flatten_rec(
             t_it!=temp.write().end();
             t_it++)
         {
-          if(t_it->second.offset_is_set &&
-             it->second.offset_is_set)
+          if(t_it->second && it->second)
           {
-            t_it->second.offset += it->second.offset;
+            *t_it->second += *it->second;
           }
           else
-            t_it->second.offset_is_set=false;
+            t_it->second.reset();
         }
 
         forall_objects(oit, temp.read())
@@ -217,7 +216,7 @@ void value_set_fit::flatten_rec(
   if(generalize_index) // this means we had recursive symbols in there
   {
     Forall_objects(it, dest.write())
-      it->second.offset_is_set = false;
+      it->second.reset();
   }
 
   seen.erase(identifier + e.suffix);
@@ -235,8 +234,8 @@ exprt value_set_fit::to_expr(const object_map_dt::value_type &it) const
 
   od.object()=object;
 
-  if(it.second.offset_is_set)
-    od.offset()=from_integer(it.second.offset, index_type());
+  if(it.second)
+    od.offset() = from_integer(*it.second, index_type());
 
   od.type()=od.object().type();
 
@@ -324,13 +323,12 @@ void value_set_fit::get_value_set(
             t_it!=temp.write().end();
             t_it++)
         {
-          if(t_it->second.offset_is_set &&
-             it->second.offset_is_set)
+          if(t_it->second && it->second)
           {
-            t_it->second.offset += it->second.offset;
+            *t_it->second += *it->second;
           }
           else
-            t_it->second.offset_is_set=false;
+            t_it->second.reset();
 
           flat_map.write()[t_it->first]=t_it->second;
         }
@@ -573,32 +571,31 @@ void value_set_fit::get_value_set_rec(
 
       forall_objects(it, pointer_expr_set.read())
       {
-        objectt object=it->second;
+        offsett offset = it->second;
 
-        if(object.offset_is_zero() &&
-           expr.operands().size()==2)
+        if(offset_is_zero(offset) && expr.operands().size() == 2)
         {
           if(expr.op0().type().id()!=ID_pointer)
           {
             mp_integer i;
             if(to_integer(expr.op0(), i))
-              object.offset_is_set=false;
+              offset.reset();
             else
-              object.offset=(expr.id()==ID_plus)? i : -i;
+              *offset = (expr.id() == ID_plus) ? i : -i;
           }
           else
           {
             mp_integer i;
             if(to_integer(expr.op1(), i))
-              object.offset_is_set=false;
+              offset.reset();
             else
-              object.offset=(expr.id()==ID_plus)? i : -i;
+              *offset = (expr.id() == ID_plus) ? i : -i;
           }
         }
         else
-          object.offset_is_set=false;
+          offset.reset();
 
-        insert(dest, it->first, object);
+        insert(dest, it->first, offset);
       }
 
       return;
@@ -737,13 +734,12 @@ void value_set_fit::get_reference_set(
             t_it!=omt.write().end();
             t_it++)
         {
-          if(t_it->second.offset_is_set &&
-             it->second.offset_is_set)
+          if(t_it->second && it->second)
           {
-            t_it->second.offset += it->second.offset;
+            *t_it->second += *it->second;
           }
           else
-            t_it->second.offset_is_set=false;
+            t_it->second.reset();
         }
 
         forall_objects(it, omt.read())
@@ -826,13 +822,12 @@ void value_set_fit::get_reference_set_sharing_rec(
               t_it!=t2.write().end();
               t_it++)
           {
-            if(t_it->second.offset_is_set &&
-               it->second.offset_is_set)
+            if(t_it->second && it->second)
             {
-              t_it->second.offset += it->second.offset;
+              *t_it->second += *it->second;
             }
             else
-              t_it->second.offset_is_set=false;
+              t_it->second.reset();
           }
 
           forall_objects(it2, t2.read())
@@ -889,17 +884,16 @@ void value_set_fit::get_reference_set_sharing_rec(
            ns.follow(object.type())!=array_type)
           index_expr.make_typecast(array.type());
 
-        objectt o=a_it->second;
+        offsett o = a_it->second;
         mp_integer i;
 
         if(offset.is_zero())
         {
         }
-        else if(!to_integer(offset, i) &&
-                o.offset_is_zero())
-          o.offset=i;
+        else if(!to_integer(offset, i) && offset_is_zero(o))
+          *o = i;
         else
-          o.offset_is_set=false;
+          o.reset();
 
         insert(dest, index_expr, o);
       }
@@ -936,7 +930,7 @@ void value_set_fit::get_reference_set_sharing_rec(
       }
       else
       {
-        objectt o=it->second;
+        offsett o = it->second;
 
         exprt member_expr(ID_member, expr.type());
         member_expr.copy_to_operands(object);
@@ -1189,7 +1183,7 @@ void value_set_fit::do_free(
         else
         {
           // adjust
-          objectt o=o_it->second;
+          offsett o = o_it->second;
           exprt tmp(object);
           to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
           insert(new_object_map, tmp, o);
diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index c893724af60..4eee62763ac 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -52,28 +52,17 @@ class value_set_fit
 
   typedef irep_idt idt;
 
-  class objectt
+  /// Represents the offset into an object: either a unique integer offset,
+  /// or an unknown value, represented by `!offset`.
+  typedef optionalt<mp_integer> offsett;
+  bool offset_is_zero(const offsett &offset) const
   {
-  public:
-    objectt():offset_is_set(false)
-    {
-    }
-
-    explicit objectt(const mp_integer &_offset):
-      offset(_offset),
-      offset_is_set(true)
-    {
-    }
-
-    mp_integer offset;
-    bool offset_is_set;
-    bool offset_is_zero() const
-    { return offset_is_set && offset.is_zero(); }
-  };
+    return offset && offset->is_zero();
+  }
 
   class object_map_dt
   {
-    typedef std::map<object_numberingt::number_type, objectt> data_typet;
+    typedef std::map<object_numberingt::number_type, offsett> data_typet;
     data_typet data;
 
   public:
@@ -94,7 +83,7 @@ class value_set_fit
 
     size_t size() const { return data.size(); }
 
-    objectt &operator[](object_numberingt::number_type i)
+    offsett &operator[](object_numberingt::number_type i)
     {
       return data[i];
     }
@@ -127,55 +116,55 @@ class value_set_fit
 
   bool insert(object_mapt &dest, const exprt &src) const
   {
-    return insert(dest, object_numbering.number(src), objectt());
+    return insert(dest, object_numbering.number(src), offsett());
   }
 
   bool insert(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert(dest, object_numbering.number(src), objectt(offset));
+    return insert(dest, object_numbering.number(src), offsett(offset_value));
   }
 
   bool insert(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const
+    const offsett &offset) const
   {
     if(dest.read().find(n)==dest.read().end())
     {
       // new
-      dest.write()[n]=object;
+      dest.write()[n] = offset;
       return true;
     }
     else
     {
-      objectt &old=dest.write()[n];
+      offsett &old_offset = dest.write()[n];
 
-      if(old.offset_is_set && object.offset_is_set)
+      if(old_offset && offset)
       {
-        if(old.offset==object.offset)
+        if(*old_offset == *offset)
           return false;
         else
         {
-          old.offset_is_set=false;
+          old_offset.reset();
           return true;
         }
       }
-      else if(!old.offset_is_set)
+      else if(!old_offset)
         return false;
       else
       {
-        old.offset_is_set=false;
+        old_offset.reset();
         return true;
       }
     }
   }
 
-  bool insert(object_mapt &dest, const exprt &expr, const objectt &object) const
+  bool insert(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert(dest, object_numbering.number(expr), object);
+    return insert(dest, object_numbering.number(expr), offset);
   }
 
   struct entryt
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index ef994c4e798..13cf42abc3c 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -143,8 +143,8 @@ void value_set_fivrt::output(
       {
         result+=from_expr(ns, identifier, o)+", ";
 
-        if(o_it->second.offset_is_set)
-          result+=integer2string(o_it->second.offset)+"";
+        if(o_it->second)
+          result += integer2string(*o_it->second) + "";
         else
           result+='*';
 
@@ -301,13 +301,12 @@ void value_set_fivrt::flatten_rec(
                   t_it!=temp.write().end();
                   t_it++)
               {
-                if(t_it->second.offset_is_set &&
-                   it->second.offset_is_set)
+                if(t_it->second && it->second)
                 {
-                  t_it->second.offset += it->second.offset;
+                  *t_it->second += *it->second;
                 }
                 else
-                  t_it->second.offset_is_set=false;
+                  t_it->second.reset();
               }
 
               forall_objects(oit, temp.read())
@@ -325,7 +324,7 @@ void value_set_fivrt::flatten_rec(
   {
     Forall_objects(it, dest.write())
     {
-      it->second.offset_is_set=false;
+      it->second.reset();
       for(std::list<const object_map_dt::vrange_listt*>::const_iterator vit =
           add_ranges.begin();
           vit!=add_ranges.end();
@@ -355,8 +354,8 @@ exprt value_set_fivrt::to_expr(object_map_dt::const_iterator it) const
 
   od.object()=object;
 
-  if(it->second.offset_is_set)
-    od.offset()=from_integer(it->second.offset, index_type());
+  if(it->second)
+    od.offset() = from_integer(*it->second, index_type());
 
   od.type()=od.object().type();
 
@@ -436,13 +435,12 @@ void value_set_fivrt::get_value_set(
             t_it!=temp.write().end();
             t_it++)
         {
-          if(t_it->second.offset_is_set &&
-             it->second.offset_is_set)
+          if(t_it->second && it->second)
           {
-            t_it->second.offset += it->second.offset;
+            *t_it->second += *it->second;
           }
           else
-            t_it->second.offset_is_set=false;
+            t_it->second.reset();
 
           flat_map.write()[t_it->first]=t_it->second;
         }
@@ -690,32 +688,31 @@ void value_set_fivrt::get_value_set_rec(
 
       forall_objects(it, pointer_expr_set.read())
       {
-        objectt object=it->second;
+        offsett offset = it->second;
 
-        if(object.offset_is_zero() &&
-           expr.operands().size()==2)
+        if(offset_is_zero(offset) && expr.operands().size() == 2)
         {
           if(expr.op0().type().id()!=ID_pointer)
           {
             mp_integer i;
             if(to_integer(expr.op0(), i))
-              object.offset_is_set=false;
+              offset.reset();
             else
-              object.offset=(expr.id()==ID_plus)? i : -i;
+              *offset = (expr.id() == ID_plus) ? i : -i;
           }
           else
           {
             mp_integer i;
             if(to_integer(expr.op1(), i))
-              object.offset_is_set=false;
+              offset.reset();
             else
-              object.offset=(expr.id()==ID_plus)? i : -i;
+              *offset = (expr.id() == ID_plus) ? i : -i;
           }
         }
         else
-          object.offset_is_set=false;
+          offset.reset();
 
-        insert_from(dest, it->first, object);
+        insert_from(dest, it->first, offset);
       }
 
       return;
@@ -850,13 +847,12 @@ void value_set_fivrt::get_reference_set(
             t_it!=omt.write().end();
             t_it++)
         {
-          if(t_it->second.offset_is_set &&
-             it->second.offset_is_set)
+          if(t_it->second && it->second)
           {
-            t_it->second.offset += it->second.offset;
+            *t_it->second += *it->second;
           }
           else
-            t_it->second.offset_is_set=false;
+            t_it->second.reset();
         }
 
         forall_objects(it, omt.read())
@@ -939,13 +935,12 @@ void value_set_fivrt::get_reference_set_sharing_rec(
               t_it!=t2.write().end();
               t_it++)
           {
-            if(t_it->second.offset_is_set &&
-               it->second.offset_is_set)
+            if(t_it->second && it->second)
             {
-              t_it->second.offset += it->second.offset;
+              *t_it->second += *it->second;
             }
             else
-              t_it->second.offset_is_set=false;
+              t_it->second.reset();
           }
 
           forall_objects(it2, t2.read())
@@ -1002,17 +997,16 @@ void value_set_fivrt::get_reference_set_sharing_rec(
            ns.follow(object.type())!=array_type)
           index_expr.make_typecast(array.type());
 
-        objectt o=a_it->second;
+        offsett o = a_it->second;
         mp_integer i;
 
         if(offset.is_zero())
         {
         }
-        else if(!to_integer(offset, i) &&
-                o.offset_is_zero())
-          o.offset=i;
+        else if(!to_integer(offset, i) && offset_is_zero(o))
+          *o = i;
         else
-          o.offset_is_set=false;
+          o.reset();
 
         insert_from(dest, index_expr, o);
       }
@@ -1051,7 +1045,7 @@ void value_set_fivrt::get_reference_set_sharing_rec(
       }
       else
       {
-        objectt o=it->second;
+        offsett o = it->second;
 
         exprt member_expr(ID_member, expr.type());
         member_expr.copy_to_operands(object);
@@ -1300,7 +1294,7 @@ void value_set_fivrt::do_free(
         else
         {
           // adjust
-          objectt o=o_it->second;
+          offsett o = o_it->second;
           exprt tmp(object);
           to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
           insert_to(new_object_map, tmp, o);
@@ -1675,39 +1669,39 @@ void value_set_fivrt::apply_code(
 bool value_set_fivrt::insert_to(
   object_mapt &dest,
   object_numberingt::number_type n,
-  const objectt &object) const
+  const offsett &offset) const
 {
   object_map_dt &map=dest.write();
   if(map.find(n)==map.end())
   {
-//    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
+    //    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
     // new
-    map[n]=object;
+    map[n] = offset;
     map.set_valid_at(n, to_function, to_target_index);
     return true;
   }
   else
   {
-//    std::cout << "UPD " << n << '\n';
-    objectt &old=map[n];
+    //    std::cout << "UPD " << n << '\n';
+    offsett &old_offset = map[n];
 
-    bool res=map.set_valid_at(n, to_function, to_target_index);
+    bool res = map.set_valid_at(n, to_function, to_target_index);
 
-    if(old.offset_is_set && object.offset_is_set)
+    if(old_offset && offset)
     {
-      if(old.offset==object.offset)
+      if(*old_offset == *offset)
         return res;
       else
       {
-        old.offset_is_set=false;
+        old_offset.reset();
         return true;
       }
     }
-    else if(!old.offset_is_set)
+    else if(!old_offset)
       return res;
     else
     {
-      old.offset_is_set=false;
+      old_offset.reset();
       return true;
     }
   }
@@ -1716,39 +1710,39 @@ bool value_set_fivrt::insert_to(
 bool value_set_fivrt::insert_from(
   object_mapt &dest,
   object_numberingt::number_type n,
-  const objectt &object) const
+  const offsett &offset) const
 {
   object_map_dt &map=dest.write();
   if(map.find(n)==map.end())
   {
-//    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
+    //    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
     // new
-    map[n]=object;
+    map[n] = offset;
     map.set_valid_at(n, from_function, from_target_index);
     return true;
   }
   else
   {
-//    std::cout << "UPD " << n << '\n';
-    objectt &old=map[n];
+    //    std::cout << "UPD " << n << '\n';
+    offsett &old_offset = map[n];
 
-    bool res=map.set_valid_at(n, from_function, from_target_index);
+    bool res = map.set_valid_at(n, from_function, from_target_index);
 
-    if(old.offset_is_set && object.offset_is_set)
+    if(old_offset && offset)
     {
-      if(old.offset==object.offset)
+      if(*old_offset == *offset)
         return res;
       else
       {
-        old.offset_is_set=false;
+        old_offset.reset();
         return true;
       }
     }
-    else if(!old.offset_is_set)
+    else if(!old_offset)
       return res;
     else
     {
-      old.offset_is_set=false;
+      old_offset.reset();
       return true;
     }
   }
diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h
index cd72529936d..d66a728c65d 100644
--- a/src/pointer-analysis/value_set_fivr.h
+++ b/src/pointer-analysis/value_set_fivr.h
@@ -50,25 +50,13 @@ class value_set_fivrt
 
   typedef irep_idt idt;
 
-  class objectt
+  /// Represents the offset into an object: either a unique integer offset,
+  /// or an unknown value, represented by `!offset`.
+  typedef optionalt<mp_integer> offsett;
+  bool offset_is_zero(const offsett &offset) const
   {
-  public:
-    objectt() :
-      offset_is_set(false)
-    {
-    }
-
-    explicit objectt(const mp_integer &_offset):
-      offset(_offset),
-      offset_is_set(true)
-    {
-    }
-
-    mp_integer offset;
-    bool offset_is_set;
-    bool offset_is_zero() const
-    { return offset_is_set && offset.is_zero(); }
-  };
+    return offset && offset->is_zero();
+  }
 
   class object_map_dt
   {
@@ -76,7 +64,7 @@ class value_set_fivrt
     object_map_dt() {}
     static const object_map_dt blank;
 
-    typedef std::map<object_numberingt::number_type, objectt> objmapt;
+    typedef std::map<object_numberingt::number_type, offsett> objmapt;
     objmapt objmap;
 
     // NOLINTNEXTLINE(readability/identifiers)
@@ -96,19 +84,19 @@ class value_set_fivrt
     bool empty() const { return objmap.empty(); }
     void clear() { objmap.clear(); validity_ranges.clear(); }
 
-    objectt &operator[](object_numberingt::number_type k)
+    offsett &operator[](object_numberingt::number_type k)
     {
       return objmap[k];
     }
 
     // operator[] is the only way to insert something!
     std::pair<iterator, bool>
-    insert(const std::pair<object_numberingt::number_type, objectt> &)
+    insert(const std::pair<object_numberingt::number_type, offsett> &)
     {
       UNREACHABLE;
     }
     iterator
-    insert(iterator, const std::pair<object_numberingt::number_type, objectt> &)
+    insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
     {
       UNREACHABLE;
     }
@@ -160,28 +148,26 @@ class value_set_fivrt
 
   bool insert_to(object_mapt &dest, const exprt &src) const
   {
-    return insert_to(dest, object_numbering.number(src), objectt());
+    return insert_to(dest, object_numbering.number(src), offsett());
   }
 
   bool insert_to(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert_to(dest, object_numbering.number(src), objectt(offset));
+    return insert_to(dest, object_numbering.number(src), offsett(offset_value));
   }
 
   bool insert_to(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const;
+    const offsett &offset) const;
 
-  bool insert_to(
-    object_mapt &dest,
-    const exprt &expr,
-    const objectt &object) const
+  bool
+  insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert_to(dest, object_numbering.number(expr), object);
+    return insert_to(dest, object_numbering.number(expr), offset);
   }
 
   bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
@@ -191,28 +177,27 @@ class value_set_fivrt
 
   bool insert_from(object_mapt &dest, const exprt &src) const
   {
-    return insert_from(dest, object_numbering.number(src), objectt());
+    return insert_from(dest, object_numbering.number(src), offsett());
   }
 
   bool insert_from(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert_from(dest, object_numbering.number(src), objectt(offset));
+    return insert_from(
+      dest, object_numbering.number(src), offsett(offset_value));
   }
 
   bool insert_from(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const;
+    const offsett &offset) const;
 
-  bool insert_from(
-    object_mapt &dest,
-    const exprt &expr,
-    const objectt &object) const
+  bool
+  insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert_from(dest, object_numbering.number(expr), object);
+    return insert_from(dest, object_numbering.number(expr), offset);
   }
 
   struct entryt
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index 5ea32f8c7c8..57eef42a5bb 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -134,8 +134,8 @@ void value_set_fivrnst::output_entry(
     {
       result+=from_expr(ns, identifier, o)+", ";
 
-      if(o_it->second.offset_is_set)
-        result+=integer2string(o_it->second.offset)+"";
+      if(o_it->second)
+        result += integer2string(*o_it->second) + "";
       else
         result+='*';
 
@@ -211,8 +211,8 @@ exprt value_set_fivrnst::to_expr(object_map_dt::const_iterator it) const
 
   od.object()=object;
 
-  if(it->second.offset_is_set)
-    od.offset()=from_integer(it->second.offset, index_type());
+  if(it->second)
+    od.offset() = from_integer(*it->second, index_type());
 
   od.type()=od.object().type();
 
@@ -476,32 +476,31 @@ void value_set_fivrnst::get_value_set_rec(
 
       forall_objects(it, pointer_expr_set.read())
       {
-        objectt object=it->second;
+        offsett offset = it->second;
 
-        if(object.offset_is_zero() &&
-           expr.operands().size()==2)
+        if(offset_is_zero(offset) && expr.operands().size() == 2)
         {
           if(expr.op0().type().id()!=ID_pointer)
           {
             mp_integer i;
             if(to_integer(expr.op0(), i))
-              object.offset_is_set=false;
+              offset.reset();
             else
-              object.offset=(expr.id()==ID_plus)? i : -i;
+              *offset = (expr.id() == ID_plus) ? i : -i;
           }
           else
           {
             mp_integer i;
             if(to_integer(expr.op1(), i))
-              object.offset_is_set=false;
+              offset.reset();
             else
-              object.offset=(expr.id()==ID_plus)? i : -i;
+              *offset = (expr.id() == ID_plus) ? i : -i;
           }
         }
         else
-          object.offset_is_set=false;
+          offset.reset();
 
-        insert_from(dest, it->first, object);
+        insert_from(dest, it->first, offset);
       }
 
       return;
@@ -689,17 +688,16 @@ void value_set_fivrnst::get_reference_set_rec(
         if(ns.follow(object.type())!=array_type)
           index_expr.make_typecast(array.type());
 
-        objectt o=a_it->second;
+        offsett o = a_it->second;
         mp_integer i;
 
         if(offset.is_zero())
         {
         }
-        else if(!to_integer(offset, i) &&
-                o.offset_is_zero())
-          o.offset=i;
+        else if(!to_integer(offset, i) && offset_is_zero(o))
+          *o = i;
         else
-          o.offset_is_set=false;
+          o.reset();
 
         insert_from(dest, index_expr, o);
       }
@@ -738,7 +736,7 @@ void value_set_fivrnst::get_reference_set_rec(
       }
       else
       {
-        objectt o=it->second;
+        offsett o = it->second;
 
         exprt member_expr(ID_member, expr.type());
         member_expr.copy_to_operands(object);
@@ -983,7 +981,7 @@ void value_set_fivrnst::do_free(
         else
         {
           // adjust
-          objectt o=o_it->second;
+          offsett o = o_it->second;
           exprt tmp(object);
           to_dynamic_object_expr(tmp).valid()=exprt(ID_unknown);
           insert_to(new_object_map, tmp, o);
@@ -1331,39 +1329,39 @@ void value_set_fivrnst::apply_code(
 bool value_set_fivrnst::insert_to(
   object_mapt &dest,
   object_numberingt::number_type n,
-  const objectt &object) const
+  const offsett &offset) const
 {
   object_map_dt &map = dest.write();
   if(map.find(n)==map.end())
   {
-//    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
+    //    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
     // new
-    map[n]=object;
+    map[n] = offset;
     map.set_valid_at(n, to_function, to_target_index);
     return true;
   }
   else
   {
-//    std::cout << "UPD " << n << '\n';
-    objectt &old=map[n];
+    //    std::cout << "UPD " << n << '\n';
+    offsett &old_offset = map[n];
 
     bool res = map.set_valid_at(n, to_function, to_target_index);
 
-    if(old.offset_is_set && object.offset_is_set)
+    if(old_offset && offset)
     {
-      if(old.offset==object.offset)
+      if(*old_offset == *offset)
         return res;
       else
       {
-        old.offset_is_set=false;
+        old_offset.reset();
         return true;
       }
     }
-    else if(!old.offset_is_set)
+    else if(!old_offset)
       return res;
     else
     {
-      old.offset_is_set=false;
+      old_offset.reset();
       return true;
     }
   }
@@ -1372,39 +1370,39 @@ bool value_set_fivrnst::insert_to(
 bool value_set_fivrnst::insert_from(
   object_mapt &dest,
   object_numberingt::number_type n,
-  const objectt &object) const
+  const offsett &offset) const
 {
   object_map_dt &map = dest.write();
   if(map.find(n)==map.end())
   {
-//    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
+    //    std::cout << "NEW(" << n << "): " << object_numbering[n] << '\n';
     // new
-    map[n]=object;
+    map[n] = offset;
     map.set_valid_at(n, from_function, from_target_index);
     return true;
   }
   else
   {
-//    std::cout << "UPD " << n << '\n';
-    objectt &old=map[n];
+    //    std::cout << "UPD " << n << '\n';
+    offsett &old_offset = map[n];
 
     bool res = map.set_valid_at(n, from_function, from_target_index);
 
-    if(old.offset_is_set && object.offset_is_set)
+    if(old_offset && offset)
     {
-      if(old.offset==object.offset)
+      if(*old_offset == *offset)
         return res;
       else
       {
-        old.offset_is_set=false;
+        old_offset.reset();
         return true;
       }
     }
-    else if(!old.offset_is_set)
+    else if(!old_offset)
       return res;
     else
     {
-      old.offset_is_set=false;
+      old_offset.reset();
       return true;
     }
   }
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
index ae77e54ef31..c2f183c3ea3 100644
--- a/src/pointer-analysis/value_set_fivrns.h
+++ b/src/pointer-analysis/value_set_fivrns.h
@@ -51,25 +51,13 @@ class value_set_fivrnst
 
   typedef irep_idt idt;
 
-  class objectt
+  /// Represents the offset into an object: either a unique integer offset,
+  /// or an unknown value, represented by `!offset`.
+  typedef optionalt<mp_integer> offsett;
+  bool offset_is_zero(offsett offset) const
   {
-  public:
-    objectt() :
-      offset_is_set(false)
-    {
-    }
-
-    explicit objectt(const mp_integer &_offset):
-      offset(_offset),
-      offset_is_set(true)
-    {
-    }
-
-    mp_integer offset;
-    bool offset_is_set;
-    bool offset_is_zero() const
-    { return offset_is_set && offset.is_zero(); }
-  };
+    return offset && offset->is_zero();
+  }
 
   class object_map_dt
   {
@@ -77,7 +65,7 @@ class value_set_fivrnst
     object_map_dt() {}
     static const object_map_dt blank;
 
-    typedef std::map<object_numberingt::number_type, objectt> objmapt;
+    typedef std::map<object_numberingt::number_type, offsett> objmapt;
     objmapt objmap;
 
     // NOLINTNEXTLINE(readability/identifiers)
@@ -97,19 +85,19 @@ class value_set_fivrnst
     bool empty() const { return objmap.empty(); }
     void clear() { objmap.clear(); validity_ranges.clear(); }
 
-    objectt &operator[](object_numberingt::number_type k)
+    offsett &operator[](object_numberingt::number_type k)
     {
       return objmap[k];
     }
 
     // operator[] is the only way to insert something!
     std::pair<iterator, bool>
-    insert(const std::pair<object_numberingt::number_type, objectt> &)
+    insert(const std::pair<object_numberingt::number_type, offsett> &)
     {
       UNREACHABLE;
     }
     iterator
-    insert(iterator, const std::pair<object_numberingt::number_type, objectt> &)
+    insert(iterator, const std::pair<object_numberingt::number_type, offsett> &)
     {
       UNREACHABLE;
     }
@@ -160,28 +148,26 @@ class value_set_fivrnst
 
   bool insert_to(object_mapt &dest, const exprt &src) const
   {
-    return insert_to(dest, object_numbering.number(src), objectt());
+    return insert_to(dest, object_numbering.number(src), offsett());
   }
 
   bool insert_to(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert_to(dest, object_numbering.number(src), objectt(offset));
+    return insert_to(dest, object_numbering.number(src), offsett(offset_value));
   }
 
   bool insert_to(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const;
+    const offsett &offset) const;
 
-  bool insert_to(
-    object_mapt &dest,
-    const exprt &expr,
-    const objectt &object) const
+  bool
+  insert_to(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert_to(dest, object_numbering.number(expr), object);
+    return insert_to(dest, object_numbering.number(expr), offset);
   }
 
   bool insert_from(object_mapt &dest, object_map_dt::const_iterator it) const
@@ -191,28 +177,27 @@ class value_set_fivrnst
 
   bool insert_from(object_mapt &dest, const exprt &src) const
   {
-    return insert_from(dest, object_numbering.number(src), objectt());
+    return insert_from(dest, object_numbering.number(src), offsett());
   }
 
   bool insert_from(
     object_mapt &dest,
     const exprt &src,
-    const mp_integer &offset) const
+    const mp_integer &offset_value) const
   {
-    return insert_from(dest, object_numbering.number(src), objectt(offset));
+    return insert_from(
+      dest, object_numbering.number(src), offsett(offset_value));
   }
 
   bool insert_from(
     object_mapt &dest,
     object_numberingt::number_type n,
-    const objectt &object) const;
+    const offsett &offset) const;
 
-  bool insert_from(
-    object_mapt &dest,
-    const exprt &expr,
-    const objectt &object) const
+  bool
+  insert_from(object_mapt &dest, const exprt &expr, const offsett &offset) const
   {
-    return insert_from(dest, object_numbering.number(expr), object);
+    return insert_from(dest, object_numbering.number(expr), offset);
   }
 
   struct entryt