How to output assertions made with z3py in SMT-LIB2 format? I can't find any mention of that in the documentation. I found a flag Z3_PRINT_SMTLIB_FULL but I don't know how to set it.
3
votes
1 Answers
1
votes
You can use the method sexpr(). For example: http://rise4fun.com/Z3Py/9t
x, y = Reals('x y')
print (x + y * 3).sexpr()
There is online documentation of the Python API. For example, the sexpr() method is documented under:
http://research.microsoft.com/en-us/um/redmond/projects/z3/z3.html#ExprRef
