Class representative bigger than class members

[bclement-ocp]

With a slightly modified version of the minimal example in #474:

logic ac f : real, real -> real

function id_2() : real = 2.

axiom ax_0 : f(f(0., 1.), 2.) <= 3.0

axiom ax_1:
  f(f(id_2, 1.), 0.) <= 0.0

function f_2_1() : real = f(2., 1.)

axiom ax_2: f_2_1 <= 0.0

goal goal_1: false

I get the following class representative (with alt-ergo -d uf):

------------- UF: Representatives map ----------------
...
  f((2),(1),(0)) --> f(f_2_1,(0)) 

But f((2), (1), (0)) is smaller than f(f_2_1, (0)) according to X.str_cmp, which I believe may break the assumptions of AC(X). I don't understand AC(X) enough to determine if this is indeed the case or not (in particular since it looks like the pair a --> b can only be between two AC terms), but recording this for future reference.

Edit: the issue is still present with #823 applied.

[bclement-ocp]

I don't know where I got that f(f_2_1, (0)) was bigger than f((2), (1), (0)); it is smaller. Closing.