Hi Ilkay,
Great question. We have seen similar cases to this.
Here is what is happening:
In each case, we have (taking for example state x):
A == 1 as the first transition. This generates 2 objectives: A == 1 true and A == 1 false
A ~= 1 is the second transition and has two objectives as well: A ~= 1 true and A ~= 1 false
The A ~= 1 false is not reachable (the objective is "dead"), because it corresponds to exactly the case where A == 1 is true (which means Design Verifier would never check that transition because the first transition is always true).
How to fix: since the second transition corresponds exactly to the case where the first condition is true, you can replace the [A ~= 1] and [B ~= 1] with default transitions (with no label). This does the exact same thing.
