Merge pull request #1164 from diffblue/trans-word-level-sequence-precondition

tautschnig · web-flow · commit d02f88c03a38 · 2025-06-25T11:56:40.000+02:00
word-level BMC: precondition for timeframe
diff --git a/src/trans-word-level/sequence.cpp b/src/trans-word-level/sequence.cpp
@@ -82,6 +82,8 @@ sequence_matchest instantiate_sequence(
   const mp_integer &t,
   const mp_integer &no_timeframes)
 {
+  PRECONDITION(t < no_timeframes);
+
   if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something
   {
     auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr);

Original file line number	Diff line number	Diff line change
`@@ -82,6 +82,8 @@ sequence_matchest instantiate_sequence(`
`82`	`82`	`const mp_integer &t,`
`83`	`83`	`const mp_integer &no_timeframes)`
`84`	`84`	`{`
	`85`	`+ PRECONDITION(t < no_timeframes);`
	`86`	`+`
`85`	`87`	`if(expr.id() == ID_sva_cycle_delay) // ##[1:2] something`
`86`	`88`	`{`
`87`	`89`	`auto &sva_cycle_delay_expr = to_sva_cycle_delay_expr(expr);`