PVS 3.1 is primarily a bug fix release, there are no new features, although the prelude has been augmented. Some of the changes do affect proofs, though our experience is that only a few proofs need adjustment, and most of these were quite easy to recognize and fix.
The bugs that have been fixed in 3.1 are mostly those reported since December 2002. Some of these fixes are to the judgement and TCC mechanism, so may have an impact on existing proofs. As usual, if it is not obvious why a proof is failing, it is often easiest to run it in parallel on an earlier version to see where it differs.
Some of the differences can be quite subtle, for example, one of the
proofs that quit working used
induct-and-simplify. There were
two possible instantiations found in an underlying
command, and in version 3.0 one of these led to a nontrivial TCC, so
the other was chosen. In version 3.1, a fix to the judgement
mechanism meant that the TCC was no longer generated, resulting in a
different instantiation. In this case the proof was repaired using
Most of the other incompatibilities are more obvious, and the proofs are easily repaired. If you have difficulties understanding why a proof has failed, or want help fixing it, send it to firstname.lastname@example.org.
Thanks to Jerry James, a number of new theories and declarations have been added to the prelude. Several judgments have been added. Remember that these generally result in fewer TCCs, and could affect proofs as noted above.