mk
open fun <T : KBvSort> mkBvNegationNoOverflowExprNoSimplify(value: KExpr<T>): KBvNegNoOverflowExpr<T>
Create BitVec neg-no-overflow check expression. Determines that BitVec arithmetic negation does not overflow.