diff --git a/regression/verilog/SVA/sequence_repetition2.desc b/regression/verilog/SVA/sequence_repetition2.desc
index ad106be7..980132a4 100644
--- a/regression/verilog/SVA/sequence_repetition2.desc
+++ b/regression/verilog/SVA/sequence_repetition2.desc
@@ -1,15 +1,15 @@
 CORE
 sequence_repetition2.sv
 --bound 10
-^\[main\.p0\] main\.x == 0\[\*\]: PROVED up to bound 10$
-^\[main\.p1\] main\.x == 1\[\*\]: PROVED up to bound 10$
-^\[main\.p2\] \(main\.x == 0\[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
-^\[main\.p3\] main\.x == 0\[\+\]: PROVED up to bound 10$
-^\[main\.p4\] main\.half_x == 0\[\*\]: PROVED up to bound 10$
-^\[main\.p5\] 0\[\*\]: PROVED up to bound 10$
-^\[main\.p6\] main\.x == 1\[\+\]: REFUTED$
-^\[main\.p7\] \(main\.x == 0\[\+\]\) #-# main\.x == 1: REFUTED$
-^\[main\.p8\] 0\[\+\]: REFUTED$
+^\[main\.p0\] main\.x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p1\] main\.x == 1 \[\*\]: PROVED up to bound 10$
+^\[main\.p2\] \(main\.x == 0 \[\+\]\) #=# main\.x == 1: PROVED up to bound 10$
+^\[main\.p3\] main\.x == 0 \[\+\]: PROVED up to bound 10$
+^\[main\.p4\] main\.half_x == 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p5\] 0 \[\*\]: PROVED up to bound 10$
+^\[main\.p6\] main\.x == 1 \[\+\]: REFUTED$
+^\[main\.p7\] \(main\.x == 0 \[\+\]\) #-# main\.x == 1: REFUTED$
+^\[main\.p8\] 0 \[\+\]: REFUTED$
 ^EXIT=10$
 ^SIGNAL=0$
 --
diff --git a/src/hw_cbmc_irep_ids.h b/src/hw_cbmc_irep_ids.h
index 18d9bb9f..d7152df8 100644
--- a/src/hw_cbmc_irep_ids.h
+++ b/src/hw_cbmc_irep_ids.h
@@ -60,7 +60,6 @@ IREP_ID_ONE(sva_cycle_delay_star)
 IREP_ID_ONE(sva_cycle_delay_plus)
 IREP_ID_ONE(sva_disable_iff)
 IREP_ID_ONE(sva_sequence_concatenation)
-IREP_ID_ONE(sva_sequence_consecutive_repetition)
 IREP_ID_ONE(sva_sequence_first_match)
 IREP_ID_ONE(sva_sequence_goto_repetition)
 IREP_ID_ONE(sva_sequence_intersect)
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
index 7d1c6fce..2c889fb8 100644
--- a/src/temporal-logic/temporal_logic.cpp
+++ b/src/temporal-logic/temporal_logic.cpp
@@ -111,7 +111,6 @@ bool is_SVA_sequence_operator(const exprt &expr)
          id == ID_sva_sequence_intersect || id == ID_sva_sequence_first_match ||
          id == ID_sva_sequence_throughout || id == ID_sva_sequence_within ||
          id == ID_sva_sequence_goto_repetition ||
-         id == ID_sva_sequence_consecutive_repetition ||
          id == ID_sva_sequence_non_consecutive_repetition ||
          id == ID_sva_sequence_repetition_star ||
          id == ID_sva_sequence_repetition_plus;
diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp
index c8d584ed..74a7ab2f 100644
--- a/src/trans-word-level/sequence.cpp
+++ b/src/trans-word-level/sequence.cpp
@@ -364,42 +364,52 @@ sequence_matchest instantiate_sequence(
 
     return result;
   }
