diff --git a/src/ebmc/completeness_threshold.cpp b/src/ebmc/completeness_threshold.cpp
index e55ab7dee..f1bb602cb 100644
--- a/src/ebmc/completeness_threshold.cpp
+++ b/src/ebmc/completeness_threshold.cpp
@@ -39,13 +39,12 @@ bool has_low_completeness_threshold(const exprt &expr)
     auto &always_expr = to_sva_ranged_always_expr(expr);
     if(has_temporal_operator(always_expr.op()))
       return false;
-    else if(always_expr.upper().is_constant())
+    else if(always_expr.to().is_constant())
     {
-      auto lower_int = numeric_cast_v<mp_integer>(always_expr.lower());
-      auto upper_int =
-        numeric_cast_v<mp_integer>(to_constant_expr(always_expr.upper()));
-      return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
-             upper_int <= 1;
+      auto from_int = numeric_cast_v<mp_integer>(always_expr.from());
+      auto to_int =
+        numeric_cast_v<mp_integer>(to_constant_expr(always_expr.to()));
+      return from_int >= 0 && from_int <= 1 && to_int >= 0 && to_int <= 1;
     }
     else
       return false;
@@ -57,10 +56,9 @@ bool has_low_completeness_threshold(const exprt &expr)
       return false;
     else
     {
-      auto lower_int = numeric_cast_v<mp_integer>(s_always_expr.lower());
-      auto upper_int = numeric_cast_v<mp_integer>(s_always_expr.upper());
-      return lower_int >= 0 && lower_int <= 1 && upper_int >= 0 &&
-             upper_int <= 1;
+      auto from_int = numeric_cast_v<mp_integer>(s_always_expr.from());
+      auto to_int = numeric_cast_v<mp_integer>(s_always_expr.to());
+      return from_int >= 0 && from_int <= 1 && to_int >= 0 && to_int <= 1;
     }
   }
   else if(
diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
index 1ba1d51ca..5e451d333 100644
--- a/src/temporal-logic/ltl_sva_to_string.cpp
+++ b/src/temporal-logic/ltl_sva_to_string.cpp
@@ -161,16 +161,16 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   {
     auto &always = to_sva_ranged_always_expr(expr);
     auto new_expr = unary_exprt{ID_sva_ranged_always, always.op()};
-    auto lower = numeric_cast_v<mp_integer>(always.lower());
+    auto from = numeric_cast_v<mp_integer>(always.from());
     if(!always.is_range())
-      return prefix("F[" + integer2string(lower) + "]", new_expr, mode);
+      return prefix("F[" + integer2string(from) + "]", new_expr, mode);
     else if(always.is_unbounded())
-      return prefix("F[" + integer2string(lower) + ":]", new_expr, mode);
+      return prefix("F[" + integer2string(from) + ":]", new_expr, mode);
     else
     {
-      auto upper = numeric_cast_v<mp_integer>(to_constant_expr(always.upper()));
+      auto to = numeric_cast_v<mp_integer>(to_constant_expr(always.to()));
       return prefix(
-        "F[" + integer2string(lower) + ":" + integer2string(upper) + "]",
+        "F[" + integer2string(from) + ":" + integer2string(to) + "]",
         new_expr,
         mode);
     }
@@ -188,19 +188,19 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     expr.id() == ID_sva_ranged_s_eventually || expr.id() == ID_sva_eventually)
   {
     PRECONDITION(mode == PROPERTY);
+
     auto &eventually = to_sva_ranged_predicate_exprt(expr);
     auto new_expr = unary_exprt{expr.id(), eventually.op()};
-    auto lower = numeric_cast_v<mp_integer>(eventually.lower());
+    auto from = numeric_cast_v<mp_integer>(eventually.from());
     if(!eventually.is_range())
-      return prefix("F[" + integer2string(lower) + "]", new_expr, mode);
+      return prefix("F[" + integer2string(from) + "]", new_expr, mode);
     else if(eventually.is_unbounded())
-      return prefix("F[" + integer2string(lower) + ":]", new_expr, mode);
+      return prefix("F[" + integer2string(from) + ":]", new_expr, mode);
     else
     {
-      auto upper =
-        numeric_cast_v<mp_integer>(to_constant_expr(eventually.upper()));
+      auto to = numeric_cast_v<mp_integer>(to_constant_expr(eventually.to()));
       return prefix(
-        "F[" + integer2string(lower) + ":" + integer2string(upper) + "]",
+        "F[" + integer2string(from) + ":" + integer2string(to) + "]",
         new_expr,
         mode);
     }
diff --git a/src/temporal-logic/nnf.cpp b/src/temporal-logic/nnf.cpp
index db29e1c24..a9297bdd8 100644
--- a/src/temporal-logic/nnf.cpp
+++ b/src/temporal-logic/nnf.cpp
@@ -79,14 +79,14 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     // not always [x:y] p --> s_eventually [x:y] not p
     auto &always = to_sva_ranged_always_expr(expr);
     return sva_ranged_s_eventually_exprt{
-      always.lower(), always.upper(), not_exprt{always.op()}};
+      always.from(), always.to(), not_exprt{always.op()}};
   }
   else if(expr.id() == ID_sva_s_always)
   {
     // not s_always [x:y] p --> eventually [x:y] not p
     auto &s_always = to_sva_s_always_expr(expr);
     return sva_eventually_exprt{
-      s_always.lower(), s_always.upper(), not_exprt{s_always.op()}};
+      s_always.from(), s_always.to(), not_exprt{s_always.op()}};
   }
   else if(expr.id() == ID_sva_s_eventually)
   {
@@ -98,7 +98,7 @@ std::optional<exprt> negate_property_node(const exprt &expr)
     // not eventually[i:j] p --> s_always[i:j] not p
     auto &eventually = to_sva_eventually_expr(expr);
     return sva_s_always_exprt{
-      eventually.lower(), eventually.upper(), not_exprt{eventually.op()}};
+      eventually.from(), eventually.to(), not_exprt{eventually.op()}};
   }
   else if(expr.id() == ID_sva_until)
   {
diff --git a/src/temporal-logic/sva_to_ltl.cpp b/src/temporal-logic/sva_to_ltl.cpp
index 836f7b485..dcdf2f99f 100644
--- a/src/temporal-logic/sva_to_ltl.cpp
+++ b/src/temporal-logic/sva_to_ltl.cpp
@@ -57,28 +57,28 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     if(rec.has_value())
     {
       // always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
-      auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
+      auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
 
       // Is there an upper end of the range?
-      if(ranged_always.upper().is_constant())
+      if(ranged_always.to().is_constant())
       {
         // upper end set
-        auto upper_int =
-          numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.upper()));
-        PRECONDITION(upper_int >= lower_int);
-        auto diff = upper_int - lower_int;
+        auto to_int =
+          numeric_cast_v<mp_integer>(to_constant_expr(ranged_always.to()));
+        PRECONDITION(to_int >= from_int);
+        auto diff = to_int - from_int;
 
         exprt::operandst conjuncts;
 
         for(auto i = 0; i <= diff; i++)
           conjuncts.push_back(n_Xes(i, rec.value()));
 
-        return n_Xes(lower_int, conjunction(conjuncts));
+        return n_Xes(from_int, conjunction(conjuncts));
       }
