AE seems stuck on a trivial test case

[pictavien]

Hi,

I'm using alt-ergo (2.4.0). AE fails to prove, at least in a reasonable amount of time, the following simple case generated by Why3 (the goal is an axiom). After inlining the function f, it works fine.

(* this is the prelude for Alt-Ergo, version >= 2.4.0 *)
(* this is a prelude for Alt-Ergo integer arithmetic *)
type string

logic match_bool : bool, 'a, 'a -> 'a

axiom match_bool_True :
  (forall z:'a. forall z1:'a. (match_bool(true, z, z1) = z))

axiom match_bool_False :
  (forall z:'a. forall z1:'a. (match_bool(false, z, z1) = z1))

axiom CompatOrderMult :
  (forall x:int. forall y:int. forall z:int. ((x <= y) -> ((0 <= z) ->
  ((x * z) <= (y * z)))))

function f(x: int) : int = (((x * x) * x) - x)

axiom f_diff :
  (forall x:int. (exists y:int. ((f((x + 1)) - f(x)) = (3 * y))))

goal f_diff2 :
  (forall x:int. (exists y:int. ((f((x + 1)) - f(x)) = (3 * y))))

[Gbury]

Sorry for the delay, I'll try and take a look at this as soon as possible.

[bclement-ocp]

Looks like this is AC(X) exploding by trying to saturate way too many equations involving f(x), f(x + 1) and variants. Either inlining f or abstracting it (making it uninterpreted) makes AltRg answer immediately because it no longer spends time with irrelevant congruences involving f.

After discussing with @Gbury there are at least 4 underlying issues that contribute to the problem:

• SAT should be able to figure out very early that we have both f_diff and its negation in the context and conclude immediately, but it doesn't.
• ~Arith receives terms like f((x - 1) + 1) which don't get normalized to f(x) (we suspect that f((x - 1) + 1) gets created by substiting x → x - 1 in f(x + 1) and it doesn't get renormalized~ This has either been fixed or was an incorrect reading of the Uf output from me (I suspect this is a byproduct of #566 )
• Trying to fix the above showed that we sometime create the term 1 + x, and substituting x + 1 instead allows AltRg to solve quickly, so this is an instance where commutative matching would help (@Halbaroth experimented with this at some point)
• And finally, the fact that AC(X) explodes is an issue in itself, although it is not clear if this case is a theory or implementation issue.