BMC: fix encoding of p U q

p U q can be refuted using a ¬q loop.

regression/ebmc/smv/smv_ltlspec_U1.desc

@@ -1,11 +1,13 @@
 CORE broken-smt-backend
 smv_ltlspec_U1.smv
---bound 10
-\[.*\] x = 1 U x = 2: PROVED up to bound 10$
-\[.*\] x != 0 U FALSE: PROVED up to bound 10$
+--bound 3
+\[.*\] TRUE U x = 3: PROVED up to bound 3$
+\[.*\] x = 1 U x = 2: PROVED up to bound 3$
+\[.*\] x <= 2 U x = 3: PROVED up to bound 3$
+\[.*\] x != 0 U FALSE: REFUTED$
 \[.*\] x = 1 U x = 3: REFUTED$
-\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: PROVED up to bound 10$
-\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: PROVED up to bound 10$
+\[.*\] x = 1 U x = 2 & x <= 2 U x = 3: PROVED up to bound 3$
+\[.*\] x = 1 U x = 2 \| x = 1 U x = 3: PROVED up to bound 3$
 ^EXIT=10$
 ^SIGNAL=0$
 --

regression/ebmc/smv/smv_ltlspec_U1.smv

@@ -5,14 +5,17 @@ VAR x : 0..10;
 ASSIGN
   init(x) := 1;
 
+  -- 1, 2, 3, 3, 3...
   next(x) :=
     case
       x>=3 : 3;
       TRUE: x+1;
     esac;
 
+LTLSPEC TRUE U x = 3 -- should pass
 LTLSPEC x = 1 U x = 2 -- should pass
-LTLSPEC x !=0 U FALSE -- should pass
+LTLSPEC x <= 2 U x = 3 -- should pass
+LTLSPEC x !=0 U FALSE -- should fail, "FALSE" never becomes true
 LTLSPEC x = 1 U x = 3 -- should fail
-LTLSPEC x = 1 U x = 2 & x<=2 U x = 3 -- should pass
+LTLSPEC x = 1 U x = 2 & x <= 2 U x = 3 -- should pass
 LTLSPEC x = 1 U x = 2 | x = 1 U x = 3 -- should pass

regression/ebmc/smv/smv_ltlspec_U2.desc

@@ -1,6 +1,6 @@
-KNOWNBUG broken-smt-backend
+CORE broken-smt-backend
 smv_ltlspec_U2.smv
---bound 10
+--bound 10 --numbered-trace
 ^\[.*\] TRUE U x = 0: REFUTED$
 ^Counterexample with 4 states:$
 ^x@0 = 1$
@@ -12,4 +12,3 @@ smv_ltlspec_U2.smv
 --
 ^warning: ignoring
 --
-The property is proven, but should be refuted.

src/hw_cbmc_irep_ids.h

@@ -9,6 +9,7 @@ IREP_ID_ONE(EX)
 IREP_ID_ONE(EU)
 IREP_ID_ONE(ER)
 IREP_ID_ONE(U)
+IREP_ID_ONE(weak_U)
 IREP_ID_ONE(R)
 IREP_ID_ONE(A)
 IREP_ID_ONE(F)

src/temporal-logic/temporal_expr.h

@@ -143,6 +143,7 @@ static inline G_exprt &to_G_expr(exprt &expr)
   return static_cast<G_exprt &>(expr);
 }
 
+/// strong until
 class U_exprt : public binary_predicate_exprt
 {
 public:
@@ -166,6 +167,30 @@ static inline U_exprt &to_U_expr(exprt &expr)
   return static_cast<U_exprt &>(expr);
 }
 
