A few years ago I made an attempt to support a Pluscal like language in Alloy. One of the features was that it traversed all the logical paths and automatically ensured the non-used variables were kept constant if not mentioned in a branch.
It never generated a lot of interest so I stopped pursuing it. I made a deplorable joke that seemed to have upset some sensitive souls and that dominated the discussion 
but reviving the part that keeps unused variables constant might be an idea.
I agree that doing it manually is very error prone and tedious.