trace length for disjunctive properties

Given a property a ∨ b with obligations at timeframe l and m, generate the
obligation for the disjunction at timeframe max{l, m}.

Author: kroening

regression/ebmc/traces/disjunction1.desc

@@ -0,0 +1,12 @@
+CORE broken-smt-backend
+disjunction1.smv
+--bound 20 --numbered-trace
+^\[spec1\] G \(X FALSE \| X X FALSE\): REFUTED$
+^Counterexample with 3 states:$
+^i@0 = 0$
+^i@1 = 1$
+^i@2 = 2$
+^EXIT=10$
+^SIGNAL=0$
+--
+^warning: ignoring

regression/ebmc/traces/disjunction1.smv

@@ -0,0 +1,12 @@
+MODULE main
+
+VAR i: 0..20;
+
+ASSIGN init(i) := 0;
+       next(i) := case
+         i >= 10 : 10;
+         TRUE   : i + 1;
+       esac;
+
+-- we need to see a trace with three states
+LTLSPEC G ((X FALSE) | (X X FALSE))

src/trans-word-level/property.cpp

@@ -78,6 +78,54 @@ bool bmc_supports_property(const exprt &expr)
 
 /*******************************************************************\
 
+Function: max_property_obligation
+
+  Inputs:
+
+ Outputs:
+
+ Purpose:
+
+\*******************************************************************/
+
+static void property_obligations_rec(
+  const exprt &property_expr,
+  decision_proceduret &,
+  const mp_integer &current,
+  const mp_integer &no_timeframes,
+  const namespacet &,
+  std::map<mp_integer, exprt::operandst> &obligations);
+
+static std::pair<mp_integer, exprt> max_property_obligation(
+  const exprt &property_expr,
+  decision_proceduret &solver,
+  const mp_integer &current,
+  const mp_integer &no_timeframes,
+  const namespacet &ns)
+{
+  // Generate one obligation, equivalent to the conjunction
+  // for the maximum timeframe.
+
+  std::map<mp_integer, exprt::operandst> obligations;
+
+  property_obligations_rec(
+    property_expr, solver, current, no_timeframes, ns, obligations);
+
+  exprt::operandst conjuncts;
+  mp_integer max_timeframe = 0;
+
+  for(auto &[timeframe, exprs] : obligations)
+  {
+    max_timeframe = std::max(max_timeframe, timeframe);
+    for(auto &conjunct : exprs)
+      conjuncts.push_back(conjunct);
+  }
+
+  return std::pair<mp_integer, exprt>{max_timeframe, conjunction(conjuncts)};
+}
+
+/*******************************************************************\
+
 Function: property_obligations_rec
 
   Inputs:
@@ -198,10 +246,28 @@ static void property_obligations_rec(
   }
   else if(property_expr.id() == ID_and)
   {
+    // generate seperate obligations for each conjunct
     for(auto &op : to_and_expr(property_expr).operands())
       property_obligations_rec(
         op, solver, current, no_timeframes, ns, obligations);
   }
+  else if(property_expr.id() == ID_or)
+  {
+    // generate one obligation, equivalent to the disjunction,
+    // for the maximum timeframe
+    mp_integer max_timeframe = 0;
+    exprt::operandst disjuncts;
+
+    for(auto &op : to_or_expr(property_expr).operands())
+    {
+      auto obligation =
+        max_property_obligation(op, solver, current, no_timeframes, ns);
+      max_timeframe = std::max(max_timeframe, obligation.first);
+      disjuncts.push_back(obligation.second);
+    }
+
+    obligations[max_timeframe].push_back(disjunction(disjuncts));
+  }
   else
   {
     // current state property