Better error when trying mask-changing iMod on non-atomic WP goal
Currently when you run iMod
on a mask-changing fupd and the goal is a WP with an expression that cannot be proven atomic, we open a subgoal that asks the user to prove atomicity. In many cases, this subgoal will be unprovable. Also in many cases, the user will be surprised by why this shows up now but didn't show up in the tutorial when they opened an invariant.
I think instead of falling back to asking the user to prove the goal, we should fall back to showing an error message, such as with the pm_error
infrastructure. The message should then give the user some useful hints for what to do.