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

PVS Bug 656


Synopsis:        PVS 2.3/2.4 problems with (assert)
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Mon Feb  4 02:25:00 2002
Originator:      Christian Jacobi
Organization:    cs.uni-sb.de
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  I have encountered a problem with (assert) in PVS 2.4. The following
  lemma is copied from a subgoal that occurs in one of our proofs:
  
  	bug: LEMMA FORALL(x: real, i:int):
  			x-i<0 IMPLIES (
  				 -(x - i) >= x - 1 * (2 * floor(ceiling(x * 1) 
 / 2)) OR
  				   x - 1 * (2 * floor(ceiling(x * 1) / 2)) < 0 
 OR
  				   ceiling(x * 1) = floor(x * 1) OR
  				   ceiling(x * 1) - x * 1 < x * 1 - floor(x * 1
 ) OR
  				   x * 1 - floor(x * 1) < ceiling(x * 1) - x * 
 1)
  
  In PVS 2.3, the lemma is proved by (skosimp*)(assert). In PVS 2.4,
  (assert) does not solve the goal. In the original proof, (assert)
  even hangs.
  
  Bye, Chris
  
  PS: do not ask me why the claim holds ;-)
  -- 
  ----------------------------------------------------------------
                                         FR 6.2 - Informatik
   Christian Jacobi                      Im Stadtwald
   Computer Science Department           D-66041 Saarbruecken
   Saarland University        			 
   Germany                               Phone: (+49) 681 3024129
                                         Fax:   (+49) 681 3024290
  ----------------------------------------------------------------
  

How-To-Repeat: 

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