mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 20:18:18 +00:00
Code Activity

#5704

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-12-12 21:10:07 -08:00
parent 0a7e003709
commit b85f2f7e86
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/api/python/z3/z3.py
View file

@ -4809,7 +4809,7 @@ def Ext(a, b):
""" """
ctx = a.ctx ctx = a.ctx
if z3_debug(): 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) return _to_expr_ref(Z3_mk_array_ext(ctx.ref(), a.as_ast(), b.as_ast()), ctx)