fix SVA sequence simplifications

Rewriting SVA sequences to SVA properties only works if these sequences are
at the property level.

Author: kroening

src/temporal-logic/normalize_property.cpp

@@ -36,6 +36,7 @@ exprt normalize_pre_sva_non_overlapped_implication(
 
 exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
 {
+#if 0
   if(expr.is_unbounded())
   {
     if(numeric_cast_v<mp_integer>(expr.from()) == 0)
@@ -51,6 +52,7 @@ exprt normalize_pre_sva_cycle_delay(sva_cycle_delay_exprt expr)
     }
   }
   else
+#endif
     return std::move(expr);
 }
 
@@ -90,12 +92,12 @@ exprt normalize_property_rec(exprt expr)
   }
   else if(expr.id() == ID_sva_cycle_delay_plus)
   {
-    expr = sva_s_nexttime_exprt{
-      sva_s_eventually_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
+//    expr = sva_s_nexttime_exprt{
+//      sva_s_eventually_exprt{to_sva_cycle_delay_plus_expr(expr).op()}};
   }
   else if(expr.id() == ID_sva_cycle_delay_star)
   {
-    expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
+//    expr = sva_s_eventually_exprt{to_sva_cycle_delay_star_expr(expr).op()};
   }
 
   // normalize the operands

src/trans-word-level/sequence.cpp

@@ -378,8 +378,7 @@ sequence_matchest instantiate_sequence(
   else
   {
     // not a sequence, evaluate as state predicate
-    auto obligations = property_obligations(expr, t, no_timeframes);
-    auto conjunction = obligations.conjunction();
-    return {{conjunction.first, conjunction.second}};
+    auto instantiated = instantiate_property(expr, t, no_timeframes);
+    return {{instantiated.first, instantiated.second}};
   }
 }