mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-04 05:19:11 +00:00
Code Activity

the documentation of Z3_model_get_func_interp() says it returns NULL if there's no interpretation

Browse source 
so let's honour that instead of throwing an exception
This commit is contained in:
Nuno Lopes 2021-02-07 12:46:36 +00:00
parent e1572096ca
commit 682b947ad3
1 changed files with 0 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/api/api_model.cpp
View file

@ -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));