649         bool is_bv() const { return sort_kind() == Z3_BV_SORT; }  in is_bv()  function
684 …unsigned bv_size() const { assert(is_bv()); unsigned r = Z3_get_bv_sort_size(ctx(), *this); check_…  in bv_size()
784         bool is_bv() const { return get_sort().is_bv(); }  in is_bv()  function
944             assert(is_bv());  in mk_from_ieee_bv()
1567         if (a.is_bv()) {  in mod()
1637 …inline expr operator==(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); r…
1638 …inline expr operator==(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); r…
1649 …inline expr operator!=(expr const & a, int b) { assert(a.is_arith() || a.is_bv() || a.is_fpa()); r…
1650 …inline expr operator!=(int a, expr const & b) { assert(b.is_arith() || b.is_bv() || b.is_fpa()); r…
1661         else if (a.is_bv() && b.is_bv()) {
1691         else if (a.is_bv() && b.is_bv()) {
1714         else if (a.is_bv() && b.is_bv()) {
1734         else if (a.is_bv() && b.is_bv()) {
1755         else if (a.is_bv()) {
1776         else if (a.is_bv() && b.is_bv()) {
1798         else if (a.is_bv() && b.is_bv()) {
1823         else if (a.is_bv() && b.is_bv()) {
1845         else if (a.is_bv() && b.is_bv()) {
1882         else if (a.is_bv()) {  in min()
1897         else if (a.is_bv()) {  in max()
1907         assert(a.is_bv());  in bvredor()
1913         assert(a.is_bv());  in bvredand()
1964         assert(sgn.is_bv() && exp.is_bv() && sig.is_bv());  in fpa_fp()
1985         assert(t.is_bv());  in sbv_to_fpa()
1992         assert(t.is_bv());  in ubv_to_fpa()