From b85f2f7e865828ba2f52efd37c1b399bcc2208ab Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Dec 2021 21:10:07 -0800 Subject: [PATCH] #5704 --- src/api/python/z3/z3.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 8e6a86cf1..ae29a0b01 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4809,7 +4809,7 @@ def Ext(a, b): """ ctx = a.ctx if z3_debug(): - _z3_assert(is_array_sort(a) and is_array(b), "arguments must be arrays") + _z3_assert(is_array_sort(a) and (is_array(b) or b.is_lambda()), "arguments must be arrays") return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)