// #TestSpec: redundant:req2; results:-1
Input x IS int

req1: Globally, it is always the case that "x>0" holds after at most 4 time units
req2: Globally, it is always the case that "x>0" holds after at most 5 time units