Maybe a reset annotation should imply that this has to happen between any two other transactions (helpful for BMC automaton)
Maybe a reset annotation should imply that this has to happen between any two other transactions (helpful for BMC automaton)