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

PVS Bug 504


Synopsis:        new-decision-procedures as default
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jan  8 02:40:02 2001
Originator:      Hendrik Tews
Organization:    inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  when I set the new decision procedures as default (eg. via
  (new-decision-procedures) in ~/.pvsemacs) PVS asks me for every
  new proof:
  
      This proof was originally done with the old decision procedures,
      which is not the default.
      Use the old ones (for this proof only)? (Yes or No) 
  
  Is this a bug or a feature?
  
  Also all TCC's that are proved via the default proof are proved
  with the old decision procedures -- contrary to my explicit
  setting.
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

 [davesc]
 New decision procedures aren't supported any more.  Leaving this
 open to ensure the selection logic supports this operation correctly
 in 3.0.

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