SVA-to-Buechi: eventually

regression/ebmc-spot/sva-buechi/eventually1.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/eventually1.sv
+--buechi --bound 20
+^\[main\.p0\] always \(main\.counter == 1 implies \(eventually \[1:2\] main\.counter == 3\)\): PROVED up to bound 20$
+^EXIT=0$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc-spot/sva-buechi/eventually2.desc

@@ -0,0 +1,8 @@
+CORE
+../../verilog/SVA/eventually2.sv
+--buechi --bound 20
+^\[main\.p0\] always \(eventually \[0:2\] main\.counter == 3\): REFUTED$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

src/temporal-logic/ltl_sva_to_string.cpp

@@ -184,20 +184,21 @@ ltl_sva_to_stringt::rec(const exprt &expr, modet mode)
     PRECONDITION(mode == PROPERTY);
     return prefix("F", expr, mode);
   }
-  else if(expr.id() == ID_sva_ranged_s_eventually)
+  else if(
+    expr.id() == ID_sva_ranged_s_eventually || expr.id() == ID_sva_eventually)
   {
     PRECONDITION(mode == PROPERTY);
-    auto &s_eventually = to_sva_ranged_s_eventually_expr(expr);
-    auto new_expr = unary_exprt{ID_sva_ranged_s_eventually, s_eventually.op()};
-    auto lower = numeric_cast_v<mp_integer>(s_eventually.lower());
-    if(!s_eventually.is_range())
+    auto &eventually = to_sva_ranged_predicate_exprt(expr);
+    auto new_expr = unary_exprt{expr.id(), eventually.op()};
+    auto lower = numeric_cast_v<mp_integer>(eventually.lower());
+    if(!eventually.is_range())
       return prefix("F[" + integer2string(lower) + "]", new_expr, mode);
-    else if(s_eventually.is_unbounded())
+    else if(eventually.is_unbounded())
       return prefix("F[" + integer2string(lower) + ":]", new_expr, mode);
     else
     {
       auto upper =
-        numeric_cast_v<mp_integer>(to_constant_expr(s_eventually.upper()));
+        numeric_cast_v<mp_integer>(to_constant_expr(eventually.upper()));
       return prefix(
         "F[" + integer2string(lower) + ":" + integer2string(upper) + "]",
         new_expr,

src/verilog/sva_expr.h

@@ -330,6 +330,20 @@ class sva_ranged_predicate_exprt : public ternary_exprt
   using ternary_exprt::op2;
 };
 
+static inline const sva_ranged_predicate_exprt &
+to_sva_ranged_predicate_exprt(const exprt &expr)
+{
+  sva_ranged_predicate_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<const sva_ranged_predicate_exprt &>(expr);
+}
+
+static inline sva_ranged_predicate_exprt &
+to_sva_ranged_predicate_exprt(exprt &expr)
+{
+  sva_ranged_predicate_exprt::check(expr, validation_modet::INVARIANT);
+  return static_cast<sva_ranged_predicate_exprt &>(expr);
+}
+
 /// A specialisation of sva_ranged_predicate_exprt where both bounds
 /// are constants.
 class sva_bounded_range_predicate_exprt : public sva_ranged_predicate_exprt