mk Bv Sign Extension Expr No Simplify
open fun <T : KBvSort> mkBvSignExtensionExprNoSimplify(extensionSize: Int, value: KExpr<T>): KBvSignExtensionExpr
Create BitVec signed extension (signext
) expression. Returns a BitVec expression with extensionSize extra sign (leftmost, highest) bits. The extra bits are prepended to the provided value.