+/// weak until
+class weak_U_exprt : public binary_predicate_exprt
+{
+public:
+  explicit weak_U_exprt(exprt op0, exprt op1)
+    : binary_predicate_exprt(std::move(op0), ID_weak_U, std::move(op1))
+  {
+  }
+};
+
+static inline const weak_U_exprt &to_weak_U_expr(const exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_weak_U);
+  weak_U_exprt::check(expr);
+  return static_cast<const weak_U_exprt &>(expr);
+}
+
+static inline weak_U_exprt &to_weak_U_expr(exprt &expr)
+{
+  PRECONDITION(expr.id() == ID_weak_U);
+  weak_U_exprt::check(expr);
+  return static_cast<weak_U_exprt &>(expr);
+}
+
 class EU_exprt : public binary_predicate_exprt
 {
 public:

src/trans-word-level/lasso.cpp

@@ -156,7 +156,7 @@ bool requires_lasso_constraints(const exprt &expr)
       subexpr_it->id() == ID_sva_until || subexpr_it->id() == ID_sva_s_until ||
       subexpr_it->id() == ID_sva_eventually ||
       subexpr_it->id() == ID_sva_s_eventually || subexpr_it->id() == ID_AF ||
-      subexpr_it->id() == ID_F)
+      subexpr_it->id() == ID_F || subexpr_it->id() == ID_U)
     {
       return true;
     }

src/trans-word-level/obligations.cpp

@@ -22,3 +22,9 @@ std::pair<mp_integer, exprt> obligationst::conjunction() const
   }
   return {max, ::conjunction(conjuncts)};
 }
+
+obligationst obligations_union(obligationst a, obligationst b)
+{
+  a.add(b);
+  return a;
+}

src/trans-word-level/obligations.h

@@ -58,4 +58,6 @@ class obligationst
   std::pair<mp_integer, exprt> conjunction() const;
 };
 
+obligationst obligations_union(obligationst, obligationst);
+
 #endif

src/trans-word-level/property.cpp

@@ -380,32 +380,26 @@ static obligationst property_obligations_rec(
     property_expr.id() == ID_sva_until ||
     property_expr.id() == ID_sva_s_until || property_expr.id() == ID_U)
   {
-    // non-overlapping until
-    // we need a lasso to refute these
-
-    // we expand: p U q <=> q ∨ (p ∧ X(p U q))
-    exprt tmp_q = to_binary_expr(property_expr).op1();
-    tmp_q = property_obligations_rec(tmp_q, solver, current, no_timeframes, ns)
-              .conjunction()
-              .second;
-
-    exprt expansion = to_binary_expr(property_expr).op0();
-    expansion =
-      property_obligations_rec(expansion, solver, current, no_timeframes, ns)
-        .conjunction()
-        .second;
+    auto &p = to_binary_expr(property_expr).lhs();
+    auto &q = to_binary_expr(property_expr).rhs();
 
-    const auto next = current + 1;
+    // p U q ≡ Fq ∧ (p W q)
+    exprt tmp = and_exprt{F_exprt{q}, weak_U_exprt{p, q}};
 
-    if(next < no_timeframes)
-    {
-      auto obligations_rec = property_obligations_rec(
-        property_expr, solver, next, no_timeframes, ns);
-      expansion = and_exprt{expansion, obligations_rec.conjunction().second};
-    }
+    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
+  }
+  else if(property_expr.id() == ID_weak_U)
+  {
+    // we expand: p W q ≡ q ∨ ( p ∧ X(p W q) )
+    auto &p = to_weak_U_expr(property_expr).lhs();
+    auto &q = to_weak_U_expr(property_expr).rhs();
 
-    DATA_INVARIANT(no_timeframes != 0, "must have timeframe");
-    return obligationst{no_timeframes - 1, or_exprt{tmp_q, expansion}};
+    // Once we reach the end of the unwinding, replace X(p W q) by 'true'.
+    auto tmp = or_exprt{
+      q,
+      (current + 1) < no_timeframes ? and_exprt{p, X_exprt{property_expr}} : p};
+
+    return property_obligations_rec(tmp, solver, current, no_timeframes, ns);
   }
   else if(property_expr.id() == ID_R)
   {