Incompleteness in linear (integer) arithmetic

[bclement-ocp]

Consider the following SMT-LIB problem:

(set-info :status unsat)
(set-logic ALL)

(declare-const x Int)
(declare-const y Int)

(assert (<= 0 x 4294967295))
(assert (<= 0 y 4294967295))

(declare-const k0 Int)
(declare-const k1 Int)

(assert (= (- x y) (* (- k0 k1) 4294967296)))

(assert (distinct x y))

(check-sat)

It is unsat, but Alt-Ergo cannot prove it and returns unknown. This can be "fixed" in different ways, for instance moving the range assertions for x and y after the distinct assertion!

This looks like it is usual intervalCalculus madness. I still have plans to migrate it to use the Domains interface instead, which might help here.