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

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



Thanks, Rick.

Sam found out that it was the same problem as reported in bug #870, and 
sent me the fix.

Hanne


icky W. Butler wrote:
> 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
>> ---------------------------------------------------------
> 


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