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

Preserving proofs when TCC numbers change



I recently installed the latest PVS upgrades and I'm rerunning some
proofs in a model I'm developing.  I'm running into a problem where
the same number of TCCs are not always generated and previous proofs
of the TCCs are not always associated with the correct TCC.

I understand that more or less TCCs may get generated in the face of
changes to PVS but it seems that PVS keeps track of previous proofs of
TCCs by name and number and the generation of an additional TCC throws
the system off.  Is there a way to preserve the proof-to-TCC
association?  I've had similar problems when small changes to a spec
caused an additional TCC to be generated.  What do others do to deal
with this?  

Thanks,

Tad