[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] model checking question




I got the following error(?) when attempting to model check a
property in PVS ..

Starting least fixed-point calculation..
Fixed-point found in 2 steps.
Formula amounts to 2163 BDD nodes.

Failed to Model check:
   could not decode binary encodings of scalars.

I assume that my property failed and it is trying (and failing) to
generate a counter example.  Is there anything I can do about this?