Temporal Logic: fix s_until_with lowering for BDD

Lower sva_s_until_with to strong release in SVA_to_LTL and teach
LTL_to_CTL to handle strong_R so the BDD engine can check these
properties. Promote the regression added in #1998 from KNOWNBUG to
CORE.

Author: kroening

CHANGELOG

@@ -1,5 +1,6 @@
 # EBMC 6.1
 
+* Fix for lowering of s_until_with to LTL
 * Verilog: $root.
 * Verilog: procedural assignments to hierarchical identifiers
 * SystemVerilog: ports for sequence and property declarations

regression/ebmc/SVA-LTL/s_until_with1.desc

@@ -1,4 +1,4 @@
-KNOWNBUG
+CORE
 s_until_with1.sv
 --bdd
 ^\[main\.p0\] always \(0 s_until_with 1\): REFUTED$

src/temporal-logic/sva_to_ltl.cpp

@@ -228,11 +228,11 @@ exprt SVA_to_LTL(exprt expr)
   }
   else if(expr.id() == ID_sva_s_until_with)
   {
-    // This is release with swapped operands
+    // This is strong release with swapped operands.
     auto &until_with = to_sva_s_until_with_expr(expr);
     auto rec_lhs = SVA_to_LTL(until_with.lhs());
     auto rec_rhs = SVA_to_LTL(until_with.rhs());
-    return R_exprt{rec_rhs, rec_lhs}; // swapped
+    return strong_R_exprt{rec_rhs, rec_lhs}; // swapped
   }
   else if(!has_temporal_operator(expr))
   {

src/temporal-logic/temporal_logic.cpp

@@ -70,7 +70,8 @@ bool is_CTL(const exprt &expr)
 bool is_LTL_operator(const exprt &expr)
 {
   auto id = expr.id();
-  return id == ID_G || id == ID_F || id == ID_X || id == ID_U || id == ID_R;
+  return id == ID_G || id == ID_F || id == ID_X || id == ID_U || id == ID_R ||
+         id == ID_strong_R;
 }
 
 bool is_LTL_past_operator(const exprt &expr)
@@ -217,6 +218,18 @@ std::optional<exprt> LTL_to_CTL(exprt expr)
     else
       return {};
   }
+  else if(expr.id() == ID_strong_R)
+  {
+    auto &strong_R = to_strong_R_expr(expr);
+    auto rec_lhs = LTL_to_CTL(strong_R.lhs());
+    auto rec_rhs = LTL_to_CTL(strong_R.rhs());
+    if(rec_lhs.has_value() && rec_rhs.has_value())
+    {
+      return and_exprt{AF_exprt{*rec_lhs}, AR_exprt{*rec_lhs, *rec_rhs}};
+    }
+    else
+      return {};
+  }
   else
     return {};
 }