goal property does not enforces initialization

its-reach might find that a goal is reachable by an empty witness if the postcondition is satisfied in the initial state of the GAL model. Since the initialization is done via an init transition in GAL, the intended initial states are only the states reached after the init transition is fired. An empty witness is therefore not a valid witness, and the conversion to GAL should reflect that.

Fix: Add a check for "_init==1" in the GAL conversion of the postcondition.