z3 - z3py 在 `Int('x')` 上引发异常

Question

在 python 之后import z3，我做了x = Int('x'). 这给了我回溯

In [16]: x = Int('x')
---------------------------------------------------------------------------
ArgumentError                             Traceback (most recent call last)
<ipython-input-16-adbc8f7df7ed> in <module>()
----> 1 x = Int('x')

/home/elliot/.local/lib/python2.7/site-packages/z3.pyc in Int(name, ctx)
   2754     """
   2755     ctx = _get_ctx(ctx)
-> 2756     return ArithRef(Z3_mk_const(ctx.ref(), to_symbol(name, ctx), IntSort(ctx).ast), ctx)
   2757 
   2758 def Ints(names, ctx=None):

/home/elliot/.local/lib/python2.7/site-packages/z3.pyc in IntSort(ctx)
   2655     """
   2656     ctx = _get_ctx(ctx)
-> 2657     return ArithSortRef(Z3_mk_int_sort(ctx.ref()), ctx)
   2658 
   2659 def RealSort(ctx=None):

/home/elliot/.local/lib/python2.7/site-packages/z3.pyc in __init__(self, ast, ctx)
    275         self.ast  = ast
    276         self.ctx  = _get_ctx(ctx)
--> 277         Z3_inc_ref(self.ctx.ref(), self.as_ast())
    278 
    279     def __del__(self):

/home/elliot/.local/lib/python2.7/site-packages/z3core.pyc in Z3_inc_ref(a0, a1)
   1252 
   1253 def Z3_inc_ref(a0, a1):
-> 1254   lib().Z3_inc_ref(a0, a1)
   1255   err = lib().Z3_get_error_code(a0)
   1256   if err != Z3_OK:

ArgumentError: argument 2: <type 'exceptions.TypeError'>: unbound method from_param() must be called with Ast instance as first argument (got int instance instead)

我用pip install angr-z3. 怎么了？