title: Use Z3 and SMT-LIB to get a maximum of two values
body: <p>How do I get the maximum of a formula using smt-lib2?</p>
  
  <p>I want something like this:</p>
  
  <pre><code>(declare-fun x () Int)
  (declare-fun y () Int)
  (declare-fun z () Int)
  (assert (= x 2))
  (assert (= y 4))
  (assert (= z (max x y))
  (check-sat)
  (get-model)
  (exit)
  </code></pre>
  
  <p>Of course, 'max' is unknown to smtlibv2.
  So, how can this be done?</p>