diff --git a/src/api/api_ast.cpp b/src/api/api_ast.cpp index a8f4d74b7..bc76d02bc 100644 --- a/src/api/api_ast.cpp +++ b/src/api/api_ast.cpp @@ -660,11 +660,14 @@ extern "C" { LOG_Z3_get_domain(c, d, i); RESET_ERROR_CODE(); CHECK_VALID_AST(d, nullptr); - if (i >= to_func_decl(d)->get_arity()) { + func_decl* _d = to_func_decl(d); + if (_d->is_associative()) + i = 0; + if (i >= _d->get_arity()) { SET_ERROR_CODE(Z3_IOB, nullptr); RETURN_Z3(nullptr); } - Z3_sort r = of_sort(to_func_decl(d)->get_domain(i)); + Z3_sort r = of_sort(_d->get_domain(i)); RETURN_Z3(r); Z3_CATCH_RETURN(nullptr); } diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index 074570b03..cf5be3e07 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -763,8 +763,6 @@ class FuncDeclRef(AstRef): >>> f.domain(1) Real """ - if z3_debug(): - _z3_assert(i < self.arity(), "Index out of bounds") return _to_sort_ref(Z3_get_domain(self.ctx_ref(), self.ast, i), self.ctx) def range(self): @@ -834,8 +832,6 @@ class FuncDeclRef(AstRef): """ args = _get_args(args) num = len(args) - if z3_debug(): - _z3_assert(num == self.arity(), "Incorrect number of arguments to %s" % self) _args = (Ast * num)() saved = [] for i in range(num):