mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 04:03:39 +00:00
Add comments
This commit is contained in:
parent
7d51353b8b
commit
e32dfad81e
|
@ -13,7 +13,10 @@ def calculate(x, n, ctx):
|
||||||
assert x.ctx == ctx
|
assert x.ctx == ctx
|
||||||
assert x.ctx != main_ctx()
|
assert x.ctx != main_ctx()
|
||||||
|
|
||||||
|
# Parallel creation of z3 object
|
||||||
condition = And(x < 2, x > n, ctx)
|
condition = And(x < 2, x > n, ctx)
|
||||||
|
|
||||||
|
# Parallel solving
|
||||||
solver = Solver(ctx=ctx)
|
solver = Solver(ctx=ctx)
|
||||||
solver.add(condition)
|
solver.add(condition)
|
||||||
solver.check()
|
solver.check()
|
||||||
|
|
Loading…
Reference in a new issue