Given an integer variable 

x with range [l,h]

and a property involving x

x ¤ Const (where ¤ in {<,>,>=,<=,==})

The verifier should check if the intersection between the range of the integer
variable and the inequality yields a non-empty set of integers. If it yields an
empty set, then a _warning_ should be issued, indicating that it is likely that
there is some lack of conformity between the model and the specification. 

In any case, such inequality can be syntactically replaced by "false" in the
property specification, thus simplifying the property to be checked.

In the case of "x != Const", if Const is not in [l,h] then the inequality can be
syntactically replaced by "true". Again, a warning should be issued to the user.