pate icon indicating copy to clipboard operation
pate copied to clipboard

Add the ability to fix assumptions during comparison

Open travitch opened this issue 3 years ago • 0 comments

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.

travitch avatar Jul 15 '21 20:07 travitch