From 3074e2b80c32640e18198115f399a74fcfc1cd2c Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 15 Aug 2019 10:24:28 -0700 Subject: [PATCH] fix #2487 Signed-off-by: Nikolaj Bjorner --- src/api/c++/z3++.h | 14 +++++++++++++- 1 file changed, 13 insertions(+), 1 deletion(-) diff --git a/src/api/c++/z3++.h b/src/api/c++/z3++.h index d90d6e2d6a3..f841f573c95 100644 --- a/src/api/c++/z3++.h +++ b/src/api/c++/z3++.h @@ -1259,10 +1259,22 @@ namespace z3 { inline expr pw(expr const & a, int b) { return pw(a, a.ctx().num_val(b, a.get_sort())); } inline expr pw(int a, expr const & b) { return pw(b.ctx().num_val(a, b.get_sort()), b); } - inline expr mod(expr const& a, expr const& b) { _Z3_MK_BIN_(a, b, Z3_mk_mod); } + inline expr mod(expr const& a, expr const& b) { + if (a.is_bv()) { + _Z3_MK_BIN_(a, b, Z3_mk_bvsmod); + } + else { + _Z3_MK_BIN_(a, b, Z3_mk_mod); + } + } inline expr mod(expr const & a, int b) { return mod(a, a.ctx().num_val(b, a.get_sort())); } inline expr mod(int a, expr const & b) { return mod(b.ctx().num_val(a, b.get_sort()), b); } + inline expr operator%(expr const& a, expr const& b) { return mod(a, b); } + inline expr operator%(expr const& a, int b) { return mod(a, b); } + inline expr operator%(int a, expr const& b) { return mod(a, b); } + + inline expr rem(expr const& a, expr const& b) { if (a.is_fpa() && b.is_fpa()) { _Z3_MK_BIN_(a, b, Z3_mk_fpa_rem);