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

PVS Bug 1016


Synopsis:        garbage output in proof buffer: Free variables in expr l
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Nov 27 10:15:01 2007
Originator:      Hendrik Tews
Organization:    cs.ru.nl
Release:         PVS 4.1
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  open any proof and do 
  
    (case "Forall(l : list[nat]) : length[below(length(l))](l) > 1")
  
  This prints 
  
    Free variables in expr l
  
  in the *pvs* buffer.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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