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

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

Hi Hanne,

Sounds like a bug to me.  Could you send me your specs and tell me which
lemma triggered this problem?  I'm not aware of any alternative ways of
getting at the information.


Hanne Gottliebsen <hago@dcs.qmul.ac.uk> 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
> ---------------------------------------------------------