Merge pull request #897 from diffblue/not_supported2

IC3: only SVA always is supported
diffblue · Jan 3, 2025 · 16d8bf7 · 16d8bf7
2 parents 0aada25 + 9a4f20c
commit 16d8bf7
Show file tree

Hide file tree

Showing 3 changed files with 11 additions and 8 deletions.
diff --git a/regression/ebmc/ic3/not_supported2.desc b/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$
+--
diff --git a/regression/ebmc/ic3/not_supported2.smv b/regression/ebmc/ic3/not_supported2.smv
@@ -0,0 +1,4 @@
+MODULE main
+
+-- not yet supported by IC3
+SPEC AG 1
diff --git a/src/ic3/m1ain.cc b/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());