@@ -576,6 +576,48 @@ static obligationst property_obligations_rec(
576
576
auto equal_expr = equal_exprt{sva_iff_expr.lhs (), sva_iff_expr.rhs ()};
577
577
return property_obligations_rec (equal_expr, current, no_timeframes);
578
578
}
579
+ else if (
580
+ property_expr.id () == ID_sva_overlapped_implication ||
581
+ property_expr.id () == ID_sva_non_overlapped_implication)
582
+ {
583
+ auto &implication = to_binary_expr (property_expr);
584
+
585
+ // The LHS is a sequence, the RHS is a property.
586
+ // The implication must hold for _all_ matches on the LHS,
587
+ // i.e., each pair of LHS match and RHS obligation yields an obligation.
588
+ const auto lhs_match_points =
589
+ instantiate_sequence (implication.lhs (), current, no_timeframes);
590
+
591
+ obligationst result;
592
+
593
+ for (auto &lhs_match_point : lhs_match_points)
594
+ {
595
+ // The RHS of the non-overlapped implication starts one timeframe later
596
+ auto t_rhs = property_expr.id () == ID_sva_non_overlapped_implication
597
+ ? lhs_match_point.first + 1
598
+ : lhs_match_point.first ;
599
+
600
+ // Do we exceed the bound? Make it 'true'
601
+ if (t_rhs >= no_timeframes)
602
+ {
603
+ DATA_INVARIANT (no_timeframes != 0 , " must have timeframe" );
604
+ return obligationst{no_timeframes - 1 , true_exprt ()};
605
+ }
606
+
607
+ // Get obligations for RHS
608
+ auto rhs_obligations_rec =
609
+ property_obligations_rec (implication.rhs (), t_rhs, no_timeframes);
610
+
611
+ for (auto &rhs_obligation : rhs_obligations_rec.map )
612
+ {
613
+ auto rhs_conjunction = conjunction (rhs_obligation.second );
614
+ auto cond = implies_exprt{lhs_match_point.second , rhs_conjunction};
615
+ result.add (rhs_obligation.first , cond);
616
+ }
617
+ }
618
+
619
+ return result;
620
+ }
579
621
else if (
580
622
property_expr.id () == ID_sva_nonoverlapped_followed_by ||
581
623
property_expr.id () == ID_sva_overlapped_followed_by)
0 commit comments