To make its computations simpler, SMV sometimes uses an abstract ``unknown value'' to represent a value that is not completely determined. For example, if we write

if(c) x := expr;then, when the condition

The `bottom` value has a special property - replacing any value
with `bottom` is a conservative abstraction in the sense that any
property we can prove using this abstraction can be proved without it
(though perhaps at a higher cost). Unfortunately, the converse is not
true. That is, sometimes replacing the value of a variable with ` bottom`, and thus avoiding a combinational variable, will lead to a
false negative result. As a trivial example, suppose we tried to
verify the property `G (x = x)`. Clearly, this is a tautology, and
should be true for any definition of `x`. However, in our case, if
`c` is false, then by default `x` will get the value ` bottom`. When evaluate `bottom = bottom` we get `bottom`
(that is, it is unknown whether two unknown values are equal). In this
case SMV's default abstraction is a bad one, since it prevents us from
proving a property which is true.

The value `bottom` can arise in several other ways. For example,
suppose that `x` and `y` are two variables of a scalarset type
`T`, and we have reduced type `T` to just the value 0, and
the abstract value `NaN` representing all the remaining values.
If both `x` and `y` have the value `NaN`, then the expression
`x = y` will yield `bottom`. That is, the truth value of the
comparison might be either 0 or 1, but SMV represents both case by
the single value `bottom` in order to avoid introducing a combinational
variable for the choice. A similar case occurs when evaluating the
expression `a[x]`. If `x` evaluates to `NaN`, then `a[x]`
evaluates to `bottom`.

The most common way in which `bottom` values lead to problems is
when they occur in the condition part of an if-then-else block. For example, suppose we had
the following SMV program:

scalarset foo undefined; module main(){ x,y : foo; a,b : boolean; if(x=y){ a := 0; b := 0; } else{ a := 1; b := 1; } p : assert G (a = b); }Clearly, the property

SMV provides two ways to avoid this kind of problem. One is automatic but potentially
costly, while the other is manual but less expensive. To solve the problem
automatically, select `Prop|Options` from the menu pane and check the box
that says ``Enumerate unknown values''. Now if you try again to verify the
property, SMV should say it is true. In fact, SMV observed that the expression
`x=y` might get the value `bottom`, and that this value might propagate
into both variables `a` and `b`. Thus, it introduced a combinational
variable for `x=y`. This in effect causes the model checker to enumerate
both possible truth values of this expression. Since the property is true in
both cases, this fixes the problem.

Unfortunately, using the ``Enumerate unknown values'' can cause a large number of combinational variables to be introduced, which can slow down the model checking process quite a lot (note, you won't see these added variables in the ``Cone'' pane, but they will be reported in the model checking transcript). In the case where the overhead resulting from ``Enumerate unknown values'' is unacceptable, it is also possible to introduce combinational variables manually for just those expressions that are causing problems. In the above case, for example, we could create a new boolean variable for the condition, as follows:

c : boolean; c := (x=y); if(c){ ...This by itself doesn't change anything. That is, since we have not explicitly asked for a nondeterministic choice in the value of

using enum(c) prove p;This says to make