From 831afa8124763dc7d78c5e0905fc5246aa4b5ea5 Mon Sep 17 00:00:00 2001 From: Zachary Wimer Date: Mon, 19 Apr 2021 17:55:23 -0700 Subject: [PATCH] Cpp api add missing fp methods (return type correction) (#5200) * added is_nan and is_inf to API * added support to to_ieee_bv * bug fix --- src/api/c++/z3++.h | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index f4991817d..acbe2a225 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -873,7 +873,7 @@ namespace z3 { /** \brief Return true if this expression is an fpa and is inf */ - bool is_inf() const { + expr is_inf() const { assert(is_fpa()); Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast); check_error(); @@ -883,7 +883,7 @@ namespace z3 { /** \brief Return true if this expression is an fpa and is NaN */ - bool is_nan() const { + expr is_nan() const { assert(is_fpa()); Z3_ast r = Z3_mk_fpa_is_nan(ctx(), m_ast); check_error(); @@ -893,7 +893,7 @@ namespace z3 { /** \brief Convert this fpa into an IEEE BV */ - bool to_ieee_bv() const { + expr to_ieee_bv() const { assert(is_fpa()); Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast), check_error();