mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-08-01 08:53:18 +00:00
Code Activity

fix logging in Z3_fpa_get_[es]bits

Browse source
This commit is contained in:
Nuno Lopes 2021-08-29 10:58:54 +01:00
parent b1bc890992
commit 9a172939e0
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/api/api_fpa.cpp
View file

@ -877,7 +877,7 @@ extern "C" {
CHECK_VALID_AST(s, 0); CHECK_VALID_AST(s, 0);
if (!is_fp_sort(c, s)) { if (!is_fp_sort(c, s)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected");
RETURN_Z3(0); return 0;
} }
return mk_c(c)->fpautil().get_ebits(to_sort(s)); return mk_c(c)->fpautil().get_ebits(to_sort(s));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);
@ -891,7 +891,7 @@ extern "C" {
CHECK_VALID_AST(s, 0); CHECK_VALID_AST(s, 0);
if (!is_fp_sort(c, s)) { if (!is_fp_sort(c, s)) {
SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected"); SET_ERROR_CODE(Z3_INVALID_ARG, "fp sort expected");
RETURN_Z3(0); return 0;
} }
return mk_c(c)->fpautil().get_sbits(to_sort(s)); return mk_c(c)->fpautil().get_sbits(to_sort(s));
Z3_CATCH_RETURN(0); Z3_CATCH_RETURN(0);