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?