Merge pull request #734 from diffblue/fix-R

BMC: fix encoding of `p R q`

Author: tautschnig

regression/ebmc/smv/smv_ltlspec_R1.desc

@@ -2,9 +2,9 @@ CORE broken-smt-backend
 smv_ltlspec_R1.smv
 --bound 10
 ^\[.*\] x >= 1 R x = 1: PROVED up to bound 10$
-^\[.*\] FALSE R x != 4: REFUTED$
+^\[.*\] FALSE R x != 4: PROVED up to bound 10$
 ^\[.*\] x = 2 R x = 1: REFUTED$
-^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: REFUTED$
+^\[.*\] x >= 1 R x = 1 & FALSE R x != 4: PROVED up to bound 10$
 ^\[.*\] x = 2 R x = 1 & x >= 1 R x = 1: REFUTED$
 ^\[.*\] x = 2 R x = 1 \| x >= 1 R x = 1: PROVED up to bound 10$
 ^EXIT=10$

regression/ebmc/smv/smv_ltlspec_R2.desc

@@ -2,7 +2,7 @@ KNOWNBUG broken-smt-backend
 smv_ltlspec_R2.smv
 --bound 10
 ^\[.*\] FALSE R x != 3: REFUTED$
-^Counterexample with 4 states:$
+^Counterexample with 3 states:$
 ^x@0 = 1$
 ^x@1 = 2$
 ^x@2 = 3$

regression/ebmc/smv/smv_ltlspec_R3.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 smv_ltlspec_R3.smv
 --bound 1
 ^\[.*\] FALSE R x != 3: PROVED up to bound 1$
@@ -7,4 +7,3 @@ smv_ltlspec_R3.smv
 --
 ^warning: ignoring
 --
-The counterexample is wrong.

regression/ebmc/smv/smv_ltlspec_R4.desc

@@ -1,4 +1,4 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 smv_ltlspec_R4.smv
 --bound 10
 ^\[.*\] FALSE R x != 0: PROVED up to bound 10$
@@ -7,4 +7,3 @@ smv_ltlspec_R4.smv
 --
 ^warning: ignoring
 --
-Property fails.

src/trans-word-level/property.cpp

@@ -405,30 +405,17 @@ static obligationst property_obligations_rec(
   {
     // we expand: p R q <=> q ∧ (p ∨ X(p R q))
     auto &R_expr = to_R_expr(property_expr);
-    auto tmp_q =
-      property_obligations_rec(R_expr.rhs(), solver, current, no_timeframes, ns)
-        .conjunction()
-        .second;
+    auto &p = R_expr.lhs();
+    auto &q = R_expr.rhs();
 
-    auto tmp_p =
-      property_obligations_rec(R_expr.lhs(), solver, current, no_timeframes, ns)
-        .conjunction()
-        .second;
+    // Once we reach the end of the unwinding, we replace X(p R q) by
+    // true, and hence the expansion becomes "q" only.
+    exprt expansion = (current + 1) < no_timeframes
+                        ? and_exprt{q, or_exprt{p, X_exprt{property_expr}}}
+                        : q;
 
-    const auto next = current + 1;
-    exprt expansion;
-
-    if(next < no_timeframes)
-    {
-      auto obligations_rec = property_obligations_rec(
-        property_expr, solver, next, no_timeframes, ns);
-      expansion = or_exprt{tmp_p, obligations_rec.conjunction().second};
-    }
-    else
-      expansion = tmp_p;
-
-    DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-    return obligationst{no_timeframes - 1, and_exprt{tmp_q, expansion}};
+    return property_obligations_rec(
+      expansion, solver, current, no_timeframes, ns);
   }
   else if(
     property_expr.id() == ID_sva_until_with ||