Simple divisibility problem diverges

[LeventErkok]

(set-logic ALL)
(declare-fun x () Int)
(declare-fun y () Int)

; if y is 0, then so is x. Otherwise y divides x. Assert that, and prove the same for (abs y)
(assert      (ite (= y 0) (= x 0) (= (mod x      y)  0)))
(assert (not (ite (= y 0) (= x 0) (= (mod x (abs y)) 0))))

(check-sat)

The above says something really simple. If y divides x, then so does abs y. There's a little proviso to avoid y = 0 division case, in which case we require x to be 0 too.

CVC5 proves this instantly. z3, alas, does not seem to terminate.

Looking at the verbose output, something about the nl-sat/grobner-basis is going on a wild-goose change?

[LeventErkok]

Even the simpler version that avoids the ite exhibits the same behavior:

(set-logic ALL)
(declare-fun x () Int)
(declare-fun y () Int)

; Assert that y divides x. Prove that so does (abs y)
(assert      (= (mod x      y)  0))
(assert (not (= (mod x (abs y)) 0)))

(check-sat)

Proves instantly with CVC5, diverges with z3.

[levnach]

@NikolajBjorner, can you please elaborate on your remark? I am not following it.

[NikolajBjorner]

The solver could add axioms like the ones I provide in the comment.
It already adds some axioms for mod/div but not these.
I don't see how else to derive the identity based on the basic set of hammers, nlsat/incremental linearization/groebner/..

[NikolajBjorner]

Given that (mod x y) = (mod x -y) holds.
Add to theory_lra.cpp and sat/smt/arith_axioms.cpp axiomatization for mod when the modulus is not a constant.