Non-intuitive vacuity reported for conflict (ReqCheck)

[alopez-developair]

The example is:

req1: Globally, it is always the case that if "A" holds, then "!B" holds for at least "10" time units.
req2: Globally, it is always the case that if "A" holds, then "B" holds as well.

Result is that req1 is vacuous (as of Ultimate 0.1.25-d7dd348).

While it's clear that there is contradiction between these two requirements, it's hard to understand why req1 would be considered to be vacuous. I do have some vague intuition that it may have to do with something like req2 making it impossible to reach certain states within req1's PEA.

Thoughts? Is there a way to improve the Reqchecker's feedback for this kind of case?

[danieldietsch]

It looks like both requirements should be vacuous, but I look into it.

[danieldietsch]

Actual reason: Invariants cannot be vacuous, they only have one state.

[danieldietsch]

Perhaps it is an example for #438