# PVS Bug 1014

Synopsis: install-proof generates garbage
Severity: serious
Priority: medium
Responsible: owre (Sam Owre)
State: open
Class: sw-bug
Arrival-Date: Tue Nov 27 10:15:00 2007
Originator: Hendrik Tews
Organization: cs.ru.nl
Release: PVS 4.1
Environment:
System:
Architecture:
Description:
Hi,
take the following two theories
A : Theory
Begin
x : lemma expt(2,2) = 4
End A
B : Theory
Begin
x : lemma expt(2,2) = 4
End B
and proof A.x with grind. Do then edit-proof on A.x, move the
cursor to B.x and do install-proof WITHOUT running the proof. Do
then edit-proof on B.x, it will look as follows:
;;; Proof x-1 for formula B.x
;;; developed with shostak decision procedures
(;; Proof x-1 for formula A.x
;; developed with shostak decision procedures
(grind))
Running the proof still works and corrects the mess.
Bye,
Hendrik
How-To-Repeat:
Fix: