diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_plus4.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_plus4.desc
new file mode 100644
index 000000000..9824e13ad
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_plus4.desc
@@ -0,0 +1,12 @@
+CORE
+../../verilog/SVA/cycle_delay_plus4.sv
+--buechi
+^\[main\.p0\] main\.x == 0 ##\[\+\] main\.x == 1: PROVED \(1-induction\)$
+^\[main\.p1\] main\.x == 0 ##\[\+\] main\.x == 2: PROVED \(1-induction\)$
+^\[main\.p2\] main\.x == 1 ##\[\+\] main\.x == 1: REFUTED$
+^\[main\.p3\] main\.x == 0 ##\[\+\] main\.x == 6: PROVED \(1-induction\)$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bdd.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bdd.desc
index 9f6f161ed..94444d682 100644
--- a/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bdd.desc
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bdd.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star1.sv
 --buechi --bdd
 ^\[main.p0\] ##\[\*\] main\.x == 2 ##1 main\.x == 3: PROVED$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-This gives the wrong answer.
diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bmc.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bmc.desc
index 5ea242c3c..67d38fd6a 100644
--- a/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bmc.desc
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star1.bmc.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star1.sv
 --buechi --bound 10
 ^\[main.p0\] ##\[\*\] main\.x == 2 ##1 main\.x == 3: PROVED up to bound 10$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-This gives the wrong answer.
diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star2.bdd.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star2.bdd.desc
index 04c96c413..138256b88 100644
--- a/regression/ebmc-spot/sva-buechi/cycle_delay_star2.bdd.desc
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star2.bdd.desc
@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/cycle_delay_star2.sv
 --buechi --bdd
-^\[main.p0\] ##\[\*\] main\.x == 4: REFUTED$
-^EXIT=10$
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star2.bmc.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star2.bmc.desc
index 4c26aa235..ea8c1d1e2 100644
--- a/regression/ebmc-spot/sva-buechi/cycle_delay_star2.bmc.desc
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star2.bmc.desc
@@ -1,8 +1,8 @@
 CORE
 ../../verilog/SVA/cycle_delay_star2.sv
 --buechi --bound 10
-^\[main.p0\] ##\[\*\] main\.x == 4: REFUTED$
-^EXIT=10$
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star3.bdd.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star3.bdd.desc
index 3063973df..18e7ed920 100644
--- a/regression/ebmc-spot/sva-buechi/cycle_delay_star3.bdd.desc
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star3.bdd.desc
@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star3.sv
 --buechi --bdd
-^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED$
 ^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-We get the wrong answer.
diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star3.bmc.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star3.bmc.desc
index 1aa7b1b28..c0006006c 100644
--- a/regression/ebmc-spot/sva-buechi/cycle_delay_star3.bmc.desc
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star3.bmc.desc
@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 ../../verilog/SVA/cycle_delay_star3.sv
 --buechi --bound 10
 ^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
@@ -7,4 +7,3 @@ KNOWNBUG
 --
 ^warning: ignoring
 --
-We get the wrong answer.
diff --git a/regression/ebmc-spot/sva-buechi/cycle_delay_star4.desc b/regression/ebmc-spot/sva-buechi/cycle_delay_star4.desc
new file mode 100644
index 000000000..484a5bd58
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/cycle_delay_star4.desc
@@ -0,0 +1,13 @@
+CORE
+../../verilog/SVA/cycle_delay_star4.sv
+--buechi
+^\[main\.p0\] main\.x == 0 ##\[\*\] main\.x == 0: PROVED \(1-induction\)$
+^\[main\.p1\] main\.x == 0 ##\[\*\] main\.x == 1: PROVED \(1-induction\)$
+^\[main\.p2\] main\.x == 0 ##\[\*\] main\.x == 2: PROVED \(1-induction\)$
+^\[main\.p3\] main\.x == 1 ##\[\*\] main\.x == 1: REFUTED$
+^\[main\.p4\] main\.x == 0 ##\[\*\] main\.x == 6: PROVED \(1-induction\)$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/cycle_delay_star2.desc b/regression/verilog/SVA/cycle_delay_star2.desc
index 1d2fc78f2..ded49663a 100644
--- a/regression/verilog/SVA/cycle_delay_star2.desc
+++ b/regression/verilog/SVA/cycle_delay_star2.desc
@@ -1,10 +1,9 @@
-KNOWNBUG
+CORE
 cycle_delay_star2.sv
 --bound 10
-^\[main.p0\] ##\[\*\] main\.x == 4: REFUTED$
-^EXIT=10$
+^\[main.p0\] ##\[\*\] main\.x == 4: PROVED up to bound 10$
+^EXIT=0$
 ^SIGNAL=0$
 --
 ^warning: ignoring
 --
