Bug 646

Given that x is a clock, the following queries yield contradicting results:

Pr [<=100] (<> (x>0 && x<=2))      => [0.9026,1]
Pr [<=100] (<> (x>0.0 && x<=2.0))  => [0, 0.097]

The first query is analysed as constraints and is correct.
In the second query the simulator fails to detect constraints and produces unbounded delays, thus overshooting the point 2.0 and the property becomes unsatisfiable.

This particular case is simple enough to recognize the constraint and perhaps solve it like one, but in general expressions like f(x)<2.0 are not solvable, therefore an integration step should be used instead in cases where f depends on a clock.

The issue was brought up by Gabriel Domingo Vilallonga.