From 2a83c54961d05fa4b35f930ffccaf318aa9bc8f2 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sat, 12 Jul 2025 15:38:47 -0700
Subject: [PATCH] BMC: exit early if there is no supported property

BMC now exits early if there is no supported property, to prevent wasting
time on generating the SAT instance.
---
 .../ebmc/engine-heuristic/unsupported1.desc   | 10 +++++++
 .../ebmc/engine-heuristic/unsupported1.smv    |  4 +++
 src/ebmc/bmc.cpp                              | 27 +++++++++++++++++++
 3 files changed, 41 insertions(+)
 create mode 100644 regression/ebmc/engine-heuristic/unsupported1.desc
 create mode 100644 regression/ebmc/engine-heuristic/unsupported1.smv

diff --git a/regression/ebmc/engine-heuristic/unsupported1.desc b/regression/ebmc/engine-heuristic/unsupported1.desc
new file mode 100644
index 000000000..0ccf1526d
--- /dev/null
+++ b/regression/ebmc/engine-heuristic/unsupported1.desc
@@ -0,0 +1,10 @@
+CORE
+unsupported1.smv
+
+^\[.*\] EX TRUE: UNKNOWN$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring
+^Generating Decision Problem
+--
diff --git a/regression/ebmc/engine-heuristic/unsupported1.smv b/regression/ebmc/engine-heuristic/unsupported1.smv
new file mode 100644
index 000000000..8ecf0ba35
--- /dev/null
+++ b/regression/ebmc/engine-heuristic/unsupported1.smv
@@ -0,0 +1,4 @@
+MODULE main
+
+-- not supported by k-induction or BMC
+CTLSPEC EX 1
diff --git a/src/ebmc/bmc.cpp b/src/ebmc/bmc.cpp
index 10d19ba63..159e1a6b1 100644
--- a/src/ebmc/bmc.cpp
+++ b/src/ebmc/bmc.cpp
@@ -203,6 +203,25 @@ handles(const exprt::operandst &exprs, decision_proceduret &solver)
   return result;
 }
 
+static bool have_supported_property(ebmc_propertiest &properties)
+{
+  bool have_supported = false;
+
+  for(auto &property : properties.properties)
+  {
+    if(property.is_disabled() || property.is_failure())
+      continue;
+
+    // Is it supported by the BMC engine?
+    if(bmc_supports_property(property.normalized_expr))
+      have_supported = true;
+    else
+      property.failure("property not supported by BMC engine");
+  }
+
+  return have_supported;
+}
+
 property_checker_resultt bmc(
   std::size_t bound,
   bool convert_only,
@@ -216,6 +235,14 @@ property_checker_resultt bmc(
   ebmc_propertiest properties = properties_in;
 
   messaget message(message_handler);
+
+  // exit early if there is no supported property
+  if(!have_supported_property(properties))
+  {
+    message.status() << "No supported property" << messaget::eom;
+    return property_checker_resultt{std::move(properties)};
+  }
+
   message.status() << "Generating Decision Problem" << messaget::eom;
 
   // convert the transition system