z3 - z3 中不等式的简化

Question

很容易看出，以下两个不等式的结合可以简化为一个等式。

(declare-const x  Int)
(declare-const y  Int)
(assert ( and ( <= ( + (* -1 x) y ) -1 ) ( <=( + (* -1 y) x ) 1 )))
(apply (and-then simplify propagate-ineqs))

我尝试了不同的策略，但没有得到想要的结果。请您指定针对此案的策略吗？