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

PVS Bug 657


Synopsis:        Loop in ASSERT
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           analyzed
Class:           sw-bug
Arrival-Date:    Mon Feb  4 12:20:00 2002
Originator:      Cesar Munoz
Organization:    icase.edu
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Hello,
  
  The commands (SKOSIMP)(ASSERT) seem to loop forever with the following
  example:
  
  loop: LEMMA
      FORALL (x,y:real):     
      x /= 6 AND x /= 0 AND y = 3/(x*x - 6*x) IMPLIES
      (x+3)/(x*(x-6)) = 1/(x-6) + y 
  
  The commands (SKOSIMP)(GROUND) and (SKOSIMP)(GRIND) exhibit the same
  problem. I'm using PVS Version 2.4 patchlevel 1 in Solaris and Linux.
  
  Cesar
  --
  Cesar A. Munoz H.       | munoz@icase.edu, C.A.Munoz@larc.nasa.gov
  Staff Scientist         | http://www.icase.edu/~munoz
  ICASE                   | Phone +1 757 864-8018  Fax +1 757 864-6134
  NASA LaRC, Mail Stop 132C, 3 West Reid Street, Hampton, VA 23681-2199,
  USA.
  

How-To-Repeat: 

Fix: 
Seems to be fixed now.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools