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

PVS Bug 683


Synopsis:        use strategy
Severity:        serious
Priority:        medium
Responsible:     dave_sc (Dave Stringer-Calvert)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Jul 22 23:10:00 2002
Originator:      John Rushby
Organization:    csl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  The grind-with-lemmas strategy distributed with pvs-2.4 uses the
  polarity?  argument to the strategy use, which is not allowed with the
  verison of use in the same distribution.
  
  John
  

How-To-Repeat: 

Fix: 
Added the priority argument to use
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools