title: Z3 support for nonlinear arithmetic
body: <p>I understand that Z3 has some supports for nonlinear arith but wondering to what extends ?   Is it possible to specify what classes of nonlinear arithmetics are supported and are not (or likely to give time out) ? Know these in advances will help me abort my task early.  </p>
  
  <p>Seems like power related stuff is not supported as shown below</p>
  
  <pre><code>def pow2(x): 
      k=Int('k')
      return Exists(k, And(k&gt;=0,2**k==x))
  
  
  prove(pow2(7))
  failed to prove
  </code></pre>