Suppose a trivial model with one declaration: clock tg; The following properties are satisfied: E<> tg>=0 Pr[<=2] (<> tg>=0) But the following fail: simulate 1000 [<=2] { tg } : 1 : tg>=0 simulate 1000 [<=2] { tg } : 1 : 0<=tg this one succeeds 100%: simulate 1000 [<=2] { tg } : 1000 : 0<tg so it seems that the issue is somehow connected with strictness of the constraint. Reported by Dmitry
Stratego-6 does not have this issue anymore.