mk Bv Signed Div Expr No Simplify
open fun <T : KBvSort> mkBvSignedDivExprNoSimplify(arg0: KExpr<T>, arg1: KExpr<T>): KBvSignedDivExpr<T>
Create BitVec arithmetic signed division (bvsdiv
) expression. The division result sign depends on the arguments signs.
See also
for the unsigned division.