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

PVS Bug 430


Synopsis:        Recognizer "equality?" for strategies has changed
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Feb  7 12:40:00 2000
Originator:      Ben L. Di Vito
Organization:    larc.nasa.gov
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  The access predicate "equality?", which was used to test formulas in
  prover strategies, has apparently been changed in 2.3 to "equation?".
  This causes previously written strategies using equality? to fail.
  The table in the prover guide on p. 104 still has the old name.
  
  ---
      Ben Di Vito                     b.l.divito@larc.nasa.gov
      1 South Wright Street, MS 130   http://shemesh.larc.nasa.gov/~bld
      NASA Langley Research Center    voice: +1-757-864-4883
      Hampton, VA 23681   USA         fax:   +1-757-864-4234

How-To-Repeat: 

Fix: 
Added a definition for equality?
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools