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

*To*: Sam Owre <owre@csl.sri.com>, pvs-help@csl.sri.com*Subject*: LOST PROOF FILES*From*: Victoria Chernyakhovsky <vchernya@ececs.uc.edu>*Date*: Mon, 27 Apr 1998 14:22:04 -0400*References*: <199804210746.AAA28138@chlorine.csl.sri.com>*Sender*: vchernya@ececs.uc.edu

Hi, We are fighting with a PVS bug in the PVS Version 2.1 (patch level 2.417). We would appreciate any help. We have a large specification with several theory files. All lemmas were proven correct with PVS 2.1 (patch2 version 2.414). If we rerun the proofs automatically we get 100% of the lemmas proven correct (after disabling the bin-files). However, if we introduce a change and want to reprove the lemmas in question, the system breaks. * In some cases, the prover was actually breaking and PVS had to be restarted. This serious problem was removed by applying more basic proof commands. * Continuing with further proofs, the PVS environment seems to exhibit an inconsitant behavior. Independent of the completeness of a proof, the proof file is corrupted. In general only some of the proofs of the theory are stored in the prf-file. We are seeking for any kind of advice to overcome these problems. As we have updated our Emacs version to 20.2.1 we are basically restricted to patch level 2.417. However, if these problems can not be overcome we would appreciate to get a hold of the earlier version of PVS 2.1 (patch2 version 2.414). As we are trying to overcome these problems for several weeks, we would appreciate immediate access to the previous version. Thank you for your help and we would be glad to receive any immediate help. Victoria Chernyakhovsky

- Prev by Date:
**Re: problem with pvs** - Next by Date:
**Re: LOST PROOF FILES** - Prev by thread:
**Re: Using MEASURE-INDUCT** - Next by thread:
**Re: LOST PROOF FILES** - Index(es):