parameters: (a, b)
return_statement: return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
docstring: A predicate the determines that bit-vector signed multiplication does not underflow
docstring_summary: A predicate the determines that bit-vector signed multiplication does not underflow
docstring_tokens: A predicate the determines that bit - vector signed multiplication does not underflow
function: def BVMulNoUnderflow(a, b):
      """A predicate the determines that bit-vector signed multiplication does not underflow"""
      _check_bv_args(a, b)
      a, b = _coerce_exprs(a, b)
      return BoolRef(Z3_mk_bvmul_no_underflow(a.ctx_ref(), a.as_ast(), b.as_ast()), a.ctx)
function_tokens: def BVMulNoUnderflow ( a , b ) : _check_bv_args ( a , b ) a , b = _coerce_exprs ( a , b ) return BoolRef ( Z3_mk_bvmul_no_underflow ( a . ctx_ref ( ) , a . as_ast ( ) , b . as_ast ( ) ) , a . ctx )