check

@JvmName(name = "check")

abstract fun check(timeout: Duration = Duration.INFINITE): KSolverStatus

Performs satisfiability check of currently asserted expressions.

satisfiability check result.

KSolverStatus.SAT assertions are satisfiable. Satisfying assignment can be retrieved via model.
KSolverStatus.UNSAT assertions are unsatisfiable. Unsat core can be retrieved via unsatCore.
KSolverStatus.UNKNOWN solver failed to check satisfiability due to timeout or internal reasons. Brief reason description may be obtained via reasonOfUnknown.

timeout

solver check timeout. When time limit is reached KSolverStatus.UNKNOWN is returned.