[INFO] crate z3_ref 0.1.4 is already in cache [INFO] testing z3_ref-0.1.4 against 1.44.0 for beta-1.45-1 [INFO] extracting crate z3_ref 0.1.4 into /workspace/builds/worker-2/source [INFO] validating manifest of crates.io crate z3_ref 0.1.4 on toolchain 1.44.0 [INFO] running `"/workspace/cargo-home/bin/cargo" "+1.44.0" "read-manifest" "--manifest-path" "Cargo.toml"` [INFO] started tweaking crates.io crate z3_ref 0.1.4 [INFO] finished tweaking crates.io crate z3_ref 0.1.4 [INFO] tweaked toml for crates.io crate z3_ref 0.1.4 written to /workspace/builds/worker-2/source/Cargo.toml [INFO] running `"/workspace/cargo-home/bin/cargo" "+1.44.0" "generate-lockfile" "--manifest-path" "Cargo.toml" "-Zno-index-update"` [INFO] running `"/workspace/cargo-home/bin/cargo" "+1.44.0" "fetch" "--locked" "--manifest-path" "Cargo.toml"` [INFO] running `"docker" "create" "-v" "/var/lib/crater-agent-workspace/builds/worker-2/target:/opt/rustwide/target:rw,Z" "-v" "/var/lib/crater-agent-workspace/builds/worker-2/source:/opt/rustwide/workdir:ro,Z" "-v" "/var/lib/crater-agent-workspace/cargo-home:/opt/rustwide/cargo-home:ro,Z" "-v" "/var/lib/crater-agent-workspace/rustup-home:/opt/rustwide/rustup-home:ro,Z" "-e" "SOURCE_DIR=/opt/rustwide/workdir" "-e" "MAP_USER_ID=0" "-e" "CARGO_TARGET_DIR=/opt/rustwide/target" "-e" "CARGO_INCREMENTAL=0" "-e" "RUST_BACKTRACE=full" "-e" "RUSTFLAGS=--cap-lints=warn" "-e" "CARGO_HOME=/opt/rustwide/cargo-home" "-e" "RUSTUP_HOME=/opt/rustwide/rustup-home" "-w" "/opt/rustwide/workdir" "-m" "1610612736" "--network" "none" "rustops/crates-build-env" "/opt/rustwide/cargo-home/bin/cargo" "+1.44.0" "build" "--frozen"` [INFO] [stderr] WARNING: Your kernel does not support swap limit capabilities or the cgroup is not mounted. Memory limited without swap. [INFO] [stdout] 1d1e78dfb4569fd25f76be1e72d35276f07d836aedf6519d692ad5604ca477b7 [INFO] running `"docker" "start" "-a" "1d1e78dfb4569fd25f76be1e72d35276f07d836aedf6519d692ad5604ca477b7"` [INFO] [stderr] sudo: setrlimit(RLIMIT_CORE): Operation not permitted [INFO] [stderr] Compiling bindgen v0.40.0 [INFO] [stderr] Compiling clang-sys v0.23.0 [INFO] [stderr] Compiling z3_ref v0.1.4 (/opt/rustwide/workdir) [INFO] [stderr] error[E0061]: this function takes 4 arguments but 2 arguments were supplied [INFO] [stderr] --> src/lib.rs:298:24 [INFO] [stderr] | [INFO] [stderr] 298 | unsafe { match z::Z3_optimize_check(self.ctx(), self.solver()) { [INFO] [stderr] | ^^^^^^^^^^^^^^^^^^^^ ---------- ------------- supplied 2 arguments [INFO] [stderr] | | [INFO] [stderr] | expected 4 arguments [INFO] [stderr] | [INFO] [stderr] ::: /opt/rustwide/target/debug/build/z3_ref-db41cdb1396ad73d/out/bindings.rs:3:125372 [INFO] [stderr] | [INFO] [stderr] 3 | pub const _STDIO_H : u32 = 1 ; pub const _FEATURES_H : u32 = 1 ; pub const _DEFAULT_SOURCE : u32 = 1 ; pub const __GLIBC_USE_ISOC2X : u32 = 0 ; pub const __USE_ISOC11 : u32 = 1 ; pub const __USE_ISOC99 : u32 = 1 ; pub const __USE_ISOC95 : u32 = 1 ; pub const __USE_POSIX_IMPLICITLY : u32 = 1 ; pub const _POSIX_SOURCE : u32 = 1 ; pub const _POSIX_C_SOURCE : u32 = 200809 ; pub const __USE_POSIX : u32 = 1 ; pub const __USE_POSIX2 : u32 = 1 ; pub const __USE_POSIX199309 : u32 = 1 ; pub const __USE_POSIX199506 : u32 = 1 ; pub const __USE_XOPEN2K : u32 = 1 ; pub const __USE_XOPEN2K8 : u32 = 1 ; pub const _ATFILE_SOURCE : u32 = 1 ; pub const __USE_MISC : u32 = 1 ; pub const __USE_ATFILE : u32 = 1 ; pub const __USE_FORTIFY_LEVEL : u32 = 0 ; pub const __GLIBC_USE_DEPRECATED_GETS : u32 = 0 ; pub const __GLIBC_USE_DEPRECATED_SCANF : u32 = 0 ; pub const _STDC_PREDEF_H : u32 = 1 ; pub const __STDC_IEC_559__ : u32 = 1 ; pub const __STDC_IEC_559_COMPLEX__ : u32 = 1 ; pub const __STDC_ISO_10646__ : u32 = 201706 ; pub const __GNU_LIBRARY__ : u32 = 6 ; pub const __GLIBC__ : u32 = 2 ; pub const __GLIBC_MINOR__ : u32 = 31 ; pub const _SYS_CDEFS_H : u32 = 1 ; pub const __glibc_c99_flexarr_available : u32 = 1 ; pub const __WORDSIZE : u32 = 64 ; pub const __WORDSIZE_TIME64_COMPAT32 : u32 = 1 ; pub const __SYSCALL_WORDSIZE : u32 = 64 ; pub const __LONG_DOUBLE_USES_FLOAT128 : u32 = 0 ; pub const __HAVE_GENERIC_SELECTION : u32 = 1 ; pub const __GLIBC_USE_LIB_EXT2 : u32 = 0 ; pub const __GLIBC_USE_IEC_60559_BFP_EXT : u32 = 0 ; pub const __GLIBC_USE_IEC_60559_BFP_EXT_C2X : u32 = 0 ; pub const __GLIBC_USE_IEC_60559_FUNCS_EXT : u32 = 0 ; pub const __GLIBC_USE_IEC_60559_FUNCS_EXT_C2X : u32 = 0 ; pub const __GLIBC_USE_IEC_60559_TYPES_EXT : u32 = 0 ; pub const __GNUC_VA_LIST : u32 = 1 ; pub const _BITS_TYPES_H : u32 = 1 ; pub const __TIMESIZE : u32 = 64 ; pub const _BITS_TYPESIZES_H : u32 = 1 ; pub const __OFF_T_MATCHES_OFF64_T : u32 = 1 ; pub const __INO_T_MATCHES_INO64_T : u32 = 1 ; pub const __RLIM_T_MATCHES_RLIM64_T : u32 = 1 ; pub const __STATFS_MATCHES_STATFS64 : u32 = 1 ; pub const __FD_SETSIZE : u32 = 1024 ; pub const _BITS_TIME64_H : u32 = 1 ; pub const _____fpos_t_defined : u32 = 1 ; pub const ____mbstate_t_defined : u32 = 1 ; pub const _____fpos64_t_defined : u32 = 1 ; pub const ____FILE_defined : u32 = 1 ; pub const __FILE_defined : u32 = 1 ; pub const __struct_FILE_defined : u32 = 1 ; pub const _IO_EOF_SEEN : u32 = 16 ; pub const _IO_ERR_SEEN : u32 = 32 ; pub const _IO_USER_LOCK : u32 = 32768 ; pub const _IOFBF : u32 = 0 ; pub const _IOLBF : u32 = 1 ; pub const _IONBF : u32 = 2 ; pub const BUFSIZ : u32 = 8192 ; pub const EOF : i32 = -1 ; pub const SEEK_SET : u32 = 0 ; pub const SEEK_CUR : u32 = 1 ; pub const SEEK_END : u32 = 2 ; pub const P_tmpdir : & 'static [ u8 ; 5usize ] = b"/tmp\0" ; pub const _BITS_STDIO_LIM_H : u32 = 1 ; pub const L_tmpnam : u32 = 20 ; pub const TMP_MAX : u32 = 238328 ; pub const FILENAME_MAX : u32 = 4096 ; pub const L_ctermid : u32 = 9 ; pub const FOPEN_MAX : u32 = 16 ; pub const true_ : u32 = 1 ; pub const false_ : u32 = 0 ; pub const __bool_true_false_are_defined : u32 = 1 ; pub const _STDINT_H : u32 = 1 ; pub const _BITS_WCHAR_H : u32 = 1 ; pub const _BITS_STDINT_INTN_H : u32 = 1 ; pub const _BITS_STDINT_UINTN_H : u32 = 1 ; pub const INT8_MIN : i32 = -128 ; pub const INT16_MIN : i32 = -32768 ; pub const INT32_MIN : i32 = -2147483648 ; pub const INT8_MAX : u32 = 127 ; pub const INT16_MAX : u32 = 32767 ; pub const INT32_MAX : u32 = 2147483647 ; pub const UINT8_MAX : u32 = 255 ; pub const UINT16_MAX : u32 = 65535 ; pub const UINT32_MAX : u32 = 4294967295 ; pub const INT_LEAST8_MIN : i32 = -128 ; pub const INT_LEAST16_MIN : i32 = -32768 ; pub const INT_LEAST32_MIN : i32 = -2147483648 ; pub const INT_LEAST8_MAX : u32 = 127 ; pub const INT_LEAST16_MAX : u32 = 32767 ; pub const INT_LEAST32_MAX : u32 = 2147483647 ; pub const UINT_LEAST8_MAX : u32 = 255 ; pub const UINT_LEAST16_MAX : u32 = 65535 ; pub const UINT_LEAST32_MAX : u32 = 4294967295 ; pub const INT_FAST8_MIN : i32 = -128 ; pub const INT_FAST16_MIN : i64 = -9223372036854775808 ; pub const INT_FAST32_MIN : i64 = -9223372036854775808 ; pub const INT_FAST8_MAX : u32 = 127 ; pub const INT_FAST16_MAX : u64 = 9223372036854775807 ; pub const INT_FAST32_MAX : u64 = 9223372036854775807 ; pub const UINT_FAST8_MAX : u32 = 255 ; pub const UINT_FAST16_MAX : i32 = -1 ; pub const UINT_FAST32_MAX : i32 = -1 ; pub const INTPTR_MIN : i64 = -9223372036854775808 ; pub const INTPTR_MAX : u64 = 9223372036854775807 ; pub const UINTPTR_MAX : i32 = -1 ; pub const PTRDIFF_MIN : i64 = -9223372036854775808 ; pub const PTRDIFF_MAX : u64 = 9223372036854775807 ; pub const SIG_ATOMIC_MIN : i32 = -2147483648 ; pub const SIG_ATOMIC_MAX : u32 = 2147483647 ; pub const SIZE_MAX : i32 = -1 ; pub const WINT_MIN : u32 = 0 ; pub const WINT_MAX : u32 = 4294967295 ; pub const Z3_TRUE : u32 = 1 ; pub const Z3_FALSE : u32 = 0 ; pub type va_list = __builtin_va_list ; pub type __gnuc_va_list = __builtin_va_list ; pub type __u_char = :: std :: os :: raw :: c_uchar ; pub type __u_short = :: std :: os :: raw :: c_ushort ; pub type __u_int = :: std :: os :: raw :: c_uint ; pub type __u_long = :: std :: os :: raw :: c_ulong ; pub type __int8_t = :: std :: os :: raw :: c_schar ; pub type __uint8_t = :: std :: os :: raw :: c_uchar ; pub type __int16_t = :: std :: os :: raw :: c_short ; pub type __uint16_t = :: std :: os :: raw :: c_ushort ; pub type __int32_t = :: std :: os :: raw :: c_int ; pub type __uint32_t = :: std :: os :: raw :: c_uint ; pub type __int64_t = :: std :: os :: raw :: c_long ; pub type __uint64_t = :: std :: os :: raw :: c_ulong ; pub type __int_least8_t = __int8_t ; pub type __uint_least8_t = __uint8_t ; pub type __int_least16_t = __int16_t ; pub type __uint_least16_t = __uint16_t ; pub type __int_least32_t = __int32_t ; pub type __uint_least32_t = __uint32_t ; pub type __int_least64_t = __int64_t ; pub type __uint_least64_t = __uint64_t ; pub type __quad_t = :: std :: os :: raw :: c_long ; pub type __u_quad_t = :: std :: os :: raw :: c_ulong ; pub type __intmax_t = :: std :: os :: raw :: c_long ; pub type __uintmax_t = :: std :: os :: raw :: c_ulong ; pub type __dev_t = :: std :: os :: raw :: c_ulong ; pub type __uid_t = :: std :: os :: raw :: c_uint ; pub type __gid_t = :: std :: os :: raw :: c_uint ; pub type __ino_t = :: std :: os :: raw :: c_ulong ; pub type __ino64_t = :: std :: os :: raw :: c_ulong ; pub type __mode_t = :: std :: os :: raw :: c_uint ; pub type __nlink_t = :: std :: os :: raw :: c_ulong ; pub type __off_t = :: std :: os :: raw :: c_long ; pub type __off64_t = :: std :: os :: raw :: c_long ; pub type __pid_t = :: std :: os :: raw :: c_int ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct __fsid_t { pub __val : [ :: std :: os :: raw :: c_int ; 2usize ] , } # [ test ] fn bindgen_test_layout___fsid_t ( ) { assert_eq ! ( :: std :: mem :: size_of :: < __fsid_t > ( ) , 8usize , concat ! ( "Size of: " , stringify ! ( __fsid_t ) ) ) ; assert_eq ! ( :: std :: mem :: align_of :: < __fsid_t > ( ) , 4usize , concat ! ( "Alignment of " , stringify ! ( __fsid_t ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __fsid_t > ( ) ) ) . __val as * const _ as usize } , 0usize , concat ! ( "Offset of field: " , stringify ! ( __fsid_t ) , "::" , stringify ! ( __val ) ) ) ; } pub type __clock_t = :: std :: os :: raw :: c_long ; pub type __rlim_t = :: std :: os :: raw :: c_ulong ; pub type __rlim64_t = :: std :: os :: raw :: c_ulong ; pub type __id_t = :: std :: os :: raw :: c_uint ; pub type __time_t = :: std :: os :: raw :: c_long ; pub type __useconds_t = :: std :: os :: raw :: c_uint ; pub type __suseconds_t = :: std :: os :: raw :: c_long ; pub type __daddr_t = :: std :: os :: raw :: c_int ; pub type __key_t = :: std :: os :: raw :: c_int ; pub type __clockid_t = :: std :: os :: raw :: c_int ; pub type __timer_t = * mut :: std :: os :: raw :: c_void ; pub type __blksize_t = :: std :: os :: raw :: c_long ; pub type __blkcnt_t = :: std :: os :: raw :: c_long ; pub type __blkcnt64_t = :: std :: os :: raw :: c_long ; pub type __fsblkcnt_t = :: std :: os :: raw :: c_ulong ; pub type __fsblkcnt64_t = :: std :: os :: raw :: c_ulong ; pub type __fsfilcnt_t = :: std :: os :: raw :: c_ulong ; pub type __fsfilcnt64_t = :: std :: os :: raw :: c_ulong ; pub type __fsword_t = :: std :: os :: raw :: c_long ; pub type __ssize_t = :: std :: os :: raw :: c_long ; pub type __syscall_slong_t = :: std :: os :: raw :: c_long ; pub type __syscall_ulong_t = :: std :: os :: raw :: c_ulong ; pub type __loff_t = __off64_t ; pub type __caddr_t = * mut :: std :: os :: raw :: c_char ; pub type __intptr_t = :: std :: os :: raw :: c_long ; pub type __socklen_t = :: std :: os :: raw :: c_uint ; pub type __sig_atomic_t = :: std :: os :: raw :: c_int ; # [ repr ( C ) ] # [ derive ( Copy , Clone ) ] pub struct __mbstate_t { pub __count : :: std :: os :: raw :: c_int , pub __value : __mbstate_t__bindgen_ty_1 , } # [ repr ( C ) ] # [ derive ( Copy , Clone ) ] pub union __mbstate_t__bindgen_ty_1 { pub __wch : :: std :: os :: raw :: c_uint , pub __wchb : [ :: std :: os :: raw :: c_char ; 4usize ] , _bindgen_union_align : u32 , } # [ test ] fn bindgen_test_layout___mbstate_t__bindgen_ty_1 ( ) { assert_eq ! ( :: std :: mem :: size_of :: < __mbstate_t__bindgen_ty_1 > ( ) , 4usize , concat ! ( "Size of: " , stringify ! ( __mbstate_t__bindgen_ty_1 ) ) ) ; assert_eq ! ( :: std :: mem :: align_of :: < __mbstate_t__bindgen_ty_1 > ( ) , 4usize , concat ! ( "Alignment of " , stringify ! ( __mbstate_t__bindgen_ty_1 ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __mbstate_t__bindgen_ty_1 > ( ) ) ) . __wch as * const _ as usize } , 0usize , concat ! ( "Offset of field: " , stringify ! ( __mbstate_t__bindgen_ty_1 ) , "::" , stringify ! ( __wch ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __mbstate_t__bindgen_ty_1 > ( ) ) ) . __wchb as * const _ as usize } , 0usize , concat ! ( "Offset of field: " , stringify ! ( __mbstate_t__bindgen_ty_1 ) , "::" , stringify ! ( __wchb ) ) ) ; } # [ test ] fn bindgen_test_layout___mbstate_t ( ) { assert_eq ! ( :: std :: mem :: size_of :: < __mbstate_t > ( ) , 8usize , concat ! ( "Size of: " , stringify ! ( __mbstate_t ) ) ) ; assert_eq ! ( :: std :: mem :: align_of :: < __mbstate_t > ( ) , 4usize , concat ! ( "Alignment of " , stringify ! ( __mbstate_t ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __mbstate_t > ( ) ) ) . __count as * const _ as usize } , 0usize , concat ! ( "Offset of field: " , stringify ! ( __mbstate_t ) , "::" , stringify ! ( __count ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __mbstate_t > ( ) ) ) . __value as * const _ as usize } , 4usize , concat ! ( "Offset of field: " , stringify ! ( __mbstate_t ) , "::" , stringify ! ( __value ) ) ) ; } # [ repr ( C ) ] # [ derive ( Copy , Clone ) ] pub struct _G_fpos_t { pub __pos : __off_t , pub __state : __mbstate_t , } # [ test ] fn bindgen_test_layout__G_fpos_t ( ) { assert_eq ! ( :: std :: mem :: size_of :: < _G_fpos_t > ( ) , 16usize , concat ! ( "Size of: " , stringify ! ( _G_fpos_t ) ) ) ; assert_eq ! ( :: std :: mem :: align_of :: < _G_fpos_t > ( ) , 8usize , concat ! ( "Alignment of " , stringify ! ( _G_fpos_t ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _G_fpos_t > ( ) ) ) . __pos as * const _ as usize } , 0usize , concat ! ( "Offset of field: " , stringify ! ( _G_fpos_t ) , "::" , stringify ! ( __pos ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _G_fpos_t > ( ) ) ) . __state as * const _ as usize } , 8usize , concat ! ( "Offset of field: " , stringify ! ( _G_fpos_t ) , "::" , stringify ! ( __state ) ) ) ; } pub type __fpos_t = _G_fpos_t ; # [ repr ( C ) ] # [ derive ( Copy , Clone ) ] pub struct _G_fpos64_t { pub __pos : __off64_t , pub __state : __mbstate_t , } # [ test ] fn bindgen_test_layout__G_fpos64_t ( ) { assert_eq ! ( :: std :: mem :: size_of :: < _G_fpos64_t > ( ) , 16usize , concat ! ( "Size of: " , stringify ! ( _G_fpos64_t ) ) ) ; assert_eq ! ( :: std :: mem :: align_of :: < _G_fpos64_t > ( ) , 8usize , concat ! ( "Alignment of " , stringify ! ( _G_fpos64_t ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _G_fpos64_t > ( ) ) ) . __pos as * const _ as usize } , 0usize , concat ! ( "Offset of field: " , stringify ! ( _G_fpos64_t ) , "::" , stringify ! ( __pos ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _G_fpos64_t > ( ) ) ) . __state as * const _ as usize } , 8usize , concat ! ( "Offset of field: " , stringify ! ( _G_fpos64_t ) , "::" , stringify ! ( __state ) ) ) ; } pub type __fpos64_t = _G_fpos64_t ; pub type __FILE = _IO_FILE ; pub type FILE = _IO_FILE ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _IO_marker { _unused : [ u8 ; 0 ] , } # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _IO_codecvt { _unused : [ u8 ; 0 ] , } # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _IO_wide_data { _unused : [ u8 ; 0 ] , } pub type _IO_lock_t = :: std :: os :: raw :: c_void ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _IO_FILE { pub _flags : :: std :: os :: raw :: c_int , pub _IO_read_ptr : * mut :: std :: os :: raw :: c_char , pub _IO_read_end : * mut :: std :: os :: raw :: c_char , pub _IO_read_base : * mut :: std :: os :: raw :: c_char , pub _IO_write_base : * mut :: std :: os :: raw :: c_char , pub _IO_write_ptr : * mut :: std :: os :: raw :: c_char , pub _IO_write_end : * mut :: std :: os :: raw :: c_char , pub _IO_buf_base : * mut :: std :: os :: raw :: c_char , pub _IO_buf_end : * mut :: std :: os :: raw :: c_char , pub _IO_save_base : * mut :: std :: os :: raw :: c_char , pub _IO_backup_base : * mut :: std :: os :: raw :: c_char , pub _IO_save_end : * mut :: std :: os :: raw :: c_char , pub _markers : * mut _IO_marker , pub _chain : * mut _IO_FILE , pub _fileno : :: std :: os :: raw :: c_int , pub _flags2 : :: std :: os :: raw :: c_int , pub _old_offset : __off_t , pub _cur_column : :: std :: os :: raw :: c_ushort , pub _vtable_offset : :: std :: os :: raw :: c_schar , pub _shortbuf : [ :: std :: os :: raw :: c_char ; 1usize ] , pub _lock : * mut _IO_lock_t , pub _offset : __off64_t , pub _codecvt : * mut _IO_codecvt , pub _wide_data : * mut _IO_wide_data , pub _freeres_list : * mut _IO_FILE , pub _freeres_buf : * mut :: std :: os :: raw :: c_void , pub __pad5 : usize , pub _mode : :: std :: os :: raw :: c_int , pub _unused2 : [ :: std :: os :: raw :: c_char ; 20usize ] , } # [ test ] fn bindgen_test_layout__IO_FILE ( ) { assert_eq ! ( :: std :: mem :: size_of :: < _IO_FILE > ( ) , 216usize , concat ! ( "Size of: " , stringify ! ( _IO_FILE ) ) ) ; assert_eq ! ( :: std :: mem :: align_of :: < _IO_FILE > ( ) , 8usize , concat ! ( "Alignment of " , stringify ! ( _IO_FILE ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _flags as * const _ as usize } , 0usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _flags ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_read_ptr as * const _ as usize } , 8usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_read_ptr ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_read_end as * const _ as usize } , 16usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_read_end ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_read_base as * const _ as usize } , 24usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_read_base ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_write_base as * const _ as usize } , 32usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_write_base ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_write_ptr as * const _ as usize } , 40usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_write_ptr ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_write_end as * const _ as usize } , 48usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_write_end ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_buf_base as * const _ as usize } , 56usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_buf_base ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_buf_end as * const _ as usize } , 64usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_buf_end ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_save_base as * const _ as usize } , 72usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_save_base ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_backup_base as * const _ as usize } , 80usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_backup_base ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _IO_save_end as * const _ as usize } , 88usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _IO_save_end ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _markers as * const _ as usize } , 96usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _markers ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _chain as * const _ as usize } , 104usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _chain ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _fileno as * const _ as usize } , 112usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _fileno ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _flags2 as * const _ as usize } , 116usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _flags2 ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _old_offset as * const _ as usize } , 120usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _old_offset ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _cur_column as * const _ as usize } , 128usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _cur_column ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _vtable_offset as * const _ as usize } , 130usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _vtable_offset ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _shortbuf as * const _ as usize } , 131usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _shortbuf ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _lock as * const _ as usize } , 136usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _lock ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _offset as * const _ as usize } , 144usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _offset ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _codecvt as * const _ as usize } , 152usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _codecvt ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _wide_data as * const _ as usize } , 160usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _wide_data ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _freeres_list as * const _ as usize } , 168usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _freeres_list ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _freeres_buf as * const _ as usize } , 176usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _freeres_buf ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . __pad5 as * const _ as usize } , 184usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( __pad5 ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _mode as * const _ as usize } , 192usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _mode ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < _IO_FILE > ( ) ) ) . _unused2 as * const _ as usize } , 196usize , concat ! ( "Offset of field: " , stringify ! ( _IO_FILE ) , "::" , stringify ! ( _unused2 ) ) ) ; } pub type off_t = __off_t ; pub type fpos_t = __fpos_t ; extern "C" { # [ link_name = "\u{1}stdin" ] pub static mut stdin : * mut FILE ; } extern "C" { # [ link_name = "\u{1}stdout" ] pub static mut stdout : * mut FILE ; } extern "C" { # [ link_name = "\u{1}stderr" ] pub static mut stderr : * mut FILE ; } extern "C" { pub fn remove ( __filename : * const :: std :: os :: raw :: c_char ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn rename ( __old : * const :: std :: os :: raw :: c_char , __new : * const :: std :: os :: raw :: c_char ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn renameat ( __oldfd : :: std :: os :: raw :: c_int , __old : * const :: std :: os :: raw :: c_char , __newfd : :: std :: os :: raw :: c_int , __new : * const :: std :: os :: raw :: c_char ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn tmpfile ( ) -> * mut FILE ; } extern "C" { pub fn tmpnam ( __s : * mut :: std :: os :: raw :: c_char ) -> * mut :: std :: os :: raw :: c_char ; } extern "C" { pub fn tmpnam_r ( __s : * mut :: std :: os :: raw :: c_char ) -> * mut :: std :: os :: raw :: c_char ; } extern "C" { pub fn tempnam ( __dir : * const :: std :: os :: raw :: c_char , __pfx : * const :: std :: os :: raw :: c_char ) -> * mut :: std :: os :: raw :: c_char ; } extern "C" { pub fn fclose ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fflush ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fflush_unlocked ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fopen ( __filename : * const :: std :: os :: raw :: c_char , __modes : * const :: std :: os :: raw :: c_char ) -> * mut FILE ; } extern "C" { pub fn freopen ( __filename : * const :: std :: os :: raw :: c_char , __modes : * const :: std :: os :: raw :: c_char , __stream : * mut FILE ) -> * mut FILE ; } extern "C" { pub fn fdopen ( __fd : :: std :: os :: raw :: c_int , __modes : * const :: std :: os :: raw :: c_char ) -> * mut FILE ; } extern "C" { pub fn fmemopen ( __s : * mut :: std :: os :: raw :: c_void , __len : usize , __modes : * const :: std :: os :: raw :: c_char ) -> * mut FILE ; } extern "C" { pub fn open_memstream ( __bufloc : * mut * mut :: std :: os :: raw :: c_char , __sizeloc : * mut usize ) -> * mut FILE ; } extern "C" { pub fn setbuf ( __stream : * mut FILE , __buf : * mut :: std :: os :: raw :: c_char ) ; } extern "C" { pub fn setvbuf ( __stream : * mut FILE , __buf : * mut :: std :: os :: raw :: c_char , __modes : :: std :: os :: raw :: c_int , __n : usize ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn setbuffer ( __stream : * mut FILE , __buf : * mut :: std :: os :: raw :: c_char , __size : usize ) ; } extern "C" { pub fn setlinebuf ( __stream : * mut FILE ) ; } extern "C" { pub fn fprintf ( __stream : * mut FILE , __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn printf ( __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn sprintf ( __s : * mut :: std :: os :: raw :: c_char , __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn vfprintf ( __s : * mut FILE , __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn vprintf ( __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn vsprintf ( __s : * mut :: std :: os :: raw :: c_char , __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn snprintf ( __s : * mut :: std :: os :: raw :: c_char , __maxlen : usize , __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn vsnprintf ( __s : * mut :: std :: os :: raw :: c_char , __maxlen : usize , __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn vdprintf ( __fd : :: std :: os :: raw :: c_int , __fmt : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn dprintf ( __fd : :: std :: os :: raw :: c_int , __fmt : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fscanf ( __stream : * mut FILE , __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn scanf ( __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn sscanf ( __s : * const :: std :: os :: raw :: c_char , __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { # [ link_name = "\u{1}__isoc99_fscanf" ] pub fn fscanf1 ( __stream : * mut FILE , __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { # [ link_name = "\u{1}__isoc99_scanf" ] pub fn scanf1 ( __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { # [ link_name = "\u{1}__isoc99_sscanf" ] pub fn sscanf1 ( __s : * const :: std :: os :: raw :: c_char , __format : * const :: std :: os :: raw :: c_char , ... ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn vfscanf ( __s : * mut FILE , __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn vscanf ( __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn vsscanf ( __s : * const :: std :: os :: raw :: c_char , __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { # [ link_name = "\u{1}__isoc99_vfscanf" ] pub fn vfscanf1 ( __s : * mut FILE , __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { # [ link_name = "\u{1}__isoc99_vscanf" ] pub fn vscanf1 ( __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { # [ link_name = "\u{1}__isoc99_vsscanf" ] pub fn vsscanf1 ( __s : * const :: std :: os :: raw :: c_char , __format : * const :: std :: os :: raw :: c_char , __arg : * mut __va_list_tag ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fgetc ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn getc ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn getchar ( ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn getc_unlocked ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn getchar_unlocked ( ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fgetc_unlocked ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fputc ( __c : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn putc ( __c : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn putchar ( __c : :: std :: os :: raw :: c_int ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fputc_unlocked ( __c : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn putc_unlocked ( __c : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn putchar_unlocked ( __c : :: std :: os :: raw :: c_int ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn getw ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn putw ( __w : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fgets ( __s : * mut :: std :: os :: raw :: c_char , __n : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> * mut :: std :: os :: raw :: c_char ; } extern "C" { pub fn __getdelim ( __lineptr : * mut * mut :: std :: os :: raw :: c_char , __n : * mut usize , __delimiter : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> __ssize_t ; } extern "C" { pub fn getdelim ( __lineptr : * mut * mut :: std :: os :: raw :: c_char , __n : * mut usize , __delimiter : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> __ssize_t ; } extern "C" { pub fn getline ( __lineptr : * mut * mut :: std :: os :: raw :: c_char , __n : * mut usize , __stream : * mut FILE ) -> __ssize_t ; } extern "C" { pub fn fputs ( __s : * const :: std :: os :: raw :: c_char , __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn puts ( __s : * const :: std :: os :: raw :: c_char ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn ungetc ( __c : :: std :: os :: raw :: c_int , __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fread ( __ptr : * mut :: std :: os :: raw :: c_void , __size : usize , __n : usize , __stream : * mut FILE ) -> :: std :: os :: raw :: c_ulong ; } extern "C" { pub fn fwrite ( __ptr : * const :: std :: os :: raw :: c_void , __size : usize , __n : usize , __s : * mut FILE ) -> :: std :: os :: raw :: c_ulong ; } extern "C" { pub fn fread_unlocked ( __ptr : * mut :: std :: os :: raw :: c_void , __size : usize , __n : usize , __stream : * mut FILE ) -> usize ; } extern "C" { pub fn fwrite_unlocked ( __ptr : * const :: std :: os :: raw :: c_void , __size : usize , __n : usize , __stream : * mut FILE ) -> usize ; } extern "C" { pub fn fseek ( __stream : * mut FILE , __off : :: std :: os :: raw :: c_long , __whence : :: std :: os :: raw :: c_int ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn ftell ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_long ; } extern "C" { pub fn rewind ( __stream : * mut FILE ) ; } extern "C" { pub fn fseeko ( __stream : * mut FILE , __off : __off_t , __whence : :: std :: os :: raw :: c_int ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn ftello ( __stream : * mut FILE ) -> __off_t ; } extern "C" { pub fn fgetpos ( __stream : * mut FILE , __pos : * mut fpos_t ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fsetpos ( __stream : * mut FILE , __pos : * const fpos_t ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn clearerr ( __stream : * mut FILE ) ; } extern "C" { pub fn feof ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn ferror ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn clearerr_unlocked ( __stream : * mut FILE ) ; } extern "C" { pub fn feof_unlocked ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn ferror_unlocked ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn perror ( __s : * const :: std :: os :: raw :: c_char ) ; } extern "C" { # [ link_name = "\u{1}sys_nerr" ] pub static mut sys_nerr : :: std :: os :: raw :: c_int ; } extern "C" { # [ link_name = "\u{1}sys_errlist" ] pub static mut sys_errlist : [ * const :: std :: os :: raw :: c_char ; 0usize ] ; } extern "C" { pub fn fileno ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn fileno_unlocked ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn popen ( __command : * const :: std :: os :: raw :: c_char , __modes : * const :: std :: os :: raw :: c_char ) -> * mut FILE ; } extern "C" { pub fn pclose ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn ctermid ( __s : * mut :: std :: os :: raw :: c_char ) -> * mut :: std :: os :: raw :: c_char ; } extern "C" { pub fn flockfile ( __stream : * mut FILE ) ; } extern "C" { pub fn ftrylockfile ( __stream : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn funlockfile ( __stream : * mut FILE ) ; } extern "C" { pub fn __uflow ( arg1 : * mut FILE ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn __overflow ( arg1 : * mut FILE , arg2 : :: std :: os :: raw :: c_int ) -> :: std :: os :: raw :: c_int ; } pub type int_least8_t = __int_least8_t ; pub type int_least16_t = __int_least16_t ; pub type int_least32_t = __int_least32_t ; pub type int_least64_t = __int_least64_t ; pub type uint_least8_t = __uint_least8_t ; pub type uint_least16_t = __uint_least16_t ; pub type uint_least32_t = __uint_least32_t ; pub type uint_least64_t = __uint_least64_t ; pub type int_fast8_t = :: std :: os :: raw :: c_schar ; pub type int_fast16_t = :: std :: os :: raw :: c_long ; pub type int_fast32_t = :: std :: os :: raw :: c_long ; pub type int_fast64_t = :: std :: os :: raw :: c_long ; pub type uint_fast8_t = :: std :: os :: raw :: c_uchar ; pub type uint_fast16_t = :: std :: os :: raw :: c_ulong ; pub type uint_fast32_t = :: std :: os :: raw :: c_ulong ; pub type uint_fast64_t = :: std :: os :: raw :: c_ulong ; pub type intmax_t = __intmax_t ; pub type uintmax_t = __uintmax_t ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_symbol { _unused : [ u8 ; 0 ] , } pub type Z3_symbol = * mut _Z3_symbol ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_literals { _unused : [ u8 ; 0 ] , } pub type Z3_literals = * mut _Z3_literals ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_config { _unused : [ u8 ; 0 ] , } pub type Z3_config = * mut _Z3_config ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_context { _unused : [ u8 ; 0 ] , } pub type Z3_context = * mut _Z3_context ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_sort { _unused : [ u8 ; 0 ] , } pub type Z3_sort = * mut _Z3_sort ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_func_decl { _unused : [ u8 ; 0 ] , } pub type Z3_func_decl = * mut _Z3_func_decl ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_ast { _unused : [ u8 ; 0 ] , } pub type Z3_ast = * mut _Z3_ast ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_app { _unused : [ u8 ; 0 ] , } pub type Z3_app = * mut _Z3_app ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_pattern { _unused : [ u8 ; 0 ] , } pub type Z3_pattern = * mut _Z3_pattern ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_model { _unused : [ u8 ; 0 ] , } pub type Z3_model = * mut _Z3_model ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_constructor { _unused : [ u8 ; 0 ] , } pub type Z3_constructor = * mut _Z3_constructor ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_constructor_list { _unused : [ u8 ; 0 ] , } pub type Z3_constructor_list = * mut _Z3_constructor_list ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_params { _unused : [ u8 ; 0 ] , } pub type Z3_params = * mut _Z3_params ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_param_descrs { _unused : [ u8 ; 0 ] , } pub type Z3_param_descrs = * mut _Z3_param_descrs ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_goal { _unused : [ u8 ; 0 ] , } pub type Z3_goal = * mut _Z3_goal ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_tactic { _unused : [ u8 ; 0 ] , } pub type Z3_tactic = * mut _Z3_tactic ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_probe { _unused : [ u8 ; 0 ] , } pub type Z3_probe = * mut _Z3_probe ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_stats { _unused : [ u8 ; 0 ] , } pub type Z3_stats = * mut _Z3_stats ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_solver { _unused : [ u8 ; 0 ] , } pub type Z3_solver = * mut _Z3_solver ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_ast_vector { _unused : [ u8 ; 0 ] , } pub type Z3_ast_vector = * mut _Z3_ast_vector ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_ast_map { _unused : [ u8 ; 0 ] , } pub type Z3_ast_map = * mut _Z3_ast_map ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_apply_result { _unused : [ u8 ; 0 ] , } pub type Z3_apply_result = * mut _Z3_apply_result ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_func_interp { _unused : [ u8 ; 0 ] , } pub type Z3_func_interp = * mut _Z3_func_interp ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_func_entry { _unused : [ u8 ; 0 ] , } pub type Z3_func_entry = * mut _Z3_func_entry ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_fixedpoint { _unused : [ u8 ; 0 ] , } pub type Z3_fixedpoint = * mut _Z3_fixedpoint ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_optimize { _unused : [ u8 ; 0 ] , } pub type Z3_optimize = * mut _Z3_optimize ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct _Z3_rcf_num { _unused : [ u8 ; 0 ] , } pub type Z3_rcf_num = * mut _Z3_rcf_num ; pub type Z3_bool = bool ; pub type Z3_string = * const :: std :: os :: raw :: c_char ; pub type Z3_char_ptr = * const :: std :: os :: raw :: c_char ; pub type Z3_string_ptr = * mut Z3_string ; pub const Z3_lbool_Z3_L_FALSE : Z3_lbool = -1 ; pub const Z3_lbool_Z3_L_UNDEF : Z3_lbool = 0 ; pub const Z3_lbool_Z3_L_TRUE : Z3_lbool = 1 ; pub type Z3_lbool = i32 ; pub const Z3_symbol_kind_Z3_INT_SYMBOL : Z3_symbol_kind = 0 ; pub const Z3_symbol_kind_Z3_STRING_SYMBOL : Z3_symbol_kind = 1 ; pub type Z3_symbol_kind = u32 ; pub const Z3_parameter_kind_Z3_PARAMETER_INT : Z3_parameter_kind = 0 ; pub const Z3_parameter_kind_Z3_PARAMETER_DOUBLE : Z3_parameter_kind = 1 ; pub const Z3_parameter_kind_Z3_PARAMETER_RATIONAL : Z3_parameter_kind = 2 ; pub const Z3_parameter_kind_Z3_PARAMETER_SYMBOL : Z3_parameter_kind = 3 ; pub const Z3_parameter_kind_Z3_PARAMETER_SORT : Z3_parameter_kind = 4 ; pub const Z3_parameter_kind_Z3_PARAMETER_AST : Z3_parameter_kind = 5 ; pub const Z3_parameter_kind_Z3_PARAMETER_FUNC_DECL : Z3_parameter_kind = 6 ; pub type Z3_parameter_kind = u32 ; pub const Z3_sort_kind_Z3_UNINTERPRETED_SORT : Z3_sort_kind = 0 ; pub const Z3_sort_kind_Z3_BOOL_SORT : Z3_sort_kind = 1 ; pub const Z3_sort_kind_Z3_INT_SORT : Z3_sort_kind = 2 ; pub const Z3_sort_kind_Z3_REAL_SORT : Z3_sort_kind = 3 ; pub const Z3_sort_kind_Z3_BV_SORT : Z3_sort_kind = 4 ; pub const Z3_sort_kind_Z3_ARRAY_SORT : Z3_sort_kind = 5 ; pub const Z3_sort_kind_Z3_DATATYPE_SORT : Z3_sort_kind = 6 ; pub const Z3_sort_kind_Z3_RELATION_SORT : Z3_sort_kind = 7 ; pub const Z3_sort_kind_Z3_FINITE_DOMAIN_SORT : Z3_sort_kind = 8 ; pub const Z3_sort_kind_Z3_FLOATING_POINT_SORT : Z3_sort_kind = 9 ; pub const Z3_sort_kind_Z3_ROUNDING_MODE_SORT : Z3_sort_kind = 10 ; pub const Z3_sort_kind_Z3_SEQ_SORT : Z3_sort_kind = 11 ; pub const Z3_sort_kind_Z3_RE_SORT : Z3_sort_kind = 12 ; pub const Z3_sort_kind_Z3_UNKNOWN_SORT : Z3_sort_kind = 1000 ; pub type Z3_sort_kind = u32 ; pub const Z3_ast_kind_Z3_NUMERAL_AST : Z3_ast_kind = 0 ; pub const Z3_ast_kind_Z3_APP_AST : Z3_ast_kind = 1 ; pub const Z3_ast_kind_Z3_VAR_AST : Z3_ast_kind = 2 ; pub const Z3_ast_kind_Z3_QUANTIFIER_AST : Z3_ast_kind = 3 ; pub const Z3_ast_kind_Z3_SORT_AST : Z3_ast_kind = 4 ; pub const Z3_ast_kind_Z3_FUNC_DECL_AST : Z3_ast_kind = 5 ; pub const Z3_ast_kind_Z3_UNKNOWN_AST : Z3_ast_kind = 1000 ; pub type Z3_ast_kind = u32 ; pub const Z3_decl_kind_Z3_OP_TRUE : Z3_decl_kind = 256 ; pub const Z3_decl_kind_Z3_OP_FALSE : Z3_decl_kind = 257 ; pub const Z3_decl_kind_Z3_OP_EQ : Z3_decl_kind = 258 ; pub const Z3_decl_kind_Z3_OP_DISTINCT : Z3_decl_kind = 259 ; pub const Z3_decl_kind_Z3_OP_ITE : Z3_decl_kind = 260 ; pub const Z3_decl_kind_Z3_OP_AND : Z3_decl_kind = 261 ; pub const Z3_decl_kind_Z3_OP_OR : Z3_decl_kind = 262 ; pub const Z3_decl_kind_Z3_OP_IFF : Z3_decl_kind = 263 ; pub const Z3_decl_kind_Z3_OP_XOR : Z3_decl_kind = 264 ; pub const Z3_decl_kind_Z3_OP_NOT : Z3_decl_kind = 265 ; pub const Z3_decl_kind_Z3_OP_IMPLIES : Z3_decl_kind = 266 ; pub const Z3_decl_kind_Z3_OP_OEQ : Z3_decl_kind = 267 ; pub const Z3_decl_kind_Z3_OP_ANUM : Z3_decl_kind = 512 ; pub const Z3_decl_kind_Z3_OP_AGNUM : Z3_decl_kind = 513 ; pub const Z3_decl_kind_Z3_OP_LE : Z3_decl_kind = 514 ; pub const Z3_decl_kind_Z3_OP_GE : Z3_decl_kind = 515 ; pub const Z3_decl_kind_Z3_OP_LT : Z3_decl_kind = 516 ; pub const Z3_decl_kind_Z3_OP_GT : Z3_decl_kind = 517 ; pub const Z3_decl_kind_Z3_OP_ADD : Z3_decl_kind = 518 ; pub const Z3_decl_kind_Z3_OP_SUB : Z3_decl_kind = 519 ; pub const Z3_decl_kind_Z3_OP_UMINUS : Z3_decl_kind = 520 ; pub const Z3_decl_kind_Z3_OP_MUL : Z3_decl_kind = 521 ; pub const Z3_decl_kind_Z3_OP_DIV : Z3_decl_kind = 522 ; pub const Z3_decl_kind_Z3_OP_IDIV : Z3_decl_kind = 523 ; pub const Z3_decl_kind_Z3_OP_REM : Z3_decl_kind = 524 ; pub const Z3_decl_kind_Z3_OP_MOD : Z3_decl_kind = 525 ; pub const Z3_decl_kind_Z3_OP_TO_REAL : Z3_decl_kind = 526 ; pub const Z3_decl_kind_Z3_OP_TO_INT : Z3_decl_kind = 527 ; pub const Z3_decl_kind_Z3_OP_IS_INT : Z3_decl_kind = 528 ; pub const Z3_decl_kind_Z3_OP_POWER : Z3_decl_kind = 529 ; pub const Z3_decl_kind_Z3_OP_STORE : Z3_decl_kind = 768 ; pub const Z3_decl_kind_Z3_OP_SELECT : Z3_decl_kind = 769 ; pub const Z3_decl_kind_Z3_OP_CONST_ARRAY : Z3_decl_kind = 770 ; pub const Z3_decl_kind_Z3_OP_ARRAY_MAP : Z3_decl_kind = 771 ; pub const Z3_decl_kind_Z3_OP_ARRAY_DEFAULT : Z3_decl_kind = 772 ; pub const Z3_decl_kind_Z3_OP_SET_UNION : Z3_decl_kind = 773 ; pub const Z3_decl_kind_Z3_OP_SET_INTERSECT : Z3_decl_kind = 774 ; pub const Z3_decl_kind_Z3_OP_SET_DIFFERENCE : Z3_decl_kind = 775 ; pub const Z3_decl_kind_Z3_OP_SET_COMPLEMENT : Z3_decl_kind = 776 ; pub const Z3_decl_kind_Z3_OP_SET_SUBSET : Z3_decl_kind = 777 ; pub const Z3_decl_kind_Z3_OP_AS_ARRAY : Z3_decl_kind = 778 ; pub const Z3_decl_kind_Z3_OP_ARRAY_EXT : Z3_decl_kind = 779 ; pub const Z3_decl_kind_Z3_OP_SET_HAS_SIZE : Z3_decl_kind = 780 ; pub const Z3_decl_kind_Z3_OP_SET_CARD : Z3_decl_kind = 781 ; pub const Z3_decl_kind_Z3_OP_BNUM : Z3_decl_kind = 1024 ; pub const Z3_decl_kind_Z3_OP_BIT1 : Z3_decl_kind = 1025 ; pub const Z3_decl_kind_Z3_OP_BIT0 : Z3_decl_kind = 1026 ; pub const Z3_decl_kind_Z3_OP_BNEG : Z3_decl_kind = 1027 ; pub const Z3_decl_kind_Z3_OP_BADD : Z3_decl_kind = 1028 ; pub const Z3_decl_kind_Z3_OP_BSUB : Z3_decl_kind = 1029 ; pub const Z3_decl_kind_Z3_OP_BMUL : Z3_decl_kind = 1030 ; pub const Z3_decl_kind_Z3_OP_BSDIV : Z3_decl_kind = 1031 ; pub const Z3_decl_kind_Z3_OP_BUDIV : Z3_decl_kind = 1032 ; pub const Z3_decl_kind_Z3_OP_BSREM : Z3_decl_kind = 1033 ; pub const Z3_decl_kind_Z3_OP_BUREM : Z3_decl_kind = 1034 ; pub const Z3_decl_kind_Z3_OP_BSMOD : Z3_decl_kind = 1035 ; pub const Z3_decl_kind_Z3_OP_BSDIV0 : Z3_decl_kind = 1036 ; pub const Z3_decl_kind_Z3_OP_BUDIV0 : Z3_decl_kind = 1037 ; pub const Z3_decl_kind_Z3_OP_BSREM0 : Z3_decl_kind = 1038 ; pub const Z3_decl_kind_Z3_OP_BUREM0 : Z3_decl_kind = 1039 ; pub const Z3_decl_kind_Z3_OP_BSMOD0 : Z3_decl_kind = 1040 ; pub const Z3_decl_kind_Z3_OP_ULEQ : Z3_decl_kind = 1041 ; pub const Z3_decl_kind_Z3_OP_SLEQ : Z3_decl_kind = 1042 ; pub const Z3_decl_kind_Z3_OP_UGEQ : Z3_decl_kind = 1043 ; pub const Z3_decl_kind_Z3_OP_SGEQ : Z3_decl_kind = 1044 ; pub const Z3_decl_kind_Z3_OP_ULT : Z3_decl_kind = 1045 ; pub const Z3_decl_kind_Z3_OP_SLT : Z3_decl_kind = 1046 ; pub const Z3_decl_kind_Z3_OP_UGT : Z3_decl_kind = 1047 ; pub const Z3_decl_kind_Z3_OP_SGT : Z3_decl_kind = 1048 ; pub const Z3_decl_kind_Z3_OP_BAND : Z3_decl_kind = 1049 ; pub const Z3_decl_kind_Z3_OP_BOR : Z3_decl_kind = 1050 ; pub const Z3_decl_kind_Z3_OP_BNOT : Z3_decl_kind = 1051 ; pub const Z3_decl_kind_Z3_OP_BXOR : Z3_decl_kind = 1052 ; pub const Z3_decl_kind_Z3_OP_BNAND : Z3_decl_kind = 1053 ; pub const Z3_decl_kind_Z3_OP_BNOR : Z3_decl_kind = 1054 ; pub const Z3_decl_kind_Z3_OP_BXNOR : Z3_decl_kind = 1055 ; pub const Z3_decl_kind_Z3_OP_CONCAT : Z3_decl_kind = 1056 ; pub const Z3_decl_kind_Z3_OP_SIGN_EXT : Z3_decl_kind = 1057 ; pub const Z3_decl_kind_Z3_OP_ZERO_EXT : Z3_decl_kind = 1058 ; pub const Z3_decl_kind_Z3_OP_EXTRACT : Z3_decl_kind = 1059 ; pub const Z3_decl_kind_Z3_OP_REPEAT : Z3_decl_kind = 1060 ; pub const Z3_decl_kind_Z3_OP_BREDOR : Z3_decl_kind = 1061 ; pub const Z3_decl_kind_Z3_OP_BREDAND : Z3_decl_kind = 1062 ; pub const Z3_decl_kind_Z3_OP_BCOMP : Z3_decl_kind = 1063 ; pub const Z3_decl_kind_Z3_OP_BSHL : Z3_decl_kind = 1064 ; pub const Z3_decl_kind_Z3_OP_BLSHR : Z3_decl_kind = 1065 ; pub const Z3_decl_kind_Z3_OP_BASHR : Z3_decl_kind = 1066 ; pub const Z3_decl_kind_Z3_OP_ROTATE_LEFT : Z3_decl_kind = 1067 ; pub const Z3_decl_kind_Z3_OP_ROTATE_RIGHT : Z3_decl_kind = 1068 ; pub const Z3_decl_kind_Z3_OP_EXT_ROTATE_LEFT : Z3_decl_kind = 1069 ; pub const Z3_decl_kind_Z3_OP_EXT_ROTATE_RIGHT : Z3_decl_kind = 1070 ; pub const Z3_decl_kind_Z3_OP_BIT2BOOL : Z3_decl_kind = 1071 ; pub const Z3_decl_kind_Z3_OP_INT2BV : Z3_decl_kind = 1072 ; pub const Z3_decl_kind_Z3_OP_BV2INT : Z3_decl_kind = 1073 ; pub const Z3_decl_kind_Z3_OP_CARRY : Z3_decl_kind = 1074 ; pub const Z3_decl_kind_Z3_OP_XOR3 : Z3_decl_kind = 1075 ; pub const Z3_decl_kind_Z3_OP_BSMUL_NO_OVFL : Z3_decl_kind = 1076 ; pub const Z3_decl_kind_Z3_OP_BUMUL_NO_OVFL : Z3_decl_kind = 1077 ; pub const Z3_decl_kind_Z3_OP_BSMUL_NO_UDFL : Z3_decl_kind = 1078 ; pub const Z3_decl_kind_Z3_OP_BSDIV_I : Z3_decl_kind = 1079 ; pub const Z3_decl_kind_Z3_OP_BUDIV_I : Z3_decl_kind = 1080 ; pub const Z3_decl_kind_Z3_OP_BSREM_I : Z3_decl_kind = 1081 ; pub const Z3_decl_kind_Z3_OP_BUREM_I : Z3_decl_kind = 1082 ; pub const Z3_decl_kind_Z3_OP_BSMOD_I : Z3_decl_kind = 1083 ; pub const Z3_decl_kind_Z3_OP_PR_UNDEF : Z3_decl_kind = 1280 ; pub const Z3_decl_kind_Z3_OP_PR_TRUE : Z3_decl_kind = 1281 ; pub const Z3_decl_kind_Z3_OP_PR_ASSERTED : Z3_decl_kind = 1282 ; pub const Z3_decl_kind_Z3_OP_PR_GOAL : Z3_decl_kind = 1283 ; pub const Z3_decl_kind_Z3_OP_PR_MODUS_PONENS : Z3_decl_kind = 1284 ; pub const Z3_decl_kind_Z3_OP_PR_REFLEXIVITY : Z3_decl_kind = 1285 ; pub const Z3_decl_kind_Z3_OP_PR_SYMMETRY : Z3_decl_kind = 1286 ; pub const Z3_decl_kind_Z3_OP_PR_TRANSITIVITY : Z3_decl_kind = 1287 ; pub const Z3_decl_kind_Z3_OP_PR_TRANSITIVITY_STAR : Z3_decl_kind = 1288 ; pub const Z3_decl_kind_Z3_OP_PR_MONOTONICITY : Z3_decl_kind = 1289 ; pub const Z3_decl_kind_Z3_OP_PR_QUANT_INTRO : Z3_decl_kind = 1290 ; pub const Z3_decl_kind_Z3_OP_PR_BIND : Z3_decl_kind = 1291 ; pub const Z3_decl_kind_Z3_OP_PR_DISTRIBUTIVITY : Z3_decl_kind = 1292 ; pub const Z3_decl_kind_Z3_OP_PR_AND_ELIM : Z3_decl_kind = 1293 ; pub const Z3_decl_kind_Z3_OP_PR_NOT_OR_ELIM : Z3_decl_kind = 1294 ; pub const Z3_decl_kind_Z3_OP_PR_REWRITE : Z3_decl_kind = 1295 ; pub const Z3_decl_kind_Z3_OP_PR_REWRITE_STAR : Z3_decl_kind = 1296 ; pub const Z3_decl_kind_Z3_OP_PR_PULL_QUANT : Z3_decl_kind = 1297 ; pub const Z3_decl_kind_Z3_OP_PR_PUSH_QUANT : Z3_decl_kind = 1298 ; pub const Z3_decl_kind_Z3_OP_PR_ELIM_UNUSED_VARS : Z3_decl_kind = 1299 ; pub const Z3_decl_kind_Z3_OP_PR_DER : Z3_decl_kind = 1300 ; pub const Z3_decl_kind_Z3_OP_PR_QUANT_INST : Z3_decl_kind = 1301 ; pub const Z3_decl_kind_Z3_OP_PR_HYPOTHESIS : Z3_decl_kind = 1302 ; pub const Z3_decl_kind_Z3_OP_PR_LEMMA : Z3_decl_kind = 1303 ; pub const Z3_decl_kind_Z3_OP_PR_UNIT_RESOLUTION : Z3_decl_kind = 1304 ; pub const Z3_decl_kind_Z3_OP_PR_IFF_TRUE : Z3_decl_kind = 1305 ; pub const Z3_decl_kind_Z3_OP_PR_IFF_FALSE : Z3_decl_kind = 1306 ; pub const Z3_decl_kind_Z3_OP_PR_COMMUTATIVITY : Z3_decl_kind = 1307 ; pub const Z3_decl_kind_Z3_OP_PR_DEF_AXIOM : Z3_decl_kind = 1308 ; pub const Z3_decl_kind_Z3_OP_PR_ASSUMPTION_ADD : Z3_decl_kind = 1309 ; pub const Z3_decl_kind_Z3_OP_PR_LEMMA_ADD : Z3_decl_kind = 1310 ; pub const Z3_decl_kind_Z3_OP_PR_REDUNDANT_DEL : Z3_decl_kind = 1311 ; pub const Z3_decl_kind_Z3_OP_PR_CLAUSE_TRAIL : Z3_decl_kind = 1312 ; pub const Z3_decl_kind_Z3_OP_PR_DEF_INTRO : Z3_decl_kind = 1313 ; pub const Z3_decl_kind_Z3_OP_PR_APPLY_DEF : Z3_decl_kind = 1314 ; pub const Z3_decl_kind_Z3_OP_PR_IFF_OEQ : Z3_decl_kind = 1315 ; pub const Z3_decl_kind_Z3_OP_PR_NNF_POS : Z3_decl_kind = 1316 ; pub const Z3_decl_kind_Z3_OP_PR_NNF_NEG : Z3_decl_kind = 1317 ; pub const Z3_decl_kind_Z3_OP_PR_SKOLEMIZE : Z3_decl_kind = 1318 ; pub const Z3_decl_kind_Z3_OP_PR_MODUS_PONENS_OEQ : Z3_decl_kind = 1319 ; pub const Z3_decl_kind_Z3_OP_PR_TH_LEMMA : Z3_decl_kind = 1320 ; pub const Z3_decl_kind_Z3_OP_PR_HYPER_RESOLVE : Z3_decl_kind = 1321 ; pub const Z3_decl_kind_Z3_OP_RA_STORE : Z3_decl_kind = 1536 ; pub const Z3_decl_kind_Z3_OP_RA_EMPTY : Z3_decl_kind = 1537 ; pub const Z3_decl_kind_Z3_OP_RA_IS_EMPTY : Z3_decl_kind = 1538 ; pub const Z3_decl_kind_Z3_OP_RA_JOIN : Z3_decl_kind = 1539 ; pub const Z3_decl_kind_Z3_OP_RA_UNION : Z3_decl_kind = 1540 ; pub const Z3_decl_kind_Z3_OP_RA_WIDEN : Z3_decl_kind = 1541 ; pub const Z3_decl_kind_Z3_OP_RA_PROJECT : Z3_decl_kind = 1542 ; pub const Z3_decl_kind_Z3_OP_RA_FILTER : Z3_decl_kind = 1543 ; pub const Z3_decl_kind_Z3_OP_RA_NEGATION_FILTER : Z3_decl_kind = 1544 ; pub const Z3_decl_kind_Z3_OP_RA_RENAME : Z3_decl_kind = 1545 ; pub const Z3_decl_kind_Z3_OP_RA_COMPLEMENT : Z3_decl_kind = 1546 ; pub const Z3_decl_kind_Z3_OP_RA_SELECT : Z3_decl_kind = 1547 ; pub const Z3_decl_kind_Z3_OP_RA_CLONE : Z3_decl_kind = 1548 ; pub const Z3_decl_kind_Z3_OP_FD_CONSTANT : Z3_decl_kind = 1549 ; pub const Z3_decl_kind_Z3_OP_FD_LT : Z3_decl_kind = 1550 ; pub const Z3_decl_kind_Z3_OP_SEQ_UNIT : Z3_decl_kind = 1551 ; pub const Z3_decl_kind_Z3_OP_SEQ_EMPTY : Z3_decl_kind = 1552 ; pub const Z3_decl_kind_Z3_OP_SEQ_CONCAT : Z3_decl_kind = 1553 ; pub const Z3_decl_kind_Z3_OP_SEQ_PREFIX : Z3_decl_kind = 1554 ; pub const Z3_decl_kind_Z3_OP_SEQ_SUFFIX : Z3_decl_kind = 1555 ; pub const Z3_decl_kind_Z3_OP_SEQ_CONTAINS : Z3_decl_kind = 1556 ; pub const Z3_decl_kind_Z3_OP_SEQ_EXTRACT : Z3_decl_kind = 1557 ; pub const Z3_decl_kind_Z3_OP_SEQ_REPLACE : Z3_decl_kind = 1558 ; pub const Z3_decl_kind_Z3_OP_SEQ_AT : Z3_decl_kind = 1559 ; pub const Z3_decl_kind_Z3_OP_SEQ_NTH : Z3_decl_kind = 1560 ; pub const Z3_decl_kind_Z3_OP_SEQ_LENGTH : Z3_decl_kind = 1561 ; pub const Z3_decl_kind_Z3_OP_SEQ_INDEX : Z3_decl_kind = 1562 ; pub const Z3_decl_kind_Z3_OP_SEQ_LAST_INDEX : Z3_decl_kind = 1563 ; pub const Z3_decl_kind_Z3_OP_SEQ_TO_RE : Z3_decl_kind = 1564 ; pub const Z3_decl_kind_Z3_OP_SEQ_IN_RE : Z3_decl_kind = 1565 ; pub const Z3_decl_kind_Z3_OP_STR_TO_INT : Z3_decl_kind = 1566 ; pub const Z3_decl_kind_Z3_OP_INT_TO_STR : Z3_decl_kind = 1567 ; pub const Z3_decl_kind_Z3_OP_RE_PLUS : Z3_decl_kind = 1568 ; pub const Z3_decl_kind_Z3_OP_RE_STAR : Z3_decl_kind = 1569 ; pub const Z3_decl_kind_Z3_OP_RE_OPTION : Z3_decl_kind = 1570 ; pub const Z3_decl_kind_Z3_OP_RE_CONCAT : Z3_decl_kind = 1571 ; pub const Z3_decl_kind_Z3_OP_RE_UNION : Z3_decl_kind = 1572 ; pub const Z3_decl_kind_Z3_OP_RE_RANGE : Z3_decl_kind = 1573 ; pub const Z3_decl_kind_Z3_OP_RE_LOOP : Z3_decl_kind = 1574 ; pub const Z3_decl_kind_Z3_OP_RE_INTERSECT : Z3_decl_kind = 1575 ; pub const Z3_decl_kind_Z3_OP_RE_EMPTY_SET : Z3_decl_kind = 1576 ; pub const Z3_decl_kind_Z3_OP_RE_FULL_SET : Z3_decl_kind = 1577 ; pub const Z3_decl_kind_Z3_OP_RE_COMPLEMENT : Z3_decl_kind = 1578 ; pub const Z3_decl_kind_Z3_OP_LABEL : Z3_decl_kind = 1792 ; pub const Z3_decl_kind_Z3_OP_LABEL_LIT : Z3_decl_kind = 1793 ; pub const Z3_decl_kind_Z3_OP_DT_CONSTRUCTOR : Z3_decl_kind = 2048 ; pub const Z3_decl_kind_Z3_OP_DT_RECOGNISER : Z3_decl_kind = 2049 ; pub const Z3_decl_kind_Z3_OP_DT_IS : Z3_decl_kind = 2050 ; pub const Z3_decl_kind_Z3_OP_DT_ACCESSOR : Z3_decl_kind = 2051 ; pub const Z3_decl_kind_Z3_OP_DT_UPDATE_FIELD : Z3_decl_kind = 2052 ; pub const Z3_decl_kind_Z3_OP_PB_AT_MOST : Z3_decl_kind = 2304 ; pub const Z3_decl_kind_Z3_OP_PB_AT_LEAST : Z3_decl_kind = 2305 ; pub const Z3_decl_kind_Z3_OP_PB_LE : Z3_decl_kind = 2306 ; pub const Z3_decl_kind_Z3_OP_PB_GE : Z3_decl_kind = 2307 ; pub const Z3_decl_kind_Z3_OP_PB_EQ : Z3_decl_kind = 2308 ; pub const Z3_decl_kind_Z3_OP_SPECIAL_RELATION_LO : Z3_decl_kind = 40960 ; pub const Z3_decl_kind_Z3_OP_SPECIAL_RELATION_PO : Z3_decl_kind = 40961 ; pub const Z3_decl_kind_Z3_OP_SPECIAL_RELATION_PLO : Z3_decl_kind = 40962 ; pub const Z3_decl_kind_Z3_OP_SPECIAL_RELATION_TO : Z3_decl_kind = 40963 ; pub const Z3_decl_kind_Z3_OP_SPECIAL_RELATION_TC : Z3_decl_kind = 40964 ; pub const Z3_decl_kind_Z3_OP_SPECIAL_RELATION_TRC : Z3_decl_kind = 40965 ; pub const Z3_decl_kind_Z3_OP_FPA_RM_NEAREST_TIES_TO_EVEN : Z3_decl_kind = 45056 ; pub const Z3_decl_kind_Z3_OP_FPA_RM_NEAREST_TIES_TO_AWAY : Z3_decl_kind = 45057 ; pub const Z3_decl_kind_Z3_OP_FPA_RM_TOWARD_POSITIVE : Z3_decl_kind = 45058 ; pub const Z3_decl_kind_Z3_OP_FPA_RM_TOWARD_NEGATIVE : Z3_decl_kind = 45059 ; pub const Z3_decl_kind_Z3_OP_FPA_RM_TOWARD_ZERO : Z3_decl_kind = 45060 ; pub const Z3_decl_kind_Z3_OP_FPA_NUM : Z3_decl_kind = 45061 ; pub const Z3_decl_kind_Z3_OP_FPA_PLUS_INF : Z3_decl_kind = 45062 ; pub const Z3_decl_kind_Z3_OP_FPA_MINUS_INF : Z3_decl_kind = 45063 ; pub const Z3_decl_kind_Z3_OP_FPA_NAN : Z3_decl_kind = 45064 ; pub const Z3_decl_kind_Z3_OP_FPA_PLUS_ZERO : Z3_decl_kind = 45065 ; pub const Z3_decl_kind_Z3_OP_FPA_MINUS_ZERO : Z3_decl_kind = 45066 ; pub const Z3_decl_kind_Z3_OP_FPA_ADD : Z3_decl_kind = 45067 ; pub const Z3_decl_kind_Z3_OP_FPA_SUB : Z3_decl_kind = 45068 ; pub const Z3_decl_kind_Z3_OP_FPA_NEG : Z3_decl_kind = 45069 ; pub const Z3_decl_kind_Z3_OP_FPA_MUL : Z3_decl_kind = 45070 ; pub const Z3_decl_kind_Z3_OP_FPA_DIV : Z3_decl_kind = 45071 ; pub const Z3_decl_kind_Z3_OP_FPA_REM : Z3_decl_kind = 45072 ; pub const Z3_decl_kind_Z3_OP_FPA_ABS : Z3_decl_kind = 45073 ; pub const Z3_decl_kind_Z3_OP_FPA_MIN : Z3_decl_kind = 45074 ; pub const Z3_decl_kind_Z3_OP_FPA_MAX : Z3_decl_kind = 45075 ; pub const Z3_decl_kind_Z3_OP_FPA_FMA : Z3_decl_kind = 45076 ; pub const Z3_decl_kind_Z3_OP_FPA_SQRT : Z3_decl_kind = 45077 ; pub const Z3_decl_kind_Z3_OP_FPA_ROUND_TO_INTEGRAL : Z3_decl_kind = 45078 ; pub const Z3_decl_kind_Z3_OP_FPA_EQ : Z3_decl_kind = 45079 ; pub const Z3_decl_kind_Z3_OP_FPA_LT : Z3_decl_kind = 45080 ; pub const Z3_decl_kind_Z3_OP_FPA_GT : Z3_decl_kind = 45081 ; pub const Z3_decl_kind_Z3_OP_FPA_LE : Z3_decl_kind = 45082 ; pub const Z3_decl_kind_Z3_OP_FPA_GE : Z3_decl_kind = 45083 ; pub const Z3_decl_kind_Z3_OP_FPA_IS_NAN : Z3_decl_kind = 45084 ; pub const Z3_decl_kind_Z3_OP_FPA_IS_INF : Z3_decl_kind = 45085 ; pub const Z3_decl_kind_Z3_OP_FPA_IS_ZERO : Z3_decl_kind = 45086 ; pub const Z3_decl_kind_Z3_OP_FPA_IS_NORMAL : Z3_decl_kind = 45087 ; pub const Z3_decl_kind_Z3_OP_FPA_IS_SUBNORMAL : Z3_decl_kind = 45088 ; pub const Z3_decl_kind_Z3_OP_FPA_IS_NEGATIVE : Z3_decl_kind = 45089 ; pub const Z3_decl_kind_Z3_OP_FPA_IS_POSITIVE : Z3_decl_kind = 45090 ; pub const Z3_decl_kind_Z3_OP_FPA_FP : Z3_decl_kind = 45091 ; pub const Z3_decl_kind_Z3_OP_FPA_TO_FP : Z3_decl_kind = 45092 ; pub const Z3_decl_kind_Z3_OP_FPA_TO_FP_UNSIGNED : Z3_decl_kind = 45093 ; pub const Z3_decl_kind_Z3_OP_FPA_TO_UBV : Z3_decl_kind = 45094 ; pub const Z3_decl_kind_Z3_OP_FPA_TO_SBV : Z3_decl_kind = 45095 ; pub const Z3_decl_kind_Z3_OP_FPA_TO_REAL : Z3_decl_kind = 45096 ; pub const Z3_decl_kind_Z3_OP_FPA_TO_IEEE_BV : Z3_decl_kind = 45097 ; pub const Z3_decl_kind_Z3_OP_FPA_BVWRAP : Z3_decl_kind = 45098 ; pub const Z3_decl_kind_Z3_OP_FPA_BV2RM : Z3_decl_kind = 45099 ; pub const Z3_decl_kind_Z3_OP_INTERNAL : Z3_decl_kind = 45100 ; pub const Z3_decl_kind_Z3_OP_UNINTERPRETED : Z3_decl_kind = 45101 ; pub type Z3_decl_kind = u32 ; pub const Z3_param_kind_Z3_PK_UINT : Z3_param_kind = 0 ; pub const Z3_param_kind_Z3_PK_BOOL : Z3_param_kind = 1 ; pub const Z3_param_kind_Z3_PK_DOUBLE : Z3_param_kind = 2 ; pub const Z3_param_kind_Z3_PK_SYMBOL : Z3_param_kind = 3 ; pub const Z3_param_kind_Z3_PK_STRING : Z3_param_kind = 4 ; pub const Z3_param_kind_Z3_PK_OTHER : Z3_param_kind = 5 ; pub const Z3_param_kind_Z3_PK_INVALID : Z3_param_kind = 6 ; pub type Z3_param_kind = u32 ; pub const Z3_ast_print_mode_Z3_PRINT_SMTLIB_FULL : Z3_ast_print_mode = 0 ; pub const Z3_ast_print_mode_Z3_PRINT_LOW_LEVEL : Z3_ast_print_mode = 1 ; pub const Z3_ast_print_mode_Z3_PRINT_SMTLIB2_COMPLIANT : Z3_ast_print_mode = 2 ; pub type Z3_ast_print_mode = u32 ; pub const Z3_error_code_Z3_OK : Z3_error_code = 0 ; pub const Z3_error_code_Z3_SORT_ERROR : Z3_error_code = 1 ; pub const Z3_error_code_Z3_IOB : Z3_error_code = 2 ; pub const Z3_error_code_Z3_INVALID_ARG : Z3_error_code = 3 ; pub const Z3_error_code_Z3_PARSER_ERROR : Z3_error_code = 4 ; pub const Z3_error_code_Z3_NO_PARSER : Z3_error_code = 5 ; pub const Z3_error_code_Z3_INVALID_PATTERN : Z3_error_code = 6 ; pub const Z3_error_code_Z3_MEMOUT_FAIL : Z3_error_code = 7 ; pub const Z3_error_code_Z3_FILE_ACCESS_ERROR : Z3_error_code = 8 ; pub const Z3_error_code_Z3_INTERNAL_FATAL : Z3_error_code = 9 ; pub const Z3_error_code_Z3_INVALID_USAGE : Z3_error_code = 10 ; pub const Z3_error_code_Z3_DEC_REF_ERROR : Z3_error_code = 11 ; pub const Z3_error_code_Z3_EXCEPTION : Z3_error_code = 12 ; pub type Z3_error_code = u32 ; pub type Z3_error_handler = :: std :: option :: Option < unsafe extern "C" fn ( c : Z3_context , e : Z3_error_code ) > ; pub const Z3_goal_prec_Z3_GOAL_PRECISE : Z3_goal_prec = 0 ; pub const Z3_goal_prec_Z3_GOAL_UNDER : Z3_goal_prec = 1 ; pub const Z3_goal_prec_Z3_GOAL_OVER : Z3_goal_prec = 2 ; pub const Z3_goal_prec_Z3_GOAL_UNDER_OVER : Z3_goal_prec = 3 ; pub type Z3_goal_prec = u32 ; extern "C" { pub fn Z3_global_param_set ( param_id : Z3_string , param_value : Z3_string ) ; } extern "C" { pub fn Z3_global_param_reset_all ( ) ; } extern "C" { pub fn Z3_global_param_get ( param_id : Z3_string , param_value : Z3_string_ptr ) -> Z3_bool ; } extern "C" { pub fn Z3_mk_config ( ) -> Z3_config ; } extern "C" { pub fn Z3_del_config ( c : Z3_config ) ; } extern "C" { pub fn Z3_set_param_value ( c : Z3_config , param_id : Z3_string , param_value : Z3_string ) ; } extern "C" { pub fn Z3_mk_context ( c : Z3_config ) -> Z3_context ; } extern "C" { pub fn Z3_mk_context_rc ( c : Z3_config ) -> Z3_context ; } extern "C" { pub fn Z3_del_context ( c : Z3_context ) ; } extern "C" { pub fn Z3_inc_ref ( c : Z3_context , a : Z3_ast ) ; } extern "C" { pub fn Z3_dec_ref ( c : Z3_context , a : Z3_ast ) ; } extern "C" { pub fn Z3_update_param_value ( c : Z3_context , param_id : Z3_string , param_value : Z3_string ) ; } extern "C" { pub fn Z3_interrupt ( c : Z3_context ) ; } extern "C" { pub fn Z3_mk_params ( c : Z3_context ) -> Z3_params ; } extern "C" { pub fn Z3_params_inc_ref ( c : Z3_context , p : Z3_params ) ; } extern "C" { pub fn Z3_params_dec_ref ( c : Z3_context , p : Z3_params ) ; } extern "C" { pub fn Z3_params_set_bool ( c : Z3_context , p : Z3_params , k : Z3_symbol , v : bool ) ; } extern "C" { pub fn Z3_params_set_uint ( c : Z3_context , p : Z3_params , k : Z3_symbol , v : :: std :: os :: raw :: c_uint ) ; } extern "C" { pub fn Z3_params_set_double ( c : Z3_context , p : Z3_params , k : Z3_symbol , v : f64 ) ; } extern "C" { pub fn Z3_params_set_symbol ( c : Z3_context , p : Z3_params , k : Z3_symbol , v : Z3_symbol ) ; } extern "C" { pub fn Z3_params_to_string ( c : Z3_context , p : Z3_params ) -> Z3_string ; } extern "C" { pub fn Z3_params_validate ( c : Z3_context , p : Z3_params , d : Z3_param_descrs ) ; } extern "C" { pub fn Z3_param_descrs_inc_ref ( c : Z3_context , p : Z3_param_descrs ) ; } extern "C" { pub fn Z3_param_descrs_dec_ref ( c : Z3_context , p : Z3_param_descrs ) ; } extern "C" { pub fn Z3_param_descrs_get_kind ( c : Z3_context , p : Z3_param_descrs , n : Z3_symbol ) -> Z3_param_kind ; } extern "C" { pub fn Z3_param_descrs_size ( c : Z3_context , p : Z3_param_descrs ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_param_descrs_get_name ( c : Z3_context , p : Z3_param_descrs , i : :: std :: os :: raw :: c_uint ) -> Z3_symbol ; } extern "C" { pub fn Z3_param_descrs_get_documentation ( c : Z3_context , p : Z3_param_descrs , s : Z3_symbol ) -> Z3_string ; } extern "C" { pub fn Z3_param_descrs_to_string ( c : Z3_context , p : Z3_param_descrs ) -> Z3_string ; } extern "C" { pub fn Z3_mk_int_symbol ( c : Z3_context , i : :: std :: os :: raw :: c_int ) -> Z3_symbol ; } extern "C" { pub fn Z3_mk_string_symbol ( c : Z3_context , s : Z3_string ) -> Z3_symbol ; } extern "C" { pub fn Z3_mk_uninterpreted_sort ( c : Z3_context , s : Z3_symbol ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_bool_sort ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_int_sort ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_real_sort ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_bv_sort ( c : Z3_context , sz : :: std :: os :: raw :: c_uint ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_finite_domain_sort ( c : Z3_context , name : Z3_symbol , size : u64 ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_array_sort ( c : Z3_context , domain : Z3_sort , range : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_array_sort_n ( c : Z3_context , n : :: std :: os :: raw :: c_uint , domain : * const Z3_sort , range : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_tuple_sort ( c : Z3_context , mk_tuple_name : Z3_symbol , num_fields : :: std :: os :: raw :: c_uint , field_names : * const Z3_symbol , field_sorts : * const Z3_sort , mk_tuple_decl : * mut Z3_func_decl , proj_decl : * mut Z3_func_decl ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_enumeration_sort ( c : Z3_context , name : Z3_symbol , n : :: std :: os :: raw :: c_uint , enum_names : * const Z3_symbol , enum_consts : * mut Z3_func_decl , enum_testers : * mut Z3_func_decl ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_list_sort ( c : Z3_context , name : Z3_symbol , elem_sort : Z3_sort , nil_decl : * mut Z3_func_decl , is_nil_decl : * mut Z3_func_decl , cons_decl : * mut Z3_func_decl , is_cons_decl : * mut Z3_func_decl , head_decl : * mut Z3_func_decl , tail_decl : * mut Z3_func_decl ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_constructor ( c : Z3_context , name : Z3_symbol , recognizer : Z3_symbol , num_fields : :: std :: os :: raw :: c_uint , field_names : * const Z3_symbol , sorts : * const Z3_sort , sort_refs : * mut :: std :: os :: raw :: c_uint ) -> Z3_constructor ; } extern "C" { pub fn Z3_del_constructor ( c : Z3_context , constr : Z3_constructor ) ; } extern "C" { pub fn Z3_mk_datatype ( c : Z3_context , name : Z3_symbol , num_constructors : :: std :: os :: raw :: c_uint , constructors : * mut Z3_constructor ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_constructor_list ( c : Z3_context , num_constructors : :: std :: os :: raw :: c_uint , constructors : * const Z3_constructor ) -> Z3_constructor_list ; } extern "C" { pub fn Z3_del_constructor_list ( c : Z3_context , clist : Z3_constructor_list ) ; } extern "C" { pub fn Z3_mk_datatypes ( c : Z3_context , num_sorts : :: std :: os :: raw :: c_uint , sort_names : * const Z3_symbol , sorts : * mut Z3_sort , constructor_lists : * mut Z3_constructor_list ) ; } extern "C" { pub fn Z3_query_constructor ( c : Z3_context , constr : Z3_constructor , num_fields : :: std :: os :: raw :: c_uint , constructor : * mut Z3_func_decl , tester : * mut Z3_func_decl , accessors : * mut Z3_func_decl ) ; } extern "C" { pub fn Z3_mk_func_decl ( c : Z3_context , s : Z3_symbol , domain_size : :: std :: os :: raw :: c_uint , domain : * const Z3_sort , range : Z3_sort ) -> Z3_func_decl ; } extern "C" { pub fn Z3_mk_app ( c : Z3_context , d : Z3_func_decl , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_const ( c : Z3_context , s : Z3_symbol , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fresh_func_decl ( c : Z3_context , prefix : Z3_string , domain_size : :: std :: os :: raw :: c_uint , domain : * const Z3_sort , range : Z3_sort ) -> Z3_func_decl ; } extern "C" { pub fn Z3_mk_fresh_const ( c : Z3_context , prefix : Z3_string , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_rec_func_decl ( c : Z3_context , s : Z3_symbol , domain_size : :: std :: os :: raw :: c_uint , domain : * const Z3_sort , range : Z3_sort ) -> Z3_func_decl ; } extern "C" { pub fn Z3_add_rec_def ( c : Z3_context , f : Z3_func_decl , n : :: std :: os :: raw :: c_uint , args : * mut Z3_ast , body : Z3_ast ) ; } extern "C" { pub fn Z3_mk_true ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_false ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_eq ( c : Z3_context , l : Z3_ast , r : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_distinct ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_not ( c : Z3_context , a : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_ite ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast , t3 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_iff ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_implies ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_xor ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_and ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_or ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_add ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_mul ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_sub ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_unary_minus ( c : Z3_context , arg : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_div ( c : Z3_context , arg1 : Z3_ast , arg2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_mod ( c : Z3_context , arg1 : Z3_ast , arg2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_rem ( c : Z3_context , arg1 : Z3_ast , arg2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_power ( c : Z3_context , arg1 : Z3_ast , arg2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_lt ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_le ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_gt ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_ge ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_divides ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_int2real ( c : Z3_context , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_real2int ( c : Z3_context , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_is_int ( c : Z3_context , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvnot ( c : Z3_context , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvredand ( c : Z3_context , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvredor ( c : Z3_context , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvand ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvor ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvxor ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvnand ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvnor ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvxnor ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvneg ( c : Z3_context , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvadd ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsub ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvmul ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvudiv ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsdiv ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvurem ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsrem ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsmod ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvult ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvslt ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvule ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsle ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvuge ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsge ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvugt ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsgt ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_concat ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_extract ( c : Z3_context , high : :: std :: os :: raw :: c_uint , low : :: std :: os :: raw :: c_uint , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_sign_ext ( c : Z3_context , i : :: std :: os :: raw :: c_uint , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_zero_ext ( c : Z3_context , i : :: std :: os :: raw :: c_uint , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_repeat ( c : Z3_context , i : :: std :: os :: raw :: c_uint , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvshl ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvlshr ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvashr ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_rotate_left ( c : Z3_context , i : :: std :: os :: raw :: c_uint , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_rotate_right ( c : Z3_context , i : :: std :: os :: raw :: c_uint , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_ext_rotate_left ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_ext_rotate_right ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_int2bv ( c : Z3_context , n : :: std :: os :: raw :: c_uint , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bv2int ( c : Z3_context , t1 : Z3_ast , is_signed : bool ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvadd_no_overflow ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast , is_signed : bool ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvadd_no_underflow ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsub_no_overflow ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsub_no_underflow ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast , is_signed : bool ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvsdiv_no_overflow ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvneg_no_overflow ( c : Z3_context , t1 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvmul_no_overflow ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast , is_signed : bool ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bvmul_no_underflow ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_select ( c : Z3_context , a : Z3_ast , i : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_select_n ( c : Z3_context , a : Z3_ast , n : :: std :: os :: raw :: c_uint , idxs : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_store ( c : Z3_context , a : Z3_ast , i : Z3_ast , v : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_store_n ( c : Z3_context , a : Z3_ast , n : :: std :: os :: raw :: c_uint , idxs : * const Z3_ast , v : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_const_array ( c : Z3_context , domain : Z3_sort , v : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_map ( c : Z3_context , f : Z3_func_decl , n : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_array_default ( c : Z3_context , array : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_as_array ( c : Z3_context , f : Z3_func_decl ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_has_size ( c : Z3_context , set : Z3_ast , k : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_sort ( c : Z3_context , ty : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_empty_set ( c : Z3_context , domain : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_full_set ( c : Z3_context , domain : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_add ( c : Z3_context , set : Z3_ast , elem : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_del ( c : Z3_context , set : Z3_ast , elem : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_union ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_intersect ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_difference ( c : Z3_context , arg1 : Z3_ast , arg2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_complement ( c : Z3_context , arg : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_member ( c : Z3_context , elem : Z3_ast , set : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_set_subset ( c : Z3_context , arg1 : Z3_ast , arg2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_array_ext ( c : Z3_context , arg1 : Z3_ast , arg2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_numeral ( c : Z3_context , numeral : Z3_string , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_real ( c : Z3_context , num : :: std :: os :: raw :: c_int , den : :: std :: os :: raw :: c_int ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_int ( c : Z3_context , v : :: std :: os :: raw :: c_int , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_unsigned_int ( c : Z3_context , v : :: std :: os :: raw :: c_uint , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_int64 ( c : Z3_context , v : i64 , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_unsigned_int64 ( c : Z3_context , v : u64 , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_bv_numeral ( c : Z3_context , sz : :: std :: os :: raw :: c_uint , bits : * const bool ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_sort ( c : Z3_context , s : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_is_seq_sort ( c : Z3_context , s : Z3_sort ) -> bool ; } extern "C" { pub fn Z3_get_seq_sort_basis ( c : Z3_context , s : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_re_sort ( c : Z3_context , seq : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_is_re_sort ( c : Z3_context , s : Z3_sort ) -> bool ; } extern "C" { pub fn Z3_get_re_sort_basis ( c : Z3_context , s : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_string_sort ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_is_string_sort ( c : Z3_context , s : Z3_sort ) -> bool ; } extern "C" { pub fn Z3_mk_string ( c : Z3_context , s : Z3_string ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_lstring ( c : Z3_context , len : :: std :: os :: raw :: c_uint , s : Z3_string ) -> Z3_ast ; } extern "C" { pub fn Z3_is_string ( c : Z3_context , s : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_get_string ( c : Z3_context , s : Z3_ast ) -> Z3_string ; } extern "C" { pub fn Z3_get_lstring ( c : Z3_context , s : Z3_ast , length : * mut :: std :: os :: raw :: c_uint ) -> Z3_string ; } extern "C" { pub fn Z3_mk_seq_empty ( c : Z3_context , seq : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_unit ( c : Z3_context , a : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_concat ( c : Z3_context , n : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_prefix ( c : Z3_context , prefix : Z3_ast , s : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_suffix ( c : Z3_context , suffix : Z3_ast , s : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_contains ( c : Z3_context , container : Z3_ast , containee : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_str_lt ( c : Z3_context , prefix : Z3_ast , s : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_str_le ( c : Z3_context , prefix : Z3_ast , s : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_extract ( c : Z3_context , s : Z3_ast , offset : Z3_ast , length : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_replace ( c : Z3_context , s : Z3_ast , src : Z3_ast , dst : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_at ( c : Z3_context , s : Z3_ast , index : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_nth ( c : Z3_context , s : Z3_ast , index : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_length ( c : Z3_context , s : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_index ( c : Z3_context , s : Z3_ast , substr : Z3_ast , offset : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_last_index ( c : Z3_context , arg1 : Z3_ast , substr : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_str_to_int ( c : Z3_context , s : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_int_to_str ( c : Z3_context , s : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_to_re ( c : Z3_context , seq : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_seq_in_re ( c : Z3_context , seq : Z3_ast , re : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_plus ( c : Z3_context , re : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_star ( c : Z3_context , re : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_option ( c : Z3_context , re : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_union ( c : Z3_context , n : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_concat ( c : Z3_context , n : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_range ( c : Z3_context , lo : Z3_ast , hi : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_loop ( c : Z3_context , r : Z3_ast , lo : :: std :: os :: raw :: c_uint , hi : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_intersect ( c : Z3_context , n : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_complement ( c : Z3_context , re : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_empty ( c : Z3_context , re : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_re_full ( c : Z3_context , re : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_linear_order ( c : Z3_context , a : Z3_sort , id : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_mk_partial_order ( c : Z3_context , a : Z3_sort , id : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_mk_piecewise_linear_order ( c : Z3_context , a : Z3_sort , id : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_mk_tree_order ( c : Z3_context , a : Z3_sort , id : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_mk_transitive_closure ( c : Z3_context , f : Z3_func_decl ) -> Z3_func_decl ; } extern "C" { pub fn Z3_mk_pattern ( c : Z3_context , num_patterns : :: std :: os :: raw :: c_uint , terms : * const Z3_ast ) -> Z3_pattern ; } extern "C" { pub fn Z3_mk_bound ( c : Z3_context , index : :: std :: os :: raw :: c_uint , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_forall ( c : Z3_context , weight : :: std :: os :: raw :: c_uint , num_patterns : :: std :: os :: raw :: c_uint , patterns : * const Z3_pattern , num_decls : :: std :: os :: raw :: c_uint , sorts : * const Z3_sort , decl_names : * const Z3_symbol , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_exists ( c : Z3_context , weight : :: std :: os :: raw :: c_uint , num_patterns : :: std :: os :: raw :: c_uint , patterns : * const Z3_pattern , num_decls : :: std :: os :: raw :: c_uint , sorts : * const Z3_sort , decl_names : * const Z3_symbol , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_quantifier ( c : Z3_context , is_forall : bool , weight : :: std :: os :: raw :: c_uint , num_patterns : :: std :: os :: raw :: c_uint , patterns : * const Z3_pattern , num_decls : :: std :: os :: raw :: c_uint , sorts : * const Z3_sort , decl_names : * const Z3_symbol , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_quantifier_ex ( c : Z3_context , is_forall : bool , weight : :: std :: os :: raw :: c_uint , quantifier_id : Z3_symbol , skolem_id : Z3_symbol , num_patterns : :: std :: os :: raw :: c_uint , patterns : * const Z3_pattern , num_no_patterns : :: std :: os :: raw :: c_uint , no_patterns : * const Z3_ast , num_decls : :: std :: os :: raw :: c_uint , sorts : * const Z3_sort , decl_names : * const Z3_symbol , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_forall_const ( c : Z3_context , weight : :: std :: os :: raw :: c_uint , num_bound : :: std :: os :: raw :: c_uint , bound : * const Z3_app , num_patterns : :: std :: os :: raw :: c_uint , patterns : * const Z3_pattern , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_exists_const ( c : Z3_context , weight : :: std :: os :: raw :: c_uint , num_bound : :: std :: os :: raw :: c_uint , bound : * const Z3_app , num_patterns : :: std :: os :: raw :: c_uint , patterns : * const Z3_pattern , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_quantifier_const ( c : Z3_context , is_forall : bool , weight : :: std :: os :: raw :: c_uint , num_bound : :: std :: os :: raw :: c_uint , bound : * const Z3_app , num_patterns : :: std :: os :: raw :: c_uint , patterns : * const Z3_pattern , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_quantifier_const_ex ( c : Z3_context , is_forall : bool , weight : :: std :: os :: raw :: c_uint , quantifier_id : Z3_symbol , skolem_id : Z3_symbol , num_bound : :: std :: os :: raw :: c_uint , bound : * const Z3_app , num_patterns : :: std :: os :: raw :: c_uint , patterns : * const Z3_pattern , num_no_patterns : :: std :: os :: raw :: c_uint , no_patterns : * const Z3_ast , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_lambda ( c : Z3_context , num_decls : :: std :: os :: raw :: c_uint , sorts : * const Z3_sort , decl_names : * const Z3_symbol , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_lambda_const ( c : Z3_context , num_bound : :: std :: os :: raw :: c_uint , bound : * const Z3_app , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_get_symbol_kind ( c : Z3_context , s : Z3_symbol ) -> Z3_symbol_kind ; } extern "C" { pub fn Z3_get_symbol_int ( c : Z3_context , s : Z3_symbol ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn Z3_get_symbol_string ( c : Z3_context , s : Z3_symbol ) -> Z3_string ; } extern "C" { pub fn Z3_get_sort_name ( c : Z3_context , d : Z3_sort ) -> Z3_symbol ; } extern "C" { pub fn Z3_get_sort_id ( c : Z3_context , s : Z3_sort ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_sort_to_ast ( c : Z3_context , s : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_is_eq_sort ( c : Z3_context , s1 : Z3_sort , s2 : Z3_sort ) -> bool ; } extern "C" { pub fn Z3_get_sort_kind ( c : Z3_context , t : Z3_sort ) -> Z3_sort_kind ; } extern "C" { pub fn Z3_get_bv_sort_size ( c : Z3_context , t : Z3_sort ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_finite_domain_sort_size ( c : Z3_context , s : Z3_sort , r : * mut u64 ) -> Z3_bool ; } extern "C" { pub fn Z3_get_array_sort_domain ( c : Z3_context , t : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_get_array_sort_range ( c : Z3_context , t : Z3_sort ) -> Z3_sort ; } extern "C" { pub fn Z3_get_tuple_sort_mk_decl ( c : Z3_context , t : Z3_sort ) -> Z3_func_decl ; } extern "C" { pub fn Z3_get_tuple_sort_num_fields ( c : Z3_context , t : Z3_sort ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_tuple_sort_field_decl ( c : Z3_context , t : Z3_sort , i : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_get_datatype_sort_num_constructors ( c : Z3_context , t : Z3_sort ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_datatype_sort_constructor ( c : Z3_context , t : Z3_sort , idx : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_get_datatype_sort_recognizer ( c : Z3_context , t : Z3_sort , idx : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_get_datatype_sort_constructor_accessor ( c : Z3_context , t : Z3_sort , idx_c : :: std :: os :: raw :: c_uint , idx_a : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_datatype_update_field ( c : Z3_context , field_access : Z3_func_decl , t : Z3_ast , value : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_get_relation_arity ( c : Z3_context , s : Z3_sort ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_relation_column ( c : Z3_context , s : Z3_sort , col : :: std :: os :: raw :: c_uint ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_atmost ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast , k : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_atleast ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast , k : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_pble ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast , coeffs : * const :: std :: os :: raw :: c_int , k : :: std :: os :: raw :: c_int ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_pbge ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast , coeffs : * const :: std :: os :: raw :: c_int , k : :: std :: os :: raw :: c_int ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_pbeq ( c : Z3_context , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast , coeffs : * const :: std :: os :: raw :: c_int , k : :: std :: os :: raw :: c_int ) -> Z3_ast ; } extern "C" { pub fn Z3_func_decl_to_ast ( c : Z3_context , f : Z3_func_decl ) -> Z3_ast ; } extern "C" { pub fn Z3_is_eq_func_decl ( c : Z3_context , f1 : Z3_func_decl , f2 : Z3_func_decl ) -> bool ; } extern "C" { pub fn Z3_get_func_decl_id ( c : Z3_context , f : Z3_func_decl ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_decl_name ( c : Z3_context , d : Z3_func_decl ) -> Z3_symbol ; } extern "C" { pub fn Z3_get_decl_kind ( c : Z3_context , d : Z3_func_decl ) -> Z3_decl_kind ; } extern "C" { pub fn Z3_get_domain_size ( c : Z3_context , d : Z3_func_decl ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_arity ( c : Z3_context , d : Z3_func_decl ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_domain ( c : Z3_context , d : Z3_func_decl , i : :: std :: os :: raw :: c_uint ) -> Z3_sort ; } extern "C" { pub fn Z3_get_range ( c : Z3_context , d : Z3_func_decl ) -> Z3_sort ; } extern "C" { pub fn Z3_get_decl_num_parameters ( c : Z3_context , d : Z3_func_decl ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_decl_parameter_kind ( c : Z3_context , d : Z3_func_decl , idx : :: std :: os :: raw :: c_uint ) -> Z3_parameter_kind ; } extern "C" { pub fn Z3_get_decl_int_parameter ( c : Z3_context , d : Z3_func_decl , idx : :: std :: os :: raw :: c_uint ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn Z3_get_decl_double_parameter ( c : Z3_context , d : Z3_func_decl , idx : :: std :: os :: raw :: c_uint ) -> f64 ; } extern "C" { pub fn Z3_get_decl_symbol_parameter ( c : Z3_context , d : Z3_func_decl , idx : :: std :: os :: raw :: c_uint ) -> Z3_symbol ; } extern "C" { pub fn Z3_get_decl_sort_parameter ( c : Z3_context , d : Z3_func_decl , idx : :: std :: os :: raw :: c_uint ) -> Z3_sort ; } extern "C" { pub fn Z3_get_decl_ast_parameter ( c : Z3_context , d : Z3_func_decl , idx : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_get_decl_func_decl_parameter ( c : Z3_context , d : Z3_func_decl , idx : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_get_decl_rational_parameter ( c : Z3_context , d : Z3_func_decl , idx : :: std :: os :: raw :: c_uint ) -> Z3_string ; } extern "C" { pub fn Z3_app_to_ast ( c : Z3_context , a : Z3_app ) -> Z3_ast ; } extern "C" { pub fn Z3_get_app_decl ( c : Z3_context , a : Z3_app ) -> Z3_func_decl ; } extern "C" { pub fn Z3_get_app_num_args ( c : Z3_context , a : Z3_app ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_app_arg ( c : Z3_context , a : Z3_app , i : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_is_eq_ast ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_get_ast_id ( c : Z3_context , t : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_ast_hash ( c : Z3_context , a : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_sort ( c : Z3_context , a : Z3_ast ) -> Z3_sort ; } extern "C" { pub fn Z3_is_well_sorted ( c : Z3_context , t : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_get_bool_value ( c : Z3_context , a : Z3_ast ) -> Z3_lbool ; } extern "C" { pub fn Z3_get_ast_kind ( c : Z3_context , a : Z3_ast ) -> Z3_ast_kind ; } extern "C" { pub fn Z3_is_app ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_is_numeral_ast ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_is_algebraic_number ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_to_app ( c : Z3_context , a : Z3_ast ) -> Z3_app ; } extern "C" { pub fn Z3_to_func_decl ( c : Z3_context , a : Z3_ast ) -> Z3_func_decl ; } extern "C" { pub fn Z3_get_numeral_string ( c : Z3_context , a : Z3_ast ) -> Z3_string ; } extern "C" { pub fn Z3_get_numeral_decimal_string ( c : Z3_context , a : Z3_ast , precision : :: std :: os :: raw :: c_uint ) -> Z3_string ; } extern "C" { pub fn Z3_get_numeral_double ( c : Z3_context , a : Z3_ast ) -> f64 ; } extern "C" { pub fn Z3_get_numerator ( c : Z3_context , a : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_get_denominator ( c : Z3_context , a : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_get_numeral_small ( c : Z3_context , a : Z3_ast , num : * mut i64 , den : * mut i64 ) -> bool ; } extern "C" { pub fn Z3_get_numeral_int ( c : Z3_context , v : Z3_ast , i : * mut :: std :: os :: raw :: c_int ) -> bool ; } extern "C" { pub fn Z3_get_numeral_uint ( c : Z3_context , v : Z3_ast , u : * mut :: std :: os :: raw :: c_uint ) -> bool ; } extern "C" { pub fn Z3_get_numeral_uint64 ( c : Z3_context , v : Z3_ast , u : * mut u64 ) -> bool ; } extern "C" { pub fn Z3_get_numeral_int64 ( c : Z3_context , v : Z3_ast , i : * mut i64 ) -> bool ; } extern "C" { pub fn Z3_get_numeral_rational_int64 ( c : Z3_context , v : Z3_ast , num : * mut i64 , den : * mut i64 ) -> bool ; } extern "C" { pub fn Z3_get_algebraic_number_lower ( c : Z3_context , a : Z3_ast , precision : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_get_algebraic_number_upper ( c : Z3_context , a : Z3_ast , precision : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_pattern_to_ast ( c : Z3_context , p : Z3_pattern ) -> Z3_ast ; } extern "C" { pub fn Z3_get_pattern_num_terms ( c : Z3_context , p : Z3_pattern ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_pattern ( c : Z3_context , p : Z3_pattern , idx : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_get_index_value ( c : Z3_context , a : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_is_quantifier_forall ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_is_quantifier_exists ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_is_lambda ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_get_quantifier_weight ( c : Z3_context , a : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_quantifier_num_patterns ( c : Z3_context , a : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_quantifier_pattern_ast ( c : Z3_context , a : Z3_ast , i : :: std :: os :: raw :: c_uint ) -> Z3_pattern ; } extern "C" { pub fn Z3_get_quantifier_num_no_patterns ( c : Z3_context , a : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_quantifier_no_pattern_ast ( c : Z3_context , a : Z3_ast , i : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_get_quantifier_num_bound ( c : Z3_context , a : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_quantifier_bound_name ( c : Z3_context , a : Z3_ast , i : :: std :: os :: raw :: c_uint ) -> Z3_symbol ; } extern "C" { pub fn Z3_get_quantifier_bound_sort ( c : Z3_context , a : Z3_ast , i : :: std :: os :: raw :: c_uint ) -> Z3_sort ; } extern "C" { pub fn Z3_get_quantifier_body ( c : Z3_context , a : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_simplify ( c : Z3_context , a : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_simplify_ex ( c : Z3_context , a : Z3_ast , p : Z3_params ) -> Z3_ast ; } extern "C" { pub fn Z3_simplify_get_help ( c : Z3_context ) -> Z3_string ; } extern "C" { pub fn Z3_simplify_get_param_descrs ( c : Z3_context ) -> Z3_param_descrs ; } extern "C" { pub fn Z3_update_term ( c : Z3_context , a : Z3_ast , num_args : :: std :: os :: raw :: c_uint , args : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_substitute ( c : Z3_context , a : Z3_ast , num_exprs : :: std :: os :: raw :: c_uint , from : * const Z3_ast , to : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_substitute_vars ( c : Z3_context , a : Z3_ast , num_exprs : :: std :: os :: raw :: c_uint , to : * const Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_translate ( source : Z3_context , a : Z3_ast , target : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_model ( c : Z3_context ) -> Z3_model ; } extern "C" { pub fn Z3_model_inc_ref ( c : Z3_context , m : Z3_model ) ; } extern "C" { pub fn Z3_model_dec_ref ( c : Z3_context , m : Z3_model ) ; } extern "C" { pub fn Z3_model_eval ( c : Z3_context , m : Z3_model , t : Z3_ast , model_completion : bool , v : * mut Z3_ast ) -> Z3_bool ; } extern "C" { pub fn Z3_model_get_const_interp ( c : Z3_context , m : Z3_model , a : Z3_func_decl ) -> Z3_ast ; } extern "C" { pub fn Z3_model_has_interp ( c : Z3_context , m : Z3_model , a : Z3_func_decl ) -> bool ; } extern "C" { pub fn Z3_model_get_func_interp ( c : Z3_context , m : Z3_model , f : Z3_func_decl ) -> Z3_func_interp ; } extern "C" { pub fn Z3_model_get_num_consts ( c : Z3_context , m : Z3_model ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_model_get_const_decl ( c : Z3_context , m : Z3_model , i : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_model_get_num_funcs ( c : Z3_context , m : Z3_model ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_model_get_func_decl ( c : Z3_context , m : Z3_model , i : :: std :: os :: raw :: c_uint ) -> Z3_func_decl ; } extern "C" { pub fn Z3_model_get_num_sorts ( c : Z3_context , m : Z3_model ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_model_get_sort ( c : Z3_context , m : Z3_model , i : :: std :: os :: raw :: c_uint ) -> Z3_sort ; } extern "C" { pub fn Z3_model_get_sort_universe ( c : Z3_context , m : Z3_model , s : Z3_sort ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_model_translate ( c : Z3_context , m : Z3_model , dst : Z3_context ) -> Z3_model ; } extern "C" { pub fn Z3_is_as_array ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_get_as_array_func_decl ( c : Z3_context , a : Z3_ast ) -> Z3_func_decl ; } extern "C" { pub fn Z3_add_func_interp ( c : Z3_context , m : Z3_model , f : Z3_func_decl , default_value : Z3_ast ) -> Z3_func_interp ; } extern "C" { pub fn Z3_add_const_interp ( c : Z3_context , m : Z3_model , f : Z3_func_decl , a : Z3_ast ) ; } extern "C" { pub fn Z3_func_interp_inc_ref ( c : Z3_context , f : Z3_func_interp ) ; } extern "C" { pub fn Z3_func_interp_dec_ref ( c : Z3_context , f : Z3_func_interp ) ; } extern "C" { pub fn Z3_func_interp_get_num_entries ( c : Z3_context , f : Z3_func_interp ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_func_interp_get_entry ( c : Z3_context , f : Z3_func_interp , i : :: std :: os :: raw :: c_uint ) -> Z3_func_entry ; } extern "C" { pub fn Z3_func_interp_get_else ( c : Z3_context , f : Z3_func_interp ) -> Z3_ast ; } extern "C" { pub fn Z3_func_interp_set_else ( c : Z3_context , f : Z3_func_interp , else_value : Z3_ast ) ; } extern "C" { pub fn Z3_func_interp_get_arity ( c : Z3_context , f : Z3_func_interp ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_func_interp_add_entry ( c : Z3_context , fi : Z3_func_interp , args : Z3_ast_vector , value : Z3_ast ) ; } extern "C" { pub fn Z3_func_entry_inc_ref ( c : Z3_context , e : Z3_func_entry ) ; } extern "C" { pub fn Z3_func_entry_dec_ref ( c : Z3_context , e : Z3_func_entry ) ; } extern "C" { pub fn Z3_func_entry_get_value ( c : Z3_context , e : Z3_func_entry ) -> Z3_ast ; } extern "C" { pub fn Z3_func_entry_get_num_args ( c : Z3_context , e : Z3_func_entry ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_func_entry_get_arg ( c : Z3_context , e : Z3_func_entry , i : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_open_log ( filename : Z3_string ) -> bool ; } extern "C" { pub fn Z3_append_log ( string : Z3_string ) ; } extern "C" { pub fn Z3_close_log ( ) ; } extern "C" { pub fn Z3_toggle_warning_messages ( enabled : bool ) ; } extern "C" { pub fn Z3_set_ast_print_mode ( c : Z3_context , mode : Z3_ast_print_mode ) ; } extern "C" { pub fn Z3_ast_to_string ( c : Z3_context , a : Z3_ast ) -> Z3_string ; } extern "C" { pub fn Z3_pattern_to_string ( c : Z3_context , p : Z3_pattern ) -> Z3_string ; } extern "C" { pub fn Z3_sort_to_string ( c : Z3_context , s : Z3_sort ) -> Z3_string ; } extern "C" { pub fn Z3_func_decl_to_string ( c : Z3_context , d : Z3_func_decl ) -> Z3_string ; } extern "C" { pub fn Z3_model_to_string ( c : Z3_context , m : Z3_model ) -> Z3_string ; } extern "C" { pub fn Z3_benchmark_to_smtlib_string ( c : Z3_context , name : Z3_string , logic : Z3_string , status : Z3_string , attributes : Z3_string , num_assumptions : :: std :: os :: raw :: c_uint , assumptions : * const Z3_ast , formula : Z3_ast ) -> Z3_string ; } extern "C" { pub fn Z3_parse_smtlib2_string ( c : Z3_context , str : Z3_string , num_sorts : :: std :: os :: raw :: c_uint , sort_names : * const Z3_symbol , sorts : * const Z3_sort , num_decls : :: std :: os :: raw :: c_uint , decl_names : * const Z3_symbol , decls : * const Z3_func_decl ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_parse_smtlib2_file ( c : Z3_context , file_name : Z3_string , num_sorts : :: std :: os :: raw :: c_uint , sort_names : * const Z3_symbol , sorts : * const Z3_sort , num_decls : :: std :: os :: raw :: c_uint , decl_names : * const Z3_symbol , decls : * const Z3_func_decl ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_eval_smtlib2_string ( arg1 : Z3_context , str : Z3_string ) -> Z3_string ; } extern "C" { pub fn Z3_get_error_code ( c : Z3_context ) -> Z3_error_code ; } extern "C" { pub fn Z3_set_error_handler ( c : Z3_context , h : Z3_error_handler ) ; } extern "C" { pub fn Z3_set_error ( c : Z3_context , e : Z3_error_code ) ; } extern "C" { pub fn Z3_get_error_msg ( c : Z3_context , err : Z3_error_code ) -> Z3_string ; } extern "C" { pub fn Z3_get_version ( major : * mut :: std :: os :: raw :: c_uint , minor : * mut :: std :: os :: raw :: c_uint , build_number : * mut :: std :: os :: raw :: c_uint , revision_number : * mut :: std :: os :: raw :: c_uint ) ; } extern "C" { pub fn Z3_get_full_version ( ) -> Z3_string ; } extern "C" { pub fn Z3_enable_trace ( tag : Z3_string ) ; } extern "C" { pub fn Z3_disable_trace ( tag : Z3_string ) ; } extern "C" { pub fn Z3_reset_memory ( ) ; } extern "C" { pub fn Z3_finalize_memory ( ) ; } extern "C" { pub fn Z3_mk_goal ( c : Z3_context , models : bool , unsat_cores : bool , proofs : bool ) -> Z3_goal ; } extern "C" { pub fn Z3_goal_inc_ref ( c : Z3_context , g : Z3_goal ) ; } extern "C" { pub fn Z3_goal_dec_ref ( c : Z3_context , g : Z3_goal ) ; } extern "C" { pub fn Z3_goal_precision ( c : Z3_context , g : Z3_goal ) -> Z3_goal_prec ; } extern "C" { pub fn Z3_goal_assert ( c : Z3_context , g : Z3_goal , a : Z3_ast ) ; } extern "C" { pub fn Z3_goal_inconsistent ( c : Z3_context , g : Z3_goal ) -> bool ; } extern "C" { pub fn Z3_goal_depth ( c : Z3_context , g : Z3_goal ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_goal_reset ( c : Z3_context , g : Z3_goal ) ; } extern "C" { pub fn Z3_goal_size ( c : Z3_context , g : Z3_goal ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_goal_formula ( c : Z3_context , g : Z3_goal , idx : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_goal_num_exprs ( c : Z3_context , g : Z3_goal ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_goal_is_decided_sat ( c : Z3_context , g : Z3_goal ) -> bool ; } extern "C" { pub fn Z3_goal_is_decided_unsat ( c : Z3_context , g : Z3_goal ) -> bool ; } extern "C" { pub fn Z3_goal_translate ( source : Z3_context , g : Z3_goal , target : Z3_context ) -> Z3_goal ; } extern "C" { pub fn Z3_goal_convert_model ( c : Z3_context , g : Z3_goal , m : Z3_model ) -> Z3_model ; } extern "C" { pub fn Z3_goal_to_string ( c : Z3_context , g : Z3_goal ) -> Z3_string ; } extern "C" { pub fn Z3_goal_to_dimacs_string ( c : Z3_context , g : Z3_goal ) -> Z3_string ; } extern "C" { pub fn Z3_mk_tactic ( c : Z3_context , name : Z3_string ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_inc_ref ( c : Z3_context , t : Z3_tactic ) ; } extern "C" { pub fn Z3_tactic_dec_ref ( c : Z3_context , g : Z3_tactic ) ; } extern "C" { pub fn Z3_mk_probe ( c : Z3_context , name : Z3_string ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_inc_ref ( c : Z3_context , p : Z3_probe ) ; } extern "C" { pub fn Z3_probe_dec_ref ( c : Z3_context , p : Z3_probe ) ; } extern "C" { pub fn Z3_tactic_and_then ( c : Z3_context , t1 : Z3_tactic , t2 : Z3_tactic ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_or_else ( c : Z3_context , t1 : Z3_tactic , t2 : Z3_tactic ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_par_or ( c : Z3_context , num : :: std :: os :: raw :: c_uint , ts : * const Z3_tactic ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_par_and_then ( c : Z3_context , t1 : Z3_tactic , t2 : Z3_tactic ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_try_for ( c : Z3_context , t : Z3_tactic , ms : :: std :: os :: raw :: c_uint ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_when ( c : Z3_context , p : Z3_probe , t : Z3_tactic ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_cond ( c : Z3_context , p : Z3_probe , t1 : Z3_tactic , t2 : Z3_tactic ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_repeat ( c : Z3_context , t : Z3_tactic , max : :: std :: os :: raw :: c_uint ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_skip ( c : Z3_context ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_fail ( c : Z3_context ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_fail_if ( c : Z3_context , p : Z3_probe ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_fail_if_not_decided ( c : Z3_context ) -> Z3_tactic ; } extern "C" { pub fn Z3_tactic_using_params ( c : Z3_context , t : Z3_tactic , p : Z3_params ) -> Z3_tactic ; } extern "C" { pub fn Z3_probe_const ( x : Z3_context , val : f64 ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_lt ( x : Z3_context , p1 : Z3_probe , p2 : Z3_probe ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_gt ( x : Z3_context , p1 : Z3_probe , p2 : Z3_probe ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_le ( x : Z3_context , p1 : Z3_probe , p2 : Z3_probe ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_ge ( x : Z3_context , p1 : Z3_probe , p2 : Z3_probe ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_eq ( x : Z3_context , p1 : Z3_probe , p2 : Z3_probe ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_and ( x : Z3_context , p1 : Z3_probe , p2 : Z3_probe ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_or ( x : Z3_context , p1 : Z3_probe , p2 : Z3_probe ) -> Z3_probe ; } extern "C" { pub fn Z3_probe_not ( x : Z3_context , p : Z3_probe ) -> Z3_probe ; } extern "C" { pub fn Z3_get_num_tactics ( c : Z3_context ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_tactic_name ( c : Z3_context , i : :: std :: os :: raw :: c_uint ) -> Z3_string ; } extern "C" { pub fn Z3_get_num_probes ( c : Z3_context ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_get_probe_name ( c : Z3_context , i : :: std :: os :: raw :: c_uint ) -> Z3_string ; } extern "C" { pub fn Z3_tactic_get_help ( c : Z3_context , t : Z3_tactic ) -> Z3_string ; } extern "C" { pub fn Z3_tactic_get_param_descrs ( c : Z3_context , t : Z3_tactic ) -> Z3_param_descrs ; } extern "C" { pub fn Z3_tactic_get_descr ( c : Z3_context , name : Z3_string ) -> Z3_string ; } extern "C" { pub fn Z3_probe_get_descr ( c : Z3_context , name : Z3_string ) -> Z3_string ; } extern "C" { pub fn Z3_probe_apply ( c : Z3_context , p : Z3_probe , g : Z3_goal ) -> f64 ; } extern "C" { pub fn Z3_tactic_apply ( c : Z3_context , t : Z3_tactic , g : Z3_goal ) -> Z3_apply_result ; } extern "C" { pub fn Z3_tactic_apply_ex ( c : Z3_context , t : Z3_tactic , g : Z3_goal , p : Z3_params ) -> Z3_apply_result ; } extern "C" { pub fn Z3_apply_result_inc_ref ( c : Z3_context , r : Z3_apply_result ) ; } extern "C" { pub fn Z3_apply_result_dec_ref ( c : Z3_context , r : Z3_apply_result ) ; } extern "C" { pub fn Z3_apply_result_to_string ( c : Z3_context , r : Z3_apply_result ) -> Z3_string ; } extern "C" { pub fn Z3_apply_result_get_num_subgoals ( c : Z3_context , r : Z3_apply_result ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_apply_result_get_subgoal ( c : Z3_context , r : Z3_apply_result , i : :: std :: os :: raw :: c_uint ) -> Z3_goal ; } extern "C" { pub fn Z3_mk_solver ( c : Z3_context ) -> Z3_solver ; } extern "C" { pub fn Z3_mk_simple_solver ( c : Z3_context ) -> Z3_solver ; } extern "C" { pub fn Z3_mk_solver_for_logic ( c : Z3_context , logic : Z3_symbol ) -> Z3_solver ; } extern "C" { pub fn Z3_mk_solver_from_tactic ( c : Z3_context , t : Z3_tactic ) -> Z3_solver ; } extern "C" { pub fn Z3_solver_translate ( source : Z3_context , s : Z3_solver , target : Z3_context ) -> Z3_solver ; } extern "C" { pub fn Z3_solver_import_model_converter ( ctx : Z3_context , src : Z3_solver , dst : Z3_solver ) ; } extern "C" { pub fn Z3_solver_get_help ( c : Z3_context , s : Z3_solver ) -> Z3_string ; } extern "C" { pub fn Z3_solver_get_param_descrs ( c : Z3_context , s : Z3_solver ) -> Z3_param_descrs ; } extern "C" { pub fn Z3_solver_set_params ( c : Z3_context , s : Z3_solver , p : Z3_params ) ; } extern "C" { pub fn Z3_solver_inc_ref ( c : Z3_context , s : Z3_solver ) ; } extern "C" { pub fn Z3_solver_dec_ref ( c : Z3_context , s : Z3_solver ) ; } extern "C" { pub fn Z3_solver_interrupt ( c : Z3_context , s : Z3_solver ) ; } extern "C" { pub fn Z3_solver_push ( c : Z3_context , s : Z3_solver ) ; } extern "C" { pub fn Z3_solver_pop ( c : Z3_context , s : Z3_solver , n : :: std :: os :: raw :: c_uint ) ; } extern "C" { pub fn Z3_solver_reset ( c : Z3_context , s : Z3_solver ) ; } extern "C" { pub fn Z3_solver_get_num_scopes ( c : Z3_context , s : Z3_solver ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_solver_assert ( c : Z3_context , s : Z3_solver , a : Z3_ast ) ; } extern "C" { pub fn Z3_solver_assert_and_track ( c : Z3_context , s : Z3_solver , a : Z3_ast , p : Z3_ast ) ; } extern "C" { pub fn Z3_solver_from_file ( c : Z3_context , s : Z3_solver , file_name : Z3_string ) ; } extern "C" { pub fn Z3_solver_from_string ( c : Z3_context , s : Z3_solver , file_name : Z3_string ) ; } extern "C" { pub fn Z3_solver_get_assertions ( c : Z3_context , s : Z3_solver ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_solver_get_units ( c : Z3_context , s : Z3_solver ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_solver_get_trail ( c : Z3_context , s : Z3_solver ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_solver_get_non_units ( c : Z3_context , s : Z3_solver ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_solver_get_levels ( c : Z3_context , s : Z3_solver , literals : Z3_ast_vector , sz : :: std :: os :: raw :: c_uint , levels : * mut :: std :: os :: raw :: c_uint ) ; } extern "C" { pub fn Z3_solver_check ( c : Z3_context , s : Z3_solver ) -> Z3_lbool ; } extern "C" { pub fn Z3_solver_check_assumptions ( c : Z3_context , s : Z3_solver , num_assumptions : :: std :: os :: raw :: c_uint , assumptions : * const Z3_ast ) -> Z3_lbool ; } extern "C" { pub fn Z3_get_implied_equalities ( c : Z3_context , s : Z3_solver , num_terms : :: std :: os :: raw :: c_uint , terms : * const Z3_ast , class_ids : * mut :: std :: os :: raw :: c_uint ) -> Z3_lbool ; } extern "C" { pub fn Z3_solver_get_consequences ( c : Z3_context , s : Z3_solver , assumptions : Z3_ast_vector , variables : Z3_ast_vector , consequences : Z3_ast_vector ) -> Z3_lbool ; } extern "C" { pub fn Z3_solver_cube ( c : Z3_context , s : Z3_solver , vars : Z3_ast_vector , backtrack_level : :: std :: os :: raw :: c_uint ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_solver_get_model ( c : Z3_context , s : Z3_solver ) -> Z3_model ; } extern "C" { pub fn Z3_solver_get_proof ( c : Z3_context , s : Z3_solver ) -> Z3_ast ; } extern "C" { pub fn Z3_solver_get_unsat_core ( c : Z3_context , s : Z3_solver ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_solver_get_reason_unknown ( c : Z3_context , s : Z3_solver ) -> Z3_string ; } extern "C" { pub fn Z3_solver_get_statistics ( c : Z3_context , s : Z3_solver ) -> Z3_stats ; } extern "C" { pub fn Z3_solver_to_string ( c : Z3_context , s : Z3_solver ) -> Z3_string ; } extern "C" { pub fn Z3_solver_to_dimacs_string ( c : Z3_context , s : Z3_solver ) -> Z3_string ; } extern "C" { pub fn Z3_stats_to_string ( c : Z3_context , s : Z3_stats ) -> Z3_string ; } extern "C" { pub fn Z3_stats_inc_ref ( c : Z3_context , s : Z3_stats ) ; } extern "C" { pub fn Z3_stats_dec_ref ( c : Z3_context , s : Z3_stats ) ; } extern "C" { pub fn Z3_stats_size ( c : Z3_context , s : Z3_stats ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_stats_get_key ( c : Z3_context , s : Z3_stats , idx : :: std :: os :: raw :: c_uint ) -> Z3_string ; } extern "C" { pub fn Z3_stats_is_uint ( c : Z3_context , s : Z3_stats , idx : :: std :: os :: raw :: c_uint ) -> bool ; } extern "C" { pub fn Z3_stats_is_double ( c : Z3_context , s : Z3_stats , idx : :: std :: os :: raw :: c_uint ) -> bool ; } extern "C" { pub fn Z3_stats_get_uint_value ( c : Z3_context , s : Z3_stats , idx : :: std :: os :: raw :: c_uint ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_stats_get_double_value ( c : Z3_context , s : Z3_stats , idx : :: std :: os :: raw :: c_uint ) -> f64 ; } extern "C" { pub fn Z3_get_estimated_alloc_size ( ) -> u64 ; } extern "C" { pub fn Z3_mk_ast_vector ( c : Z3_context ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_ast_vector_inc_ref ( c : Z3_context , v : Z3_ast_vector ) ; } extern "C" { pub fn Z3_ast_vector_dec_ref ( c : Z3_context , v : Z3_ast_vector ) ; } extern "C" { pub fn Z3_ast_vector_size ( c : Z3_context , v : Z3_ast_vector ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_ast_vector_get ( c : Z3_context , v : Z3_ast_vector , i : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_ast_vector_set ( c : Z3_context , v : Z3_ast_vector , i : :: std :: os :: raw :: c_uint , a : Z3_ast ) ; } extern "C" { pub fn Z3_ast_vector_resize ( c : Z3_context , v : Z3_ast_vector , n : :: std :: os :: raw :: c_uint ) ; } extern "C" { pub fn Z3_ast_vector_push ( c : Z3_context , v : Z3_ast_vector , a : Z3_ast ) ; } extern "C" { pub fn Z3_ast_vector_translate ( s : Z3_context , v : Z3_ast_vector , t : Z3_context ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_ast_vector_to_string ( c : Z3_context , v : Z3_ast_vector ) -> Z3_string ; } extern "C" { pub fn Z3_mk_ast_map ( c : Z3_context ) -> Z3_ast_map ; } extern "C" { pub fn Z3_ast_map_inc_ref ( c : Z3_context , m : Z3_ast_map ) ; } extern "C" { pub fn Z3_ast_map_dec_ref ( c : Z3_context , m : Z3_ast_map ) ; } extern "C" { pub fn Z3_ast_map_contains ( c : Z3_context , m : Z3_ast_map , k : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_ast_map_find ( c : Z3_context , m : Z3_ast_map , k : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_ast_map_insert ( c : Z3_context , m : Z3_ast_map , k : Z3_ast , v : Z3_ast ) ; } extern "C" { pub fn Z3_ast_map_erase ( c : Z3_context , m : Z3_ast_map , k : Z3_ast ) ; } extern "C" { pub fn Z3_ast_map_reset ( c : Z3_context , m : Z3_ast_map ) ; } extern "C" { pub fn Z3_ast_map_size ( c : Z3_context , m : Z3_ast_map ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_ast_map_keys ( c : Z3_context , m : Z3_ast_map ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_ast_map_to_string ( c : Z3_context , m : Z3_ast_map ) -> Z3_string ; } extern "C" { pub fn Z3_algebraic_is_value ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_is_pos ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_is_neg ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_is_zero ( c : Z3_context , a : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_sign ( c : Z3_context , a : Z3_ast ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn Z3_algebraic_add ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_algebraic_sub ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_algebraic_mul ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_algebraic_div ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_algebraic_root ( c : Z3_context , a : Z3_ast , k : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_algebraic_power ( c : Z3_context , a : Z3_ast , k : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_algebraic_lt ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_gt ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_le ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_ge ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_eq ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_neq ( c : Z3_context , a : Z3_ast , b : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_algebraic_roots ( c : Z3_context , p : Z3_ast , n : :: std :: os :: raw :: c_uint , a : * mut Z3_ast ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_algebraic_eval ( c : Z3_context , p : Z3_ast , n : :: std :: os :: raw :: c_uint , a : * mut Z3_ast ) -> :: std :: os :: raw :: c_int ; } extern "C" { pub fn Z3_polynomial_subresultants ( c : Z3_context , p : Z3_ast , q : Z3_ast , x : Z3_ast ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_rcf_del ( c : Z3_context , a : Z3_rcf_num ) ; } extern "C" { pub fn Z3_rcf_mk_rational ( c : Z3_context , val : Z3_string ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_mk_small_int ( c : Z3_context , val : :: std :: os :: raw :: c_int ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_mk_pi ( c : Z3_context ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_mk_e ( c : Z3_context ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_mk_infinitesimal ( c : Z3_context ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_mk_roots ( c : Z3_context , n : :: std :: os :: raw :: c_uint , a : * const Z3_rcf_num , roots : * mut Z3_rcf_num ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_rcf_add ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_sub ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_mul ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_div ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_neg ( c : Z3_context , a : Z3_rcf_num ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_inv ( c : Z3_context , a : Z3_rcf_num ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_power ( c : Z3_context , a : Z3_rcf_num , k : :: std :: os :: raw :: c_uint ) -> Z3_rcf_num ; } extern "C" { pub fn Z3_rcf_lt ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> bool ; } extern "C" { pub fn Z3_rcf_gt ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> bool ; } extern "C" { pub fn Z3_rcf_le ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> bool ; } extern "C" { pub fn Z3_rcf_ge ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> bool ; } extern "C" { pub fn Z3_rcf_eq ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> bool ; } extern "C" { pub fn Z3_rcf_neq ( c : Z3_context , a : Z3_rcf_num , b : Z3_rcf_num ) -> bool ; } extern "C" { pub fn Z3_rcf_num_to_string ( c : Z3_context , a : Z3_rcf_num , compact : bool , html : bool ) -> Z3_string ; } extern "C" { pub fn Z3_rcf_num_to_decimal_string ( c : Z3_context , a : Z3_rcf_num , prec : :: std :: os :: raw :: c_uint ) -> Z3_string ; } extern "C" { pub fn Z3_rcf_get_numerator_denominator ( c : Z3_context , a : Z3_rcf_num , n : * mut Z3_rcf_num , d : * mut Z3_rcf_num ) ; } extern "C" { pub fn Z3_mk_fixedpoint ( c : Z3_context ) -> Z3_fixedpoint ; } extern "C" { pub fn Z3_fixedpoint_inc_ref ( c : Z3_context , d : Z3_fixedpoint ) ; } extern "C" { pub fn Z3_fixedpoint_dec_ref ( c : Z3_context , d : Z3_fixedpoint ) ; } extern "C" { pub fn Z3_fixedpoint_add_rule ( c : Z3_context , d : Z3_fixedpoint , rule : Z3_ast , name : Z3_symbol ) ; } extern "C" { pub fn Z3_fixedpoint_add_fact ( c : Z3_context , d : Z3_fixedpoint , r : Z3_func_decl , num_args : :: std :: os :: raw :: c_uint , args : * mut :: std :: os :: raw :: c_uint ) ; } extern "C" { pub fn Z3_fixedpoint_assert ( c : Z3_context , d : Z3_fixedpoint , axiom : Z3_ast ) ; } extern "C" { pub fn Z3_fixedpoint_query ( c : Z3_context , d : Z3_fixedpoint , query : Z3_ast ) -> Z3_lbool ; } extern "C" { pub fn Z3_fixedpoint_query_relations ( c : Z3_context , d : Z3_fixedpoint , num_relations : :: std :: os :: raw :: c_uint , relations : * const Z3_func_decl ) -> Z3_lbool ; } extern "C" { pub fn Z3_fixedpoint_get_answer ( c : Z3_context , d : Z3_fixedpoint ) -> Z3_ast ; } extern "C" { pub fn Z3_fixedpoint_get_reason_unknown ( c : Z3_context , d : Z3_fixedpoint ) -> Z3_string ; } extern "C" { pub fn Z3_fixedpoint_update_rule ( c : Z3_context , d : Z3_fixedpoint , a : Z3_ast , name : Z3_symbol ) ; } extern "C" { pub fn Z3_fixedpoint_get_num_levels ( c : Z3_context , d : Z3_fixedpoint , pred : Z3_func_decl ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_fixedpoint_get_cover_delta ( c : Z3_context , d : Z3_fixedpoint , level : :: std :: os :: raw :: c_int , pred : Z3_func_decl ) -> Z3_ast ; } extern "C" { pub fn Z3_fixedpoint_add_cover ( c : Z3_context , d : Z3_fixedpoint , level : :: std :: os :: raw :: c_int , pred : Z3_func_decl , property : Z3_ast ) ; } extern "C" { pub fn Z3_fixedpoint_get_statistics ( c : Z3_context , d : Z3_fixedpoint ) -> Z3_stats ; } extern "C" { pub fn Z3_fixedpoint_register_relation ( c : Z3_context , d : Z3_fixedpoint , f : Z3_func_decl ) ; } extern "C" { pub fn Z3_fixedpoint_set_predicate_representation ( c : Z3_context , d : Z3_fixedpoint , f : Z3_func_decl , num_relations : :: std :: os :: raw :: c_uint , relation_kinds : * const Z3_symbol ) ; } extern "C" { pub fn Z3_fixedpoint_get_rules ( c : Z3_context , f : Z3_fixedpoint ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_fixedpoint_get_assertions ( c : Z3_context , f : Z3_fixedpoint ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_fixedpoint_set_params ( c : Z3_context , f : Z3_fixedpoint , p : Z3_params ) ; } extern "C" { pub fn Z3_fixedpoint_get_help ( c : Z3_context , f : Z3_fixedpoint ) -> Z3_string ; } extern "C" { pub fn Z3_fixedpoint_get_param_descrs ( c : Z3_context , f : Z3_fixedpoint ) -> Z3_param_descrs ; } extern "C" { pub fn Z3_fixedpoint_to_string ( c : Z3_context , f : Z3_fixedpoint , num_queries : :: std :: os :: raw :: c_uint , queries : * mut Z3_ast ) -> Z3_string ; } extern "C" { pub fn Z3_fixedpoint_from_string ( c : Z3_context , f : Z3_fixedpoint , s : Z3_string ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_fixedpoint_from_file ( c : Z3_context , f : Z3_fixedpoint , s : Z3_string ) -> Z3_ast_vector ; } pub type Z3_fixedpoint_reduce_assign_callback_fptr = :: std :: option :: Option < unsafe extern "C" fn ( arg1 : * mut :: std :: os :: raw :: c_void , arg2 : Z3_func_decl , arg3 : :: std :: os :: raw :: c_uint , arg4 : * const Z3_ast , arg5 : :: std :: os :: raw :: c_uint , arg6 : * const Z3_ast ) > ; pub type Z3_fixedpoint_reduce_app_callback_fptr = :: std :: option :: Option < unsafe extern "C" fn ( arg1 : * mut :: std :: os :: raw :: c_void , arg2 : Z3_func_decl , arg3 : :: std :: os :: raw :: c_uint , arg4 : * const Z3_ast , arg5 : * mut Z3_ast ) > ; extern "C" { pub fn Z3_fixedpoint_init ( c : Z3_context , d : Z3_fixedpoint , state : * mut :: std :: os :: raw :: c_void ) ; } extern "C" { pub fn Z3_fixedpoint_set_reduce_assign_callback ( c : Z3_context , d : Z3_fixedpoint , cb : Z3_fixedpoint_reduce_assign_callback_fptr ) ; } extern "C" { pub fn Z3_fixedpoint_set_reduce_app_callback ( c : Z3_context , d : Z3_fixedpoint , cb : Z3_fixedpoint_reduce_app_callback_fptr ) ; } pub type Z3_fixedpoint_new_lemma_eh = :: std :: option :: Option < unsafe extern "C" fn ( state : * mut :: std :: os :: raw :: c_void , lemma : Z3_ast , level : :: std :: os :: raw :: c_uint ) > ; pub type Z3_fixedpoint_predecessor_eh = :: std :: option :: Option < unsafe extern "C" fn ( state : * mut :: std :: os :: raw :: c_void ) > ; pub type Z3_fixedpoint_unfold_eh = :: std :: option :: Option < unsafe extern "C" fn ( state : * mut :: std :: os :: raw :: c_void ) > ; extern "C" { pub fn Z3_fixedpoint_add_callback ( ctx : Z3_context , f : Z3_fixedpoint , state : * mut :: std :: os :: raw :: c_void , new_lemma_eh : Z3_fixedpoint_new_lemma_eh , predecessor_eh : Z3_fixedpoint_predecessor_eh , unfold_eh : Z3_fixedpoint_unfold_eh ) ; } extern "C" { pub fn Z3_fixedpoint_add_constraint ( c : Z3_context , d : Z3_fixedpoint , e : Z3_ast , lvl : :: std :: os :: raw :: c_uint ) ; } extern "C" { pub fn Z3_mk_optimize ( c : Z3_context ) -> Z3_optimize ; } extern "C" { pub fn Z3_optimize_inc_ref ( c : Z3_context , d : Z3_optimize ) ; } extern "C" { pub fn Z3_optimize_dec_ref ( c : Z3_context , d : Z3_optimize ) ; } extern "C" { pub fn Z3_optimize_assert ( c : Z3_context , o : Z3_optimize , a : Z3_ast ) ; } extern "C" { pub fn Z3_optimize_assert_and_track ( c : Z3_context , o : Z3_optimize , a : Z3_ast , t : Z3_ast ) ; } extern "C" { pub fn Z3_optimize_assert_soft ( c : Z3_context , o : Z3_optimize , a : Z3_ast , weight : Z3_string , id : Z3_symbol ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_optimize_maximize ( c : Z3_context , o : Z3_optimize , t : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_optimize_minimize ( c : Z3_context , o : Z3_optimize , t : Z3_ast ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_optimize_push ( c : Z3_context , d : Z3_optimize ) ; } extern "C" { pub fn Z3_optimize_pop ( c : Z3_context , d : Z3_optimize ) ; } extern "C" { pub fn Z3_optimize_check ( c : Z3_context , o : Z3_optimize , num_assumptions : :: std :: os :: raw :: c_uint , assumptions : * const Z3_ast ) -> Z3_lbool ; } extern "C" { pub fn Z3_optimize_get_reason_unknown ( c : Z3_context , d : Z3_optimize ) -> Z3_string ; } extern "C" { pub fn Z3_optimize_get_model ( c : Z3_context , o : Z3_optimize ) -> Z3_model ; } extern "C" { pub fn Z3_optimize_get_unsat_core ( c : Z3_context , o : Z3_optimize ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_optimize_set_params ( c : Z3_context , o : Z3_optimize , p : Z3_params ) ; } extern "C" { pub fn Z3_optimize_get_param_descrs ( c : Z3_context , o : Z3_optimize ) -> Z3_param_descrs ; } extern "C" { pub fn Z3_optimize_get_lower ( c : Z3_context , o : Z3_optimize , idx : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_optimize_get_upper ( c : Z3_context , o : Z3_optimize , idx : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_optimize_get_lower_as_vector ( c : Z3_context , o : Z3_optimize , idx : :: std :: os :: raw :: c_uint ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_optimize_get_upper_as_vector ( c : Z3_context , o : Z3_optimize , idx : :: std :: os :: raw :: c_uint ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_optimize_to_string ( c : Z3_context , o : Z3_optimize ) -> Z3_string ; } extern "C" { pub fn Z3_optimize_from_string ( c : Z3_context , o : Z3_optimize , s : Z3_string ) ; } extern "C" { pub fn Z3_optimize_from_file ( c : Z3_context , o : Z3_optimize , s : Z3_string ) ; } extern "C" { pub fn Z3_optimize_get_help ( c : Z3_context , t : Z3_optimize ) -> Z3_string ; } extern "C" { pub fn Z3_optimize_get_statistics ( c : Z3_context , d : Z3_optimize ) -> Z3_stats ; } extern "C" { pub fn Z3_optimize_get_assertions ( c : Z3_context , o : Z3_optimize ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_optimize_get_objectives ( c : Z3_context , o : Z3_optimize ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_mk_fpa_rounding_mode_sort ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_round_nearest_ties_to_even ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_rne ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_round_nearest_ties_to_away ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_rna ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_round_toward_positive ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_rtp ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_round_toward_negative ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_rtn ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_round_toward_zero ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_rtz ( c : Z3_context ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_sort ( c : Z3_context , ebits : :: std :: os :: raw :: c_uint , sbits : :: std :: os :: raw :: c_uint ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_sort_half ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_sort_16 ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_sort_single ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_sort_32 ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_sort_double ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_sort_64 ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_sort_quadruple ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_sort_128 ( c : Z3_context ) -> Z3_sort ; } extern "C" { pub fn Z3_mk_fpa_nan ( c : Z3_context , s : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_inf ( c : Z3_context , s : Z3_sort , negative : bool ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_zero ( c : Z3_context , s : Z3_sort , negative : bool ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_fp ( c : Z3_context , sgn : Z3_ast , exp : Z3_ast , sig : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_numeral_float ( c : Z3_context , v : f32 , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_numeral_double ( c : Z3_context , v : f64 , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_numeral_int ( c : Z3_context , v : :: std :: os :: raw :: c_int , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_numeral_int_uint ( c : Z3_context , sgn : bool , exp : :: std :: os :: raw :: c_int , sig : :: std :: os :: raw :: c_uint , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_numeral_int64_uint64 ( c : Z3_context , sgn : bool , exp : i64 , sig : u64 , ty : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_abs ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_neg ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_add ( c : Z3_context , rm : Z3_ast , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_sub ( c : Z3_context , rm : Z3_ast , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_mul ( c : Z3_context , rm : Z3_ast , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_div ( c : Z3_context , rm : Z3_ast , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_fma ( c : Z3_context , rm : Z3_ast , t1 : Z3_ast , t2 : Z3_ast , t3 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_sqrt ( c : Z3_context , rm : Z3_ast , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_rem ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_round_to_integral ( c : Z3_context , rm : Z3_ast , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_min ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_max ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_leq ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_lt ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_geq ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_gt ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_eq ( c : Z3_context , t1 : Z3_ast , t2 : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_is_normal ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_is_subnormal ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_is_zero ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_is_infinite ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_is_nan ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_is_negative ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_is_positive ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_fp_bv ( c : Z3_context , bv : Z3_ast , s : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_fp_float ( c : Z3_context , rm : Z3_ast , t : Z3_ast , s : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_fp_real ( c : Z3_context , rm : Z3_ast , t : Z3_ast , s : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_fp_signed ( c : Z3_context , rm : Z3_ast , t : Z3_ast , s : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_fp_unsigned ( c : Z3_context , rm : Z3_ast , t : Z3_ast , s : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_ubv ( c : Z3_context , rm : Z3_ast , t : Z3_ast , sz : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_sbv ( c : Z3_context , rm : Z3_ast , t : Z3_ast , sz : :: std :: os :: raw :: c_uint ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_real ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_fpa_get_ebits ( c : Z3_context , s : Z3_sort ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_fpa_get_sbits ( c : Z3_context , s : Z3_sort ) -> :: std :: os :: raw :: c_uint ; } extern "C" { pub fn Z3_fpa_is_numeral_nan ( c : Z3_context , t : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_fpa_is_numeral_inf ( c : Z3_context , t : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_fpa_is_numeral_zero ( c : Z3_context , t : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_fpa_is_numeral_normal ( c : Z3_context , t : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_fpa_is_numeral_subnormal ( c : Z3_context , t : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_fpa_is_numeral_positive ( c : Z3_context , t : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_fpa_is_numeral_negative ( c : Z3_context , t : Z3_ast ) -> bool ; } extern "C" { pub fn Z3_fpa_get_numeral_sign_bv ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_fpa_get_numeral_significand_bv ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_fpa_get_numeral_sign ( c : Z3_context , t : Z3_ast , sgn : * mut :: std :: os :: raw :: c_int ) -> bool ; } extern "C" { pub fn Z3_fpa_get_numeral_significand_string ( c : Z3_context , t : Z3_ast ) -> Z3_string ; } extern "C" { pub fn Z3_fpa_get_numeral_significand_uint64 ( c : Z3_context , t : Z3_ast , n : * mut u64 ) -> bool ; } extern "C" { pub fn Z3_fpa_get_numeral_exponent_string ( c : Z3_context , t : Z3_ast , biased : bool ) -> Z3_string ; } extern "C" { pub fn Z3_fpa_get_numeral_exponent_int64 ( c : Z3_context , t : Z3_ast , n : * mut i64 , biased : bool ) -> bool ; } extern "C" { pub fn Z3_fpa_get_numeral_exponent_bv ( c : Z3_context , t : Z3_ast , biased : bool ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_ieee_bv ( c : Z3_context , t : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_mk_fpa_to_fp_int_real ( c : Z3_context , rm : Z3_ast , exp : Z3_ast , sig : Z3_ast , s : Z3_sort ) -> Z3_ast ; } extern "C" { pub fn Z3_fixedpoint_query_from_lvl ( c : Z3_context , d : Z3_fixedpoint , query : Z3_ast , lvl : :: std :: os :: raw :: c_uint ) -> Z3_lbool ; } extern "C" { pub fn Z3_fixedpoint_get_ground_sat_answer ( c : Z3_context , d : Z3_fixedpoint ) -> Z3_ast ; } extern "C" { pub fn Z3_fixedpoint_get_rules_along_trace ( c : Z3_context , d : Z3_fixedpoint ) -> Z3_ast_vector ; } extern "C" { pub fn Z3_fixedpoint_get_rule_names_along_trace ( c : Z3_context , d : Z3_fixedpoint ) -> Z3_symbol ; } extern "C" { pub fn Z3_fixedpoint_add_invariant ( c : Z3_context , d : Z3_fixedpoint , pred : Z3_func_decl , property : Z3_ast ) ; } extern "C" { pub fn Z3_fixedpoint_get_reachable ( c : Z3_context , d : Z3_fixedpoint , pred : Z3_func_decl ) -> Z3_ast ; } extern "C" { pub fn Z3_qe_model_project ( c : Z3_context , m : Z3_model , num_bounds : :: std :: os :: raw :: c_uint , bound : * const Z3_app , body : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_qe_model_project_skolem ( c : Z3_context , m : Z3_model , num_bounds : :: std :: os :: raw :: c_uint , bound : * const Z3_app , body : Z3_ast , map : Z3_ast_map ) -> Z3_ast ; } extern "C" { pub fn Z3_model_extrapolate ( c : Z3_context , m : Z3_model , fml : Z3_ast ) -> Z3_ast ; } extern "C" { pub fn Z3_qe_lite ( c : Z3_context , vars : Z3_ast_vector , body : Z3_ast ) -> Z3_ast ; } pub type __builtin_va_list = [ __va_list_tag ; 1usize ] ; # [ repr ( C ) ] # [ derive ( Debug , Copy , Clone ) ] pub struct __va_list_tag { pub gp_offset : :: std :: os :: raw :: c_uint , pub fp_offset : :: std :: os :: raw :: c_uint , pub overflow_arg_area : * mut :: std :: os :: raw :: c_void , pub reg_save_area : * mut :: std :: os :: raw :: c_void , } # [ test ] fn bindgen_test_layout___va_list_tag ( ) { assert_eq ! ( :: std :: mem :: size_of :: < __va_list_tag > ( ) , 24usize , concat ! ( "Size of: " , stringify ! ( __va_list_tag ) ) ) ; assert_eq ! ( :: std :: mem :: align_of :: < __va_list_tag > ( ) , 8usize , concat ! ( "Alignment of " , stringify ! ( __va_list_tag ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __va_list_tag > ( ) ) ) . gp_offset as * const _ as usize } , 0usize , concat ! ( "Offset of field: " , stringify ! ( __va_list_tag ) , "::" , stringify ! ( gp_offset ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __va_list_tag > ( ) ) ) . fp_offset as * const _ as usize } , 4usize , concat ! ( "Offset of field: " , stringify ! ( __va_list_tag ) , "::" , stringify ! ( fp_offset ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __va_list_tag > ( ) ) ) . overflow_arg_area as * const _ as usize } , 8usize , concat ! ( "Offset of field: " , stringify ! ( __va_list_tag ) , "::" , stringify ! ( overflow_arg_area ) ) ) ; assert_eq ! ( unsafe { & ( * ( :: std :: ptr :: null :: < __va_list_tag > ( ) ) ) . reg_save_area as * const _ as usize } , 16usize , concat ! ( "Offset of field: " , stringify ! ( __va_list_tag ) , "::" , stringify ! ( reg_save_area ) ) ) ; } [INFO] [stderr] | ------------------------------------------------------------------------------------------------------------------------------------------------------------ defined here [INFO] [stderr] [INFO] [stderr] error: aborting due to previous error [INFO] [stderr] [INFO] [stderr] For more information about this error, try `rustc --explain E0061`. [INFO] [stderr] error: could not compile `z3_ref`. [INFO] [stderr] [INFO] [stderr] To learn more, run the command again with --verbose. [INFO] running `"docker" "inspect" "1d1e78dfb4569fd25f76be1e72d35276f07d836aedf6519d692ad5604ca477b7"` [INFO] running `"docker" "rm" "-f" "1d1e78dfb4569fd25f76be1e72d35276f07d836aedf6519d692ad5604ca477b7"` [INFO] [stdout] 1d1e78dfb4569fd25f76be1e72d35276f07d836aedf6519d692ad5604ca477b7