When used with -tempinduct mode, -seq causes assertions to be ignored in the first N steps. While this has uses for reset modelling, for these test cases it is unnecessary and could lead to failures slipping through uncaught.
I suspect most of these have slipped through as they have just been copy-pasted from existing tests - Could be good to clarify the wording in the sat help to make it clear how this behaviour works
When used with -tempinduct mode, -seq causes assertions to be ignored in the first N steps. While this has uses for reset modelling, for these test cases it is unnecessary and could lead to failures slipping through uncaught.
I suspect most of these have slipped through as they have just been copy-pasted from existing tests - Could be good to clarify the wording in the
sathelp to make it clear how this behaviour works