I have a model and I do the liveness checking then the result is Satisfied. Then I just remove the guard of a transition which is, to me, always True. Then the result is unsatisfied.
I need more information on how to replicate the issue.
From the description I could just speculate that maybe it is an expected behavior, i.e. maybe the guarded edge leads to a location where infinite delay is possible, and thus is a counteraxmple that the target predicate is no longer satisfiable.
Please upload a model or a minimal example.
Alternatively, could you try it with newer release?
Perhaps the issue has been fixed already.