Method getUnsatCore

src/api/java/Solver.java:334–339

The unsat core of the last Check. Remarks: The unsat core is a subset of Assertions 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.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));        
        return core.ToBoolExprArray();
    }

    /**
     * Retrieve currently inferred units.