-The BMC engine gives the wrong answer.
diff --git a/regression/verilog/SVA/cycle_delay_star2.sv b/regression/verilog/SVA/cycle_delay_star2.sv
index 470d32967..70570805d 100644
--- a/regression/verilog/SVA/cycle_delay_star2.sv
+++ b/regression/verilog/SVA/cycle_delay_star2.sv
@@ -8,7 +8,8 @@ module main(input clk);
   always @(posedge clk)
     if(x<3) x++;
 
-  // fails -- 4 is never reached
+  // 4 is never reached, but this doesn't fail the property
+  // owing to weak sequence semantics.
   initial p0: assert property (##[*] x==4);
 
 endmodule
diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
index 1e0a5994a..d5d288703 100644
--- a/src/temporal-logic/ltl_sva_to_string.cpp
+++ b/src/temporal-logic/ltl_sva_to_string.cpp
@@ -419,17 +419,45 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
   }
   else if(expr.id() == ID_sva_cycle_delay_star) // ##[*] something
   {
+    // ##[*] x ---> 1[*] ; x
+    // w ##[*] x ---> w : 1[*] ; x
     PRECONDITION(mode == SVA_SEQUENCE);
-    auto new_expr = unary_exprt{
-      ID_sva_cycle_delay_star, to_sva_cycle_delay_star_expr(expr).rhs()};
-    return suffix("[*]", new_expr, mode);
+    auto &cycle_delay_expr = to_sva_cycle_delay_star_expr(expr);
+    if(cycle_delay_expr.has_lhs())
+    {
+      auto new_expr = binary_exprt{
+        cycle_delay_expr.lhs(),
+        ID_sva_cycle_delay_star,
+        cycle_delay_expr.rhs()};
+      return infix(" : 1[*] ; ", new_expr, mode);
+    }
+    else
+    {
+      auto new_expr =
+        unary_exprt{ID_sva_cycle_delay_star, cycle_delay_expr.rhs()};
+      return prefix("1[*] ; ", new_expr, mode);
+    }
   }
   else if(expr.id() == ID_sva_cycle_delay_plus) // ##[+] something
   {
+    // ##[+] x ---> 1[+] ; x
+    // w ##[+] x ---> w : 1[+] ; x
     PRECONDITION(mode == SVA_SEQUENCE);
-    auto new_expr = unary_exprt{
-      ID_sva_cycle_delay_star, to_sva_cycle_delay_plus_expr(expr).rhs()};
-    return suffix("[+]", new_expr, mode);
+    auto &cycle_delay_expr = to_sva_cycle_delay_plus_expr(expr);
+    if(cycle_delay_expr.has_lhs())
+    {
+      auto new_expr = binary_exprt{
+        cycle_delay_expr.lhs(),
+        ID_sva_cycle_delay_plus,
+        cycle_delay_expr.rhs()};
+      return infix(" : 1[+] ; ", new_expr, mode);
+    }
+    else
+    {
+      auto new_expr =
+        unary_exprt{ID_sva_cycle_delay_plus, cycle_delay_expr.rhs()};
+      return prefix("1[+] ; ", new_expr, mode);
+    }
   }
   else if(expr.id() == ID_if)
   {
diff --git a/src/verilog/sva_expr.h b/src/verilog/sva_expr.h
index d0ab309e9..6282c7804 100644
--- a/src/verilog/sva_expr.h
+++ b/src/verilog/sva_expr.h
@@ -1203,6 +1203,7 @@ static inline sva_cycle_delay_exprt &to_sva_cycle_delay_expr(exprt &expr)
 class sva_cycle_delay_plus_exprt : public binary_exprt
 {
 public:
+  /// The operands are sequences, the LHS is optional, indicated by nil.
   explicit sva_cycle_delay_plus_exprt(exprt __lhs, exprt __rhs)
     : binary_exprt(
         std::move(__lhs),
@@ -1212,6 +1213,11 @@ class sva_cycle_delay_plus_exprt : public binary_exprt
   {
   }
 
+  bool has_lhs() const
+  {
+    return lhs().is_not_nil();
+  }
+
   // ##[1:$] op
   exprt lower() const;
 };
@@ -1235,6 +1241,7 @@ to_sva_cycle_delay_plus_expr(exprt &expr)
 class sva_cycle_delay_star_exprt : public binary_exprt
 {
 public:
+  /// The operands are a sequences, the LHS is optional, indicated by nil.
   explicit sva_cycle_delay_star_exprt(exprt __lhs, exprt __rhs)
     : binary_exprt(
         std::move(__lhs),
@@ -1244,6 +1251,11 @@ class sva_cycle_delay_star_exprt : public binary_exprt
   {
   }
 
+  bool has_lhs() const
+  {
+    return lhs().is_not_nil();
+  }
+
   // ##[0:$] op
   exprt lower() const;
 };