Method mkConcat

src/api/java/Context.java:1515–1521

Bit-vector concatenation. Remarks: The arguments must have a bit-vector sort. @return The result is a bit-vector of size n1+n2, where n1 (n2) is the size of t1 (t2).

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

     *
     **/
    public BitVecExpr mkConcat(Expr<BitVecSort> t1, Expr<BitVecSort> t2)
    {
        checkContextMatch(t1);
        checkContextMatch(t2);
        return new BitVecExpr(this, Native.mkConcat(nCtx(),
                t1.getNativeObject(), t2.getNativeObject()));
    }

    /**
     * Bit-vector extraction.