Hi,

I am a newbie using Redlog to solve floating point constraints.

I recently re-installed my machine and hence I also re-installed redcsl from SVN by following the instruction at http://sourceforge.net/apps/mediawiki/reduce-algebra/index.php?title=Installation

However, after I was able to get redcsl installed, redcsl seems to work in an unexpected way.

This is the command that I typed in redcsl IDE:

Redlog Development Version, Sat Mar 23 15:07:38 2013
(C) A. Dolzmann and T. Sturm
http://www.redlog.eu/

5: rlset R;

7: phi1:=rlall((((((x <> 1.)) or ((y <> 1.))) or ((x > 1.))) or ((x = y))));
\phi\mathrm{:=}\forall x\forall y\left(\left(\left(x-1\,\neq\, 0\,\vee\, y-1\,\neq\, 0\right)\,\vee\, x-1\,>\, 0\right)\,\vee\, x-y=0\right)

8: rlqe phi1;
\mathrm{false}

The PROBLEM is that redcsl returns FALSE (which is not correct). The formula phi I wanted to prove is:

x=1.0 and y=1.0 and x<=1.0 imply x=y (which should be correct).

Note that x<=1.0 is indeed redudant due to x=1.0.
However, if we omit x<=1.0, the outcome is correct.

4: phi2:=rlall(((((x <> 1.)) or ((y <> 1.)))  or ((x = y))));
\phi\mathrm{:=}\forall x\forall y\left(\left(x-1\,\neq\, 0\,\vee\, y-1\,\neq\, 0\right)\,\vee\, x-y=0\right)

5: rlqe phi2;
\mathrm{true}

However, if I use the older version of redlog in another machine of mine, then the

REDLOG DEVELOPMENT VERSION, Wed Jan 12 16:27:06 2011
(C) 1995-2009 A. Dolzmann and T. Sturm
http://www.redlog.eu/

Then, I got the correct result for "rlqe phi1;" which is TRUE.

Would it be the case that the latest version of redlog from SVN is error-prone?

THank you so much for your help.

Best regards,

Khanh