fix trivial_sva(...)

The rewrites in trivial_sva that depend on the operands must be done
post-traversal, not pre-traversal.

Author: kroening

src/temporal-logic/trivial_sva.cpp

@@ -23,6 +23,12 @@ static std::optional<exprt> is_state_predicate(const exprt &expr)
 exprt trivial_sva(exprt expr)
 {
   // pre-traversal
+
+  // rewrite the operands, recursively
+  for(auto &op : expr.operands())
+    op = trivial_sva(op);
+
+  // post-traversal
   if(expr.id() == ID_sva_overlapped_implication)
   {
     // Same as regular implication if lhs and rhs are not sequences.
@@ -115,13 +121,7 @@ exprt trivial_sva(exprt expr)
   {
     expr = to_sva_case_expr(expr).lower();
   }
-
-  // rewrite the operands, recursively
-  for(auto &op : expr.operands())
-    op = trivial_sva(op);
-
-  // post-traversal
-  if(
+  else if(
     expr.id() == ID_sva_weak || expr.id() == ID_sva_strong ||
     expr.id() == ID_sva_implicit_weak || expr.id() == ID_sva_implicit_strong)
   {

unit/temporal-logic/trivial_sva.cpp

@@ -54,7 +54,10 @@ SCENARIO("Simplifying a trivial SVA formula")
       trivial_sva(weak(sva_and_exprt{
         sva_and_exprt{seq(p), seq(q), sequence_type}})) == and_exprt{p, q});
 
-    // The below fails
-    // REQUIRE(trivial_sva(weak(sva_and_exprt{sva_and_exprt{p_seq, sva_or_exprt{q_seq, r_seq, sequence_type}, sequence_type}})) == and_exprt{p, or_exprt{q, r}});
+    REQUIRE(
+      trivial_sva(weak(sva_and_exprt{sva_and_exprt{
+        seq(p),
+        sva_or_exprt{seq(q), seq(r), sequence_type},
+        sequence_type}})) == and_exprt{p, or_exprt{q, r}});
   }
 }