UnknownExplanation

This enum represents the explanation for an unknown solver result (see Result).

class cvc5.UnknownExplanation(value)

The UnknownExplanation enum

INCOMPLETE

Incomplete theory solver.

INTERRUPTED

Solver was interrupted.

MEMOUT

Memory limit reached.

OTHER

Other reason.

REQUIRES_CHECK_AGAIN

Requires another satisfiability check

REQUIRES_FULL_CHECK

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

RESOURCEOUT

Resource limit reached.

TIMEOUT

Time limit reached.

UNKNOWN_REASON

No specific reason given.

UNSUPPORTED

Unsupported feature encountered.