initial
assume [rst]

always -1
assert (= [-1:mem] [mem])