By definition, a signal's value is always in the range of its type. When a signal is assigned a value that is not an element of its declared type, the resulting value of the signal is not defined by the SMV semantics, except that it must be a value in the type of the signal.
Another way to view this is that any assignment
x := expr;
is treated as if it were a shorthand for:
x := (expr in TYPE) ? expr : TYPE;
where TYPE is the set of values in the type of signal x.
This means that if the value of expr is not in the set TYPE, then the value of x is chosen nondeterministically from
the set TYPE. See the next section for a discussion of
nondeterministic choice.