You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If an if statement has no else clause, and its then clause ends in an assume statement, then the enabling condition is attached to the first statement following the if. In other words, that if-following statement will block on the condition whether or not the then branch was taken. This is non-intuitive and thus likely to be surprising and unexpected to developers.
Similarly, if an if statement has an else clause, and that else clause ends in an assume statement, the enabling condition is attached to the first statement following the if. This is also non-intuitive.
For these reasons, it seems useful to ensure that there's always a PC at the end of each then and else clause that's distinct from the PC of the subsequent instruction. That will require adding some extra steps that do nothing other than advance the PC from the clause-ending PC to the subsequent one.
The text was updated successfully, but these errors were encountered:
jaylorch
changed the title
Assume at end of then clause attaches to subsequent statement
Assume at end of if clause attaches to subsequent statement
Mar 25, 2021
If an if statement has no else clause, and its then clause ends in an assume statement, then the enabling condition is attached to the first statement following the if. In other words, that if-following statement will block on the condition whether or not the then branch was taken. This is non-intuitive and thus likely to be surprising and unexpected to developers.
Similarly, if an if statement has an else clause, and that else clause ends in an assume statement, the enabling condition is attached to the first statement following the if. This is also non-intuitive.
For these reasons, it seems useful to ensure that there's always a PC at the end of each then and else clause that's distinct from the PC of the subsequent instruction. That will require adding some extra steps that do nothing other than advance the PC from the clause-ending PC to the subsequent one.
The text was updated successfully, but these errors were encountered: