Enum z3_sys::ErrorCode

#[repr(u32)]
pub enum ErrorCode {
    OK,
    SortError,
    IOB,
    InvalidArg,
    ParserError,
    NoParser,
    InvalidPattern,
    MemoutFail,
    FileAccessError,
    InternalFatal,
    InvalidUsage,
    DecRefError,
    Exception,
}

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_smtlib2_string or Z3_parse_smtlib2_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.

Trait Implementations

impl Clone for ErrorCode

fn clone(&self) -> ErrorCode

Returns a copy of the value.

fn clone_from(&mut self, source: &Self)

Performs copy-assignment from source.

impl Debug for ErrorCode

fn fmt(&self, f: &mut Formatter<'_>) -> Result

Formats the value using the given formatter.

impl Hash for ErrorCode

fn hash<__H: Hasher>(&self, state: &mut __H)

Feeds this value into the given Hasher.

fn hash_slice<H>(data: &[Self], state: &mut H)where H: Hasher, Self: Sized,

Feeds a slice of this type into the given Hasher.

impl PartialEq<ErrorCode> for ErrorCode

fn eq(&self, other: &ErrorCode) -> bool

This method tests for self and other values to be equal, and is used by ==.

fn ne(&self, other: &Rhs) -> bool

This method tests for !=. The default implementation is almost always sufficient, and should not be overridden without very good reason.

impl Copy for ErrorCode

impl Eq for ErrorCode

impl StructuralEq for ErrorCode

impl StructuralPartialEq for ErrorCode