z3 - z3 の不等式の論理積の単純化

Question

次の 2 つの不等式の結合を 1 つの等式に単純化できることは簡単にわかります。

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

さまざまな戦術を試しましたが、望んだ結果は得られませんでした。この場合の戦術を教えてください。