weak, strong and implicit SVA sequence properties are SVA operators

is_SVA_operator(...) now recognizes weak, strong and implicit SVA sequence
properties.

Author: kroening

src/ebmc/completeness_threshold.cpp

@@ -63,6 +63,16 @@ bool has_low_completeness_threshold(const exprt &expr)
              upper_int <= 1;
     }
   }
+  else if(
+    expr.id() == ID_sva_strong || expr.id() == ID_sva_weak ||
+    expr.id() == ID_sva_sequence_property)
+  {
+    auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
+    if(!is_SVA_sequence_operator(sequence))
+      return true;
+    else
+      return false;
+  }
   else
     return false;
 }

src/temporal-logic/temporal_logic.cpp

@@ -132,7 +132,9 @@ bool is_SVA_operator(const exprt &expr)
          id == ID_sva_overlapped_implication ||
          id == ID_sva_non_overlapped_implication ||
          id == ID_sva_overlapped_followed_by ||
-         id == ID_sva_nonoverlapped_followed_by;
+         id == ID_sva_nonoverlapped_followed_by ||
+         id == ID_sva_sequence_property || id == ID_sva_weak ||
+         id == ID_sva_strong;
 }
 
 bool is_SVA(const exprt &expr)

src/trans-word-level/property.cpp

@@ -527,10 +527,23 @@ static obligationst property_obligations_rec(
       return property_obligations_rec(
         op_negated_opt.value(), current, no_timeframes);
     }
-    else if(is_SVA_sequence_operator(op))
+    else if(
+      op.id() == ID_sva_strong || op.id() == ID_sva_weak ||
+      op.id() == ID_sva_sequence_property)
     {
-      return obligationst{
-        instantiate_property(property_expr, current, no_timeframes)};
+      // The sequence must not match.
+      auto &sequence = to_sva_sequence_property_expr_base(op).sequence();
+
+      const auto matches =
+        instantiate_sequence(sequence, current, no_timeframes);
+      obligationst obligations;
+
+      for(auto &match : matches)
+      {
+        obligations.add(match.end_time, not_exprt{match.condition});
+      }
+
+      return obligations;
     }
     else if(is_temporal_operator(op))
     {