Merge pull request #453 from diffblue/bmc-top-level-conjuction

BMC now splits up top-level conjunction

regression/ebmc/smv/module1.desc

@@ -0,0 +1,8 @@
+CORE
+module1.smv
+--bound 10
+^EXIT=0$
+^SIGNAL=0$
+^\[main::spec1\] AG subA.flag & AG subB.flag: PROVED up to bound 10$
+--
+^warning: ignoring

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;

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;
   }
@@ -188,6 +196,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