stp.BVMulNoUnderflow

stp.BVMulNoUnderflow(a, b)