Skip to content

Commit 391880b

Browse files
authored
Add missing ::z3::sdiv to z3++.h (#7947)
1 parent 6173a0d commit 391880b

File tree

1 file changed

+8
-0
lines changed

1 file changed

+8
-0
lines changed

src/api/c++/z3++.h

Lines changed: 8 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -2173,7 +2173,15 @@ namespace z3 {
21732173
inline expr ugt(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvugt(a.ctx(), a, b)); }
21742174
inline expr ugt(expr const & a, int b) { return ugt(a, a.ctx().num_val(b, a.get_sort())); }
21752175
inline expr ugt(int a, expr const & b) { return ugt(b.ctx().num_val(a, b.get_sort()), b); }
2176+
21762177
/**
2178+
\brief signed division operator for bitvectors.
2179+
*/
2180+
inline expr sdiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvsdiv(a.ctx(), a, b)); }
2181+
inline expr sdiv(expr const & a, int b) { return sdiv(a, a.ctx().num_val(b, a.get_sort())); }
2182+
inline expr sdiv(int a, expr const & b) { return sdiv(b.ctx().num_val(a, b.get_sort()), b); }
2183+
2184+
/**
21772185
\brief unsigned division operator for bitvectors.
21782186
*/
21792187
inline expr udiv(expr const & a, expr const & b) { return to_expr(a.ctx(), Z3_mk_bvudiv(a.ctx(), a, b)); }

0 commit comments

Comments
 (0)