Infinite loop(s) with AC(X)

[bclement-ocp]

Related to arithmetic constants (also works with int, fix incoming):

logic p : real -> real
logic ac u : real, real -> real

axiom h0: 0.0 = p(1.0)
axiom h1: forall m : real. p(1.0+m) = u(p(0.0),p(m))
goal g: false

Related to omega procedure in Arith (actually not, see below):

; alt-ergo <
(set-logic ALL)
(declare-const a Int)
(declare-const b Int)
(declare-const x Int)
(declare-const y Int)
(assert (= (* a b) (+ y x)))
(assert (= (* a a) (+ x x)))
(check-sat)

This example involves the fresh ac terms created by subst_bigger in the Arith module, but after further examination that seems to be unrelated to the actual bug. Simpler reproducer without integers or multiplication:

logic x, y, k, z : real

logic ac u : real, real -> real

(* Note: must not write u(y, x)!
   Something about interning order... *)
axiom h0: u(y, y) = -u(x, y)
axiom h1: u(k, -u(x, y)) = u(y, 1.0 - u(x, y))
axiom h2: z = u(y, -u(x, y))

goal g: false

[bclement-ocp]

In the last example we generate the following rewrite rules (the first two are directly from the input problem, the 3rd one is generated while processing the critical pair on $k y (-y x)$ ):

$$ \begin{array}{rcl} y^2 & \rightsquigarrow & - y x \\ k (- y x) & \rightsquigarrow & y (1 - y x) \\ z (1 - y x) & \rightsquigarrow & z k y \\ \end{array} $$

causing a loop:

$$ z k y^2 \rightsquigarrow z k (- y x) \rightsquigarrow z y (1 - y x) \rightsquigarrow z k y^2 $$

How do we end up in this situation? Let's look at the behavior of Ac.compare.

• For $y^2 \rightsquigarrow - yx$, $-yx$ is NOT an AC term while $y^2$ is, so $y^2$ is bigger (even though $x > y$!).
• For $k (-y x) \rightsquigarrow y (1 - yx)$, we compare the leaves: ${ k, y, x }$ and ${ y, y, x }$. Since we have $k > y$, $k (- y x)$ is bigger.
• For $z (1 - yx) \rightsquigarrow z k y$, we compare the leaves: ${ z, x, y }$ and ${ z, k, y }$. Since we have $x > k$, $z (1 - yx)$ is bigger.

So… one of these is wrong, and we need to understand which one — but I don't think it can be the first one…

Note: I initially thought this was related to the fact we are ignoring the $1$ in the ordering, but that doesn't actually seem to be the case; everything breaks the same way if we take into consideration the $1$ but use $2 - yx$ instead of $-yx$.