The problem is that the Memory write happened in the same time step as the memory read. As a consequence, in this line, the "read event" was overwritten by the "write event".
This is also not witgen's fault, because there would have been no way to satisfy the constraints of the memory machine: There can't be any rows with the same (addr, time_step) pair, i.e., the same cell cannot be accessed twice in the same time-step.
Possibly we could fail hard in this case, which would have uncovered this bug before. But I'm not sure, because while solving the block machine, we might also process the same call to memory multiple times, in which case we want it to be a no-op after the first time.
Fixes the bug shown in the description of #2153.
The problem is that the Memory write happened in the same time step as the memory read. As a consequence, in this line, the "read event" was overwritten by the "write event".
This is also not witgen's fault, because there would have been no way to satisfy the constraints of the memory machine: There can't be any rows with the same
(addr, time_step)pair, i.e., the same cell cannot be accessed twice in the same time-step.Possibly we could fail hard in this case, which would have uncovered this bug before. But I'm not sure, because while solving the block machine, we might also process the same call to memory multiple times, in which case we want it to be a no-op after the first time.