3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00

Bugfix for Z3_is_numeral for finite-domain numerals.

Relates to #318
This commit is contained in:
Christoph M. Wintersteiger 2015-12-02 14:41:46 +00:00
parent 52bbd67cd3
commit 00ce124db3

View file

@ -149,7 +149,8 @@ extern "C" {
mk_c(c)->autil().is_numeral(e) ||
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)->fpautil().is_rm_numeral(e) ||
mk_c(c)->datalog_util().is_numeral_ext(e);
Z3_CATCH_RETURN(Z3_FALSE);
}