title: simplification of conjunction of inequalities in z3
body: <p>It is easy to see, that conjunction of two following inequalities could be simplified to one equality.</p>
  
  <pre><code>(declare-const x  Int)
  (declare-const y  Int)
  (assert ( and ( &lt;= ( + (* -1 x) y ) -1 ) ( &lt;=( + (* -1 y) x ) 1 )))
  (apply (and-then simplify propagate-ineqs))
  </code></pre>
  
  <p>I try different tactics, but wanted result was not obtained. Could you, please, specify tactic for this case?</p>