Method mkBVSub

src/api/java/Context.java:1297–1303

Two's complement subtraction. Remarks: The arguments must have the same bit-vector sort.

(Expr<BitVecSort> t1, Expr<BitVecSort> t2)

     * bit-vector sort.
     **/
    public BitVecExpr mkBVSub(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkBvsub(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    /**
     * Two's complement multiplication.