-  else if(expr.id() == ID_sva_sequence_consecutive_repetition) // [*...]
+  else if(expr.id() == ID_sva_sequence_repetition_star) // [*...]
   {
-    // x[*n] is syntactic sugar for x ##1 ... ##1 x, with n repetitions
-    auto &repetition = to_sva_sequence_consecutive_repetition_expr(expr);
-    return instantiate_sequence(
-      repetition.lower(), semantics, t, no_timeframes);
-  }
-  else if(
-    expr.id() == ID_sva_sequence_repetition_plus ||
-    expr.id() == ID_sva_sequence_repetition_star)
-  {
-    // x[+] and x[*]
-    auto &op = to_unary_expr(expr).op();
+    auto &repetition = to_sva_sequence_repetition_star_expr(expr);
+    if(repetition.is_unbounded() && repetition.repetitions_given())
+    {
+      // [*x:$]
+      auto from = numeric_cast_v<mp_integer>(repetition.from());
+      auto &op = repetition.op();
 
-    // Is x a sequence or a state predicate?
-    if(is_SVA_sequence_operator(op))
-      PRECONDITION(false); // no support
+      // Is op a sequence or a state predicate?
+      if(is_SVA_sequence_operator(op))
+        PRECONDITION(false); // no support
 
-    sequence_matchest result;
+      sequence_matchest result;
 
-    // we incrementally add conjuncts to the condition
-    exprt::operandst conjuncts;
+      // we incrementally add conjuncts to the condition
+      exprt::operandst conjuncts;
 
-    for(mp_integer u = t; u < no_timeframes; ++u)
-    {
-      // does x hold in state u?
-      auto cond_u = instantiate(op, u, no_timeframes);
-      conjuncts.push_back(cond_u);
-      result.push_back({u, conjunction(conjuncts)});
-    }
+      for(mp_integer u = t; u < no_timeframes; ++u)
+      {
+        // does op hold in timeframe u?
+        auto cond_u = instantiate(op, u, no_timeframes);
+        conjuncts.push_back(cond_u);
 
-    // In addition to the above, x[*] allows an empty match.
-    if(expr.id() == ID_sva_sequence_repetition_star)
-      result.push_back({t, true_exprt{}});
+        if(conjuncts.size() >= from)
+          result.push_back({u, conjunction(conjuncts)});
+      }
 
-    return result;
+      // Empty match allowed?
+      if(from == 0)
+        result.push_back({t, true_exprt{}});
+
+      return result;
+    }
+    else
+    {
+      // [*], [*n], [*x:y]
+      return instantiate_sequence(
+        repetition.lower(), semantics, t, no_timeframes);
+    }
+  }
+  else if(expr.id() == ID_sva_sequence_repetition_plus) // [+]
+  {
+    auto &repetition = to_sva_sequence_repetition_plus_expr(expr);
+    return instantiate_sequence(
+      repetition.lower(), semantics, t, no_timeframes);
   }
   else if(expr.id() == ID_sva_sequence_goto_repetition) // [->...]
   {
diff --git a/src/verilog/expr2verilog.cpp b/src/verilog/expr2verilog.cpp
index b4b0aefe..2bdd4060 100644
--- a/src/verilog/expr2verilog.cpp
+++ b/src/verilog/expr2verilog.cpp
@@ -629,18 +629,21 @@ expr2verilogt::resultt expr2verilogt::convert_sva_sequence_repetition(
 
   std::string dest = op_rec.s + " [" + name;
 
-  if(expr.is_range())
+  if(expr.repetitions_given())
   {
-    dest += convert_rec(expr.from()).s;
-    dest += ':';
+    if(expr.is_range())
+    {
+      dest += convert_rec(expr.from()).s;
+      dest += ':';
 
-    if(expr.is_unbounded())
-      dest += '$';
+      if(expr.is_unbounded())
+        dest += "$";
+      else
+        dest += convert_rec(expr.to()).s;
+    }
     else
-      dest += convert_rec(expr.to()).s;
+      dest += convert_rec(expr.repetitions()).s;
   }
-  else
-    dest += convert_rec(expr.repetitions()).s;
 
   dest += ']';
 
@@ -1850,23 +1853,17 @@ expr2verilogt::resultt expr2verilogt::convert_rec(const exprt &src)
     return precedence = verilog_precedencet::MIN,
            convert_sva_unary("always", to_sva_always_expr(src));
 
-  else if(src.id() == ID_sva_sequence_repetition_star)
-    return precedence = verilog_precedencet::MIN,
-           convert_sva_unary(to_unary_expr(src), "[*]");
-  // not sure about precedence
-
   else if(src.id() == ID_sva_sequence_repetition_plus)
-    return precedence = verilog_precedencet::MIN,
-           convert_sva_unary(to_unary_expr(src), "[+]");
-  // not sure about precedence
+    return convert_sva_sequence_repetition(
+      "+", to_sva_sequence_repetition_plus_expr(src));
 
   else if(src.id() == ID_sva_sequence_non_consecutive_repetition)
     return convert_sva_sequence_repetition(
       "=", to_sva_sequence_non_consecutive_repetition_expr(src));
 
-  else if(src.id() == ID_sva_sequence_consecutive_repetition)
+  else if(src.id() == ID_sva_sequence_repetition_star)
     return convert_sva_sequence_repetition(
-      "*", to_sva_sequence_consecutive_repetition_expr(src));
+      "*", to_sva_sequence_repetition_star_expr(src));
 
   else if(src.id() == ID_sva_sequence_goto_repetition)
     return convert_sva_sequence_repetition(
diff --git a/src/verilog/parser.y b/src/verilog/parser.y
index 16fdba2c..bd55c56d 100644
--- a/src/verilog/parser.y
+++ b/src/verilog/parser.y
@@ -2690,7 +2690,7 @@ sequence_abbrev:
 
 consecutive_repetition:
 	  "[*" const_or_range_expression ']'
-		{ init($$, ID_sva_sequence_consecutive_repetition);
+		{ init($$, ID_sva_sequence_repetition_star);
 		  if(stack_expr($2).id() == ID_sva_cycle_delay)
 		    swapop($$, $2);
 		  else
@@ -2700,9 +2700,13 @@ consecutive_repetition:
 		  }
 		}
 	| "[*" ']'
-		{ init($$, ID_sva_sequence_repetition_star); }
+		{ init($$, ID_sva_sequence_repetition_star);
+		  stack_expr($$).add_to_operands(nil_exprt{}, nil_exprt{});
+		}
 	| "[+" ']'
-		{ init($$, ID_sva_sequence_repetition_plus); }
+		{ init($$, ID_sva_sequence_repetition_plus);
+		  stack_expr($$).add_to_operands(nil_exprt{}, nil_exprt{});
+		}
 	;
 
 non_consecutive_repetition:
diff --git a/src/verilog/sva_expr.cpp b/src/verilog/sva_expr.cpp
index 37d5ad2f..34bfd162 100644
--- a/src/verilog/sva_expr.cpp
+++ b/src/verilog/sva_expr.cpp
@@ -57,12 +57,25 @@ exprt sva_case_exprt::lowering() const
     disjunction(disjuncts), case_items.front().result(), reduced_rec};
 }
 
