Method check

src/api/java/Solver.java:235–248

Checks whether the assertions in the solver are consistent or not. Remarks: @see #getModel @see #getUnsatCore @see #getProof

(Expr<BoolSort>... assumptions)

     * @see #getProof
     **/
    @SafeVarargs
    public final Status check(Expr<BoolSort>... assumptions)
    {
        Z3_lbool r;
        if (assumptions == null) {
            r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
                getNativeObject()));
        } else {
            r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
                .nCtx(), getNativeObject(), assumptions.length, AST
                .arrayToNative(assumptions)));
        }
	return lboolToStatus(r);
    }

    /**
     * Checks whether the assertions in the solver are consistent or not.