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.
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.