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

[Steve Johnson <sjohnson@xxxxxxxxxxxxxx>]

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
Starting pvs-cmulisp -qq ...
Warning:  #<Command Line Switch "qq"> is an illegal switch
CMU Common Lisp 19d (19D), running on yosemitesam.cs.indiana.edu
With core: /nfs/nfs2/home/data/software/rhel/pvs4.1/bin/ix86-Linux/runtime/pvs-cmulisp.core
Dumped on: Tue, 2007-10-30 17:55:38-04:00 on photon.csl.sri.com
See <http://www.cons.org/cmucl/> for support information.
Loaded subsystems:
    Python 1.1, target Intel x86
    CLOS based on Gerd's PCL 2004/04/14 03:32:47
;;; Opening as shared library /l/pvs/bin/ix86-Linux/runtime/mu.so ...
;;; Done.
;;; Opening as shared library /l/pvs/bin/ix86-Linux/runtime/ws1s.so ...
;;; Done.
; Loading #P"/nfs/nfs2/home/data/software/rhel/pvs4.1/bin/ix86-Linux/runtime/bdd-cmu.x86f".
; Loading #P"/nfs/nfs2/home/data/software/rhel/pvs4.1/bin/ix86-Linux/runtime/mu-cmu.x86f".
; Loading #P"/nfs/nfs2/home/data/software/rhel/pvs4.1/bin/ix86-Linux/runtime/dfa-foreign-cmu.x86f".

* 
* 

A_0 :  

  |-------
{1}   ((p => q) AND p) => q

Rule? (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
A_0 :  

{-1}  (p => q)
{-2}  p
  |-------
{1}   q

Rule? (split)
Splitting conjunctions,
this yields  2 subgoals: 
A_0.1 :  

{-1}  q
[-2]  p
  |-------
[1]   q

which is trivially true.

This completes the proof of A_0.1.

A_0.2 :  

[-1]  p
  |-------
{1}   p
[2]   q

which is trivially true.

This completes the proof of A_0.2.

Q.E.D.



Run time  = 0.05 secs.
Real time = 1.605 secs.

NIL
* 

A_3 :  

  |-------
{1}   NOT (p AND q) IFF (NOT p OR NOT q)

Rule? (split)
Splitting conjunctions,
this yields  2 subgoals: 
A_3.1 :  

  |-------
{1}   NOT (p AND q) IMPLIES (NOT p OR NOT q)

Rule? (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
A_3.1 :  

{-1}  p
{-2}  q
  |-------
{1}   (p AND q)

Rule? (split)
Splitting conjunctions,
this yields  2 subgoals: 
A_3.1.1 :  

[-1]  p
[-2]  q
  |-------
{1}   p

which is trivially true.

This completes the proof of A_3.1.1.

A_3.1.2 :  

[-1]  p
[-2]  q
  |-------
{1}   q

which is trivially true.

This completes the proof of A_3.1.2.


This completes the proof of A_3.1.

A_3.2 :  

  |-------
{1}   (NOT p OR NOT q) IMPLIES NOT (p AND q)

Rule? (flatten)
Applying disjunctive simplification to flatten sequent,
this simplifies to: 
A_3.2 :  

{-1}  (NOT p OR NOT q)
{-2}  p
{-3}  q
  |-------

Rule? (split)
Splitting conjunctions,
this yields  2 subgoals: 
A_3.2.1 :  

[-1]  p
[-2]  q
  |-------
{1}   p

which is trivially true.

This completes the proof of A_3.2.1.

A_3.2.2 :  

[-1]  p
[-2]  q
  |-------
{1}   q

which is trivially true.

This completes the proof of A_3.2.2.


This completes the proof of A_3.2.

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: 
*