Z3_error_code class abstract

\brief Z3 error codes (See #Z3_get_error_code).

  • Z3_OK: No error.
  • Z3_SORT_ERROR: User tried to build an invalid (type incorrect) AST.
  • Z3_IOB: Index out of bounds.
  • Z3_INVALID_ARG: Invalid argument was provided.
  • Z3_PARSER_ERROR: An error occurred when parsing a string or file.
  • Z3_NO_PARSER: Parser output is not available, that is, user didn't invoke #Z3_parse_smtlib2_string or #Z3_parse_smtlib2_file.
  • Z3_INVALID_PATTERN: Invalid pattern was used to build a quantifier.
  • Z3_MEMOUT_FAIL: A memory allocation failure was encountered.
  • Z3_FILE_ACCESS_ERRROR: A file could not be accessed.
  • Z3_INVALID_USAGE: API call is invalid in the current state.
  • Z3_INTERNAL_FATAL: An error internal to Z3 occurred.
  • Z3_DEC_REF_ERROR: Trying to decrement the reference counter of an AST that was deleted or the reference counter was not initialized with #Z3_inc_ref.
  • Z3_EXCEPTION: Internal Z3 exception. Additional details can be retrieved using #Z3_get_error_msg.

Constructors

Z3_error_code()

Properties

hashCode → int
The hash code for this object.
no setterinherited
runtimeType → Type
A representation of the runtime type of the object.
no setterinherited

Methods

noSuchMethod(Invocation invocation) → dynamic
Invoked when a nonexistent method or property is accessed.
inherited
toString() → String
A string representation of this object.
inherited

Operators

operator ==(Object other) → bool
The equality operator.
inherited

Constants

DEC_REF_ERROR → const int
EXCEPTION → const int
FILE_ACCESS_ERROR → const int
INTERNAL_FATAL → const int
INVALID_ARG → const int
INVALID_PATTERN → const int
INVALID_USAGE → const int
IOB → const int
MEMOUT_FAIL → const int
NO_PARSER → const int
OK → const int
PARSER_ERROR → const int
SORT_ERROR → const int