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

PVS Bug 507


Synopsis:        prover breaks with tuples and (replace)
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jan  8 04:00:04 2001
Originator:      Joachim van den Berg
Organization:    cicero.cs.kun.nl
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  Dear Sam, Dave,
  
  The prover breaks on the example below. Applying a (skosimp*) and a 
  (replace -2) leads to a proof state
  
  {-1}  =(t!1)
  [-2]  (0, 0) = t!1
    |-------
  [1]   b!1
  
  
  Doing an (assert) afterwards, the prover breaks.
  Hopefully, this can be fixed soon!
  
  
  Best,
  Joachim van den Berg
  
  --
  
  ReplaceBug : THEORY 
  BEGIN
  
    t : VAR [nat, nat]
    b : VAR boolean
  
    % ("" (SKOSIMP*) (REPLACE -2) (ASSERT))
    foo : LEMMA
      0 = 0 AND (0,0) = t IMPLIES b
  
  END ReplaceBug
  

How-To-Repeat: 

Fix: 
Fixed replace* to not assume that the replacement of a tuple-expr returns
a tuple-expr.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools