From 5356c4f7dde850e38c63468fad72c42ed6f4c460 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 12 Oct 2018 22:44:23 -0700 Subject: [PATCH] remove class from enum class, add default to avoid compiler warning Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index ff953ca8f..e009113fb 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -139,7 +139,7 @@ namespace z3 { */ class context { public: - enum class rounding_mode { + enum rounding_mode { RNA, RNE, RTP, @@ -2693,11 +2693,12 @@ namespace z3 { inline sort context::fpa_rounding_mode() { switch (m_rounding_mode) { - case rounding_mode::RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx)); - case rounding_mode::RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx)); - case rounding_mode::RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx)); - case rounding_mode::RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx)); - case rounding_mode::RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx)); + case rounding_mode::RNA: return sort(*this, Z3_mk_fpa_rna(m_ctx)); + case rounding_mode::RNE: return sort(*this, Z3_mk_fpa_rne(m_ctx)); + case rounding_mode::RTP: return sort(*this, Z3_mk_fpa_rtp(m_ctx)); + case rounding_mode::RTN: return sort(*this, Z3_mk_fpa_rtn(m_ctx)); + case rounding_mode::RTZ: return sort(*this, Z3_mk_fpa_rtz(m_ctx)); + default: return sort(*this); } }