Z3Py: Vector with defined context does not add their elements to context.

[rakovskij-stanislav]

>>> from z3 import *
>>> ctx # checking "ctx" is not defined in globals/locals
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
NameError: name 'ctx' is not defined
>>> ctx = Context() # making new context
>>> a = IntVector("a", 12, ctx=ctx)
>>> a[0].ctx == ctx
False      # so there is an error. It's expectable elements of vector with defined context will be own by it
>>> s = Solver(ctx=ctx)
>>> s.add(a[0] == 8) # of course, there will be an error
Traceback (most recent call last):
  File "<stdin>", line 1, in <module>
  File "/home/egor/.local/lib/python3.6/site-packages/z3/z3.py", line 6572, in add
    self.assert_exprs(*args)
  File "/home/egor/.local/lib/python3.6/site-packages/z3/z3.py", line 6560, in assert_exprs
    arg = s.cast(arg)
  File "/home/egor/.local/lib/python3.6/site-packages/z3/z3.py", line 1391, in cast
    _z3_assert(self.eq(val.sort()), "Value cannot be converted into a Z3 Boolean value")
  File "/home/egor/.local/lib/python3.6/site-packages/z3/z3.py", line 96, in _z3_assert
    raise Z3Exception(msg)
z3.z3types.Z3Exception: Value cannot be converted into a Z3 Boolean value
>>> b = Int("b", ctx=ctx)
>>> s.add(b==19) # everything is OK with Int, not InvVector
>>>

[rakovskij-stanislav]

Thank you)