Z3py Context usage-CodePudding

I don't understand how to use contexts in Z3/Z3py. The following example returns context mismatch but if I change the And into an == or Implies it works, and if I remove the context from the declaration of x I get z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value. 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.

from z3 import *

ctx=Context()
solver=Solver(ctx=ctx)
x=Bool('x',ctx=ctx)
solver.add(And(x,x))
print(solver.check())

Traceback (most recent call last):
  File "minimal_test.py", line 6, in <module>
    solver.add(And(x,x))
  File "[...].local/lib/python3.7/site-packages/z3/z3.py", line 1727, in And
    _z3_assert(ctx_args is None or ctx_args == ctx, "context mismatch")
  File "[...].local/lib/python3.7/site-packages/z3/z3.py", line 96, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: context mismatch

CodePudding user response：

The program, as you gave in your question runs just fine for me, producing sat. So, I'm not sure why you're seeing what you're seeing, except perhaps you've an extremely old version of z3 that had a bug or something. (Github master is at 4.11.2; I'm using 4.9.2; what version do you have?)

If you remove the context from the declaration of x, you'll get "z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value" because the x was created in the global context but the solver is created in a particular context. In general, if you have multiple contexts then simply declare all your variables with that context. (By default, they'll all use a global context; which works fine when you don't have explicit declarations.) Functions like And/Or/Implies simply use the context of their arguments to figure out which context to create the expression in.

So, the program as you gave in your question is the correct way to use contexts. Not clear to me why it's failing for you; perhaps you had many versions of this program and somehow confused which one is which?