simplify false R ψ to G ψ

This simplification enables printing shorter counterexample traces.

Author: kroening

regression/smv/LTL/smv_ltlspec_R2.desc

@@ -1,6 +1,6 @@
-KNOWNBUG broken-smt-backend
+CORE
 smv_ltlspec_R2.smv
---bound 10
+--bound 10 --numbered-trace
 ^\[.*\] FALSE V x != 3: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = 1$
@@ -11,4 +11,3 @@ smv_ltlspec_R2.smv
 --
 ^warning: ignoring
 --
-The trace has too many states.

regression/smv/LTL/smv_ltlspec_V2.desc

@@ -1,6 +1,6 @@
-KNOWNBUG broken-smt-backend
+CORE
 smv_ltlspec_V2.smv
---bound 10
+--bound 10 --numbered-trace
 ^\[.*\] FALSE V x != 3: REFUTED$
 ^Counterexample with 3 states:$
 ^x@0 = 1$
@@ -11,4 +11,3 @@ smv_ltlspec_V2.smv
 --
 ^warning: ignoring
 --
-The trace has too many states.

src/temporal-logic/normalize_property.cpp

@@ -103,6 +103,14 @@ exprt normalize_property_rec(exprt expr)
     op = normalize_property_rec(op); // recursive call
 
   // post-traversal
+  if(expr.id() == ID_R)
+  {
+    if(to_R_expr(expr).lhs().is_false())
+    {
+      // false R ψ ≡ G ψ
+      expr = G_exprt{to_R_expr(expr).rhs()};
+    }
+  }
 
   return expr;
 }

src/temporal-logic/normalize_property.h

@@ -40,6 +40,7 @@ Author: Daniel Kroening, dkr@amazon.com
 /// ¬¬φ --> φ
 /// ¬Gφ --> F¬φ
 /// ¬Fφ --> G¬φ
+/// false R ψ --> G ψ
 exprt normalize_property(exprt);
 
 #endif