z3.cabal:    * "Z3.Base.C" provides the raw foreign imports from Z3's C API.
src/Z3/Base/C.hsc:-- Z3 API foreign imports.
src/Z3/Base/C.hsc:Add here the foreign import to support a new API function:
src/Z3/Base/C.hsc:* Take a look to a few others foreign imports and follow the same coding style.
src/Z3/Base/C.hsc:* Place the foreign import in the right section, according to the Z3's API documentation.
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_config"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_del_config"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_set_param_value"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_context_rc"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_del_context"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_int_symbol"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_string_symbol"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_sort_to_ast"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_uninterpreted_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bool_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_int_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_real_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bv_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_array_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_tuple_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_constructor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_del_constructor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_datatype"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_constructor_list"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_del_constructor_list"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_datatypes"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_func_decl"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_app"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_const"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_fresh_const"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_fresh_func_decl"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_true"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_false"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_eq"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_distinct"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_not"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_ite"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_iff"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_implies"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_xor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_and"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_or"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_add"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_mul"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_sub"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_unary_minus"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_div"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_mod"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_rem"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_lt"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_le"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_gt"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_ge"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_int2real"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_real2int"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_is_int"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvnot"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvredand"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvredor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvand"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvxor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvnand"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvnor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvxnor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvneg"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvadd"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsub"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvmul"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvudiv"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsdiv"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvurem"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsrem"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsmod"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvult"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvslt"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvule"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsle"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvuge"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsge"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvugt"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsgt"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_concat"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_extract"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_sign_ext"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_zero_ext"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_repeat"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvshl"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvlshr"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvashr"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_rotate_left"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_rotate_right"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_ext_rotate_left"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_ext_rotate_right"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_int2bv"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bv2int"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvadd_no_overflow"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvadd_no_underflow"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsub_no_overflow"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsub_no_underflow"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvsdiv_no_overflow"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvneg_no_overflow"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvmul_no_overflow"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bvmul_no_underflow"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_select"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_store"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_const_array"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_map"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_array_default"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_empty_set"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_full_set"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_add"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_del"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_union"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_intersect"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_difference"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_complement"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_member"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_set_subset"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_numeral"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_real"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_int"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_unsigned_int"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_int64"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_unsigned_int64"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_pattern"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_bound"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_forall"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_exists"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_forall_const"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_exists_const"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_decl_to_ast"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_ast_kind"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_is_app"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_app_num_args"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_app_arg"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_app_decl"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_datatype_sort_num_constructors"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_datatype_sort_constructor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_datatype_sort_recognizer"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_datatype_sort_constructor_accessor"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_decl_name"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_symbol_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_sort_kind"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_bv_sort_size"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_app_to_ast"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_array_sort_domain"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_array_sort_range"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_bool_value"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_numeral_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_arity"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_domain"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_range"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_to_app"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_pattern_to_ast"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_simplify"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_simplify_ex"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_is_quantifier_forall"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_weight"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_num_patterns"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_pattern_ast"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_num_no_patterns"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_no_pattern_ast"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_num_bound"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_bound_name"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_bound_sort"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_quantifier_body"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_substitute_vars"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_ast_vector_size"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_ast_vector_get"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_ast_vector_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_ast_vector_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_eval"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_get_const_interp"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_get_func_interp"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_has_interp"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_get_num_consts"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_get_num_funcs"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_get_const_decl"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_get_func_decl"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_is_as_array"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_as_array_func_decl"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_add_func_interp"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_add_const_interp"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_interp_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_interp_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_interp_get_num_entries"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_interp_get_entry"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_interp_get_else"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_interp_get_arity"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_entry_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_entry_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_entry_get_value"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_entry_get_num_args"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_entry_get_arg"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_index_value"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_model_to_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_params"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_params_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_params_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_params_set_bool"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_params_set_uint"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_params_set_double"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_params_set_symbol"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_params_to_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_interpolant"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_interpolation_context"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_interpolant"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_compute_interpolant"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_read_interpolation_problem"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_check_interpolant"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_interpolation_profile"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_write_interpolation_problem"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_tactic"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_tactic_and_then"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_tactic_or_else"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_tactic_skip"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_tactic_try_for"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_tactic_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_tactic_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_tactic_apply"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_apply_result_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_apply_result_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_apply_result_get_num_subgoals"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_apply_result_get_subgoal"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_goal"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_goal_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_goal_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_goal_assert"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_goal_size"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_goal_formula"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_solver"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_simple_solver"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_solver_for_logic"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_get_help"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_set_params"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_push"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_pop"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_get_num_scopes"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_reset"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_assert"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_assert_and_track"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_check"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_check_assumptions"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_get_model"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_get_unsat_core"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_get_reason_unknown"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_solver_to_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_set_ast_print_mode"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_ast_to_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_pattern_to_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_sort_to_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_func_decl_to_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_benchmark_to_smtlib_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_parse_smtlib2_string"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_parse_smtlib2_file"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_parser_error"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_error_code"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_set_error_handler"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_set_error"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_error_msg"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_error_msg_ex"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_get_version"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_mk_fixedpoint"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_push"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_pop"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_inc_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_dec_ref"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_set_params"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_add_rule"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_register_relation"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_get_answer"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_get_assertions"
src/Z3/Base/C.hsc:foreign import ccall unsafe "Z3_fixedpoint_query_relations"