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

PVS Bug 454


Synopsis:        problems with decision proc.
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Fri Mar 24 09:40:00 2000
Originator:      Aaron Ballard
Organization:    mchp.siemens.de
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Hello,
  
  Neither (assert) nor (grind) will prove the following sequent:
  
  
  {-1}  SeqAV(av_array(AVs_new!1)(1)) <= seqHE(post!1)
  [-2]  SeqAV(AV!1) = seqHE(post!1)
    |-------
  {1}   SeqAV(av_array(AVs_new!1)(1)) < seqHE(post!1)
  [2]   seqHE(post!1) = SeqAV(av_array(AVs_new!1)(1))
  
  
  A similar problem occurred in another context, if you would like to
  see that one too.  There, I proved two lemmas, for each using grind,
  then introduced the lemmas into the problem sequent, instantiated,
  split the resulting implication (because the decision procedures
  wouldn't recognize expressions for rewriting within the implication) 
  then asserted successfully.
  
  This problem started part way through a proof, and seems, because of
  the two lemmas I mentioned, not to affect other proofs.
  
  Sincerely,
  Aaron Ballard

How-To-Repeat: 

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