pate
pate copied to clipboard
Add the ability to fix assumptions during comparison
After we do an initial run of the verifier, we will have a differential summary that describes how the behavior of the program differs at an interesting program location.
We might then want to enable the user to assume that they are in the condition that should not change. Let them "fix" that assumption in scope and then re-run the verifier to ensure that nothing else is broken.