diff --git a/regression/ebmc-spot/sva-buechi/followed-by5.bdd.desc b/regression/ebmc-spot/sva-buechi/followed-by5.bdd.desc
new file mode 100644
index 00000000..cb27fa82
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/followed-by5.bdd.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+followed-by5.sv
+--buechi --bdd
+^\[main\.p0\] \(1 \[\*0\]\) #=# main\.x == 0: PROVED$
+^\[main\.p1\] \(1 \[\*0\]\) #-# 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Empty LHS sequences are not implemented.
diff --git a/regression/ebmc-spot/sva-buechi/followed-by5.bmc.desc b/regression/ebmc-spot/sva-buechi/followed-by5.bmc.desc
new file mode 100644
index 00000000..3040b72c
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/followed-by5.bmc.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+followed-by5.sv
+--buechi --bound 2
+^\[main\.p0\] \(1 \[\*0\]\) #=# main\.x == 0: PROVED$
+^\[main\.p1\] \(1 \[\*0\]\) #-# 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Empty LHS sequences are not implemented.
diff --git a/regression/verilog/SVA/followed-by5.bdd.desc b/regression/verilog/SVA/followed-by5.bdd.desc
new file mode 100644
index 00000000..259f923b
--- /dev/null
+++ b/regression/verilog/SVA/followed-by5.bdd.desc
@@ -0,0 +1,10 @@
+CORE
+followed-by5.sv
+--bdd
+^\[main\.p0\] \(1 \[\*0\]\) #=# main\.x == 0: PROVED$
+^\[main\.p1\] \(1 \[\*0\]\) #-# 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/verilog/SVA/followed-by5.bmc.desc b/regression/verilog/SVA/followed-by5.bmc.desc
new file mode 100644
index 00000000..41eb5269
--- /dev/null
+++ b/regression/verilog/SVA/followed-by5.bmc.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+followed-by5.sv
+--bound 2
+^\[main\.p0\] \(1 \[\*0\]\) #=# main\.x == 0: PROVED$
+^\[main\.p1\] \(1 \[\*0\]\) #-# 1: REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
+Empty LHS sequences are not implemented.
diff --git a/regression/verilog/SVA/followed-by5.sv b/regression/verilog/SVA/followed-by5.sv
new file mode 100644
index 00000000..e35c6a3b
--- /dev/null
+++ b/regression/verilog/SVA/followed-by5.sv
@@ -0,0 +1,17 @@
+module main(input clk);
+
+  reg [31:0] x;
+
+  initial x=0;
+
+  // 0, 1, ...
+  always @(posedge clk)
+    x<=x+1;
+
+  // expected to pass: the rhs is evaluated in time frame 0
+  initial p0: assert property (1[*0] #=# x==0);
+
+  // expected to fail: the lhs is empty, and the rhs overlaps with the lhs
+  initial p1: assert property (1[*0] #-# 1);
+
+endmodule