diff --git a/src/analyses/dependence_graph.cpp b/src/analyses/dependence_graph.cpp
index cb2e30eb946..86ce3cc8f5b 100644
--- a/src/analyses/dependence_graph.cpp
+++ b/src/analyses/dependence_graph.cpp
@@ -125,22 +125,28 @@ void dep_graph_domaint::control_dependencies(
 }
 
 static bool may_be_def_use_pair(
-  const mp_integer &w_start,
-  const mp_integer &w_end,
-  const mp_integer &r_start,
-  const mp_integer &r_end)
+  const range_spect &w_start,
+  const range_spect &w_end,
+  const range_spect &r_start,
+  const range_spect &r_end)
 {
-  assert(w_start>=0);
-  assert(r_start>=0);
+  PRECONDITION(w_start >= range_spect{0});
+  PRECONDITION(r_start >= range_spect{0});
 
-  if((w_end!=-1 && w_end <= r_start) || // we < rs
-     (r_end!=-1 && w_start >= r_end)) // re < we
+  if(
+    (!w_end.is_unknown() && w_end <= r_start) || // we < rs
+    (!r_end.is_unknown() && w_start >= r_end))   // re < we
+  {
     return false;
+  }
   else if(w_start >= r_start) // rs <= ws < we,re
     return true;
-  else if(w_end==-1 ||
-          (r_end!=-1 && w_end > r_start)) // ws <= rs < we,re
+  else if(
+    w_end.is_unknown() ||
+    (!r_end.is_unknown() && w_end > r_start)) // ws <= rs < we,re
+  {
     return true;
+  }
   else
     return false;
 }
