LIBRARY "Z3_DBG"
EXPORTS
	Z3_mk_config @3
	Z3_del_config @4
	Z3_set_param_value @5
	Z3_mk_context @6
	Z3_mk_context_rc @7
	Z3_del_context @8
	Z3_inc_ref @9
	Z3_dec_ref @10
	Z3_update_param_value @11
	Z3_get_param_value @12
	Z3_interrupt @13
	Z3_mk_params @14
	Z3_params_inc_ref @15
	Z3_params_dec_ref @16
	Z3_params_set_bool @17
	Z3_params_set_uint @18
	Z3_params_set_double @19
	Z3_params_set_symbol @20
	Z3_params_to_string @21
	Z3_params_validate @22
	Z3_param_descrs_inc_ref @23
	Z3_param_descrs_dec_ref @24
	Z3_param_descrs_get_kind @25
	Z3_param_descrs_size @26
	Z3_param_descrs_get_name @27
	Z3_param_descrs_to_string @28
	Z3_mk_int_symbol @29
	Z3_mk_string_symbol @30
	Z3_mk_uninterpreted_sort @31
	Z3_mk_bool_sort @32
	Z3_mk_int_sort @33
	Z3_mk_real_sort @34
	Z3_mk_bv_sort @35
	Z3_mk_finite_domain_sort @36
	Z3_mk_array_sort @37
	Z3_mk_tuple_sort @38
	Z3_mk_enumeration_sort @39
	Z3_mk_list_sort @40
	Z3_mk_constructor @41
	Z3_del_constructor @42
	Z3_mk_datatype @43
	Z3_mk_constructor_list @44
	Z3_del_constructor_list @45
	Z3_mk_datatypes @46
	Z3_query_constructor @47
	Z3_mk_func_decl @48
	Z3_mk_app @49
	Z3_mk_const @50
	Z3_mk_fresh_func_decl @51
	Z3_mk_fresh_const @52
	Z3_mk_true @53
	Z3_mk_false @54
	Z3_mk_eq @55
	Z3_mk_distinct @56
	Z3_mk_not @57
	Z3_mk_ite @58
	Z3_mk_iff @59
	Z3_mk_implies @60
	Z3_mk_xor @61
	Z3_mk_and @62
	Z3_mk_or @63
	Z3_mk_add @64
	Z3_mk_mul @65
	Z3_mk_sub @66
	Z3_mk_unary_minus @67
	Z3_mk_div @68
	Z3_mk_mod @69
	Z3_mk_rem @70
	Z3_mk_power @71
	Z3_mk_lt @72
	Z3_mk_le @73
	Z3_mk_gt @74
	Z3_mk_ge @75
	Z3_mk_int2real @76
	Z3_mk_real2int @77
	Z3_mk_is_int @78
	Z3_mk_bvnot @79
	Z3_mk_bvredand @80
	Z3_mk_bvredor @81
	Z3_mk_bvand @82
	Z3_mk_bvor @83
	Z3_mk_bvxor @84
	Z3_mk_bvnand @85
	Z3_mk_bvnor @86
	Z3_mk_bvxnor @87
	Z3_mk_bvneg @88
	Z3_mk_bvadd @89
	Z3_mk_bvsub @90
	Z3_mk_bvmul @91
	Z3_mk_bvudiv @92
	Z3_mk_bvsdiv @93
	Z3_mk_bvurem @94
	Z3_mk_bvsrem @95
	Z3_mk_bvsmod @96
	Z3_mk_bvult @97
	Z3_mk_bvslt @98
	Z3_mk_bvule @99
	Z3_mk_bvsle @100
	Z3_mk_bvuge @101
	Z3_mk_bvsge @102
	Z3_mk_bvugt @103
	Z3_mk_bvsgt @104
	Z3_mk_concat @105
	Z3_mk_extract @106
	Z3_mk_sign_ext @107
	Z3_mk_zero_ext @108
	Z3_mk_repeat @109
	Z3_mk_bvshl @110
	Z3_mk_bvlshr @111
	Z3_mk_bvashr @112
	Z3_mk_rotate_left @113
	Z3_mk_rotate_right @114
	Z3_mk_ext_rotate_left @115
	Z3_mk_ext_rotate_right @116
	Z3_mk_int2bv @117
	Z3_mk_bv2int @118
	Z3_mk_bvadd_no_overflow @119
	Z3_mk_bvadd_no_underflow @120
	Z3_mk_bvsub_no_overflow @121
	Z3_mk_bvsub_no_underflow @122
	Z3_mk_bvsdiv_no_overflow @123
	Z3_mk_bvneg_no_overflow @124
	Z3_mk_bvmul_no_overflow @125
	Z3_mk_bvmul_no_underflow @126
	Z3_mk_select @127
	Z3_mk_store @128
	Z3_mk_const_array @129
	Z3_mk_map @130
	Z3_mk_array_default @131
	Z3_mk_set_sort @132
	Z3_mk_empty_set @133
	Z3_mk_full_set @134
	Z3_mk_set_add @135
	Z3_mk_set_del @136
	Z3_mk_set_union @137
	Z3_mk_set_intersect @138
	Z3_mk_set_difference @139
	Z3_mk_set_complement @140
	Z3_mk_set_member @141
	Z3_mk_set_subset @142
	Z3_mk_numeral @143
	Z3_mk_real @144
	Z3_mk_int @145
	Z3_mk_unsigned_int @146
	Z3_mk_int64 @147
	Z3_mk_unsigned_int64 @148
	Z3_mk_pattern @149
	Z3_mk_bound @150
	Z3_mk_forall @151
	Z3_mk_exists @152
	Z3_mk_quantifier @153
	Z3_mk_quantifier_ex @154
	Z3_mk_forall_const @155
	Z3_mk_exists_const @156
	Z3_mk_quantifier_const @157
	Z3_mk_quantifier_const_ex @158
	Z3_get_symbol_kind @159
	Z3_get_symbol_int @160
	Z3_get_symbol_string @161
	Z3_get_sort_name @162
	Z3_get_sort_id @163
	Z3_sort_to_ast @164
	Z3_is_eq_sort @165
	Z3_get_sort_kind @166
	Z3_get_bv_sort_size @167
	Z3_get_finite_domain_sort_size @168
	Z3_get_array_sort_domain @169
	Z3_get_array_sort_range @170
	Z3_get_tuple_sort_mk_decl @171
	Z3_get_tuple_sort_num_fields @172
	Z3_get_tuple_sort_field_decl @173
	Z3_get_datatype_sort_num_constructors @174
	Z3_get_datatype_sort_constructor @175
	Z3_get_datatype_sort_recognizer @176
	Z3_get_datatype_sort_constructor_accessor @177
	Z3_get_relation_arity @178
	Z3_get_relation_column @179
	Z3_func_decl_to_ast @180
	Z3_is_eq_func_decl @181
	Z3_get_func_decl_id @182
	Z3_get_decl_name @183
	Z3_get_decl_kind @184
	Z3_get_domain_size @185
	Z3_get_arity @186
	Z3_get_domain @187
	Z3_get_range @188
	Z3_get_decl_num_parameters @189
	Z3_get_decl_parameter_kind @190
	Z3_get_decl_int_parameter @191
	Z3_get_decl_double_parameter @192
	Z3_get_decl_symbol_parameter @193
	Z3_get_decl_sort_parameter @194
	Z3_get_decl_ast_parameter @195
	Z3_get_decl_func_decl_parameter @196
	Z3_get_decl_rational_parameter @197
	Z3_app_to_ast @198
	Z3_get_app_decl @199
	Z3_get_app_num_args @200
	Z3_get_app_arg @201
	Z3_is_eq_ast @202
	Z3_get_ast_id @203
	Z3_get_ast_hash @204
	Z3_get_sort @205
	Z3_is_well_sorted @206
	Z3_get_bool_value @207
	Z3_get_ast_kind @208
	Z3_is_app @209
	Z3_is_numeral_ast @210
	Z3_is_algebraic_number @211
	Z3_to_app @212
	Z3_to_func_decl @213
	Z3_get_numeral_string @214
	Z3_get_numeral_decimal_string @215
	Z3_get_numerator @216
	Z3_get_denominator @217
	Z3_get_numeral_small @218
	Z3_get_numeral_int @219
	Z3_get_numeral_uint @220
	Z3_get_numeral_uint64 @221
	Z3_get_numeral_int64 @222
	Z3_get_numeral_rational_int64 @223
	Z3_get_algebraic_number_lower @224
	Z3_get_algebraic_number_upper @225
	Z3_pattern_to_ast @226
	Z3_get_pattern_num_terms @227
	Z3_get_pattern @228
	Z3_get_index_value @229
	Z3_is_quantifier_forall @230
	Z3_get_quantifier_weight @231
	Z3_get_quantifier_num_patterns @232
	Z3_get_quantifier_pattern_ast @233
	Z3_get_quantifier_num_no_patterns @234
	Z3_get_quantifier_no_pattern_ast @235
	Z3_get_quantifier_num_bound @236
	Z3_get_quantifier_bound_name @237
	Z3_get_quantifier_bound_sort @238
	Z3_get_quantifier_body @239
	Z3_simplify @240
	Z3_simplify_ex @241
	Z3_simplify_get_help @242
	Z3_simplify_get_param_descrs @243
	Z3_update_term @244
	Z3_substitute @245
	Z3_substitute_vars @246
	Z3_translate @247
	Z3_model_inc_ref @248
	Z3_model_dec_ref @249
	Z3_model_eval @250
	Z3_model_get_const_interp @251
	Z3_model_get_func_interp @252
	Z3_model_get_num_consts @253
	Z3_model_get_const_decl @254
	Z3_model_get_num_funcs @255
	Z3_model_get_func_decl @256
	Z3_model_get_num_sorts @257
	Z3_model_get_sort @258
	Z3_model_get_sort_universe @259
	Z3_is_as_array @260
	Z3_get_as_array_func_decl @261
	Z3_func_interp_inc_ref @262
	Z3_func_interp_dec_ref @263
	Z3_func_interp_get_num_entries @264
	Z3_func_interp_get_entry @265
	Z3_func_interp_get_else @266
	Z3_func_interp_get_arity @267
	Z3_func_entry_inc_ref @268
	Z3_func_entry_dec_ref @269
	Z3_func_entry_get_value @270
	Z3_func_entry_get_num_args @271
	Z3_func_entry_get_arg @272
	Z3_open_log @273
	Z3_append_log @274
	Z3_close_log @275
	Z3_toggle_warning_messages @276
	Z3_set_ast_print_mode @277
	Z3_ast_to_string @278
	Z3_pattern_to_string @279
	Z3_sort_to_string @280
	Z3_func_decl_to_string @281
	Z3_model_to_string @282
	Z3_benchmark_to_smtlib_string @283
	Z3_parse_smtlib2_string @284
	Z3_parse_smtlib2_file @285
	Z3_parse_smtlib_string @286
	Z3_parse_smtlib_file @287
	Z3_get_smtlib_num_formulas @288
	Z3_get_smtlib_formula @289
	Z3_get_smtlib_num_assumptions @290
	Z3_get_smtlib_assumption @291
	Z3_get_smtlib_num_decls @292
	Z3_get_smtlib_decl @293
	Z3_get_smtlib_num_sorts @294
	Z3_get_smtlib_sort @295
	Z3_get_smtlib_error @296
	Z3_parse_z3_string @297
	Z3_parse_z3_file @298
	Z3_get_error_code @299
	Z3_set_error_handler @300
	Z3_set_error @301
	Z3_get_error_msg @302
	Z3_get_error_msg_ex @303
	Z3_get_version @304
	Z3_reset_memory @305
	Z3_mk_theory @306
	Z3_theory_get_ext_data @307
	Z3_theory_mk_sort @308
	Z3_theory_mk_value @309
	Z3_theory_mk_constant @310
	Z3_theory_mk_func_decl @311
	Z3_theory_get_context @312
	Z3_set_delete_callback @313
	Z3_set_reduce_app_callback @314
	Z3_set_reduce_eq_callback @315
	Z3_set_reduce_distinct_callback @316
	Z3_set_new_app_callback @317
	Z3_set_new_elem_callback @318
	Z3_set_init_search_callback @319
	Z3_set_push_callback @320
	Z3_set_pop_callback @321
	Z3_set_restart_callback @322
	Z3_set_reset_callback @323
	Z3_set_final_check_callback @324
	Z3_set_new_eq_callback @325
	Z3_set_new_diseq_callback @326
	Z3_set_new_assignment_callback @327
	Z3_set_new_relevant_callback @328
	Z3_theory_assert_axiom @329
	Z3_theory_assume_eq @330
	Z3_theory_enable_axiom_simplification @331
	Z3_theory_get_eqc_root @332
	Z3_theory_get_eqc_next @333
	Z3_theory_get_num_parents @334
	Z3_theory_get_parent @335
	Z3_theory_is_value @336
	Z3_theory_is_decl @337
	Z3_theory_get_num_elems @338
	Z3_theory_get_elem @339
	Z3_theory_get_num_apps @340
	Z3_theory_get_app @341
	Z3_mk_fixedpoint @342
	Z3_fixedpoint_inc_ref @343
	Z3_fixedpoint_dec_ref @344
	Z3_fixedpoint_add_rule @345
	Z3_fixedpoint_add_fact @346
	Z3_fixedpoint_assert @347
	Z3_fixedpoint_query @348
	Z3_fixedpoint_query_relations @349
	Z3_fixedpoint_get_answer @350
	Z3_fixedpoint_get_reason_unknown @351
	Z3_fixedpoint_update_rule @352
	Z3_fixedpoint_get_num_levels @353
	Z3_fixedpoint_get_cover_delta @354
	Z3_fixedpoint_add_cover @355
	Z3_fixedpoint_get_statistics @356
	Z3_fixedpoint_register_relation @357
	Z3_fixedpoint_set_predicate_representation @358
	Z3_fixedpoint_simplify_rules @359
	Z3_fixedpoint_set_params @360
	Z3_fixedpoint_get_help @361
	Z3_fixedpoint_get_param_descrs @362
	Z3_fixedpoint_to_string @363
	Z3_fixedpoint_push @364
	Z3_fixedpoint_pop @365
	Z3_fixedpoint_init @366
	Z3_fixedpoint_set_reduce_assign_callback @367
	Z3_fixedpoint_set_reduce_app_callback @368
	Z3_mk_ast_vector @369
	Z3_ast_vector_inc_ref @370
	Z3_ast_vector_dec_ref @371
	Z3_ast_vector_size @372
	Z3_ast_vector_get @373
	Z3_ast_vector_set @374
	Z3_ast_vector_resize @375
	Z3_ast_vector_push @376
	Z3_ast_vector_translate @377
	Z3_ast_vector_to_string @378
	Z3_mk_ast_map @379
	Z3_ast_map_inc_ref @380
	Z3_ast_map_dec_ref @381
	Z3_ast_map_contains @382
	Z3_ast_map_find @383
	Z3_ast_map_insert @384
	Z3_ast_map_erase @385
	Z3_ast_map_reset @386
	Z3_ast_map_size @387
	Z3_ast_map_keys @388
	Z3_ast_map_to_string @389
	Z3_mk_goal @390
	Z3_goal_inc_ref @391
	Z3_goal_dec_ref @392
	Z3_goal_precision @393
	Z3_goal_assert @394
	Z3_goal_inconsistent @395
	Z3_goal_depth @396
	Z3_goal_reset @397
	Z3_goal_size @398
	Z3_goal_formula @399
	Z3_goal_num_exprs @400
	Z3_goal_is_decided_sat @401
	Z3_goal_is_decided_unsat @402
	Z3_goal_translate @403
	Z3_goal_to_string @404
	Z3_mk_tactic @405
	Z3_tactic_inc_ref @406
	Z3_tactic_dec_ref @407
	Z3_mk_probe @408
	Z3_probe_inc_ref @409
	Z3_probe_dec_ref @410
	Z3_tactic_and_then @411
	Z3_tactic_or_else @412
	Z3_tactic_par_or @413
	Z3_tactic_par_and_then @414
	Z3_tactic_try_for @415
	Z3_tactic_when @416
	Z3_tactic_cond @417
	Z3_tactic_repeat @418
	Z3_tactic_skip @419
	Z3_tactic_fail @420
	Z3_tactic_fail_if @421
	Z3_tactic_fail_if_not_decided @422
	Z3_tactic_using_params @423
	Z3_probe_const @424
	Z3_probe_lt @425
	Z3_probe_gt @426
	Z3_probe_le @427
	Z3_probe_ge @428
	Z3_probe_eq @429
	Z3_probe_and @430
	Z3_probe_or @431
	Z3_probe_not @432
	Z3_get_num_tactics @433
	Z3_get_tactic_name @434
	Z3_get_num_probes @435
	Z3_get_probe_name @436
	Z3_tactic_get_help @437
	Z3_tactic_get_param_descrs @438
	Z3_tactic_get_descr @439
	Z3_probe_get_descr @440
	Z3_probe_apply @441
	Z3_tactic_apply @442
	Z3_tactic_apply_ex @443
	Z3_apply_result_inc_ref @444
	Z3_apply_result_dec_ref @445
	Z3_apply_result_to_string @446
	Z3_apply_result_get_num_subgoals @447
	Z3_apply_result_get_subgoal @448
	Z3_apply_result_convert_model @449
	Z3_mk_solver @450
	Z3_mk_simple_solver @451
	Z3_mk_solver_for_logic @452
	Z3_mk_solver_from_tactic @453
	Z3_solver_get_help @454
	Z3_solver_get_param_descrs @455
	Z3_solver_set_params @456
	Z3_solver_inc_ref @457
	Z3_solver_dec_ref @458
	Z3_solver_push @459
	Z3_solver_pop @460
	Z3_solver_reset @461
	Z3_solver_get_num_scopes @462
	Z3_solver_assert @463
	Z3_solver_get_assertions @464
	Z3_solver_check @465
	Z3_solver_check_assumptions @466
	Z3_solver_get_model @467
	Z3_solver_get_proof @468
	Z3_solver_get_unsat_core @469
	Z3_solver_get_reason_unknown @470
	Z3_solver_get_statistics @471
	Z3_solver_to_string @472
	Z3_stats_to_string @473
	Z3_stats_inc_ref @474
	Z3_stats_dec_ref @475
	Z3_stats_size @476
	Z3_stats_get_key @477
	Z3_stats_is_uint @478
	Z3_stats_is_double @479
	Z3_stats_get_uint_value @480
	Z3_stats_get_double_value @481
	Z3_mk_injective_function @482
	Z3_set_logic @483
	Z3_push @484
	Z3_pop @485
	Z3_get_num_scopes @486
	Z3_persist_ast @487
	Z3_assert_cnstr @488
	Z3_check_and_get_model @489
	Z3_check @490
	Z3_check_assumptions @491
	Z3_get_implied_equalities @492
	Z3_del_model @493
	Z3_soft_check_cancel @494
	Z3_get_search_failure @495
	Z3_mk_label @496
	Z3_get_relevant_labels @497
	Z3_get_relevant_literals @498
	Z3_get_guessed_literals @499
	Z3_del_literals @500
	Z3_get_num_literals @501
	Z3_get_label_symbol @502
	Z3_get_literal @503
	Z3_disable_literal @504
	Z3_block_literals @505
	Z3_get_model_num_constants @506
	Z3_get_model_constant @507
	Z3_get_model_num_funcs @508
	Z3_get_model_func_decl @509
	Z3_eval_func_decl @510
	Z3_is_array_value @511
	Z3_get_array_value @512
	Z3_get_model_func_else @513
	Z3_get_model_func_num_entries @514
	Z3_get_model_func_entry_num_args @515
	Z3_get_model_func_entry_arg @516
	Z3_get_model_func_entry_value @517
	Z3_eval @518
	Z3_eval_decl @519
	Z3_context_to_string @520
	Z3_statistics_to_string @521
	Z3_get_context_assignment @522
	Z3_mk_polynomial_manager @523
	Z3_del_polynomial_manager @524
	Z3_mk_zero_polynomial @525
	Z3_polynomial_inc_ref @526
	Z3_polynomial_dec_ref @527
	Z3_polynomial_to_string @528
