diff --git a/regression/ebmc-spot/sva-buechi/sequence2.desc b/regression/ebmc-spot/sva-buechi/sequence2.desc
new file mode 100644
index 000000000..974f6c1ef
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sequence2.desc
@@ -0,0 +1,10 @@
+CORE
+../../verilog/SVA/sequence2.sv
+--buechi --bound 10
+^\[main\.p0] weak\(##\[0:\$\] main\.x == 10\): PROVED up to bound 10$
+^\[main\.p1] strong\(##\[0:\$\] main\.x == 10\): UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/regression/ebmc-spot/sva-buechi/strong1.desc b/regression/ebmc-spot/sva-buechi/strong1.desc
new file mode 100644
index 000000000..aee695e79
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/strong1.desc
@@ -0,0 +1,9 @@
+CORE
+../../verilog/SVA/strong1.sv
+--buechi --bound 4
+^\[main\.p0\] strong\(##\[0:9\] main\.x == 5\): UNSUPPORTED: not convertible to Buechi$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/src/ebmc/instrument_buechi.cpp b/src/ebmc/instrument_buechi.cpp
index ba95ebebc..d94adcf8a 100644
--- a/src/ebmc/instrument_buechi.cpp
+++ b/src/ebmc/instrument_buechi.cpp
@@ -27,6 +27,7 @@ void instrument_buechi(
       !is_LTL(property.normalized_expr) &&
       !is_Buechi_SVA(property.normalized_expr))
     {
+      property.unsupported("not convertible to Buechi");
       continue;
     }
 
diff --git a/src/temporal-logic/temporal_logic.cpp b/src/temporal-logic/temporal_logic.cpp
index a93d55d63..2ae4155f1 100644
--- a/src/temporal-logic/temporal_logic.cpp
+++ b/src/temporal-logic/temporal_logic.cpp
@@ -217,7 +217,18 @@ std::optional<exprt> LTL_to_CTL(exprt expr)
 bool is_Buechi_SVA(const exprt &expr)
 {
   auto unsupported_operator = [](const exprt &expr)
-  { return is_temporal_operator(expr) && !is_SVA_operator(expr); };
+  {
+    // ltl2tgba produces the wrong anser for [->n] and [=n]
+    if(
+      expr.id() == ID_sva_implicit_strong || expr.id() == ID_sva_strong ||
+      expr.id() == ID_sva_sequence_goto_repetition ||
+      expr.id() == ID_sva_sequence_non_consecutive_repetition)
+    {
+      return true;
+    }
+    else
+      return is_temporal_operator(expr) && !is_SVA_operator(expr);
+  };
 
   return !has_subexpr(expr, unsupported_operator);
 }