mk
open fun <T : KBvSort> mkBvSubNoUnderflowExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>, isSigned: Boolean): KBvSubNoUnderflowExpr<T>
Create BitVec sub-no-underflow check expression. Determines that BitVec arithmetic subtraction does not underflow. An underflow occurs when the subtraction result value is lower than min supported value.
See also
for the overflow check.