(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 yafter 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.
Consider the following SMT-LIB problem:
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 forx
andy
after thedistinct
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.