I once made a PlusCal like interpreter in the Alloy code base. There I analyzed the branches (implies) and made sure to add instructions when one branch set a var that was not set in the other branch. This seemed to work well but I have no idea how theoretically solid it was and nobody got excited … so it has been lingering since. From a user point of view I think it would be really a huge gain.