ksmt-core/io.ksmt/KContext/mkBvExtractExpr

mkBvExtractExpr

open fun <T : KBvSort> mkBvExtractExpr(high: Int, low: Int, value: KExpr<T>): KExpr<KBvSort>

Create BitVec extract (extract) expression. Extract bits from low (including) to high (including) as a new BitVec.