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


Hi Victoria,

I'd like to look into this problem immediately, but I need some means of
recreating the problem.  Could you send a dump of your specification (use
M-x dump-pvs-files) and perhaps the scenario(s) that cause these problems?


> From:    Victoria Chernyakhovsky <vchernya@ececs.uc.edu>
> Date:    Mon, 27 Apr 1998 14:22:04 EDT
> To:      Sam Owre <owre@csl.sri.com>, pvs-help@csl.sri.com
> 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