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

PVS Bug 695


Synopsis:        assert problem with floor
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Jul 30 17:00:00 2002
Originator:      Sam Owre
Organization:    csl.sri.com
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  floor_plus in the prelude never finishes the proof:
  
  ("" (skolem!) (expand "fractional") (assert))
  
  Sam
  

How-To-Repeat: 

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