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

PVS Bug 539


Synopsis:        old/new decision procedures confuse pvs
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Mar 20 13:00:03 2001
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  Load the following theory into pvs type-check it and 
  invoke x-step-proof on lemma a
  
      A : Theory
      begin
  
        a : Lemma 1=2
      end A
  
  Quit the proof but leave the TK window open. Change now
  from old to new decision procedures by 
  new-decision-procedures, invoke x-step-proof on a again and
  answer yes for the choice of decision procedures. There
  won't appear any sequent in the *pvs* buffer and pvs changes to
  interrupt state.
  
  Bye,
  
  Hendrik
  

How-To-Repeat: 

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