diff --git a/src/options/option_exception.h b/src/options/option_exception.h index 27beb06dc48..ae1589cdc3c 100644 --- a/src/options/option_exception.h +++ b/src/options/option_exception.h @@ -49,7 +49,23 @@ class CVC5_EXPORT OptionException : public cvc5::internal::Exception /** * Class representing an option-parsing exception such as badly-typed - * or missing arguments, arguments out of bounds, etc. + * or missing arguments, arguments out of bounds, etc. This class is identical + * to the above one but is treated as an unrecoverable exception in the API. + * + * At a high level, this exception is used when the user requests a legal + * combination of options. It is *not* used in other cases, e.g. where the + * user requests an option that does not exist. + * + * In particular, we use this exception in two places: + * (1) If the SetDefaults detects an options misconfiguration e.g. at the + * beginning of a `check-sat` command, in which case any exception is treated + * as unrecoverable. + * (2) If we discover an illegal combination of options during a `set-option` + * command (e.g. due to restrictions on `safe-options`). + * + * The latter is made a fatal exception for consistency, since some + * options misconfigurations are discovered during SetDefaults and others + * are detected eagerly, where in either case we should abort. */ class CVC5_EXPORT FatalOptionException : public cvc5::internal::Exception {