Method mkBVAdd

src/api/java/Context.java:1284–1290

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

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

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

    /**
     * Two's complement subtraction.