[Analysis] Bound check raises issue when initial value is the same as lower bound
- create a model with a state automaton
- in the state automaton, add an (integer) internal variable
- define as initial value 0 and as lower bound 0 as well
- open the semantic inspector
- in the “direct analyses” tab, click on “Check variable ranges”
Observe that NuSMV fails.
The problem seems generalizable to any case where the initial value is the same as the lower bound.
(from redmine: issue id 2541, created on 2016-03-29, closed on 2016-08-02)