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:

1: load redlog;

2: rlabout();
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