-exprt sva_sequence_consecutive_repetition_exprt::lower() const
+exprt sva_sequence_repetition_plus_exprt::lower() const
+{
+  // [+] is the same as [*1:$]
+  return sva_sequence_repetition_star_exprt{
+    op(), from_integer(1, integer_typet{}), infinity_exprt{integer_typet{}}};
+}
+
+exprt sva_sequence_repetition_star_exprt::lower() const
 {
   PRECONDITION(
     op().type().id() == ID_bool || op().type().id() == ID_verilog_sva_sequence);
 
-  if(!is_range())
+  if(!repetitions_given())
+  {
+    // op[*] is the same as op[*0:$]
+    return sva_sequence_repetition_star_exprt{
+      op(), from_integer(0, integer_typet{}), infinity_exprt{integer_typet{}}};
+  }
+  else if(!is_range())
   {
     // expand x[*n] into x ##1 x ##1 ...
     auto n = numeric_cast_v<mp_integer>(repetitions());
@@ -94,14 +107,13 @@ exprt sva_sequence_consecutive_repetition_exprt::lower() const
     DATA_INVARIANT(
       to_int >= from_int, "number of repetitions must be interval");
 
-    exprt result = sva_sequence_consecutive_repetition_exprt{op(), from()};
+    exprt result = sva_sequence_repetition_star_exprt{op(), from()};
 
     for(mp_integer n = from_int + 1; n <= to_int; ++n)
     {
       auto n_expr = from_integer(n, integer_typet{});
       result = sva_or_exprt{
-        std::move(result),
-        sva_sequence_consecutive_repetition_exprt{op(), n_expr}};
+        std::move(result), sva_sequence_repetition_star_exprt{op(), n_expr}};
     }
 
     return result;
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
index 455cb5bc..48818ab6 100644
--- a/src/verilog/sva_expr.h
+++ b/src/verilog/sva_expr.h
@@ -1325,10 +1325,22 @@ inline sva_case_exprt &to_sva_case_expr(exprt &expr)
 }
 
 /// Base class for [->...], [*...], [=...]
