#[repr(u32)]
pub enum ErrorCode {
Show 13 variants
OK,
SortError,
IOB,
InvalidArg,
ParserError,
NoParser,
InvalidPattern,
MemoutFail,
FileAccessError,
InternalFatal,
InvalidUsage,
DecRefError,
Exception,
}
Expand description
Z3 error codes (See Z3_get_error_code
).
This corresponds to Z3_error_code
in the C API.
Variants§
OK
No error.
This corresponds to Z3_OK
in the C API.
SortError
User tried to build an invalid (type incorrect) AST.
This corresponds to Z3_SORT_ERROR
in the C API.
IOB
Index out of bounds.
This corresponds to Z3_IOB
in the C API.
InvalidArg
Invalid argument was provided.
This corresponds to Z3_INVALID_ARG
in the C API.
ParserError
An error occurred when parsing a string or file.
This corresponds to Z3_PARSER_ERROR
in the C API.
NoParser
Parser output is not available, that is, user didn’t invoke
Z3_parse_smtlib_string
or
Z3_parse_smtlib_file
.
This corresponds to Z3_NO_PARSER
in the C API.
InvalidPattern
Invalid pattern was used to build a quantifier.
This corresponds to Z3_INVALID_PATTERN
in the C API.
MemoutFail
A memory allocation failure was encountered.
This corresponds to Z3_MEMOUT_FAIL
in the C API.
FileAccessError
A file could not be accessed.
This corresponds to Z3_FILE_ACCESS_ERRROR
in the C API.
InternalFatal
An error internal to Z3 occurred.
This corresponds to Z3_INTERNAL_FATAL
in the C API.
InvalidUsage
API call is invalid in the current state.
This corresponds to Z3_INVALID_USAGE
in the C API.
DecRefError
Trying to decrement the reference counter of an AST that was
deleted or the reference counter was not initialized with
Z3_inc_ref
.
This corresponds to Z3_DEC_REF_ERROR
in the C API.
Exception
Internal Z3 exception. Additional details can be retrieved
using Z3_get_error_msg
.
This corresponds to Z3_EXCEPTION
in the C API.