Merge pull request #1067 from diffblue/sva_sequence_property

weak, strong and implicit SVA sequence properties are SVA operators

Author: tautschnig

src/ebmc/completeness_threshold.cpp

@@ -63,6 +63,20 @@ 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_implicit_strong || expr.id() == ID_sva_implicit_weak)
+  {
+    auto &sequence = to_sva_sequence_property_expr_base(expr).sequence();
+    if(!is_SVA_sequence_operator(sequence))
+      return true;
+    else
+      return false;
+  }
+  else if(expr.id() == ID_sva_sequence_property)
+  {
+    PRECONDITION(false); // should have been turned into implicit weak/strong
+  }
   else
     return false;
 }

src/temporal-logic/temporal_logic.cpp

@@ -132,7 +132,10 @@ 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 || id == ID_sva_implicit_weak ||
+         id == ID_sva_implicit_strong;
 }
 
 bool is_SVA(const exprt &expr)