Merge pull request #1132 from diffblue/buechi-sva-s_until_with

SVA-to-Buechi: release/until operators

Author: tautschnig

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
+--

src/temporal-logic/ltl_sva_to_string.cpp

@@ -267,13 +267,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 ||