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

# PVS Bug 945

```Synopsis:        PVS 3.3 release candidate testing
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Tue Jan 24 13:45:00 2006
Originator:      "Ricky W. Butler"
Organization:    larc.nasa.gov
Release:         PVS 3.2
Environment:
System:
Architecture:

Description:
Sam,
I have begun testing the PBS 3.3 beta with our libraries.  Here is a
problem I found in the "reals" library.

If you rerun lemma "harmonic_polynomial_real_rec" in the
harmonic_polynomials theory you will encounter subgoals such as

harmonic_polynomial_real_rec.1.1.1.1.1.1.2.1 :

{-1}  0 >= 0
{-2}  i!1 = 0
|-------
{1}   real_pred(F2(0))

If you issue command (reveal -2) you get

{-1}  (LAMBDA (i_1: nat):
x *
(LAMBDA (i_1: nat):
IF i_1 > n OR odd?(i_1) THEN 0
ELSE C(n, i_1) * (-1) ^ (i_1 / 2) *
(IF i_1 = 0 THEN x ^ n
ELSIF i_1 = n THEN y ^ n
ELSE x ^ (n - i_1) * y ^ i_1
ENDIF)
ENDIF)
(i_1))
= F2
[-2]  0 >= 0
[-3]  i!1 = 0
|-------
[1]   real_pred(F2(0))

If you try command (replace -1 * RL) nothing happens.

(replace -1 * RL)
No change on: (replace -1 * RL)

The system should know that F2(0) is an integer and hence real
but does not.

There are several more subgoals with this same problem.

Rick

How-To-Repeat:

Fix:
This is the same bug as #935, and has been fixed.  The problem is that the
prover is now case-sensitive, and RL was being quietly ignored (as would
any invalid entry).  The fix now allows any case for lr or rl, and
complains for invalid values.
```
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools