[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.

Rick


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.
>
>Thanks,
>Hanne
>--
>---------------------------------------------------------
>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
>---------------------------------------------------------