diff --git a/src/pointer-analysis/value_set_fi.h b/src/pointer-analysis/value_set_fi.h
index 77d4c1f54ec..c893724af60 100644
--- a/src/pointer-analysis/value_set_fi.h
+++ b/src/pointer-analysis/value_set_fi.h
@@ -73,7 +73,7 @@ class value_set_fit
 
   class object_map_dt
   {
-    typedef std::map<unsigned, objectt> data_typet;
+    typedef std::map<object_numberingt::number_type, objectt> data_typet;
     data_typet data;
 
   public:
@@ -94,7 +94,10 @@ class value_set_fit
 
     size_t size() const { return data.size(); }
 
-    objectt &operator[](unsigned i) { return data[i]; }
+    objectt &operator[](object_numberingt::number_type i)
+    {
+      return data[i];
+    }
 
     template <typename It>
     void insert(It b, It e) { data.insert(b, e); }
@@ -135,7 +138,10 @@ class value_set_fit
     return insert(dest, object_numbering.number(src), objectt(offset));
   }
 
-  bool insert(object_mapt &dest, unsigned n, const objectt &object) const
+  bool insert(
+    object_mapt &dest,
+    object_numberingt::number_type n,
+    const objectt &object) const
   {
     if(dest.read().find(n)==dest.read().end())
     {
diff --git a/src/pointer-analysis/value_set_fivr.cpp b/src/pointer-analysis/value_set_fivr.cpp
index 8ab9ff2c117..ef994c4e798 100644
--- a/src/pointer-analysis/value_set_fivr.cpp
+++ b/src/pointer-analysis/value_set_fivr.cpp
@@ -1674,7 +1674,7 @@ void value_set_fivrt::apply_code(
 
 bool value_set_fivrt::insert_to(
   object_mapt &dest,
-  unsigned n,
+  object_numberingt::number_type n,
   const objectt &object) const
 {
   object_map_dt &map=dest.write();
@@ -1715,7 +1715,7 @@ bool value_set_fivrt::insert_to(
 
 bool value_set_fivrt::insert_from(
   object_mapt &dest,
-  unsigned n,
+  object_numberingt::number_type n,
   const objectt &object) const
 {
   object_map_dt &map=dest.write();
diff --git a/src/pointer-analysis/value_set_fivr.h b/src/pointer-analysis/value_set_fivr.h
index 322b2ea2fc9..cd72529936d 100644
--- a/src/pointer-analysis/value_set_fivr.h
+++ b/src/pointer-analysis/value_set_fivr.h
@@ -76,7 +76,7 @@ class value_set_fivrt
     object_map_dt() {}
     static const object_map_dt blank;
 
-    typedef std::map<unsigned, objectt> objmapt;
+    typedef std::map<object_numberingt::number_type, objectt> objmapt;
     objmapt objmap;
 
     // NOLINTNEXTLINE(readability/identifiers)
@@ -84,7 +84,10 @@ class value_set_fivrt
     // NOLINTNEXTLINE(readability/identifiers)
     typedef objmapt::iterator iterator;
 
-    const_iterator find(unsigned k) { return objmap.find(k); }
+    const_iterator find(object_numberingt::number_type k)
+    {
+      return objmap.find(k);
+    }
     iterator begin() { return objmap.begin(); }
     const_iterator begin() const { return objmap.begin(); }
     iterator end() { return objmap.end(); }
@@ -93,17 +96,19 @@ class value_set_fivrt
     bool empty() const { return objmap.empty(); }
     void clear() { objmap.clear(); validity_ranges.clear(); }
 
-    objectt &operator[](unsigned k)
+    objectt &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<unsigned, objectt>&)
+    std::pair<iterator, bool>
+    insert(const std::pair<object_numberingt::number_type, objectt> &)
     {
       UNREACHABLE;
     }
-    iterator insert(iterator, const std::pair<unsigned, objectt>&)
+    iterator
+    insert(iterator, const std::pair<object_numberingt::number_type, objectt> &)
     {
       UNREACHABLE;
     }
@@ -166,7 +171,10 @@ class value_set_fivrt
     return insert_to(dest, object_numbering.number(src), objectt(offset));
   }
 
-  bool insert_to(object_mapt &dest, unsigned n, const objectt &object) const;
+  bool insert_to(
+    object_mapt &dest,
+    object_numberingt::number_type n,
+    const objectt &object) const;
 
   bool insert_to(
     object_mapt &dest,
@@ -194,7 +202,10 @@ class value_set_fivrt
     return insert_from(dest, object_numbering.number(src), objectt(offset));
   }
 
-  bool insert_from(object_mapt &dest, unsigned n, const objectt &object) const;
+  bool insert_from(
+    object_mapt &dest,
+    object_numberingt::number_type n,
+    const objectt &object) const;
 
   bool insert_from(
     object_mapt &dest,
diff --git a/src/pointer-analysis/value_set_fivrns.cpp b/src/pointer-analysis/value_set_fivrns.cpp
index a405e2d2242..5ea32f8c7c8 100644
--- a/src/pointer-analysis/value_set_fivrns.cpp
+++ b/src/pointer-analysis/value_set_fivrns.cpp
@@ -1330,7 +1330,7 @@ void value_set_fivrnst::apply_code(
 
 bool value_set_fivrnst::insert_to(
   object_mapt &dest,
-  unsigned n,
+  object_numberingt::number_type n,
   const objectt &object) const
 {
   object_map_dt &map = dest.write();
@@ -1371,7 +1371,7 @@ bool value_set_fivrnst::insert_to(
 
 bool value_set_fivrnst::insert_from(
   object_mapt &dest,
-  unsigned n,
+  object_numberingt::number_type n,
   const objectt &object) const
 {
   object_map_dt &map = dest.write();
diff --git a/src/pointer-analysis/value_set_fivrns.h b/src/pointer-analysis/value_set_fivrns.h
index d3b452c0408..ae77e54ef31 100644
--- a/src/pointer-analysis/value_set_fivrns.h
+++ b/src/pointer-analysis/value_set_fivrns.h
@@ -77,7 +77,7 @@ class value_set_fivrnst
     object_map_dt() {}
     static const object_map_dt blank;
 
-    typedef std::map<unsigned, objectt> objmapt;
+    typedef std::map<object_numberingt::number_type, objectt> objmapt;
     objmapt objmap;
 
     // NOLINTNEXTLINE(readability/identifiers)
@@ -85,7 +85,10 @@ class value_set_fivrnst
     // NOLINTNEXTLINE(readability/identifiers)
     typedef objmapt::iterator iterator;
 
-    const_iterator find(unsigned k) { return objmap.find(k); }
+    const_iterator find(object_numberingt::number_type k)
+    {
+      return objmap.find(k);
+    }
     iterator begin() { return objmap.begin(); }
     const_iterator begin() const { return objmap.begin(); }
     iterator end() { return objmap.end(); }
@@ -94,17 +97,19 @@ class value_set_fivrnst
     bool empty() const { return objmap.empty(); }
     void clear() { objmap.clear(); validity_ranges.clear(); }
 
-    objectt &operator[](unsigned k)
+    objectt &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<unsigned, objectt>&)
+    std::pair<iterator, bool>
+    insert(const std::pair<object_numberingt::number_type, objectt> &)
     {
       UNREACHABLE;
     }
-    iterator insert(iterator, const std::pair<unsigned, objectt>&)
+    iterator
+    insert(iterator, const std::pair<object_numberingt::number_type, objectt> &)
     {
       UNREACHABLE;
     }
@@ -166,7 +171,10 @@ class value_set_fivrnst
     return insert_to(dest, object_numbering.number(src), objectt(offset));
   }
 
-  bool insert_to(object_mapt &dest, unsigned n, const objectt &object) const;
+  bool insert_to(
+    object_mapt &dest,
+    object_numberingt::number_type n,
+    const objectt &object) const;
 
   bool insert_to(
     object_mapt &dest,
@@ -194,7 +202,10 @@ class value_set_fivrnst
     return insert_from(dest, object_numbering.number(src), objectt(offset));
   }
 
-  bool insert_from(object_mapt &dest, unsigned n, const objectt &object) const;
+  bool insert_from(
+    object_mapt &dest,
+    object_numberingt::number_type n,
+    const objectt &object) const;
 
   bool insert_from(
     object_mapt &dest,