word-level BMC: precondition for timeframe

kroening · kroening · commit a6a73c273540 · 2025-06-19T14:44:56.000+09:00
This adds a PRECONDITION on the starting timeframe to the word-level SVA
sequence encoding.
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);`