If a user has asserted multiple relations or values, he might repair the state by removing any of them, not necessarily the last one. In that case, we would get a list of valid executions, however the - now outdated - error message would still persist. Fix that by iterating over the partial execution array and marking all of them as confirmed when we get a new execution. This is slightly wasteful, because we update the array for every new execution we get, but realistically speaking this pales compared to the necessary rendering, and there won't be many executions.
- Open https://pseuco.com/#/edit/remote/0eicrm56aorld6yvwz57
- Use the "Memory Model Analysis" action
- Add a "write-seen" assertion from the read to the write of 3.
- Add a "value was read" assert with value 2.
- Undo the "write-seen" assertion.
Without this patch:
- The error message is still there.
With this patch:
- The error is no longer there, as it should be.