I found (by modifying alt-ergo configuration to add an incorrect switch) that `Call_provers.analyze_result` returns `Unknown` if no regex matches the prover output. This seems incorrect to me, I thought that `Unknown` meant that the prover returned `Unknown` explicitly. Instead it should return `Failure` or even `HighFailure`, which is also the documentation: ``` type prover_answer = | Valid (** The task is valid according to the prover *) | Invalid (** The task is invalid *) | Timeout (** the task timeouts, ie it takes more time than specified *) | OutOfMemory (** the task runs out of memory *) | StepLimitExceeded (** the task required more steps than the limit provided *) | Unknown of string (** The prover can't determine if the task is valid *) | Failure of string (** The prover reports a failure *) | HighFailure (** An error occured during the call to the prover or none of the given regexps match the output of the prover *) ``` What do you think?