z3-opti

    Configuration config = Configuration.defaultConfiguration();


    Z3FormulaManager mgr = Z3FormulaManager.create(null, config);

    // TODO: without type casts?..
    Z3RationalFormulaManager rfmgr =
        (Z3RationalFormulaManager) mgr.getRationalFormulaManager();

    Z3TheoremProver prover = new Z3TheoremProver(mgr);

    NumeralFormula.RationalFormula x = rfmgr.makeVariable("x");
    NumeralFormula.RationalFormula ten = rfmgr.makeNumber(BigInteger.ONE);

    // Assert x <= 10
    prover.push(rfmgr.lessThan(x, ten));

    // Maximize for x.  // TODO: without type casts?
    int response = prover.isOpt((Z3Formula) x, true);
    System.out.println("Is UNSAT = " + prover.isUnsat());

    System.out.println("Got response = " + response);

    // OK now let's try to get a model.
    Model model = prover.getModel();

    // TODO: looks like I keep getting back a number zero, while I clearly want ten.
    System.out.println("Got model: " + model);