diff --git a/regression/ebmc-spot/sva-buechi/sva_until1.desc b/regression/ebmc-spot/sva-buechi/sva_until1.desc
new file mode 100644
index 000000000..8a704ecc2
--- /dev/null
+++ b/regression/ebmc-spot/sva-buechi/sva_until1.desc
@@ -0,0 +1,11 @@
+CORE
+../../verilog/SVA/sva_until1.sv
+--buechi
+^\[main\.p0\] always \(main.a until_with main.b\): REFUTED$
+^\[main\.p1\] always \(main.a until main.b\): REFUTED$
+^\[main\.p2\] always \(main.a s_until main.b\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+--
diff --git a/src/temporal-logic/ltl_sva_to_string.cpp b/src/temporal-logic/ltl_sva_to_string.cpp
index 10729071d..6481757ee 100644
--- a/src/temporal-logic/ltl_sva_to_string.cpp
+++ b/src/temporal-logic/ltl_sva_to_string.cpp
@@ -249,13 +249,27 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     PRECONDITION(mode == PROPERTY);
     return infix(" U ", expr, mode);
   }
+  else if(expr.id() == ID_sva_until)
+  {
+    PRECONDITION(mode == PROPERTY);
+    return infix(" W ", expr, mode);
+  }
   else if(expr.id() == ID_sva_s_until_with)
   {
-    // This is release with swapped operands
+    // This is strong release with swapped operands
     PRECONDITION(mode == PROPERTY);
     auto &until_with = to_sva_s_until_with_expr(expr);
-    auto R = R_exprt{until_with.rhs(), until_with.lhs()}; // swapped
-    return rec(R, mode);
+    auto new_expr =
+      strong_R_exprt{until_with.rhs(), until_with.lhs()}; // swapped
+    return infix(" M ", new_expr, mode);
+  }
+  else if(expr.id() == ID_sva_until_with)
+  {
+    // This is weak release with swapped operands
+    PRECONDITION(mode == PROPERTY);
+    auto &until_with = to_sva_until_with_expr(expr);
+    auto new_expr = R_exprt{until_with.rhs(), until_with.lhs()}; // swapped
+    return infix(" R ", new_expr, mode);
   }
   else if(
     expr.id() == ID_sva_weak || expr.id() == ID_sva_strong ||