Merge pull request #897 from diffblue/not_supported2

IC3: only SVA always is supported

Author: tautschnig

regression/ebmc/ic3/not_supported2.desc

@@ -0,0 +1,7 @@
+CORE
+not_supported2.smv
+--ic3
+^\[.*\] AG TRUE: FAILURE: property not supported by IC3 engine$
+^EXIT=10$
+^SIGNAL=0$
+--

regression/ebmc/ic3/not_supported2.smv

@@ -0,0 +1,4 @@
+MODULE main
+
+-- not yet supported by IC3
+SPEC AG 1

src/ic3/m1ain.cc

@@ -60,14 +60,6 @@ bool ic3_supports_property(const exprt &expr)
 {
   if(!is_temporal_operator(expr))
     return false;
-  else if(expr.id() == ID_AG)
-  {
-    return !has_temporal_operator(to_AG_expr(expr).op());
-  }
-  else if(expr.id() == ID_G)
-  {
-    return !has_temporal_operator(to_G_expr(expr).op());
-  }
   else if(expr.id() == ID_sva_always)
   {
     return !has_temporal_operator(to_sva_always_expr(expr).op());