Merge pull request #1187 from diffblue/k-induction-fail-early

k-induction: fail early when there is no suitable property

Author: tautschnig

src/ebmc/k_induction.cpp

@@ -104,6 +104,22 @@ property_checker_resultt k_induction(
   // copy
   auto properties_copy = properties;
 
+  // Are there any properties suitable for k-induction?
+  // Fail early if not.
+  if(!k_inductiont::have_supported_property(properties.properties))
+  {
+    for(auto &property : properties_copy.properties)
+    {
+      if(
+        !property.is_assumed() && !property.is_disabled() &&
+        !property.is_proved())
+      {
+        property.unsupported("unsupported by k-induction");
+      }
+    }
+    return property_checker_resultt{properties_copy};
+  }
+
   k_inductiont(
     k, transition_system, properties_copy, solver_factory, message_handler)();