UnknownExplanation

enum cvc5 :: UnknownExplanation

The different reasons for returning an “unknown” result.

Values:

enumerator REQUIRES_FULL_CHECK

Full satisfiability check required (e.g., if only preprocessing was performed).

enumerator INCOMPLETE

Incomplete theory solver.

enumerator TIMEOUT

Time limit reached.

enumerator RESOURCEOUT

Resource limit reached.

enumerator MEMOUT

Memory limit reached.

enumerator INTERRUPTED

Solver was interrupted.

enumerator UNSUPPORTED

Unsupported feature encountered.

enumerator OTHER

Other reason.

enumerator UNKNOWN_REASON

No specific reason given.