Merge pull request #1188 from diffblue/buechi-unsupported

Buechi: mark unconverted properties as unsupported

Author: kroening

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

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

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;
     }
 

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);
 }