From 44d77a978a97fbadefe0cc964c53f24c3679b6d7 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 20 Apr 2021 09:27:46 -0700 Subject: [PATCH] cw review comments #5200 --- src/api/c++/z3++.h | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index acbe2a225..24547891e 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -871,9 +871,9 @@ namespace z3 { bool is_well_sorted() const { bool r = Z3_is_well_sorted(ctx(), m_ast); check_error(); return r; } /** - \brief Return true if this expression is an fpa and is inf + \brief Return Boolean expression to test whether expression is inf */ - expr is_inf() const { + expr mk_is_inf() const { assert(is_fpa()); Z3_ast r = Z3_mk_fpa_is_infinite(ctx(), m_ast); check_error(); @@ -881,9 +881,9 @@ namespace z3 { } /** - \brief Return true if this expression is an fpa and is NaN + \brief Return Boolean expression to test for whether expression is a NaN */ - expr is_nan() const { + expr mk_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 */ - expr to_ieee_bv() const { + expr mk_to_ieee_bv() const { assert(is_fpa()); Z3_ast r = Z3_mk_fpa_to_ieee_bv(ctx(), m_ast), check_error();