Method getUnsatCore

src/api/java/Optimize.java:271–275

The unsat core of the last Check. Remarks: The unsat core is a subset of Assumptions The result is empty if Check was not invoked before, if its results was not UNSATISFIABLE, or if core production is disabled. @throws Z3Exception

()

     * @throws Z3Exception
     **/
    public BoolExpr[] getUnsatCore()
    {
        ASTVector core = new ASTVector(getContext(), Native.optimizeGetUnsatCore(getContext().nCtx(), getNativeObject()));        
        return core.ToBoolExprArray();
    }

    /**
     *  Declare an arithmetical maximization objective.