From 9cf99e26a6aaa2acc6b5a496088a85d06a1bd16a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 3 Feb 2019 19:54:08 +0100 Subject: [PATCH] fix #2123 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 4de05d31c..7185f520b 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4490,11 +4490,15 @@ def K(dom, v): return ArrayRef(Z3_mk_const_array(ctx.ref(), dom.ast, v.as_ast()), ctx) def Ext(a, b): - """Return extensionality index for arrays. + """Return extensionality index for one-dimensional arrays. + >> a, b = Consts('a b', SetSort(IntSort())) + >> Ext(a, b) + Ext(a, b) """ + ctx = a.ctx if __debug__: - _z3_assert(is_array(a) and is_array(b)) - return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast())); + _z3_assert(is_array(a) and is_array(b), "arguments must be arrays") + return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx) def is_select(a): """Return `True` if `a` is a Z3 array select application.