From 6b599ed5d745b8393fb309f1c8357921890973e8 Mon Sep 17 00:00:00 2001
From: Daniel Kroening <dkr@amazon.com>
Date: Sun, 21 Apr 2024 17:42:52 -0700
Subject: [PATCH] BMC now splits up top-level conjunction

BMC on a property with a top-level conjunction now splits up conjunctions,
to form separate sets of obligations.
---
 regression/ebmc/smv/module1.desc  |  8 ++++++++
 regression/ebmc/smv/module1.smv   | 13 +++++++++++++
 src/trans-word-level/property.cpp | 14 ++++++++++++++
 3 files changed, 35 insertions(+)
 create mode 100644 regression/ebmc/smv/module1.desc
 create mode 100644 regression/ebmc/smv/module1.smv

diff --git a/regression/ebmc/smv/module1.desc b/regression/ebmc/smv/module1.desc
new file mode 100644
index 000000000..2f569395d
--- /dev/null
+++ b/regression/ebmc/smv/module1.desc
@@ -0,0 +1,8 @@
+CORE
+module1.smv
+--bound 10
+^EXIT=0$
+^SIGNAL=0$
+^\[main::spec1\] AG main::var::subA.flag & AG main::var::subB.flag: PROVED up to bound 10$
+--
+^warning: ignoring
diff --git a/regression/ebmc/smv/module1.smv b/regression/ebmc/smv/module1.smv
new file mode 100644
index 000000000..8b338a9e2
--- /dev/null
+++ b/regression/ebmc/smv/module1.smv
@@ -0,0 +1,13 @@
+MODULE main
+
+VAR subA : my-module;
+    subB : my-module;
+
+SPEC AG subA.flag & AG subB.flag
+
+MODULE my-module
+
+VAR flag : boolean;
+
+ASSIGN init(flag) := 1;
+ASSIGN next(flag) := 1;
diff --git a/src/trans-word-level/property.cpp b/src/trans-word-level/property.cpp
index 6061b10cd..baa77a3f3 100644
--- a/src/trans-word-level/property.cpp
+++ b/src/trans-word-level/property.cpp
@@ -41,6 +41,14 @@ bool bmc_supports_property(const exprt &expr)
   {
     if(!has_temporal_operator(expr))
       return true; // initial state only
+    else if(
+      expr.id() == ID_and || expr.id() == ID_or || expr.id() == ID_implies)
+    {
+      for(auto &op : expr.operands())
+        if(!bmc_supports_property(op))
+          return false;
+      return true;
+    }
     else
       return false;
   }
@@ -153,6 +161,12 @@ static void property_obligations_rec(
       property_obligations_rec(phi, solver, c, no_timeframes, ns, obligations);
     }
   }
+  else if(property_expr.id() == ID_and)
+  {
+    for(auto &op : to_and_expr(property_expr).operands())
+      property_obligations_rec(
+        op, solver, current, no_timeframes, ns, obligations);
+  }
   else
   {
     // current state property