Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

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: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools