RE: [PVS-Help] PVS 4, errors in Proof buffer?

["Baldwin Rusty O Civ AFIT/ENGE" <Rusty.Baldwin@xxxxxxxx>]

I was at the PVS class in Nov this year and had the same question.  The
answer appears to be that CMU-Lisp is the culprit.  This message does
not occur with Allegro Lisp.

It's seems to be benign (but disconcerting)...

Rusty 

-----Original Message-----
From: pvs-help-bounces+rusty.baldwin=afit.edu@csl.sri.com
[mailto:pvs-help-bounces+rusty.baldwin=afit.edu@csl.sri.com] On Behalf
Of Steve Johnson
Sent: Thursday, December 13, 2007 2:53 PM
To: pvs-help@csl.sri.com; Paul S. Miner
Subject: [PVS-Help] PVS 4, errors in Proof buffer?

Does anyone recognize this symptom?
I'm running PVS 4 on some old sources and get an error in the
proof-buffer.
The full buffer content is attached, but the last few lines are:

    <PVS *proof* buffer>
     .
     .
     .
    Q.E.D.

    Help! 12 nested errors.  KERNEL:*MAXIMUM-ERROR-DEPTH* exceeded.

    Debug  (type H for help)

    (UNIX::SIGSEGV-HANDLER #<unused-arg> #<unused-arg> #.(SYSTEM:INT-SAP
    #x3FFFCA64))
    Source:
    *

I removed existing *.pvscontext* and *pvsbin/ *before invoking the
Prover.
*M-x step-proof* does not generate this error.
Any ideas?

Thanks,
Steve Johnson