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

PVS Bug 738


Synopsis:        edit-proof takes much longer when the prover is active
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Mon Feb  3 11:50:03 2003
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.0
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  in PVS 3.0 the command M-x edit-proof takes much longer when the
  prover is active. On my 1 GHz Athlon I have for instance:
  
  edit-prove on the last lemma
  LPartFun_to_SPartFun_CompositionPreservation of the prelude
  finishes immediately.
  
  However, if I start a proof on
  LPartFun_to_SPartFun_CompositionPreservation edit-proof on
  LPartFun_to_SPartFun_CompositionPreservation takes three seconds!
  
  The delay increases with the size of the proof. Sometimes I have
  to wait for 10-20 seconds.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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