ksmt-core/io.ksmt/KContext/mkBvSignedDivExpr

mkBvSignedDivExpr

open fun <T : KBvSort> mkBvSignedDivExpr(arg0: KExpr<T>, arg1: KExpr<T>): KExpr<T>

Create BitVec arithmetic signed division (bvsdiv) expression. The division result sign depends on the arguments signs.

See also

for the unsigned division.