From 682b947ad392428911f30bc5c2dccf6ba32051c0 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 7 Feb 2021 12:46:36 +0000 Subject: [PATCH] the documentation of Z3_model_get_func_interp() says it returns NULL if there's no interpretation so let's honour that instead of throwing an exception --- src/api/api_model.cpp | 1 - 1 file changed, 1 deletion(-) diff --git a/src/api/api_model.cpp b/src/api/api_model.cpp index 1fd9ad1f9..61d0931a2 100644 --- a/src/api/api_model.cpp +++ b/src/api/api_model.cpp @@ -89,7 +89,6 @@ extern "C" { CHECK_NON_NULL(m, nullptr); func_interp * _fi = to_model_ref(m)->get_func_interp(to_func_decl(f)); if (!_fi) { - SET_ERROR_CODE(Z3_INVALID_ARG, nullptr); RETURN_Z3(nullptr); } Z3_func_interp_ref * fi = alloc(Z3_func_interp_ref, *mk_c(c), to_model_ref(m));