mk
open fun <T : KBvSort> mkBvExtractExprNoSimplify(high: Int, low: Int, value: KExpr<T>): KBvExtractExpr
Create BitVec extract (extract) expression. Extract bits from low (including) to high (including) as a new BitVec.