If you run into a bug using PVS, you can try searching through the system manuals, or the recently created PVS Google Groups page.
Please don't waste your valuable time deciding if it is a real bug, or trying to minimize it. Even if it is a misunderstanding on your part, it indicates that the documentation should be improved. The main thing is to let us know about the bug, and ideally send enough information that we can recreate it; we will contact you if we need more.
Typically we need the specification and proof files to recreate the problem. Under Emacs, M-x dump-pvs-files generates a single file that can be sent to us, but you can also simply create a tar or zip file. If the specifications depend on libraries (other than the NASA pvslib), you should send those as well, in separate dump/tar/zip files. Note that you should probably exclude the pvsbin sudirectory, unless that is relevant to the bug, as many mailers have size restrictions. If it's still too large, you can use the split command (part of Linux/MacOSX) to break the file into smaller chunks and send them separately.
The information should be sent to us at pvs-bugs@csl.sri.com.
Note: we tend to be open about bugs reported to us, and may use them for regression testing, or as examples for topics of discussion, FAQs, etc. Please tell us if anything you send is confidential, and we will make sure to treat your information accordingly.