diff --git a/src/analyses/goto_rw.cpp b/src/analyses/goto_rw.cpp
index b5da8044e44..0116f8376fe 100644
--- a/src/analyses/goto_rw.cpp
+++ b/src/analyses/goto_rw.cpp
@@ -102,11 +102,12 @@ void rw_range_sett::get_objects_complex_imag(
     pointer_offset_bits(to_complex_type(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 sub_size = range_spect::to_range_spect(*subtype_bits);
+  CHECK_RETURN(sub_size > range_spect{0});
 
-  range_spect offset=
-    (range_start==-1 || expr.id()==ID_complex_real) ? 0 : sub_size;
+  range_spect offset =
+    (range_start.is_unknown() || expr.id() == ID_complex_real) ? range_spect{0}
+                                                               : sub_size;
 
   get_objects_rec(mode, op, range_start + offset, size);
 }
@@ -153,10 +154,10 @@ void rw_range_sett::get_objects_byte_extract(
 
   auto index = numeric_cast<mp_integer>(simp_offset);
   if(
-    range_start == -1 || !index.has_value() ||
+    range_start.is_unknown() || !index.has_value() ||
     !object_size_bits_opt.has_value())
   {
-    get_objects_rec(mode, be.op(), -1, size);
+    get_objects_rec(mode, be.op(), range_spect::unknown(), size);
   }
   else
   {
@@ -170,12 +171,15 @@ void rw_range_sett::get_objects_byte_extract(
       ns);
     range_spect offset = range_start;
     if(*index > 0)
-      offset += map.map_bit(numeric_cast_v<std::size_t>(*index));
+    {
+      offset += range_spect::to_range_spect(
+        map.map_bit(numeric_cast_v<std::size_t>(*index)));
+    }
     else
     {
       // outside the bounds of immediate byte-extract operand, might still be in
       // bounds of a parent object
-      offset += to_range_spect(*index);
+      offset += range_spect::to_range_spect(*index);
     }
     get_objects_rec(mode, be.op(), offset, size);
   }
@@ -191,17 +195,23 @@ void rw_range_sett::get_objects_shift(
 
   auto op_bits = pointer_offset_bits(shift.op().type(), ns);
 
-  range_spect src_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
+  range_spect src_size = op_bits.has_value()
+                           ? range_spect::to_range_spect(*op_bits)
+                           : range_spect::unknown();
 
   const auto dist = numeric_cast<mp_integer>(simp_distance);
-  if(range_start == -1 || size == -1 || src_size == -1 || !dist.has_value())
+  if(
+    range_start.is_unknown() || size.is_unknown() || src_size.is_unknown() ||
+    !dist.has_value())
   {
-    get_objects_rec(mode, shift.op(), -1, -1);
-    get_objects_rec(mode, shift.distance(), -1, -1);
+    get_objects_rec(
+      mode, shift.op(), range_spect::unknown(), range_spect::unknown());
+    get_objects_rec(
+      mode, shift.distance(), range_spect::unknown(), range_spect::unknown());
   }
   else
   {
-    const range_spect dist_r = to_range_spect(*dist);
+    const range_spect dist_r = range_spect::to_range_spect(*dist);
 
     // not sure whether to worry about
     // config.ansi_c.endianness==configt::ansi_ct::IS_LITTLE_ENDIAN
@@ -214,10 +224,10 @@ void rw_range_sett::get_objects_shift(
 
       range_spect sh_size=std::min(size, src_size-sh_range_start);
 
-      if(sh_range_start>=0 && sh_range_start<src_size)
+      if(sh_range_start >= range_spect{0} && sh_range_start < src_size)
         get_objects_rec(mode, shift.op(), sh_range_start, sh_size);
     }
-    if(src_size - dist_r >= 0)
+    if(src_size >= dist_r)
     {
       range_spect sh_size=std::min(size, src_size-dist_r);
 
@@ -234,7 +244,9 @@ void rw_range_sett::get_objects_member(
 {
   const typet &type = expr.struct_op().type();
 
-  if(type.id() == ID_union || type.id() == ID_union_tag || range_start == -1)
+  if(
+    type.id() == ID_union || type.id() == ID_union_tag ||
+    range_start.is_unknown())
   {
     get_objects_rec(mode, expr.struct_op(), range_start, size);
     return;
@@ -245,15 +257,13 @@ void rw_range_sett::get_objects_member(
   auto offset_bits =
     member_offset_bits(struct_type, expr.get_component_name(), ns);
 
-  range_spect offset;
+  range_spect offset = range_spect::unknown();
 
   if(offset_bits.has_value())
   {
-    offset = to_range_spect(*offset_bits);
+    offset = range_spect::to_range_spect(*offset_bits);
     offset += range_start;
   }
-  else
-    offset = -1;
 
   get_objects_rec(mode, expr.struct_op(), offset, size);
 }
@@ -267,7 +277,7 @@ void rw_range_sett::get_objects_index(
   if(expr.array().id() == ID_null_object)
     return;
 
-  range_spect sub_size=0;
+  range_spect sub_size = range_spect::unknown();
   const typet &type = expr.array().type();
 
   if(type.id()==ID_vector)
@@ -276,7 +286,8 @@ void rw_range_sett::get_objects_index(
 
     auto subtype_bits = pointer_offset_bits(vector_type.element_type(), ns);
 
-    sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
+    if(subtype_bits.has_value())
+      sub_size = range_spect::to_range_spect(*subtype_bits);
   }
   else if(type.id()==ID_array)
   {
@@ -284,7 +295,8 @@ void rw_range_sett::get_objects_index(
 
     auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
 
-    sub_size = subtype_bits.has_value() ? to_range_spect(*subtype_bits) : -1;
+    if(subtype_bits.has_value())
+      sub_size = range_spect::to_range_spect(*subtype_bits);
   }
   else
     return;
@@ -295,14 +307,16 @@ void rw_range_sett::get_objects_index(
   if(!index.has_value())
     get_objects_rec(get_modet::READ, expr.index());
 
-  if(range_start == -1 || sub_size == -1 || !index.has_value())
-    get_objects_rec(mode, expr.array(), -1, size);
+  if(range_start.is_unknown() || sub_size.is_unknown() || !index.has_value())
+    get_objects_rec(mode, expr.array(), range_spect::unknown(), size);
   else
+  {
     get_objects_rec(
       mode,
       expr.array(),
-      range_start + to_range_spect(*index * sub_size),
+      range_start + range_spect::to_range_spect(*index) * sub_size,
       size);
+  }
 }
 
 void rw_range_sett::get_objects_array(
@@ -315,28 +329,30 @@ void rw_range_sett::get_objects_array(
 
   auto subtype_bits = pointer_offset_bits(array_type.element_type(), ns);
 
-  range_spect sub_size;
-
-  if(subtype_bits.has_value())
-    sub_size = to_range_spect(*subtype_bits);
-  else
+  if(!subtype_bits.has_value())
   {
     forall_operands(it, expr)
-      get_objects_rec(mode, *it, 0, -1);
+      get_objects_rec(mode, *it, range_spect{0}, range_spect::unknown());
 
     return;
   }
 
-  range_spect offset=0;
-  range_spect full_r_s=range_start==-1 ? 0 : range_start;
-  range_spect full_r_e=
-    size==-1 ? sub_size*expr.operands().size() : full_r_s+size;
+  range_spect sub_size = range_spect::to_range_spect(*subtype_bits);
+
+  range_spect offset{0};
+  range_spect full_r_s =
+    range_start.is_unknown() ? range_spect{0} : range_start;
+  range_spect full_r_e =
+    size.is_unknown()
+      ? sub_size * range_spect::to_range_spect(expr.operands().size())
+      : full_r_s + size;
 
   forall_operands(it, expr)
   {
     if(full_r_s<=offset+sub_size && full_r_e>offset)
     {
-      range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
+      range_spect cur_r_s =
+        full_r_s <= offset ? range_spect{0} : full_r_s - offset;
       range_spect cur_r_e=
         full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
 
@@ -358,39 +374,47 @@ void rw_range_sett::get_objects_struct(
 
   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 full_size = struct_bits.has_value()
+                            ? range_spect::to_range_spect(*struct_bits)
+                            : range_spect::unknown();
 
-  range_spect offset=0;
-  range_spect full_r_s=range_start==-1 ? 0 : range_start;
-  range_spect full_r_e=size==-1 || full_size==-1 ? -1 : full_r_s+size;
+  range_spect offset = range_spect{0};
+  range_spect full_r_s =
+    range_start.is_unknown() ? range_spect{0} : range_start;
+  range_spect full_r_e = size.is_unknown() || full_size.is_unknown()
+                           ? range_spect::unknown()
+                           : full_r_s + size;
 
   forall_operands(it, expr)
   {
     auto it_bits = pointer_offset_bits(it->type(), ns);
 
-    range_spect sub_size = it_bits.has_value() ? to_range_spect(*it_bits) : -1;
+    range_spect sub_size = it_bits.has_value()
+                             ? range_spect::to_range_spect(*it_bits)
+                             : range_spect::unknown();
 
-    if(offset==-1)
+    if(offset.is_unknown())
     {
-      get_objects_rec(mode, *it, 0, sub_size);
+      get_objects_rec(mode, *it, range_spect{0}, sub_size);
     }
-    else if(sub_size==-1)
+    else if(sub_size.is_unknown())
     {
-      if(full_r_e==-1 || full_r_e>offset)
+      if(full_r_e.is_unknown() || full_r_e > offset)
       {
-        range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
+        range_spect cur_r_s =
+          full_r_s <= offset ? range_spect{0} : full_r_s - offset;
 
-        get_objects_rec(mode, *it, cur_r_s, -1);
+        get_objects_rec(mode, *it, cur_r_s, range_spect::unknown());
       }
 
-      offset=-1;
+      offset = range_spect::unknown();
     }
-    else if(full_r_e==-1)
+    else if(full_r_e.is_unknown())
     {
       if(full_r_s<=offset+sub_size)
       {
-        range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
+        range_spect cur_r_s =
+          full_r_s <= offset ? range_spect{0} : full_r_s - offset;
 
         get_objects_rec(mode, *it, cur_r_s, sub_size-cur_r_s);
       }
@@ -399,7 +423,8 @@ void rw_range_sett::get_objects_struct(
     }
     else if(full_r_s<=offset+sub_size && full_r_e>offset)
     {
-      range_spect cur_r_s=full_r_s<=offset ? 0 : full_r_s-offset;
+      range_spect cur_r_s =
+        full_r_s <= offset ? range_spect{0} : full_r_s - offset;
       range_spect cur_r_e=
         full_r_e>offset+sub_size ? sub_size : full_r_e-offset;
 
@@ -420,11 +445,13 @@ void rw_range_sett::get_objects_typecast(
 
   auto op_bits = pointer_offset_bits(op.type(), ns);
 
-  range_spect new_size = op_bits.has_value() ? to_range_spect(*op_bits) : -1;
+  range_spect new_size = op_bits.has_value()
+                           ? range_spect::to_range_spect(*op_bits)
+                           : range_spect::unknown();
 
-  if(range_start==-1)
-    new_size=-1;
-  else if(new_size!=-1)
+  if(range_start.is_unknown())
+    new_size = range_spect::unknown();
+  else if(!new_size.is_unknown())
   {
     if(new_size<=range_start)
       return;
@@ -560,26 +587,31 @@ void rw_range_sett::get_objects_rec(
 
     auto symbol_bits = pointer_offset_bits(symbol.type(), ns);
 
-    range_spect full_size =
-      symbol_bits.has_value() ? to_range_spect(*symbol_bits) : -1;
+    range_spect full_size = symbol_bits.has_value()
+                              ? range_spect::to_range_spect(*symbol_bits)
+                              : range_spect::unknown();
 
-    if(full_size==0 ||
-       (full_size>0 && range_start>=full_size))
+    if(
+      !full_size.is_unknown() &&
+      (full_size == range_spect{0} ||
+       (full_size > range_spect{0} && !range_start.is_unknown() &&
+        range_start >= full_size)))
     {
       // nothing to do, these are effectively constants (like function
       // symbols or structs with no members)
       // OR: invalid memory accesses
     }
-    else if(range_start>=0)
+    else if(!range_start.is_unknown() && range_start >= range_spect{0})
     {
-      range_spect range_end=size==-1 ? -1 : range_start+size;
-      if(size!=-1 && full_size!=-1)
+      range_spect range_end =
+        size.is_unknown() ? range_spect::unknown() : range_start + size;
+      if(!size.is_unknown() && !full_size.is_unknown())
         range_end=std::min(range_end, full_size);
 
       add(mode, identifier, range_start, range_end);
     }
     else
-      add(mode, identifier, 0, -1);
+      add(mode, identifier, range_spect{0}, range_spect::unknown());
   }
   else if(mode==get_modet::READ && expr.id()==ID_address_of)
     get_objects_address_of(to_address_of_expr(expr).object());
@@ -609,9 +641,11 @@ void rw_range_sett::get_objects_rec(get_modet mode, const exprt &expr)
 {
   auto expr_bits = pointer_offset_bits(expr.type(), ns);
 
-  range_spect size = expr_bits.has_value() ? to_range_spect(*expr_bits) : -1;
+  range_spect size = expr_bits.has_value()
+                       ? range_spect::to_range_spect(*expr_bits)
+                       : range_spect::unknown();
 
-  get_objects_rec(mode, expr, 0, size);
+  get_objects_rec(mode, expr, range_spect{0}, size);
 }
 
 void rw_range_sett::get_objects_rec(const typet &type)
@@ -633,7 +667,8 @@ void rw_range_sett::get_array_objects(
 {
   object_descriptor_exprt ode;
   ode.build(dereference_exprt{skip_typecast(pointer)}, ns);
-  get_objects_rec(mode, ode.root_object(), -1, -1);
+  get_objects_rec(
+    mode, ode.root_object(), range_spect::unknown(), range_spect::unknown());
 }
 
 void rw_range_set_value_sett::get_objects_dereference(
@@ -653,22 +688,20 @@ void rw_range_set_value_sett::get_objects_dereference(
 
   auto type_bits = pointer_offset_bits(object.type(), ns);
 
-  range_spect new_size;
+  range_spect new_size = range_spect::unknown();
 
   if(type_bits.has_value())
   {
-    new_size = to_range_spect(*type_bits);
+    new_size = range_spect::to_range_spect(*type_bits);
 
-    if(range_start == -1 || new_size <= range_start)
-      new_size = -1;
+    if(range_start.is_unknown() || new_size <= range_start)
+      new_size = range_spect::unknown();
     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/goto_rw.h b/src/analyses/goto_rw.h
index d1093695508..4d7ad1d0370 100644
--- a/src/analyses/goto_rw.h
+++ b/src/analyses/goto_rw.h
@@ -54,15 +54,110 @@ class range_domain_baset
   virtual void output(const namespacet &ns, std::ostream &out) const=0;
 };
 
-typedef int range_spect;
+/// Data type to describe upper and lower bounds of the range of bits that a
+/// read or write access may affect. Each of the bounds may be not known or not
+/// constant, which is expressed using \ref range_spect::unknown.
+class range_spect
+{
+public:
+  using value_type = int;
+
+  explicit range_spect(value_type v) : v(v)
+  {
+  }
+
+  static range_spect unknown()
+  {
+    return range_spect{-1};
+  }
+
+  bool is_unknown() const
+  {
+    return *this == unknown();
+  }
+
+  static range_spect to_range_spect(const mp_integer &size)
+  {
+    PRECONDITION(size.is_long());
+    mp_integer::llong_t ll = size.to_long();
+    CHECK_RETURN(ll <= std::numeric_limits<range_spect::value_type>::max());
+    CHECK_RETURN(ll >= std::numeric_limits<range_spect::value_type>::min());
+    return range_spect{(value_type)ll};
+  }
+
+  bool operator<(const range_spect &other) const
+  {
+    PRECONDITION(!is_unknown() && !other.is_unknown());
+    return v < other.v;
+  }
+
+  bool operator<=(const range_spect &other) const
+  {
+    PRECONDITION(!is_unknown() && !other.is_unknown());
+    return v <= other.v;
+  }
+
+  bool operator>(const range_spect &other) const
+  {
+    PRECONDITION(!is_unknown() && !other.is_unknown());
+    return v > other.v;
+  }
+
+  bool operator>=(const range_spect &other) const
+  {
+    PRECONDITION(!is_unknown() && !other.is_unknown());
+    return v >= other.v;
+  }
+
+  bool operator==(const range_spect &other) const
+  {
+    return v == other.v;
+  }
+
+  range_spect operator+(const range_spect &other) const
+  {
+    if(is_unknown() || other.is_unknown())
+      return range_spect::unknown();
+    return range_spect::to_range_spect(mp_integer{v} + mp_integer{other.v});
+  }
+
+  range_spect &operator+=(const range_spect &other)
+  {
+    range_spect result = *this + other;
+    v = result.v;
+    return *this;
+  }
+
+  range_spect operator-(const range_spect &other) const
+  {
+    if(is_unknown() || other.is_unknown())
+      return range_spect::unknown();
+    return range_spect::to_range_spect(mp_integer{v} - mp_integer{other.v});
+  }
+
+  range_spect &operator-=(const range_spect &other)
+  {
+    range_spect result = *this - other;
+    v = result.v;
+    return *this;
+  }
+
+  range_spect operator*(const range_spect &other) const
+  {
+    if(is_unknown() || other.is_unknown())
+      return range_spect::unknown();
+    return range_spect::to_range_spect(mp_integer{v} * mp_integer{other.v});
+  }
+
+private:
+  value_type v;
+  friend std::ostream &operator<<(std::ostream &, const range_spect &);
+};
 
-inline range_spect to_range_spect(const mp_integer &size)
+inline std::ostream &operator<<(std::ostream &os, const range_spect &r)
 {
-  assert(size.is_long());
-  mp_integer::llong_t ll=size.to_long();
-  assert(ll<=std::numeric_limits<range_spect>::max());
-  assert(ll>=std::numeric_limits<range_spect>::min());
-  return (range_spect)ll;
+  os << r.v;
+  return os;
 }
 
 // each element x represents a range of bits [x.first, x.second.first)
diff --git a/src/analyses/reaching_definitions.cpp b/src/analyses/reaching_definitions.cpp
index d7ffa9bc26a..2dea301e912 100644
--- a/src/analyses/reaching_definitions.cpp
+++ b/src/analyses/reaching_definitions.cpp
@@ -219,9 +219,15 @@ void rd_range_domaint::transform_function_call(
 
       auto param_bits = pointer_offset_bits(param.type(), ns);
       if(param_bits.has_value())
-        gen(from, identifier, 0, to_range_spect(*param_bits));
+      {
+        gen(
+          from,
+          identifier,
+          range_spect{0},
+          range_spect::to_range_spect(*param_bits));
+      }
       else
-        gen(from, identifier, 0, -1);
+        gen(from, identifier, range_spect{0}, range_spect::unknown());
     }
   }
   else
@@ -337,9 +343,9 @@ void rd_range_domaint::kill(
   const range_spect &range_start,
   const range_spect &range_end)
 {
-  assert(range_start>=0);
-  // -1 for objects of infinite/unknown size
-  if(range_end==-1)
+  PRECONDITION(range_start >= range_spect{0});
+
+  if(range_end.is_unknown())
   {
     kill_inf(identifier, range_start);
     return;
@@ -363,12 +369,13 @@ void rd_range_domaint::kill(
 
     if(v.bit_begin >= range_end)
       ++it;
-    else if(v.bit_end!=-1 &&
-            v.bit_end <= range_start)
+    else if(!v.bit_end.is_unknown() && v.bit_end <= range_start)
+    {
       ++it;
-    else if(v.bit_begin >= range_start &&
-            v.bit_end!=-1 &&
-            v.bit_end <= range_end) // rs <= a < b <= re
+    }
+    else if(
+      v.bit_begin >= range_start && !v.bit_end.is_unknown() &&
+      v.bit_end <= range_end) // rs <= a < b <= re
     {
       clear_export_cache=true;
 
@@ -384,8 +391,7 @@ void rd_range_domaint::kill(
 
       entry->second.erase(it++);
     }
-    else if(v.bit_end==-1 ||
-            v.bit_end > range_end) // a <= rs < re < b
+    else if(v.bit_end.is_unknown() || v.bit_end > range_end) // a <= rs < re < b
     {
       clear_export_cache=true;
 
@@ -436,7 +442,7 @@ void rd_range_domaint::kill_inf(
   const irep_idt &,
   const range_spect &range_start)
 {
-  assert(range_start>=0);
+  PRECONDITION(range_start >= range_spect{0});
 
 #if 0
   valuest::iterator entry=values.find(identifier);
@@ -477,20 +483,13 @@ bool rd_range_domaint::gen(
   const range_spect &range_end)
 {
   // objects of size 0 like union U { signed : 0; };
-  if(range_start==0 && range_end==0)
+  if(range_start == range_spect{0} && range_end == range_spect{0})
     return false;
 
-  assert(range_start>=0);
-
-  // -1 for objects of infinite/unknown size
-  assert(range_end>range_start || range_end==-1);
-
-  reaching_definitiont v;
-  v.identifier=identifier;
-  v.definition_at=from;
-  v.bit_begin=range_start;
-  v.bit_end=range_end;
+  PRECONDITION(range_start >= range_spect{0});
+  PRECONDITION(range_end == range_spect::unknown() || range_end > range_start);
 
+  reaching_definitiont v{identifier, from, range_start, range_end};
   if(!values[identifier].insert(bv_container->add(v)).second)
     return false;
 
diff --git a/src/analyses/reaching_definitions.h b/src/analyses/reaching_definitions.h
index e7021eb38c4..0987362ef2b 100644
--- a/src/analyses/reaching_definitions.h
+++ b/src/analyses/reaching_definitions.h
@@ -92,10 +92,20 @@ struct reaching_definitiont
   /// The two integers below define a range of bits (i.e. the begin and end bit
   /// indices) which represent the value of the variable. So, the integers
   /// represents the half-open interval `[bit_begin, bit_end)` of bits.
-  /// However, `bit_end` can also be set a special value `-1`, which means
-  /// infinite/unknown index.
   range_spect bit_begin;
   range_spect bit_end;
+
+  reaching_definitiont(
+    const irep_idt &identifier,
+    const ai_domain_baset::locationt &definition_at,
+    const range_spect &bit_begin,
+    const range_spect &bit_end)
+    : identifier(identifier),
+      definition_at(definition_at),
+      bit_begin(bit_begin),
+      bit_end(bit_end)
+  {
+  }
 };
 
 /// In order to use instances of this structure as keys in ordered containers,
@@ -109,15 +119,27 @@ inline bool operator<(
   if(b.definition_at<a.definition_at)
     return false;
 
-  if(a.bit_begin<b.bit_begin)
-    return true;
-  if(b.bit_begin<a.bit_begin)
-    return false;
+  if(a.bit_begin.is_unknown() != b.bit_begin.is_unknown())
+    return a.bit_begin.is_unknown();
 
-  if(a.bit_end<b.bit_end)
-    return true;
-  if(b.bit_end<a.bit_end)
-    return false;
+  if(!a.bit_begin.is_unknown())
+  {
+    if(a.bit_begin < b.bit_begin)
+      return true;
+    if(b.bit_begin < a.bit_begin)
+      return false;
+  }
+
+  if(a.bit_end.is_unknown() != b.bit_end.is_unknown())
+    return a.bit_end.is_unknown();
+
+  if(!a.bit_end.is_unknown())
+  {
+    if(a.bit_end < b.bit_end)
+      return true;
+    if(b.bit_end < a.bit_end)
+      return false;
+  }
 
   // we do not expect comparison of unrelated definitions
   // as this operator< is only used in sparse_bitvector_analysist