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

Re: [PVS-Help] M-x status-proofchain problem

I have seen this.  Sometimes if you kill all bins and contexts for 
everything and
re-prove from the ground up it will disappear.


At 05:42 AM 10/4/2005, Hanne Gottliebsen wrote:
>I'm trying to run M-x status-proofchain to find out just why PVS thinks a 
>particular lemma is proven incompletely.
>However, when I place the cursor on the lemma and run M-x 
>status-proofchain, I get an error (emacs window splits with an error 
>output buffer) saying Error: the assertion
>Am I using it wrong? Have you seen this before? Is there an other way for 
>me to figure out what unproven lemma this particular one is relying on?
>I'm running PVS3.2.
>Dr. Hanne Gottliebsen    Department of Computer Science
>hago@dcs.qmul.ac.uk      Queen Mary, University of London
>Ph: +44 (0) 207 882 5259
>   - I want a single-skin cotton tent like Mr Weasley's