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