title: z3py optimization as variables chosen from a list
body: <p>For the example, how to write code in z3py to maximize value of a+b+c+d as a,b,c,d are all chosen from list [1,2,3,4,5,6,7,8], which is given as the input. a, b, c, d are distinct values.</p>
  
  <pre><code>a, b, c, d = Ints("a b c d")
  o = Optimize()
  list = [1,2,3,4,5,6,7,8]
  o.maximize(a+b+c+d)
  </code></pre>
  
  <p>how to write code corresponding to choose "a b c d" value from list. The correct out value of a+b+c+d is 26
  Thanks!</p>