From 6fcba26ea6c695628fa701aee0e8cf78141ba8d0 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 12 Feb 2017 09:56:49 -0800 Subject: [PATCH] make parameters accessible from expressions. Issue #896 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index f1fde1720..6729d99b5 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -868,6 +868,9 @@ class ExprRef(AstRef): _args, sz = _to_ast_array((a, b)) return BoolRef(Z3_mk_distinct(self.ctx_ref(), 2, _args), self.ctx) + def params(self): + return self.decl().params() + def decl(self): """Return the Z3 function declaration associated with a Z3 application.