diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 63092b2cf..10ede0922 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -50,14 +50,13 @@ extern "C" { Z3_CATCH; } - Z3_ast Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) { + Z3_ast_opt Z3_API Z3_model_get_const_interp(Z3_context c, Z3_model m, Z3_func_decl a) { Z3_TRY; LOG_Z3_model_get_const_interp(c, m, a); RESET_ERROR_CODE(); CHECK_NON_NULL(m, 0); expr * r = to_model_ref(m)->get_const_interp(to_func_decl(a)); if (!r) { - SET_ERROR_CODE(Z3_INVALID_ARG); RETURN_Z3(0); } mk_c(c)->save_ast_trail(r); diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index 6e8544770..9fb664819 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1582,6 +1582,9 @@ namespace z3 { return static_cast(i) < num_consts() ? get_const_decl(i) : get_func_decl(i - num_consts()); } + // returns interpretation of constant declaration c. + // If c is not assigned any value in the model it returns + // an expression with a null ast reference. expr get_const_interp(func_decl c) const { check_context(*this, c); Z3_ast r = Z3_model_get_const_interp(ctx(), m_model, c); diff --git a/src/api/python/z3.py b/src/api/python/z3.py index 848883ba3..2126cf0fe 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -5516,7 +5516,10 @@ class ModelRef(Z3PPObject): decl = decl.decl() try: if decl.arity() == 0: - r = _to_expr_ref(Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast), self.ctx) + _r = Z3_model_get_const_interp(self.ctx.ref(), self.model, decl.ast) + if _r.value is None: + return None + r = _to_expr_ref(_r, self.ctx) if is_as_array(r): return self.get_interp(get_as_array_func(r)) else: