Method getProof

src/api/java/Solver.java:315–323

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

()

     * @throws Z3Exception
     **/
    public Expr<?> getProof()
    {
        long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
        if (x == 0) {
            return null;
        } else {
            return Expr.create(getContext(), x);
        }
    }

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