-/// The ... constraint may be x, x:y, x:$
+/// The ... constraint may be blank, x, x:y, x:$
 class sva_sequence_repetition_exprt : public ternary_exprt
 {
 public:
+  /// number of repetitions not given, e.g., [*] or [+]
+  sva_sequence_repetition_exprt(exprt __op, irep_idt __id)
+    : ternary_exprt{
+        __id,
+        std::move(__op),
+        nil_exprt{},
+        nil_exprt{},
+        verilog_sva_sequence_typet{}}
+  {
+  }
+
+  /// fixed number of repetitions
   sva_sequence_repetition_exprt(
     exprt __op,
     irep_idt __id,
@@ -1342,6 +1354,7 @@ class sva_sequence_repetition_exprt : public ternary_exprt
   {
   }
 
+  /// bounded range for the number of repetitions
   sva_sequence_repetition_exprt(
     exprt __op,
     irep_idt __id,
@@ -1356,6 +1369,21 @@ class sva_sequence_repetition_exprt : public ternary_exprt
   {
   }
 
+  /// unbounded range for the number of repetitions
+  sva_sequence_repetition_exprt(
+    exprt __op,
+    irep_idt __id,
+    constant_exprt __from,
+    infinity_exprt __to)
+    : ternary_exprt{
+        __id,
+        std::move(__op),
+        std::move(__from),
+        std::move(__to),
+        verilog_sva_sequence_typet{}}
+  {
+  }
+
   // May be a sequence for [*...], Boolean otherwise
   const exprt &op() const
   {
@@ -1367,16 +1395,22 @@ class sva_sequence_repetition_exprt : public ternary_exprt
     return op0();
   }
 
+  /// true if number of repetitions is given
+  bool repetitions_given() const
+  {
+    return op1().is_not_nil();
+  }
+
   // The number of repetitions must be a constant after elaboration.
   const constant_exprt &repetitions() const
   {
-    PRECONDITION(!is_range());
+    PRECONDITION(repetitions_given() && !is_range());
     return static_cast<const constant_exprt &>(op1());
   }
 
   constant_exprt &repetitions()
   {
-    PRECONDITION(!is_range());
+    PRECONDITION(repetitions_given() && !is_range());
     return static_cast<constant_exprt &>(op1());
   }
 
@@ -1434,49 +1468,105 @@ to_sva_sequence_repetition_expr(exprt &expr)
   return static_cast<sva_sequence_repetition_exprt &>(expr);
 }
 
-class sva_sequence_consecutive_repetition_exprt
-  : public sva_sequence_repetition_exprt
+/// op[+]
+class sva_sequence_repetition_plus_exprt : public sva_sequence_repetition_exprt
 {
 public:
-  sva_sequence_consecutive_repetition_exprt(
-    exprt __op,
-    constant_exprt __repetitions)
+  /// The operand is a sequence
+  explicit sva_sequence_repetition_plus_exprt(exprt op)
+    : sva_sequence_repetition_exprt{
+        std::move(op),
+        ID_sva_sequence_repetition_plus}
+  {
+  }
+
+  // op[*1:$]
+  exprt lower() const;
+};
+
+static inline const sva_sequence_repetition_plus_exprt &
+to_sva_sequence_repetition_plus_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_repetition_plus);
+  sva_sequence_repetition_plus_exprt::check(expr);
+  return static_cast<const sva_sequence_repetition_plus_exprt &>(expr);
+}
+
+static inline sva_sequence_repetition_plus_exprt &
+to_sva_sequence_repetition_plus_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_sva_sequence_repetition_plus);
+  sva_sequence_repetition_plus_exprt::check(expr);
+  return static_cast<sva_sequence_repetition_plus_exprt &>(expr);
+}
+
+/// [*] or [*n] or [*x:y] or [*x:$]
+class sva_sequence_repetition_star_exprt : public sva_sequence_repetition_exprt
+{
+public:
+  /// op[*]
+  explicit sva_sequence_repetition_star_exprt(exprt __op)
     : sva_sequence_repetition_exprt{
         std::move(__op),
-        ID_sva_sequence_consecutive_repetition,
+        ID_sva_sequence_repetition_star}
+  {
+  }
+
+  /// op[*n]
+  sva_sequence_repetition_star_exprt(exprt __op, constant_exprt __repetitions)
+    : sva_sequence_repetition_exprt{
+        std::move(__op),
+        ID_sva_sequence_repetition_star,
         std::move(__repetitions)}
   {
   }
 
-  sva_sequence_consecutive_repetition_exprt(
+  /// op[*x:y]
+  sva_sequence_repetition_star_exprt(
     exprt __op,
     constant_exprt __from,
     constant_exprt __to)
     : sva_sequence_repetition_exprt{
         std::move(__op),
-        ID_sva_sequence_consecutive_repetition,
+        ID_sva_sequence_repetition_star,
+        std::move(__from),
+        std::move(__to)}
+  {
+  }
+
+  /// op[*x:$]
+  sva_sequence_repetition_star_exprt(
+    exprt __op,
+    constant_exprt __from,
+    infinity_exprt __to)
+    : sva_sequence_repetition_exprt{
+        std::move(__op),
+        ID_sva_sequence_repetition_star,
         std::move(__from),
         std::move(__to)}
   {
   }
 
+  /// [*] --> [0:$]
+  /// [*n] --> op ##1 op ##1 op ...
+  /// [*x:y] --> op[*x] or op[*x+1] or ... or op[*y]
   exprt lower() const;
 };
 
-inline const sva_sequence_consecutive_repetition_exprt &
-to_sva_sequence_consecutive_repetition_expr(const exprt &expr)
+inline const sva_sequence_repetition_star_exprt &
+to_sva_sequence_repetition_star_expr(const exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_sequence_consecutive_repetition);
-  sva_sequence_consecutive_repetition_exprt::check(expr);
-  return static_cast<const sva_sequence_consecutive_repetition_exprt &>(expr);
+  PRECONDITION(expr.id() == ID_sva_sequence_repetition_star);
+  sva_sequence_repetition_star_exprt::check(expr);
+  return static_cast<const sva_sequence_repetition_star_exprt &>(expr);
 }
 
