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