Method bitvectorExample1

examples/java/JavaExample.java:1396–1413

(Context ctx)

    // machine integers
    // / </remarks>
    public void bitvectorExample1(Context ctx) throws TestFailedException
    {
        System.out.println("BitvectorExample1");
        Log.append("BitvectorExample1");

        BitVecSort bv_type = ctx.mkBitVecSort(32);
        BitVecExpr x = (BitVecExpr) ctx.mkConst("x", bv_type);
        BitVecNum zero = (BitVecNum) ctx.mkNumeral("0", bv_type);
        BitVecNum ten = ctx.mkBV(10, 32);
        BitVecExpr x_minus_ten = ctx.mkBVSub(x, ten);
        /* bvsle is signed less than or equal to */
        BoolExpr c1 = ctx.mkBVSLE(x, ten);
        BoolExpr c2 = ctx.mkBVSLE(x_minus_ten, zero);
        BoolExpr thm = ctx.mkIff(c1, c2);
        System.out
                .println("disprove: x - 10 <= 0 IFF x <= 10 for (32-bit) machine integers");
        disprove(ctx, thm, false);
    }

    // / Find x and y such that: x ^ y - 103 == x * y