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

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

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