From 541aba308cdd01070515e11c9d5e3fbab98d27a2 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 17 Oct 2022 10:27:15 -0700 Subject: [PATCH] fix #6401 Signed-off-by: Nikolaj Bjorner --- 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 8f227649c..ca3bc6f53 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6653,7 +6653,7 @@ class ModelRef(Z3PPObject): n = Z3_func_entry_get_num_args(x.ctx_ref(), e.entry) v = AstVector() for j in range(n): - v.push(entry.arg_value(j)) + v.push(e.arg_value(j)) val = Z3_func_entry_get_value(x.ctx_ref(), e.entry) Z3_func_interp_add_entry(x.ctx_ref(), fi2.f, v.vector, val) return