title: Z3py Context usage
body: <p>I don't understand how to use contexts in Z3/Z3py. The following example returns <code>context mismatch</code> but if I change the <code>And</code> into an <code>==</code> or <code>Implies</code> it works, and if I remove the context from the declaration of <code>x</code> I get <code>z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value</code>. Why? I know that I don't need context in this simple example but I need to parallelize a more complex script that uses Z3py.</p>
  <pre><code>from z3 import *
  
  ctx=Context()
  solver=Solver(ctx=ctx)
  x=Bool('x',ctx=ctx)
  solver.add(And(x,x))
  print(solver.check())
  </code></pre>
  <pre><code>Traceback (most recent call last):
    File &quot;minimal_test.py&quot;, line 6, in &lt;module&gt;
      solver.add(And(x,x))
    File &quot;[...].local/lib/python3.7/site-packages/z3/z3.py&quot;, line 1727, in And
      _z3_assert(ctx_args is None or ctx_args == ctx, &quot;context mismatch&quot;)
    File &quot;[...].local/lib/python3.7/site-packages/z3/z3.py&quot;, line 96, in _z3_assert
      raise Z3Exception(msg)
  z3.z3types.Z3Exception: context mismatch
  </code></pre>