Model-Checking: if no else exists for an if-statement in code specification for model-checking, the checker throws an exception
Additionally, the exception has no meaningful name.
Maybe the model-checker could add an empty “else”?
(from redmine: issue id 2031, created on 2014-06-20, closed on 2014-07-21)