-      else if(ranged_always.upper().id() == ID_infinity)
+      else if(ranged_always.to().id() == ID_infinity)
       {
         // always [l:$] op ---> X ... X G op
-        return n_Xes(lower_int, G_exprt{rec.value()});
+        return n_Xes(from_int, G_exprt{rec.value()});
       }
       else
         PRECONDITION(false);
@@ -93,17 +93,17 @@ std::optional<exprt> SVA_to_LTL(exprt expr)
     if(rec.has_value())
     {
       // s_always [l:u] op ---> X ... X (op ∧ X op ∧ ... ∧ X ... X op)
-      auto lower_int = numeric_cast_v<mp_integer>(ranged_always.lower());
-      auto upper_int = numeric_cast_v<mp_integer>(ranged_always.upper());
-      PRECONDITION(upper_int >= lower_int);
-      auto diff = upper_int - lower_int;
+      auto from_int = numeric_cast_v<mp_integer>(ranged_always.from());
+      auto to_int = numeric_cast_v<mp_integer>(ranged_always.to());
+      PRECONDITION(to_int >= from_int);
+      auto diff = to_int - from_int;
 
       exprt::operandst conjuncts;
 
       for(auto i = 0; i <= diff; i++)
         conjuncts.push_back(n_Xes(i, rec.value()));
 
-      return n_Xes(lower_int, conjunction(conjuncts));
+      return n_Xes(from_int, conjunction(conjuncts));
     }
     else
       return {};
