mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-28 03:15:50 +00:00
Code Activity

#7001 - align is_numeral without to behavior if is_numeral with return numeral.

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-19 10:43:14 -08:00
parent 35bc522dae
commit 32f8705ac3
1 changed files with 7 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

15
src/api/api_numeral.cpp
View file

@ -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);
}