// #TestSpec: redundant:; results:-1
CONST MAX_TIME IS 0.5
Input A IS bool
Input C IS int
Input B IS bool
Input Y IS bool
Input Z IS bool

ID000: Globally, it is always the case that if "A" holds, then "B " holds after at most "MAX_TIME " time units
ID001: Globally, it is always the case that if "A && C == 1 " holds, then "A" holds after at most "MAX_TIME " time units
ID002: Globally, it is always the case that if "C == 1 && D" holds, then "D " holds after at most "MAX_TIME " time units
ID003: Globally, it is always the case that if "Y" holds, then "Z " holds after at most "MAX_TIME " time units