Method getModel

src/api/java/Solver.java:296–304

The model of the last Check. Remarks: The result is null if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled. @throws Z3Exception

()

     * @throws Z3Exception
     **/
    public Model getModel()
    {
        long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
        if (x == 0) {
            return null;
        } else {
            return new Model(getContext(), x);
        }
    }

    /**
     * The proof of the last {@code Check}.