2

In python, after import z3, I did x = Int('x'). This gave me the traceback

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)

I installed z3 with pip install angr-z3. What's wrong?

Patrick Trentin
  • 7,126
  • 3
  • 23
  • 40
Elliot Gorokhovsky
  • 3,610
  • 2
  • 31
  • 56
  • `'x'` is undefined as a symbol?? – Nikos M. Dec 16 '15 at 00:28
  • I've never seen this or similar errors, it may well be that the pip package is out of date (and 4.4.2 is not released yet, so this is unstable). Can you tell me what system you are trying to run this on? – Christoph Wintersteiger Dec 16 '15 at 13:15
  • 1
    At the moment, the angr-z3 package is broken, but I have no way to tell whether this is related to your problem at all. Can you get and compile the latest master to see whether the problem also exists there? – Christoph Wintersteiger Dec 16 '15 at 15:19
  • @ChristophWintersteiger Thanks! Now it works. You might want to post an answer saying angr-z3 is broken for other people who run into this problem; I'll accept it. – Elliot Gorokhovsky Dec 18 '15 at 00:52
  • Fantastic, thanks for letting us know! I wasn't aware of that package before, but I'm in contact with the authors now to get this sorted out. – Christoph Wintersteiger Dec 18 '15 at 11:46

0 Answers0