-inline sva_sequence_consecutive_repetition_exprt &
-to_sva_sequence_consecutive_repetition_expr(exprt &expr)
+inline sva_sequence_repetition_star_exprt &
+to_sva_sequence_repetition_star_expr(exprt &expr)
 {
-  PRECONDITION(expr.id() == ID_sva_sequence_consecutive_repetition);
-  sva_sequence_consecutive_repetition_exprt::check(expr);
-  return static_cast<sva_sequence_consecutive_repetition_exprt &>(expr);
+  PRECONDITION(expr.id() == ID_sva_sequence_repetition_star);
+  sva_sequence_repetition_star_exprt::check(expr);
+  return static_cast<sva_sequence_repetition_star_exprt &>(expr);
 }
 
 class sva_sequence_goto_repetition_exprt : public sva_sequence_repetition_exprt
diff --git a/src/verilog/verilog_typecheck_sva.cpp b/src/verilog/verilog_typecheck_sva.cpp
index fe29b935..f0dd53fd 100644
--- a/src/verilog/verilog_typecheck_sva.cpp
+++ b/src/verilog/verilog_typecheck_sva.cpp
@@ -86,14 +86,10 @@ exprt verilog_typecheck_exprt::convert_unary_sva(unary_exprt expr)
     return std::move(expr);
   }
   else if(
-    expr.id() == ID_sva_cycle_delay_plus ||         // ##[+]
-    expr.id() == ID_sva_cycle_delay_star ||         // ##[*]
-    expr.id() == ID_sva_sequence_repetition_plus || // x[+]
-    expr.id() == ID_sva_sequence_repetition_star)   // x[*}
+    expr.id() == ID_sva_cycle_delay_plus || // ##[+]
+    expr.id() == ID_sva_cycle_delay_star)   // ##[*]
   {
     // These take a sequence as argument.
-    // For some, the grammar allows properties to implement and/or over
-    // sequences. Check here that the argument is a sequence.
     convert_sva(expr.op());
     require_sva_sequence(expr.op());
     expr.type() = verilog_sva_sequence_typet{};
@@ -319,7 +315,7 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
 
     return std::move(expr);
   }
-  else if(expr.id() == ID_sva_sequence_consecutive_repetition) // x[*1:2]
+  else if(expr.id() == ID_sva_sequence_repetition_star) // x[*1:2]
   {
     // This expression takes a sequence as argument.
     // The grammar allows properties to implement and/or over
@@ -327,7 +323,8 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
     convert_sva(expr.op0());
     require_sva_sequence(expr.op0());
 
-    convert_expr(expr.op1());
+    if(expr.op1().is_not_nil())
+      convert_expr(expr.op1());
 
     if(expr.op2().is_not_nil())
       convert_expr(expr.op2());
@@ -335,6 +332,18 @@ exprt verilog_typecheck_exprt::convert_ternary_sva(ternary_exprt expr)
     expr.type() = verilog_sva_sequence_typet{};
     return std::move(expr);
   }
+  else if(expr.id() == ID_sva_sequence_repetition_plus) // x[+]
+  {
+    // These take a sequence as argument.
+    // The grammar allows properties to implement and/or over
+    // sequences. Check here that the argument is a sequence.
+    // op1() and op2() are nil.
+    // The forms op[+x] and op[+x:y] do not exist.
+    convert_sva(expr.op0());
+    require_sva_sequence(expr.op0());
+    expr.type() = verilog_sva_sequence_typet{};
+    return std::move(expr);
+  }
   else if(
     expr.id() == ID_sva_sequence_non_consecutive_repetition ||
     expr.id() == ID_sva_sequence_goto_repetition)