From 32f8705ac32b9369955f02f465ccd3cd8e2abd7a Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 19 Nov 2023 10:43:14 -0800 Subject: [PATCH] #7001 - align is_numeral without to behavior if is_numeral with return numeral. --- src/api/api_numeral.cpp | 15 +++++++-------- 1 file changed, 7 insertions(+), 8 deletions(-) diff --git a/src/api/api_numeral.cpp b/src/api/api_numeral.cpp index 7d8c00fbe..ebac4de31 100644 --- a/src/api/api_numeral.cpp +++ b/src/api/api_numeral.cpp @@ -29,13 +29,12 @@ bool is_numeral_sort(Z3_context c, Z3_sort ty) { if (!ty) return false; sort * _ty = to_sort(ty); family_id fid = _ty->get_family_id(); - if (fid != mk_c(c)->get_arith_fid() && - fid != mk_c(c)->get_bv_fid() && - fid != mk_c(c)->get_datalog_fid() && - fid != mk_c(c)->get_fpa_fid()) { - return false; - } - return true; + return + fid == mk_c(c)->get_arith_fid() || + fid == mk_c(c)->get_bv_fid() || + fid == mk_c(c)->get_datalog_fid() || + fid == mk_c(c)->get_fpa_fid(); + } static bool check_numeral_sort(Z3_context c, Z3_sort ty) { @@ -152,7 +151,7 @@ extern "C" { mk_c(c)->bvutil().is_numeral(e) || mk_c(c)->fpautil().is_numeral(e) || mk_c(c)->fpautil().is_rm_numeral(e) || - mk_c(c)->datalog_util().is_numeral_ext(e); + mk_c(c)->datalog_util().is_numeral(e); Z3_CATCH_RETURN(false); }