diff --git a/src/temporal-logic/trivial_sva.cpp b/src/temporal-logic/trivial_sva.cpp
index 60477f4da..242cc22b2 100644
--- a/src/temporal-logic/trivial_sva.cpp
+++ b/src/temporal-logic/trivial_sva.cpp
@@ -113,7 +113,7 @@ exprt trivial_sva(exprt expr)
   }
   else if(expr.id() == ID_sva_case)
   {
-    expr = to_sva_case_expr(expr).lowering();
+    expr = to_sva_case_expr(expr).lower();
   }
 
   // rewrite the operands, recursively
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index 624cd7196..ca609bbf4 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -213,16 +213,14 @@ static obligationst property_obligations_rec(
     const auto &eventually_expr = to_sva_eventually_expr(property_expr);
     const auto &op = eventually_expr.op();
 
-    mp_integer lower;
-    if(to_integer_non_constant(eventually_expr.lower(), lower))
-      throw "failed to convert sva_eventually index";
+    mp_integer from = numeric_cast_v<mp_integer>(eventually_expr.from());
 
-    mp_integer upper;
-    if(to_integer_non_constant(eventually_expr.upper(), upper))
+    mp_integer to;
+    if(to_integer_non_constant(eventually_expr.to(), to))
       throw "failed to convert sva_eventually index";
 
     // We rely on NNF.
-    if(current + lower >= no_timeframes || current + upper >= no_timeframes)
+    if(current + from >= no_timeframes || current + to >= no_timeframes)
     {
       DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
       return obligationst{no_timeframes - 1, true_exprt()};
@@ -230,7 +228,7 @@ static obligationst property_obligations_rec(
 
     exprt::operandst disjuncts = {};
 
-    for(mp_integer u = current + lower; u <= current + upper; ++u)
+    for(mp_integer u = current + from; u <= current + to; ++u)
     {
       auto obligations_rec = property_obligations_rec(op, u, no_timeframes);
       disjuncts.push_back(obligations_rec.conjunction().second);
@@ -283,29 +281,24 @@ static obligationst property_obligations_rec(
   }
   else if(property_expr.id() == ID_sva_ranged_s_eventually)
   {
-    auto &phi = to_sva_ranged_s_eventually_expr(property_expr).op();
-    auto &lower = to_sva_ranged_s_eventually_expr(property_expr).lower();
-    auto &upper = to_sva_ranged_s_eventually_expr(property_expr).upper();
+    const auto &s_eventually = to_sva_ranged_s_eventually_expr(property_expr);
+    auto from = numeric_cast_v<mp_integer>(s_eventually.from());
 
-    auto from_opt = numeric_cast<mp_integer>(lower);
-    if(!from_opt.has_value())
-      throw ebmc_errort() << "failed to convert SVA s_eventually from index";
-
-    if(*from_opt < 0)
+    if(from < 0)
       throw ebmc_errort() << "SVA s_eventually from index must not be negative";
 
-    auto from = std::min(no_timeframes - 1, current + *from_opt);
+    from = std::min(no_timeframes - 1, current + from);
 
     mp_integer to;
 
-    if(upper.id() == ID_infinity)
+    if(s_eventually.is_unbounded())
     {
       throw ebmc_errort()
         << "failed to convert SVA s_eventually to index (infinity)";
     }
     else
     {
-      auto to_opt = numeric_cast<mp_integer>(upper);
+      auto to_opt = numeric_cast<mp_integer>(s_eventually.to());
       if(!to_opt.has_value())
         throw ebmc_errort() << "failed to convert SVA s_eventually to index";
       to = std::min(current + *to_opt, no_timeframes - 1);
@@ -316,7 +309,8 @@ static obligationst property_obligations_rec(
 
     for(mp_integer c = from; c <= to; ++c)
     {
-      auto tmp = property_obligations_rec(phi, c, no_timeframes).conjunction();
+      auto tmp = property_obligations_rec(s_eventually.op(), c, no_timeframes)
+                   .conjunction();
       time = std::max(time, tmp.first);
       disjuncts.push_back(tmp.second);
     }
@@ -330,14 +324,14 @@ static obligationst property_obligations_rec(
     auto &phi = property_expr.id() == ID_sva_ranged_always
                   ? to_sva_ranged_always_expr(property_expr).op()
                   : to_sva_s_always_expr(property_expr).op();
-    auto &lower = property_expr.id() == ID_sva_ranged_always
-                    ? to_sva_ranged_always_expr(property_expr).lower()
-                    : to_sva_s_always_expr(property_expr).lower();
-    auto &upper = property_expr.id() == ID_sva_ranged_always
-                    ? to_sva_ranged_always_expr(property_expr).upper()
-                    : to_sva_s_always_expr(property_expr).upper();
-
-    auto from_opt = numeric_cast<mp_integer>(lower);
+    auto &from_expr = property_expr.id() == ID_sva_ranged_always
+                        ? to_sva_ranged_always_expr(property_expr).from()
+                        : to_sva_s_always_expr(property_expr).from();
+    auto &to_expr = property_expr.id() == ID_sva_ranged_always
+                      ? to_sva_ranged_always_expr(property_expr).to()
+                      : to_sva_s_always_expr(property_expr).to();
+
+    auto from_opt = numeric_cast<mp_integer>(from_expr);
     if(!from_opt.has_value())
       throw ebmc_errort() << "failed to convert SVA always from index";
 
@@ -348,13 +342,13 @@ static obligationst property_obligations_rec(
 
     mp_integer to;
 
-    if(upper.id() == ID_infinity)
+    if(to_expr.id() == ID_infinity)
     {
       to = no_timeframes - 1;
     }
     else
     {
-      auto to_opt = numeric_cast<mp_integer>(upper);
+      auto to_opt = numeric_cast<mp_integer>(to_expr);
       if(!to_opt.has_value())
         throw ebmc_errort() << "failed to convert SVA always to index";
       to = std::min(current + *to_opt, no_timeframes - 1);
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index c9a0ec2c8..c79aa20d9 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -460,11 +460,11 @@ expr2verilogt::resultt expr2verilogt::convert_sva_ranged_predicate(
 {
   std::string range_str;
 
-  range_str = "[" + convert(src.lower()) + ':';
-  if(src.upper().id() == ID_infinity)
+  range_str = "[" + convert(src.from()) + ':';
+  if(src.is_unbounded())
     range_str += "$";
   else
-    range_str += convert(src.upper());
+    range_str += convert(src.to());
   range_str += "] ";
 
   auto &src_op = src.op();
diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp
index ce5530893..613007d10 100644
--- a/src/verilog/sva_expr.cpp
+++ b/src/verilog/sva_expr.cpp
@@ -29,7 +29,7 @@ exprt sva_cycle_delay_star_exprt::lower() const
     op()};
 }
 
-exprt sva_case_exprt::lowering() const
+exprt sva_case_exprt::lower() const
 {
   auto &case_items = this->case_items();
 
@@ -51,7 +51,7 @@ exprt sva_case_exprt::lowering() const
   reduced.case_items().erase(reduced.case_items().begin());
 
   // rec. call
-  auto reduced_rec = reduced.lowering();
+  auto reduced_rec = reduced.lower();
 
   return if_exprt{
     disjunction(disjuncts), case_items.front().result(), reduced_rec};
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
index 4c145145d..2f410f8d7 100644
--- a/src/verilog/sva_expr.h
+++ b/src/verilog/sva_expr.h
@@ -272,24 +272,24 @@ class sva_ranged_predicate_exprt : public ternary_exprt
 public:
   sva_ranged_predicate_exprt(
     irep_idt __id,
-    constant_exprt __lower,
-    exprt __upper,
+    constant_exprt __from,
+    exprt __to,
     exprt __op)
     : ternary_exprt(
         __id,
-        std::move(__lower),
-        std::move(__upper),
+        std::move(__from),
+        std::move(__to),
         std::move(__op),
         bool_typet{})
   {
   }
 
-  const constant_exprt &lower() const
+  const constant_exprt &from() const
   {
     return static_cast<const constant_exprt &>(op0());
   }
 
-  constant_exprt &lower()
+  constant_exprt &from()
   {
     return static_cast<constant_exprt &>(op0());
   }
@@ -304,12 +304,12 @@ class sva_ranged_predicate_exprt : public ternary_exprt
     return op1().id() == ID_infinity;
   }
 
-  const exprt &upper() const
+  const exprt &to() const
   {
     return op1();
   }
 
-  exprt &upper()
+  exprt &to()
   {
     return op1();
   }
@@ -351,40 +351,37 @@ class sva_bounded_range_predicate_exprt : public sva_ranged_predicate_exprt
 public:
   sva_bounded_range_predicate_exprt(
     irep_idt __id,
-    constant_exprt __lower,
-    constant_exprt __upper,
+    constant_exprt __from,
+    constant_exprt __to,
     exprt __op)
     : sva_ranged_predicate_exprt(
         __id,
-        std::move(__lower),
-        std::move(__upper),
+        std::move(__from),
+        std::move(__to),
         std::move(__op))
   {
   }
 
-  const constant_exprt &upper() const
+  const constant_exprt &to() const
   {
     return static_cast<const constant_exprt &>(
-      sva_ranged_predicate_exprt::upper());
+      sva_ranged_predicate_exprt::to());
   }
 
-  constant_exprt &upper()
+  constant_exprt &to()
   {
-    return static_cast<constant_exprt &>(sva_ranged_predicate_exprt::upper());
+    return static_cast<constant_exprt &>(sva_ranged_predicate_exprt::to());
   }
 };
 
 class sva_eventually_exprt : public sva_bounded_range_predicate_exprt
 {
 public:
-  sva_eventually_exprt(
-    constant_exprt __lower,
-    constant_exprt __upper,
-    exprt __op)
+  sva_eventually_exprt(constant_exprt __from, constant_exprt __to, exprt __op)
     : sva_bounded_range_predicate_exprt(
         ID_sva_eventually,
-        std::move(__lower),
-        std::move(__upper),
+        std::move(__from),
+        std::move(__to),
         std::move(__op))
   {
   }
@@ -433,13 +430,13 @@ class sva_ranged_s_eventually_exprt : public sva_ranged_predicate_exprt
 {
 public:
   explicit sva_ranged_s_eventually_exprt(
-    constant_exprt lower,
-    exprt upper,
+    constant_exprt from,
+    exprt to,
     exprt op)
     : sva_ranged_predicate_exprt(
         ID_sva_ranged_s_eventually,
-        std::move(lower),
-        std::move(upper),
+        std::move(from),
+        std::move(to),
         std::move(op))
   {
   }
@@ -487,11 +484,11 @@ static inline sva_always_exprt &to_sva_always_expr(exprt &expr)
 class sva_ranged_always_exprt : public sva_ranged_predicate_exprt
 {
 public:
-  sva_ranged_always_exprt(constant_exprt lower, exprt upper, exprt op)
+  sva_ranged_always_exprt(constant_exprt from, exprt to, exprt op)
     : sva_ranged_predicate_exprt(
         ID_sva_ranged_always,
-        std::move(lower),
-        std::move(upper),
+        std::move(from),
+        std::move(to),
         std::move(op))
   {
   }
@@ -515,11 +512,11 @@ static inline sva_ranged_always_exprt &to_sva_ranged_always_expr(exprt &expr)
 class sva_s_always_exprt : public sva_bounded_range_predicate_exprt
 {
 public:
-  sva_s_always_exprt(constant_exprt lower, constant_exprt upper, exprt op)
+  sva_s_always_exprt(constant_exprt from, constant_exprt to, exprt op)
     : sva_bounded_range_predicate_exprt(
         ID_sva_s_always,
-        std::move(lower),
-        std::move(upper),
+        std::move(from),
+        std::move(to),
         std::move(op))
   {
   }
@@ -1360,7 +1357,7 @@ class sva_case_exprt : public binary_predicate_exprt
     return (case_itemst &)(op1().operands());
   }
 
-  exprt lowering() const;
+  exprt lower() const;
 
 protected:
   using binary_predicate_exprt::op0;