From dbf93c5fbdf458396c38993fdcac54f4e0803824 Mon Sep 17 00:00:00 2001 From: Walden Yan Date: Sun, 1 Jan 2023 18:27:54 -0500 Subject: [PATCH] Fixing array select for lambda expressions in Python API (#6516) * fix: making array select work for lambda expressions * more elegant solution --- src/api/python/z3/z3.py | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 695bb939f..074570b03 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -4597,10 +4597,10 @@ class ArrayRef(ExprRef): def _array_select(ar, arg): if isinstance(arg, tuple): - args = [ar.domain_n(i).cast(arg[i]) for i in range(len(arg))] + args = [ar.sort().domain_n(i).cast(arg[i]) for i in range(len(arg))] _args, sz = _to_ast_array(args) return _to_expr_ref(Z3_mk_select_n(ar.ctx_ref(), ar.as_ast(), sz, _args), ar.ctx) - arg = ar.domain().cast(arg) + arg = ar.sort().domain().cast(arg) return _to_expr_ref(Z3_mk_select(ar.ctx_ref(), ar.as_ast(), arg.as_ast()), ar.ctx)