diff --git a/Microsoft.Z3/Native.cs b/Microsoft.Z3/Native.cs
index b923cce35..0c0349a78 100644
--- a/Microsoft.Z3/Native.cs
+++ b/Microsoft.Z3/Native.cs
@@ -1132,6 +1132,9 @@ namespace Microsoft.Z3
             [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
             public extern static IntPtr Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, uint a2);
 
+            [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
+            public extern static IntPtr Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1);
+
             [DllImport(Z3_DLL_NAME, CallingConvention = CallingConvention.Cdecl, CharSet = CharSet.Ansi)]
             public extern static void Z3_interrupt(Z3_context a0);
 
@@ -4293,6 +4296,14 @@ namespace Microsoft.Z3
             return r;
         }
 
+        public static string Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1) {
+            IntPtr r = LIB.Z3_param_descrs_to_string(a0, a1);
+            Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
+            if (err != Z3_error_code.Z3_OK)
+                throw new Z3Exception(Marshal.PtrToStringAnsi(LIB.Z3_get_error_msg_ex(a0, (uint)err)));
+            return Marshal.PtrToStringAnsi(r);
+        }
+
         public static void Z3_interrupt(Z3_context a0) {
             LIB.Z3_interrupt(a0);
             Z3_error_code err = (Z3_error_code)LIB.Z3_get_error_code(a0);
diff --git a/dll/z3.def b/dll/z3.def
index d56875d92..e65e8b225 100644
--- a/dll/z3.def
+++ b/dll/z3.def
@@ -25,497 +25,498 @@ EXPORTS
 	Z3_param_descrs_get_kind @23
 	Z3_param_descrs_size @24
 	Z3_param_descrs_get_name @25
-	Z3_mk_int_symbol @26
-	Z3_mk_string_symbol @27
-	Z3_mk_uninterpreted_sort @28
-	Z3_mk_bool_sort @29
-	Z3_mk_int_sort @30
-	Z3_mk_real_sort @31
-	Z3_mk_bv_sort @32
-	Z3_mk_finite_domain_sort @33
-	Z3_mk_array_sort @34
-	Z3_mk_tuple_sort @35
-	Z3_mk_enumeration_sort @36
-	Z3_mk_list_sort @37
-	Z3_mk_constructor @38
-	Z3_del_constructor @39
-	Z3_mk_datatype @40
-	Z3_mk_constructor_list @41
-	Z3_del_constructor_list @42
-	Z3_mk_datatypes @43
-	Z3_query_constructor @44
-	Z3_mk_func_decl @45
-	Z3_mk_app @46
-	Z3_mk_const @47
-	Z3_mk_fresh_func_decl @48
-	Z3_mk_fresh_const @49
-	Z3_mk_true @50
-	Z3_mk_false @51
-	Z3_mk_eq @52
-	Z3_mk_distinct @53
-	Z3_mk_not @54
-	Z3_mk_ite @55
-	Z3_mk_iff @56
-	Z3_mk_implies @57
-	Z3_mk_xor @58
-	Z3_mk_and @59
-	Z3_mk_or @60
-	Z3_mk_add @61
-	Z3_mk_mul @62
-	Z3_mk_sub @63
-	Z3_mk_unary_minus @64
-	Z3_mk_div @65
-	Z3_mk_mod @66
-	Z3_mk_rem @67
-	Z3_mk_power @68
-	Z3_mk_lt @69
-	Z3_mk_le @70
-	Z3_mk_gt @71
-	Z3_mk_ge @72
-	Z3_mk_int2real @73
-	Z3_mk_real2int @74
-	Z3_mk_is_int @75
-	Z3_mk_bvnot @76
-	Z3_mk_bvredand @77
-	Z3_mk_bvredor @78
-	Z3_mk_bvand @79
-	Z3_mk_bvor @80
-	Z3_mk_bvxor @81
-	Z3_mk_bvnand @82
-	Z3_mk_bvnor @83
-	Z3_mk_bvxnor @84
-	Z3_mk_bvneg @85
-	Z3_mk_bvadd @86
-	Z3_mk_bvsub @87
-	Z3_mk_bvmul @88
-	Z3_mk_bvudiv @89
-	Z3_mk_bvsdiv @90
-	Z3_mk_bvurem @91
-	Z3_mk_bvsrem @92
-	Z3_mk_bvsmod @93
-	Z3_mk_bvult @94
-	Z3_mk_bvslt @95
-	Z3_mk_bvule @96
-	Z3_mk_bvsle @97
-	Z3_mk_bvuge @98
-	Z3_mk_bvsge @99
-	Z3_mk_bvugt @100
-	Z3_mk_bvsgt @101
-	Z3_mk_concat @102
-	Z3_mk_extract @103
-	Z3_mk_sign_ext @104
-	Z3_mk_zero_ext @105
-	Z3_mk_repeat @106
-	Z3_mk_bvshl @107
-	Z3_mk_bvlshr @108
-	Z3_mk_bvashr @109
-	Z3_mk_rotate_left @110
-	Z3_mk_rotate_right @111
-	Z3_mk_ext_rotate_left @112
-	Z3_mk_ext_rotate_right @113
-	Z3_mk_int2bv @114
-	Z3_mk_bv2int @115
-	Z3_mk_bvadd_no_overflow @116
-	Z3_mk_bvadd_no_underflow @117
-	Z3_mk_bvsub_no_overflow @118
-	Z3_mk_bvsub_no_underflow @119
-	Z3_mk_bvsdiv_no_overflow @120
-	Z3_mk_bvneg_no_overflow @121
-	Z3_mk_bvmul_no_overflow @122
-	Z3_mk_bvmul_no_underflow @123
-	Z3_mk_select @124
-	Z3_mk_store @125
-	Z3_mk_const_array @126
-	Z3_mk_map @127
-	Z3_mk_array_default @128
-	Z3_mk_set_sort @129
-	Z3_mk_empty_set @130
-	Z3_mk_full_set @131
-	Z3_mk_set_add @132
-	Z3_mk_set_del @133
-	Z3_mk_set_union @134
-	Z3_mk_set_intersect @135
-	Z3_mk_set_difference @136
-	Z3_mk_set_complement @137
-	Z3_mk_set_member @138
-	Z3_mk_set_subset @139
-	Z3_mk_numeral @140
-	Z3_mk_real @141
-	Z3_mk_int @142
-	Z3_mk_unsigned_int @143
-	Z3_mk_int64 @144
-	Z3_mk_unsigned_int64 @145
-	Z3_mk_pattern @146
-	Z3_mk_bound @147
-	Z3_mk_forall @148
-	Z3_mk_exists @149
-	Z3_mk_quantifier @150
-	Z3_mk_quantifier_ex @151
-	Z3_mk_forall_const @152
-	Z3_mk_exists_const @153
-	Z3_mk_quantifier_const @154
-	Z3_mk_quantifier_const_ex @155
-	Z3_get_symbol_kind @156
-	Z3_get_symbol_int @157
-	Z3_get_symbol_string @158
-	Z3_get_sort_name @159
-	Z3_get_sort_id @160
-	Z3_sort_to_ast @161
-	Z3_is_eq_sort @162
-	Z3_get_sort_kind @163
-	Z3_get_bv_sort_size @164
-	Z3_get_finite_domain_sort_size @165
-	Z3_get_array_sort_domain @166
-	Z3_get_array_sort_range @167
-	Z3_get_tuple_sort_mk_decl @168
-	Z3_get_tuple_sort_num_fields @169
-	Z3_get_tuple_sort_field_decl @170
-	Z3_get_datatype_sort_num_constructors @171
-	Z3_get_datatype_sort_constructor @172
-	Z3_get_datatype_sort_recognizer @173
-	Z3_get_datatype_sort_constructor_accessor @174
-	Z3_get_relation_arity @175
-	Z3_get_relation_column @176
-	Z3_func_decl_to_ast @177
-	Z3_is_eq_func_decl @178
-	Z3_get_func_decl_id @179
-	Z3_get_decl_name @180
-	Z3_get_decl_kind @181
-	Z3_get_domain_size @182
-	Z3_get_arity @183
-	Z3_get_domain @184
-	Z3_get_range @185
-	Z3_get_decl_num_parameters @186
-	Z3_get_decl_parameter_kind @187
-	Z3_get_decl_int_parameter @188
-	Z3_get_decl_double_parameter @189
-	Z3_get_decl_symbol_parameter @190
-	Z3_get_decl_sort_parameter @191
-	Z3_get_decl_ast_parameter @192
-	Z3_get_decl_func_decl_parameter @193
-	Z3_get_decl_rational_parameter @194
-	Z3_app_to_ast @195
-	Z3_get_app_decl @196
-	Z3_get_app_num_args @197
-	Z3_get_app_arg @198
-	Z3_is_eq_ast @199
-	Z3_get_ast_id @200
-	Z3_get_ast_hash @201
-	Z3_get_sort @202
-	Z3_is_well_sorted @203
-	Z3_get_bool_value @204
-	Z3_get_ast_kind @205
-	Z3_is_app @206
-	Z3_is_numeral_ast @207
-	Z3_is_algebraic_number @208
-	Z3_to_app @209
-	Z3_to_func_decl @210
-	Z3_get_numeral_string @211
-	Z3_get_numeral_decimal_string @212
-	Z3_get_numerator @213
-	Z3_get_denominator @214
-	Z3_get_numeral_small @215
-	Z3_get_numeral_int @216
-	Z3_get_numeral_uint @217
-	Z3_get_numeral_uint64 @218
-	Z3_get_numeral_int64 @219
-	Z3_get_numeral_rational_int64 @220
-	Z3_get_algebraic_number_lower @221
-	Z3_get_algebraic_number_upper @222
-	Z3_pattern_to_ast @223
-	Z3_get_pattern_num_terms @224
-	Z3_get_pattern @225
-	Z3_get_index_value @226
-	Z3_is_quantifier_forall @227
-	Z3_get_quantifier_weight @228
-	Z3_get_quantifier_num_patterns @229
-	Z3_get_quantifier_pattern_ast @230
-	Z3_get_quantifier_num_no_patterns @231
-	Z3_get_quantifier_no_pattern_ast @232
-	Z3_get_quantifier_num_bound @233
-	Z3_get_quantifier_bound_name @234
-	Z3_get_quantifier_bound_sort @235
-	Z3_get_quantifier_body @236
-	Z3_simplify @237
-	Z3_simplify_ex @238
-	Z3_simplify_get_help @239
-	Z3_simplify_get_param_descrs @240
-	Z3_update_term @241
-	Z3_substitute @242
-	Z3_substitute_vars @243
-	Z3_translate @244
-	Z3_model_inc_ref @245
-	Z3_model_dec_ref @246
-	Z3_model_eval @247
-	Z3_model_get_const_interp @248
-	Z3_model_get_func_interp @249
-	Z3_model_get_num_consts @250
-	Z3_model_get_const_decl @251
-	Z3_model_get_num_funcs @252
-	Z3_model_get_func_decl @253
-	Z3_model_get_num_sorts @254
-	Z3_model_get_sort @255
-	Z3_model_get_sort_universe @256
-	Z3_is_as_array @257
-	Z3_get_as_array_func_decl @258
-	Z3_func_interp_inc_ref @259
-	Z3_func_interp_dec_ref @260
-	Z3_func_interp_get_num_entries @261
-	Z3_func_interp_get_entry @262
-	Z3_func_interp_get_else @263
-	Z3_func_interp_get_arity @264
-	Z3_func_entry_inc_ref @265
-	Z3_func_entry_dec_ref @266
-	Z3_func_entry_get_value @267
-	Z3_func_entry_get_num_args @268
-	Z3_func_entry_get_arg @269
-	Z3_open_log @270
-	Z3_append_log @271
-	Z3_close_log @272
-	Z3_toggle_warning_messages @273
-	Z3_set_ast_print_mode @274
-	Z3_ast_to_string @275
-	Z3_pattern_to_string @276
-	Z3_sort_to_string @277
-	Z3_func_decl_to_string @278
-	Z3_model_to_string @279
-	Z3_benchmark_to_smtlib_string @280
-	Z3_parse_smtlib2_string @281
-	Z3_parse_smtlib2_file @282
-	Z3_parse_smtlib_string @283
-	Z3_parse_smtlib_file @284
-	Z3_get_smtlib_num_formulas @285
-	Z3_get_smtlib_formula @286
-	Z3_get_smtlib_num_assumptions @287
-	Z3_get_smtlib_assumption @288
-	Z3_get_smtlib_num_decls @289
-	Z3_get_smtlib_decl @290
-	Z3_get_smtlib_num_sorts @291
-	Z3_get_smtlib_sort @292
-	Z3_get_smtlib_error @293
-	Z3_parse_z3_string @294
-	Z3_parse_z3_file @295
-	Z3_get_error_code @296
-	Z3_set_error_handler @297
-	Z3_set_error @298
-	Z3_get_error_msg @299
-	Z3_get_error_msg_ex @300
-	Z3_get_version @301
-	Z3_reset_memory @302
-	Z3_mk_theory @303
-	Z3_theory_get_ext_data @304
-	Z3_theory_mk_sort @305
-	Z3_theory_mk_value @306
-	Z3_theory_mk_constant @307
-	Z3_theory_mk_func_decl @308
-	Z3_theory_get_context @309
-	Z3_set_delete_callback @310
-	Z3_set_reduce_app_callback @311
-	Z3_set_reduce_eq_callback @312
-	Z3_set_reduce_distinct_callback @313
-	Z3_set_new_app_callback @314
-	Z3_set_new_elem_callback @315
-	Z3_set_init_search_callback @316
-	Z3_set_push_callback @317
-	Z3_set_pop_callback @318
-	Z3_set_restart_callback @319
-	Z3_set_reset_callback @320
-	Z3_set_final_check_callback @321
-	Z3_set_new_eq_callback @322
-	Z3_set_new_diseq_callback @323
-	Z3_set_new_assignment_callback @324
-	Z3_set_new_relevant_callback @325
-	Z3_theory_assert_axiom @326
-	Z3_theory_assume_eq @327
-	Z3_theory_enable_axiom_simplification @328
-	Z3_theory_get_eqc_root @329
-	Z3_theory_get_eqc_next @330
-	Z3_theory_get_num_parents @331
-	Z3_theory_get_parent @332
-	Z3_theory_is_value @333
-	Z3_theory_is_decl @334
-	Z3_theory_get_num_elems @335
-	Z3_theory_get_elem @336
-	Z3_theory_get_num_apps @337
-	Z3_theory_get_app @338
-	Z3_mk_fixedpoint @339
-	Z3_fixedpoint_inc_ref @340
-	Z3_fixedpoint_dec_ref @341
-	Z3_fixedpoint_add_rule @342
-	Z3_fixedpoint_add_fact @343
-	Z3_fixedpoint_assert @344
-	Z3_fixedpoint_query @345
-	Z3_fixedpoint_query_relations @346
-	Z3_fixedpoint_get_answer @347
-	Z3_fixedpoint_get_reason_unknown @348
-	Z3_fixedpoint_update_rule @349
-	Z3_fixedpoint_get_num_levels @350
-	Z3_fixedpoint_get_cover_delta @351
-	Z3_fixedpoint_add_cover @352
-	Z3_fixedpoint_get_statistics @353
-	Z3_fixedpoint_register_relation @354
-	Z3_fixedpoint_set_predicate_representation @355
-	Z3_fixedpoint_simplify_rules @356
-	Z3_fixedpoint_set_params @357
-	Z3_fixedpoint_get_help @358
-	Z3_fixedpoint_get_param_descrs @359
-	Z3_fixedpoint_to_string @360
-	Z3_fixedpoint_push @361
-	Z3_fixedpoint_pop @362
-	Z3_fixedpoint_init @363
-	Z3_fixedpoint_set_reduce_assign_callback @364
-	Z3_fixedpoint_set_reduce_app_callback @365
-	Z3_mk_ast_vector @366
-	Z3_ast_vector_inc_ref @367
-	Z3_ast_vector_dec_ref @368
-	Z3_ast_vector_size @369
-	Z3_ast_vector_get @370
-	Z3_ast_vector_set @371
-	Z3_ast_vector_resize @372
-	Z3_ast_vector_push @373
-	Z3_ast_vector_translate @374
-	Z3_ast_vector_to_string @375
-	Z3_mk_ast_map @376
-	Z3_ast_map_inc_ref @377
-	Z3_ast_map_dec_ref @378
-	Z3_ast_map_contains @379
-	Z3_ast_map_find @380
-	Z3_ast_map_insert @381
-	Z3_ast_map_erase @382
-	Z3_ast_map_reset @383
-	Z3_ast_map_size @384
-	Z3_ast_map_keys @385
-	Z3_ast_map_to_string @386
-	Z3_mk_goal @387
-	Z3_goal_inc_ref @388
-	Z3_goal_dec_ref @389
-	Z3_goal_precision @390
-	Z3_goal_assert @391
-	Z3_goal_inconsistent @392
-	Z3_goal_depth @393
-	Z3_goal_reset @394
-	Z3_goal_size @395
-	Z3_goal_formula @396
-	Z3_goal_num_exprs @397
-	Z3_goal_is_decided_sat @398
-	Z3_goal_is_decided_unsat @399
-	Z3_goal_translate @400
-	Z3_goal_to_string @401
-	Z3_mk_tactic @402
-	Z3_tactic_inc_ref @403
-	Z3_tactic_dec_ref @404
-	Z3_mk_probe @405
-	Z3_probe_inc_ref @406
-	Z3_probe_dec_ref @407
-	Z3_tactic_and_then @408
-	Z3_tactic_or_else @409
-	Z3_tactic_par_or @410
-	Z3_tactic_par_and_then @411
-	Z3_tactic_try_for @412
-	Z3_tactic_when @413
-	Z3_tactic_cond @414
-	Z3_tactic_repeat @415
-	Z3_tactic_skip @416
-	Z3_tactic_fail @417
-	Z3_tactic_fail_if @418
-	Z3_tactic_fail_if_not_decided @419
-	Z3_tactic_using_params @420
-	Z3_probe_const @421
-	Z3_probe_lt @422
-	Z3_probe_gt @423
-	Z3_probe_le @424
-	Z3_probe_ge @425
-	Z3_probe_eq @426
-	Z3_probe_and @427
-	Z3_probe_or @428
-	Z3_probe_not @429
-	Z3_get_num_tactics @430
-	Z3_get_tactic_name @431
-	Z3_get_num_probes @432
-	Z3_get_probe_name @433
-	Z3_tactic_get_help @434
-	Z3_tactic_get_param_descrs @435
-	Z3_tactic_get_descr @436
-	Z3_probe_get_descr @437
-	Z3_probe_apply @438
-	Z3_tactic_apply @439
-	Z3_tactic_apply_ex @440
-	Z3_apply_result_inc_ref @441
-	Z3_apply_result_dec_ref @442
-	Z3_apply_result_to_string @443
-	Z3_apply_result_get_num_subgoals @444
-	Z3_apply_result_get_subgoal @445
-	Z3_apply_result_convert_model @446
-	Z3_mk_solver @447
-	Z3_mk_simple_solver @448
-	Z3_mk_solver_for_logic @449
-	Z3_mk_solver_from_tactic @450
-	Z3_solver_get_help @451
-	Z3_solver_get_param_descrs @452
-	Z3_solver_set_params @453
-	Z3_solver_inc_ref @454
-	Z3_solver_dec_ref @455
-	Z3_solver_push @456
-	Z3_solver_pop @457
-	Z3_solver_reset @458
-	Z3_solver_get_num_scopes @459
-	Z3_solver_assert @460
-	Z3_solver_get_assertions @461
-	Z3_solver_check @462
-	Z3_solver_check_assumptions @463
-	Z3_solver_get_model @464
-	Z3_solver_get_proof @465
-	Z3_solver_get_unsat_core @466
-	Z3_solver_get_reason_unknown @467
-	Z3_solver_get_statistics @468
-	Z3_solver_to_string @469
-	Z3_stats_to_string @470
-	Z3_stats_inc_ref @471
-	Z3_stats_dec_ref @472
-	Z3_stats_size @473
-	Z3_stats_get_key @474
-	Z3_stats_is_uint @475
-	Z3_stats_is_double @476
-	Z3_stats_get_uint_value @477
-	Z3_stats_get_double_value @478
-	Z3_mk_injective_function @479
-	Z3_set_logic @480
-	Z3_push @481
-	Z3_pop @482
-	Z3_get_num_scopes @483
-	Z3_persist_ast @484
-	Z3_assert_cnstr @485
-	Z3_check_and_get_model @486
-	Z3_check @487
-	Z3_check_assumptions @488
-	Z3_get_implied_equalities @489
-	Z3_del_model @490
-	Z3_soft_check_cancel @491
-	Z3_get_search_failure @492
-	Z3_mk_label @493
-	Z3_get_relevant_labels @494
-	Z3_get_relevant_literals @495
-	Z3_get_guessed_literals @496
-	Z3_del_literals @497
-	Z3_get_num_literals @498
-	Z3_get_label_symbol @499
-	Z3_get_literal @500
-	Z3_disable_literal @501
-	Z3_block_literals @502
-	Z3_get_model_num_constants @503
-	Z3_get_model_constant @504
-	Z3_get_model_num_funcs @505
-	Z3_get_model_func_decl @506
-	Z3_eval_func_decl @507
-	Z3_is_array_value @508
-	Z3_get_array_value @509
-	Z3_get_model_func_else @510
-	Z3_get_model_func_num_entries @511
-	Z3_get_model_func_entry_num_args @512
-	Z3_get_model_func_entry_arg @513
-	Z3_get_model_func_entry_value @514
-	Z3_eval @515
-	Z3_eval_decl @516
-	Z3_context_to_string @517
-	Z3_statistics_to_string @518
-	Z3_get_context_assignment @519
+	Z3_param_descrs_to_string @26
+	Z3_mk_int_symbol @27
+	Z3_mk_string_symbol @28
+	Z3_mk_uninterpreted_sort @29
+	Z3_mk_bool_sort @30
+	Z3_mk_int_sort @31
+	Z3_mk_real_sort @32
+	Z3_mk_bv_sort @33
+	Z3_mk_finite_domain_sort @34
+	Z3_mk_array_sort @35
+	Z3_mk_tuple_sort @36
+	Z3_mk_enumeration_sort @37
+	Z3_mk_list_sort @38
+	Z3_mk_constructor @39
+	Z3_del_constructor @40
+	Z3_mk_datatype @41
+	Z3_mk_constructor_list @42
+	Z3_del_constructor_list @43
+	Z3_mk_datatypes @44
+	Z3_query_constructor @45
+	Z3_mk_func_decl @46
+	Z3_mk_app @47
+	Z3_mk_const @48
+	Z3_mk_fresh_func_decl @49
+	Z3_mk_fresh_const @50
+	Z3_mk_true @51
+	Z3_mk_false @52
+	Z3_mk_eq @53
+	Z3_mk_distinct @54
+	Z3_mk_not @55
+	Z3_mk_ite @56
+	Z3_mk_iff @57
+	Z3_mk_implies @58
+	Z3_mk_xor @59
+	Z3_mk_and @60
+	Z3_mk_or @61
+	Z3_mk_add @62
+	Z3_mk_mul @63
+	Z3_mk_sub @64
+	Z3_mk_unary_minus @65
+	Z3_mk_div @66
+	Z3_mk_mod @67
+	Z3_mk_rem @68
+	Z3_mk_power @69
+	Z3_mk_lt @70
+	Z3_mk_le @71
+	Z3_mk_gt @72
+	Z3_mk_ge @73
+	Z3_mk_int2real @74
+	Z3_mk_real2int @75
+	Z3_mk_is_int @76
+	Z3_mk_bvnot @77
+	Z3_mk_bvredand @78
+	Z3_mk_bvredor @79
+	Z3_mk_bvand @80
+	Z3_mk_bvor @81
+	Z3_mk_bvxor @82
+	Z3_mk_bvnand @83
+	Z3_mk_bvnor @84
+	Z3_mk_bvxnor @85
+	Z3_mk_bvneg @86
+	Z3_mk_bvadd @87
+	Z3_mk_bvsub @88
+	Z3_mk_bvmul @89
+	Z3_mk_bvudiv @90
+	Z3_mk_bvsdiv @91
+	Z3_mk_bvurem @92
+	Z3_mk_bvsrem @93
+	Z3_mk_bvsmod @94
+	Z3_mk_bvult @95
+	Z3_mk_bvslt @96
+	Z3_mk_bvule @97
+	Z3_mk_bvsle @98
+	Z3_mk_bvuge @99
+	Z3_mk_bvsge @100
+	Z3_mk_bvugt @101
+	Z3_mk_bvsgt @102
+	Z3_mk_concat @103
+	Z3_mk_extract @104
+	Z3_mk_sign_ext @105
+	Z3_mk_zero_ext @106
+	Z3_mk_repeat @107
+	Z3_mk_bvshl @108
+	Z3_mk_bvlshr @109
+	Z3_mk_bvashr @110
+	Z3_mk_rotate_left @111
+	Z3_mk_rotate_right @112
+	Z3_mk_ext_rotate_left @113
+	Z3_mk_ext_rotate_right @114
+	Z3_mk_int2bv @115
+	Z3_mk_bv2int @116
+	Z3_mk_bvadd_no_overflow @117
+	Z3_mk_bvadd_no_underflow @118
+	Z3_mk_bvsub_no_overflow @119
+	Z3_mk_bvsub_no_underflow @120
+	Z3_mk_bvsdiv_no_overflow @121
+	Z3_mk_bvneg_no_overflow @122
+	Z3_mk_bvmul_no_overflow @123
+	Z3_mk_bvmul_no_underflow @124
+	Z3_mk_select @125
+	Z3_mk_store @126
+	Z3_mk_const_array @127
+	Z3_mk_map @128
+	Z3_mk_array_default @129
+	Z3_mk_set_sort @130
+	Z3_mk_empty_set @131
+	Z3_mk_full_set @132
+	Z3_mk_set_add @133
+	Z3_mk_set_del @134
+	Z3_mk_set_union @135
+	Z3_mk_set_intersect @136
+	Z3_mk_set_difference @137
+	Z3_mk_set_complement @138
+	Z3_mk_set_member @139
+	Z3_mk_set_subset @140
+	Z3_mk_numeral @141
+	Z3_mk_real @142
+	Z3_mk_int @143
+	Z3_mk_unsigned_int @144
+	Z3_mk_int64 @145
+	Z3_mk_unsigned_int64 @146
+	Z3_mk_pattern @147
+	Z3_mk_bound @148
+	Z3_mk_forall @149
+	Z3_mk_exists @150
+	Z3_mk_quantifier @151
+	Z3_mk_quantifier_ex @152
+	Z3_mk_forall_const @153
+	Z3_mk_exists_const @154
+	Z3_mk_quantifier_const @155
+	Z3_mk_quantifier_const_ex @156
+	Z3_get_symbol_kind @157
+	Z3_get_symbol_int @158
+	Z3_get_symbol_string @159
+	Z3_get_sort_name @160
+	Z3_get_sort_id @161
+	Z3_sort_to_ast @162
+	Z3_is_eq_sort @163
+	Z3_get_sort_kind @164
+	Z3_get_bv_sort_size @165
+	Z3_get_finite_domain_sort_size @166
+	Z3_get_array_sort_domain @167
+	Z3_get_array_sort_range @168
+	Z3_get_tuple_sort_mk_decl @169
+	Z3_get_tuple_sort_num_fields @170
+	Z3_get_tuple_sort_field_decl @171
+	Z3_get_datatype_sort_num_constructors @172
+	Z3_get_datatype_sort_constructor @173
+	Z3_get_datatype_sort_recognizer @174
+	Z3_get_datatype_sort_constructor_accessor @175
+	Z3_get_relation_arity @176
+	Z3_get_relation_column @177
+	Z3_func_decl_to_ast @178
+	Z3_is_eq_func_decl @179
+	Z3_get_func_decl_id @180
+	Z3_get_decl_name @181
+	Z3_get_decl_kind @182
+	Z3_get_domain_size @183
+	Z3_get_arity @184
+	Z3_get_domain @185
+	Z3_get_range @186
+	Z3_get_decl_num_parameters @187
+	Z3_get_decl_parameter_kind @188
+	Z3_get_decl_int_parameter @189
+	Z3_get_decl_double_parameter @190
+	Z3_get_decl_symbol_parameter @191
+	Z3_get_decl_sort_parameter @192
+	Z3_get_decl_ast_parameter @193
+	Z3_get_decl_func_decl_parameter @194
+	Z3_get_decl_rational_parameter @195
+	Z3_app_to_ast @196
+	Z3_get_app_decl @197
+	Z3_get_app_num_args @198
+	Z3_get_app_arg @199
+	Z3_is_eq_ast @200
+	Z3_get_ast_id @201
+	Z3_get_ast_hash @202
+	Z3_get_sort @203
+	Z3_is_well_sorted @204
+	Z3_get_bool_value @205
+	Z3_get_ast_kind @206
+	Z3_is_app @207
+	Z3_is_numeral_ast @208
+	Z3_is_algebraic_number @209
+	Z3_to_app @210
+	Z3_to_func_decl @211
+	Z3_get_numeral_string @212
+	Z3_get_numeral_decimal_string @213
+	Z3_get_numerator @214
+	Z3_get_denominator @215
+	Z3_get_numeral_small @216
+	Z3_get_numeral_int @217
+	Z3_get_numeral_uint @218
+	Z3_get_numeral_uint64 @219
+	Z3_get_numeral_int64 @220
+	Z3_get_numeral_rational_int64 @221
+	Z3_get_algebraic_number_lower @222
+	Z3_get_algebraic_number_upper @223
+	Z3_pattern_to_ast @224
+	Z3_get_pattern_num_terms @225
+	Z3_get_pattern @226
+	Z3_get_index_value @227
+	Z3_is_quantifier_forall @228
+	Z3_get_quantifier_weight @229
+	Z3_get_quantifier_num_patterns @230
+	Z3_get_quantifier_pattern_ast @231
+	Z3_get_quantifier_num_no_patterns @232
+	Z3_get_quantifier_no_pattern_ast @233
+	Z3_get_quantifier_num_bound @234
+	Z3_get_quantifier_bound_name @235
+	Z3_get_quantifier_bound_sort @236
+	Z3_get_quantifier_body @237
+	Z3_simplify @238
+	Z3_simplify_ex @239
+	Z3_simplify_get_help @240
+	Z3_simplify_get_param_descrs @241
+	Z3_update_term @242
+	Z3_substitute @243
+	Z3_substitute_vars @244
+	Z3_translate @245
+	Z3_model_inc_ref @246
+	Z3_model_dec_ref @247
+	Z3_model_eval @248
+	Z3_model_get_const_interp @249
+	Z3_model_get_func_interp @250
+	Z3_model_get_num_consts @251
+	Z3_model_get_const_decl @252
+	Z3_model_get_num_funcs @253
+	Z3_model_get_func_decl @254
+	Z3_model_get_num_sorts @255
+	Z3_model_get_sort @256
+	Z3_model_get_sort_universe @257
+	Z3_is_as_array @258
+	Z3_get_as_array_func_decl @259
+	Z3_func_interp_inc_ref @260
+	Z3_func_interp_dec_ref @261
+	Z3_func_interp_get_num_entries @262
+	Z3_func_interp_get_entry @263
+	Z3_func_interp_get_else @264
+	Z3_func_interp_get_arity @265
+	Z3_func_entry_inc_ref @266
+	Z3_func_entry_dec_ref @267
+	Z3_func_entry_get_value @268
+	Z3_func_entry_get_num_args @269
+	Z3_func_entry_get_arg @270
+	Z3_open_log @271
+	Z3_append_log @272
+	Z3_close_log @273
+	Z3_toggle_warning_messages @274
+	Z3_set_ast_print_mode @275
+	Z3_ast_to_string @276
+	Z3_pattern_to_string @277
+	Z3_sort_to_string @278
+	Z3_func_decl_to_string @279
+	Z3_model_to_string @280
+	Z3_benchmark_to_smtlib_string @281
+	Z3_parse_smtlib2_string @282
+	Z3_parse_smtlib2_file @283
+	Z3_parse_smtlib_string @284
+	Z3_parse_smtlib_file @285
+	Z3_get_smtlib_num_formulas @286
+	Z3_get_smtlib_formula @287
+	Z3_get_smtlib_num_assumptions @288
+	Z3_get_smtlib_assumption @289
+	Z3_get_smtlib_num_decls @290
+	Z3_get_smtlib_decl @291
+	Z3_get_smtlib_num_sorts @292
+	Z3_get_smtlib_sort @293
+	Z3_get_smtlib_error @294
+	Z3_parse_z3_string @295
+	Z3_parse_z3_file @296
+	Z3_get_error_code @297
+	Z3_set_error_handler @298
+	Z3_set_error @299
+	Z3_get_error_msg @300
+	Z3_get_error_msg_ex @301
+	Z3_get_version @302
+	Z3_reset_memory @303
+	Z3_mk_theory @304
+	Z3_theory_get_ext_data @305
+	Z3_theory_mk_sort @306
+	Z3_theory_mk_value @307
+	Z3_theory_mk_constant @308
+	Z3_theory_mk_func_decl @309
+	Z3_theory_get_context @310
+	Z3_set_delete_callback @311
+	Z3_set_reduce_app_callback @312
+	Z3_set_reduce_eq_callback @313
+	Z3_set_reduce_distinct_callback @314
+	Z3_set_new_app_callback @315
+	Z3_set_new_elem_callback @316
+	Z3_set_init_search_callback @317
+	Z3_set_push_callback @318
+	Z3_set_pop_callback @319
+	Z3_set_restart_callback @320
+	Z3_set_reset_callback @321
+	Z3_set_final_check_callback @322
+	Z3_set_new_eq_callback @323
+	Z3_set_new_diseq_callback @324
+	Z3_set_new_assignment_callback @325
+	Z3_set_new_relevant_callback @326
+	Z3_theory_assert_axiom @327
+	Z3_theory_assume_eq @328
+	Z3_theory_enable_axiom_simplification @329
+	Z3_theory_get_eqc_root @330
+	Z3_theory_get_eqc_next @331
+	Z3_theory_get_num_parents @332
+	Z3_theory_get_parent @333
+	Z3_theory_is_value @334
+	Z3_theory_is_decl @335
+	Z3_theory_get_num_elems @336
+	Z3_theory_get_elem @337
+	Z3_theory_get_num_apps @338
+	Z3_theory_get_app @339
+	Z3_mk_fixedpoint @340
+	Z3_fixedpoint_inc_ref @341
+	Z3_fixedpoint_dec_ref @342
+	Z3_fixedpoint_add_rule @343
+	Z3_fixedpoint_add_fact @344
+	Z3_fixedpoint_assert @345
+	Z3_fixedpoint_query @346
+	Z3_fixedpoint_query_relations @347
+	Z3_fixedpoint_get_answer @348
+	Z3_fixedpoint_get_reason_unknown @349
+	Z3_fixedpoint_update_rule @350
+	Z3_fixedpoint_get_num_levels @351
+	Z3_fixedpoint_get_cover_delta @352
+	Z3_fixedpoint_add_cover @353
+	Z3_fixedpoint_get_statistics @354
+	Z3_fixedpoint_register_relation @355
+	Z3_fixedpoint_set_predicate_representation @356
+	Z3_fixedpoint_simplify_rules @357
+	Z3_fixedpoint_set_params @358
+	Z3_fixedpoint_get_help @359
+	Z3_fixedpoint_get_param_descrs @360
+	Z3_fixedpoint_to_string @361
+	Z3_fixedpoint_push @362
+	Z3_fixedpoint_pop @363
+	Z3_fixedpoint_init @364
+	Z3_fixedpoint_set_reduce_assign_callback @365
+	Z3_fixedpoint_set_reduce_app_callback @366
+	Z3_mk_ast_vector @367
+	Z3_ast_vector_inc_ref @368
+	Z3_ast_vector_dec_ref @369
+	Z3_ast_vector_size @370
+	Z3_ast_vector_get @371
+	Z3_ast_vector_set @372
+	Z3_ast_vector_resize @373
+	Z3_ast_vector_push @374
+	Z3_ast_vector_translate @375
+	Z3_ast_vector_to_string @376
+	Z3_mk_ast_map @377
+	Z3_ast_map_inc_ref @378
+	Z3_ast_map_dec_ref @379
+	Z3_ast_map_contains @380
+	Z3_ast_map_find @381
+	Z3_ast_map_insert @382
+	Z3_ast_map_erase @383
+	Z3_ast_map_reset @384
+	Z3_ast_map_size @385
+	Z3_ast_map_keys @386
+	Z3_ast_map_to_string @387
+	Z3_mk_goal @388
+	Z3_goal_inc_ref @389
+	Z3_goal_dec_ref @390
+	Z3_goal_precision @391
+	Z3_goal_assert @392
+	Z3_goal_inconsistent @393
+	Z3_goal_depth @394
+	Z3_goal_reset @395
+	Z3_goal_size @396
+	Z3_goal_formula @397
+	Z3_goal_num_exprs @398
+	Z3_goal_is_decided_sat @399
+	Z3_goal_is_decided_unsat @400
+	Z3_goal_translate @401
+	Z3_goal_to_string @402
+	Z3_mk_tactic @403
+	Z3_tactic_inc_ref @404
+	Z3_tactic_dec_ref @405
+	Z3_mk_probe @406
+	Z3_probe_inc_ref @407
+	Z3_probe_dec_ref @408
+	Z3_tactic_and_then @409
+	Z3_tactic_or_else @410
+	Z3_tactic_par_or @411
+	Z3_tactic_par_and_then @412
+	Z3_tactic_try_for @413
+	Z3_tactic_when @414
+	Z3_tactic_cond @415
+	Z3_tactic_repeat @416
+	Z3_tactic_skip @417
+	Z3_tactic_fail @418
+	Z3_tactic_fail_if @419
+	Z3_tactic_fail_if_not_decided @420
+	Z3_tactic_using_params @421
+	Z3_probe_const @422
+	Z3_probe_lt @423
+	Z3_probe_gt @424
+	Z3_probe_le @425
+	Z3_probe_ge @426
+	Z3_probe_eq @427
+	Z3_probe_and @428
+	Z3_probe_or @429
+	Z3_probe_not @430
+	Z3_get_num_tactics @431
+	Z3_get_tactic_name @432
+	Z3_get_num_probes @433
+	Z3_get_probe_name @434
+	Z3_tactic_get_help @435
+	Z3_tactic_get_param_descrs @436
+	Z3_tactic_get_descr @437
+	Z3_probe_get_descr @438
+	Z3_probe_apply @439
+	Z3_tactic_apply @440
+	Z3_tactic_apply_ex @441
+	Z3_apply_result_inc_ref @442
+	Z3_apply_result_dec_ref @443
+	Z3_apply_result_to_string @444
+	Z3_apply_result_get_num_subgoals @445
+	Z3_apply_result_get_subgoal @446
+	Z3_apply_result_convert_model @447
+	Z3_mk_solver @448
+	Z3_mk_simple_solver @449
+	Z3_mk_solver_for_logic @450
+	Z3_mk_solver_from_tactic @451
+	Z3_solver_get_help @452
+	Z3_solver_get_param_descrs @453
+	Z3_solver_set_params @454
+	Z3_solver_inc_ref @455
+	Z3_solver_dec_ref @456
+	Z3_solver_push @457
+	Z3_solver_pop @458
+	Z3_solver_reset @459
+	Z3_solver_get_num_scopes @460
+	Z3_solver_assert @461
+	Z3_solver_get_assertions @462
+	Z3_solver_check @463
+	Z3_solver_check_assumptions @464
+	Z3_solver_get_model @465
+	Z3_solver_get_proof @466
+	Z3_solver_get_unsat_core @467
+	Z3_solver_get_reason_unknown @468
+	Z3_solver_get_statistics @469
+	Z3_solver_to_string @470
+	Z3_stats_to_string @471
+	Z3_stats_inc_ref @472
+	Z3_stats_dec_ref @473
+	Z3_stats_size @474
+	Z3_stats_get_key @475
+	Z3_stats_is_uint @476
+	Z3_stats_is_double @477
+	Z3_stats_get_uint_value @478
+	Z3_stats_get_double_value @479
+	Z3_mk_injective_function @480
+	Z3_set_logic @481
+	Z3_push @482
+	Z3_pop @483
+	Z3_get_num_scopes @484
+	Z3_persist_ast @485
+	Z3_assert_cnstr @486
+	Z3_check_and_get_model @487
+	Z3_check @488
+	Z3_check_assumptions @489
+	Z3_get_implied_equalities @490
+	Z3_del_model @491
+	Z3_soft_check_cancel @492
+	Z3_get_search_failure @493
+	Z3_mk_label @494
+	Z3_get_relevant_labels @495
+	Z3_get_relevant_literals @496
+	Z3_get_guessed_literals @497
+	Z3_del_literals @498
+	Z3_get_num_literals @499
+	Z3_get_label_symbol @500
+	Z3_get_literal @501
+	Z3_disable_literal @502
+	Z3_block_literals @503
+	Z3_get_model_num_constants @504
+	Z3_get_model_constant @505
+	Z3_get_model_num_funcs @506
+	Z3_get_model_func_decl @507
+	Z3_eval_func_decl @508
+	Z3_is_array_value @509
+	Z3_get_array_value @510
+	Z3_get_model_func_else @511
+	Z3_get_model_func_num_entries @512
+	Z3_get_model_func_entry_num_args @513
+	Z3_get_model_func_entry_arg @514
+	Z3_get_model_func_entry_value @515
+	Z3_eval @516
+	Z3_eval_decl @517
+	Z3_context_to_string @518
+	Z3_statistics_to_string @519
+	Z3_get_context_assignment @520
diff --git a/dll/z3_dbg.def b/dll/z3_dbg.def
index 0c830c94e..e74292bd3 100644
--- a/dll/z3_dbg.def
+++ b/dll/z3_dbg.def
@@ -25,497 +25,498 @@ EXPORTS
 	Z3_param_descrs_get_kind @23
 	Z3_param_descrs_size @24
 	Z3_param_descrs_get_name @25
-	Z3_mk_int_symbol @26
-	Z3_mk_string_symbol @27
-	Z3_mk_uninterpreted_sort @28
-	Z3_mk_bool_sort @29
-	Z3_mk_int_sort @30
-	Z3_mk_real_sort @31
-	Z3_mk_bv_sort @32
-	Z3_mk_finite_domain_sort @33
-	Z3_mk_array_sort @34
-	Z3_mk_tuple_sort @35
-	Z3_mk_enumeration_sort @36
-	Z3_mk_list_sort @37
-	Z3_mk_constructor @38
-	Z3_del_constructor @39
-	Z3_mk_datatype @40
-	Z3_mk_constructor_list @41
-	Z3_del_constructor_list @42
-	Z3_mk_datatypes @43
-	Z3_query_constructor @44
-	Z3_mk_func_decl @45
-	Z3_mk_app @46
-	Z3_mk_const @47
-	Z3_mk_fresh_func_decl @48
-	Z3_mk_fresh_const @49
-	Z3_mk_true @50
-	Z3_mk_false @51
-	Z3_mk_eq @52
-	Z3_mk_distinct @53
-	Z3_mk_not @54
-	Z3_mk_ite @55
-	Z3_mk_iff @56
-	Z3_mk_implies @57
-	Z3_mk_xor @58
-	Z3_mk_and @59
-	Z3_mk_or @60
-	Z3_mk_add @61
-	Z3_mk_mul @62
-	Z3_mk_sub @63
-	Z3_mk_unary_minus @64
-	Z3_mk_div @65
-	Z3_mk_mod @66
-	Z3_mk_rem @67
-	Z3_mk_power @68
-	Z3_mk_lt @69
-	Z3_mk_le @70
-	Z3_mk_gt @71
-	Z3_mk_ge @72
-	Z3_mk_int2real @73
-	Z3_mk_real2int @74
-	Z3_mk_is_int @75
-	Z3_mk_bvnot @76
-	Z3_mk_bvredand @77
-	Z3_mk_bvredor @78
-	Z3_mk_bvand @79
-	Z3_mk_bvor @80
-	Z3_mk_bvxor @81
-	Z3_mk_bvnand @82
-	Z3_mk_bvnor @83
-	Z3_mk_bvxnor @84
-	Z3_mk_bvneg @85
-	Z3_mk_bvadd @86
-	Z3_mk_bvsub @87
-	Z3_mk_bvmul @88
-	Z3_mk_bvudiv @89
-	Z3_mk_bvsdiv @90
-	Z3_mk_bvurem @91
-	Z3_mk_bvsrem @92
-	Z3_mk_bvsmod @93
-	Z3_mk_bvult @94
-	Z3_mk_bvslt @95
-	Z3_mk_bvule @96
-	Z3_mk_bvsle @97
-	Z3_mk_bvuge @98
-	Z3_mk_bvsge @99
-	Z3_mk_bvugt @100
-	Z3_mk_bvsgt @101
-	Z3_mk_concat @102
-	Z3_mk_extract @103
-	Z3_mk_sign_ext @104
-	Z3_mk_zero_ext @105
-	Z3_mk_repeat @106
-	Z3_mk_bvshl @107
-	Z3_mk_bvlshr @108
-	Z3_mk_bvashr @109
-	Z3_mk_rotate_left @110
-	Z3_mk_rotate_right @111
-	Z3_mk_ext_rotate_left @112
-	Z3_mk_ext_rotate_right @113
-	Z3_mk_int2bv @114
-	Z3_mk_bv2int @115
-	Z3_mk_bvadd_no_overflow @116
-	Z3_mk_bvadd_no_underflow @117
-	Z3_mk_bvsub_no_overflow @118
-	Z3_mk_bvsub_no_underflow @119
-	Z3_mk_bvsdiv_no_overflow @120
-	Z3_mk_bvneg_no_overflow @121
-	Z3_mk_bvmul_no_overflow @122
-	Z3_mk_bvmul_no_underflow @123
-	Z3_mk_select @124
-	Z3_mk_store @125
-	Z3_mk_const_array @126
-	Z3_mk_map @127
-	Z3_mk_array_default @128
-	Z3_mk_set_sort @129
-	Z3_mk_empty_set @130
-	Z3_mk_full_set @131
-	Z3_mk_set_add @132
-	Z3_mk_set_del @133
-	Z3_mk_set_union @134
-	Z3_mk_set_intersect @135
-	Z3_mk_set_difference @136
-	Z3_mk_set_complement @137
-	Z3_mk_set_member @138
-	Z3_mk_set_subset @139
-	Z3_mk_numeral @140
-	Z3_mk_real @141
-	Z3_mk_int @142
-	Z3_mk_unsigned_int @143
-	Z3_mk_int64 @144
-	Z3_mk_unsigned_int64 @145
-	Z3_mk_pattern @146
-	Z3_mk_bound @147
-	Z3_mk_forall @148
-	Z3_mk_exists @149
-	Z3_mk_quantifier @150
-	Z3_mk_quantifier_ex @151
-	Z3_mk_forall_const @152
-	Z3_mk_exists_const @153
-	Z3_mk_quantifier_const @154
-	Z3_mk_quantifier_const_ex @155
-	Z3_get_symbol_kind @156
-	Z3_get_symbol_int @157
-	Z3_get_symbol_string @158
-	Z3_get_sort_name @159
-	Z3_get_sort_id @160
-	Z3_sort_to_ast @161
-	Z3_is_eq_sort @162
-	Z3_get_sort_kind @163
-	Z3_get_bv_sort_size @164
-	Z3_get_finite_domain_sort_size @165
-	Z3_get_array_sort_domain @166
-	Z3_get_array_sort_range @167
-	Z3_get_tuple_sort_mk_decl @168
-	Z3_get_tuple_sort_num_fields @169
-	Z3_get_tuple_sort_field_decl @170
-	Z3_get_datatype_sort_num_constructors @171
-	Z3_get_datatype_sort_constructor @172
-	Z3_get_datatype_sort_recognizer @173
-	Z3_get_datatype_sort_constructor_accessor @174
-	Z3_get_relation_arity @175
-	Z3_get_relation_column @176
-	Z3_func_decl_to_ast @177
-	Z3_is_eq_func_decl @178
-	Z3_get_func_decl_id @179
-	Z3_get_decl_name @180
-	Z3_get_decl_kind @181
-	Z3_get_domain_size @182
-	Z3_get_arity @183
-	Z3_get_domain @184
-	Z3_get_range @185
-	Z3_get_decl_num_parameters @186
-	Z3_get_decl_parameter_kind @187
-	Z3_get_decl_int_parameter @188
-	Z3_get_decl_double_parameter @189
-	Z3_get_decl_symbol_parameter @190
-	Z3_get_decl_sort_parameter @191
-	Z3_get_decl_ast_parameter @192
-	Z3_get_decl_func_decl_parameter @193
-	Z3_get_decl_rational_parameter @194
-	Z3_app_to_ast @195
-	Z3_get_app_decl @196
-	Z3_get_app_num_args @197
-	Z3_get_app_arg @198
-	Z3_is_eq_ast @199
-	Z3_get_ast_id @200
-	Z3_get_ast_hash @201
-	Z3_get_sort @202
-	Z3_is_well_sorted @203
-	Z3_get_bool_value @204
-	Z3_get_ast_kind @205
-	Z3_is_app @206
-	Z3_is_numeral_ast @207
-	Z3_is_algebraic_number @208
-	Z3_to_app @209
-	Z3_to_func_decl @210
-	Z3_get_numeral_string @211
-	Z3_get_numeral_decimal_string @212
-	Z3_get_numerator @213
-	Z3_get_denominator @214
-	Z3_get_numeral_small @215
-	Z3_get_numeral_int @216
-	Z3_get_numeral_uint @217
-	Z3_get_numeral_uint64 @218
-	Z3_get_numeral_int64 @219
-	Z3_get_numeral_rational_int64 @220
-	Z3_get_algebraic_number_lower @221
-	Z3_get_algebraic_number_upper @222
-	Z3_pattern_to_ast @223
-	Z3_get_pattern_num_terms @224
-	Z3_get_pattern @225
-	Z3_get_index_value @226
-	Z3_is_quantifier_forall @227
-	Z3_get_quantifier_weight @228
-	Z3_get_quantifier_num_patterns @229
-	Z3_get_quantifier_pattern_ast @230
-	Z3_get_quantifier_num_no_patterns @231
-	Z3_get_quantifier_no_pattern_ast @232
-	Z3_get_quantifier_num_bound @233
-	Z3_get_quantifier_bound_name @234
-	Z3_get_quantifier_bound_sort @235
-	Z3_get_quantifier_body @236
-	Z3_simplify @237
-	Z3_simplify_ex @238
-	Z3_simplify_get_help @239
-	Z3_simplify_get_param_descrs @240
-	Z3_update_term @241
-	Z3_substitute @242
-	Z3_substitute_vars @243
-	Z3_translate @244
-	Z3_model_inc_ref @245
-	Z3_model_dec_ref @246
-	Z3_model_eval @247
-	Z3_model_get_const_interp @248
-	Z3_model_get_func_interp @249
-	Z3_model_get_num_consts @250
-	Z3_model_get_const_decl @251
-	Z3_model_get_num_funcs @252
-	Z3_model_get_func_decl @253
-	Z3_model_get_num_sorts @254
-	Z3_model_get_sort @255
-	Z3_model_get_sort_universe @256
-	Z3_is_as_array @257
-	Z3_get_as_array_func_decl @258
-	Z3_func_interp_inc_ref @259
-	Z3_func_interp_dec_ref @260
-	Z3_func_interp_get_num_entries @261
-	Z3_func_interp_get_entry @262
-	Z3_func_interp_get_else @263
-	Z3_func_interp_get_arity @264
-	Z3_func_entry_inc_ref @265
-	Z3_func_entry_dec_ref @266
-	Z3_func_entry_get_value @267
-	Z3_func_entry_get_num_args @268
-	Z3_func_entry_get_arg @269
-	Z3_open_log @270
-	Z3_append_log @271
-	Z3_close_log @272
-	Z3_toggle_warning_messages @273
-	Z3_set_ast_print_mode @274
-	Z3_ast_to_string @275
-	Z3_pattern_to_string @276
-	Z3_sort_to_string @277
-	Z3_func_decl_to_string @278
-	Z3_model_to_string @279
-	Z3_benchmark_to_smtlib_string @280
-	Z3_parse_smtlib2_string @281
-	Z3_parse_smtlib2_file @282
-	Z3_parse_smtlib_string @283
-	Z3_parse_smtlib_file @284
-	Z3_get_smtlib_num_formulas @285
-	Z3_get_smtlib_formula @286
-	Z3_get_smtlib_num_assumptions @287
-	Z3_get_smtlib_assumption @288
-	Z3_get_smtlib_num_decls @289
-	Z3_get_smtlib_decl @290
-	Z3_get_smtlib_num_sorts @291
-	Z3_get_smtlib_sort @292
-	Z3_get_smtlib_error @293
-	Z3_parse_z3_string @294
-	Z3_parse_z3_file @295
-	Z3_get_error_code @296
-	Z3_set_error_handler @297
-	Z3_set_error @298
-	Z3_get_error_msg @299
-	Z3_get_error_msg_ex @300
-	Z3_get_version @301
-	Z3_reset_memory @302
-	Z3_mk_theory @303
-	Z3_theory_get_ext_data @304
-	Z3_theory_mk_sort @305
-	Z3_theory_mk_value @306
-	Z3_theory_mk_constant @307
-	Z3_theory_mk_func_decl @308
-	Z3_theory_get_context @309
-	Z3_set_delete_callback @310
-	Z3_set_reduce_app_callback @311
-	Z3_set_reduce_eq_callback @312
-	Z3_set_reduce_distinct_callback @313
-	Z3_set_new_app_callback @314
-	Z3_set_new_elem_callback @315
-	Z3_set_init_search_callback @316
-	Z3_set_push_callback @317
-	Z3_set_pop_callback @318
-	Z3_set_restart_callback @319
-	Z3_set_reset_callback @320
-	Z3_set_final_check_callback @321
-	Z3_set_new_eq_callback @322
-	Z3_set_new_diseq_callback @323
-	Z3_set_new_assignment_callback @324
-	Z3_set_new_relevant_callback @325
-	Z3_theory_assert_axiom @326
-	Z3_theory_assume_eq @327
-	Z3_theory_enable_axiom_simplification @328
-	Z3_theory_get_eqc_root @329
-	Z3_theory_get_eqc_next @330
-	Z3_theory_get_num_parents @331
-	Z3_theory_get_parent @332
-	Z3_theory_is_value @333
-	Z3_theory_is_decl @334
-	Z3_theory_get_num_elems @335
-	Z3_theory_get_elem @336
-	Z3_theory_get_num_apps @337
-	Z3_theory_get_app @338
-	Z3_mk_fixedpoint @339
-	Z3_fixedpoint_inc_ref @340
-	Z3_fixedpoint_dec_ref @341
-	Z3_fixedpoint_add_rule @342
-	Z3_fixedpoint_add_fact @343
-	Z3_fixedpoint_assert @344
-	Z3_fixedpoint_query @345
-	Z3_fixedpoint_query_relations @346
-	Z3_fixedpoint_get_answer @347
-	Z3_fixedpoint_get_reason_unknown @348
-	Z3_fixedpoint_update_rule @349
-	Z3_fixedpoint_get_num_levels @350
-	Z3_fixedpoint_get_cover_delta @351
-	Z3_fixedpoint_add_cover @352
-	Z3_fixedpoint_get_statistics @353
-	Z3_fixedpoint_register_relation @354
-	Z3_fixedpoint_set_predicate_representation @355
-	Z3_fixedpoint_simplify_rules @356
-	Z3_fixedpoint_set_params @357
-	Z3_fixedpoint_get_help @358
-	Z3_fixedpoint_get_param_descrs @359
-	Z3_fixedpoint_to_string @360
-	Z3_fixedpoint_push @361
-	Z3_fixedpoint_pop @362
-	Z3_fixedpoint_init @363
-	Z3_fixedpoint_set_reduce_assign_callback @364
-	Z3_fixedpoint_set_reduce_app_callback @365
-	Z3_mk_ast_vector @366
-	Z3_ast_vector_inc_ref @367
-	Z3_ast_vector_dec_ref @368
-	Z3_ast_vector_size @369
-	Z3_ast_vector_get @370
-	Z3_ast_vector_set @371
-	Z3_ast_vector_resize @372
-	Z3_ast_vector_push @373
-	Z3_ast_vector_translate @374
-	Z3_ast_vector_to_string @375
-	Z3_mk_ast_map @376
-	Z3_ast_map_inc_ref @377
-	Z3_ast_map_dec_ref @378
-	Z3_ast_map_contains @379
-	Z3_ast_map_find @380
-	Z3_ast_map_insert @381
-	Z3_ast_map_erase @382
-	Z3_ast_map_reset @383
-	Z3_ast_map_size @384
-	Z3_ast_map_keys @385
-	Z3_ast_map_to_string @386
-	Z3_mk_goal @387
-	Z3_goal_inc_ref @388
-	Z3_goal_dec_ref @389
-	Z3_goal_precision @390
-	Z3_goal_assert @391
-	Z3_goal_inconsistent @392
-	Z3_goal_depth @393
-	Z3_goal_reset @394
-	Z3_goal_size @395
-	Z3_goal_formula @396
-	Z3_goal_num_exprs @397
-	Z3_goal_is_decided_sat @398
-	Z3_goal_is_decided_unsat @399
-	Z3_goal_translate @400
-	Z3_goal_to_string @401
-	Z3_mk_tactic @402
-	Z3_tactic_inc_ref @403
-	Z3_tactic_dec_ref @404
-	Z3_mk_probe @405
-	Z3_probe_inc_ref @406
-	Z3_probe_dec_ref @407
-	Z3_tactic_and_then @408
-	Z3_tactic_or_else @409
-	Z3_tactic_par_or @410
-	Z3_tactic_par_and_then @411
-	Z3_tactic_try_for @412
-	Z3_tactic_when @413
-	Z3_tactic_cond @414
-	Z3_tactic_repeat @415
-	Z3_tactic_skip @416
-	Z3_tactic_fail @417
-	Z3_tactic_fail_if @418
-	Z3_tactic_fail_if_not_decided @419
-	Z3_tactic_using_params @420
-	Z3_probe_const @421
-	Z3_probe_lt @422
-	Z3_probe_gt @423
-	Z3_probe_le @424
-	Z3_probe_ge @425
-	Z3_probe_eq @426
-	Z3_probe_and @427
-	Z3_probe_or @428
-	Z3_probe_not @429
-	Z3_get_num_tactics @430
-	Z3_get_tactic_name @431
-	Z3_get_num_probes @432
-	Z3_get_probe_name @433
-	Z3_tactic_get_help @434
-	Z3_tactic_get_param_descrs @435
-	Z3_tactic_get_descr @436
-	Z3_probe_get_descr @437
-	Z3_probe_apply @438
-	Z3_tactic_apply @439
-	Z3_tactic_apply_ex @440
-	Z3_apply_result_inc_ref @441
-	Z3_apply_result_dec_ref @442
-	Z3_apply_result_to_string @443
-	Z3_apply_result_get_num_subgoals @444
-	Z3_apply_result_get_subgoal @445
-	Z3_apply_result_convert_model @446
-	Z3_mk_solver @447
-	Z3_mk_simple_solver @448
-	Z3_mk_solver_for_logic @449
-	Z3_mk_solver_from_tactic @450
-	Z3_solver_get_help @451
-	Z3_solver_get_param_descrs @452
-	Z3_solver_set_params @453
-	Z3_solver_inc_ref @454
-	Z3_solver_dec_ref @455
-	Z3_solver_push @456
-	Z3_solver_pop @457
-	Z3_solver_reset @458
-	Z3_solver_get_num_scopes @459
-	Z3_solver_assert @460
-	Z3_solver_get_assertions @461
-	Z3_solver_check @462
-	Z3_solver_check_assumptions @463
-	Z3_solver_get_model @464
-	Z3_solver_get_proof @465
-	Z3_solver_get_unsat_core @466
-	Z3_solver_get_reason_unknown @467
-	Z3_solver_get_statistics @468
-	Z3_solver_to_string @469
-	Z3_stats_to_string @470
-	Z3_stats_inc_ref @471
-	Z3_stats_dec_ref @472
-	Z3_stats_size @473
-	Z3_stats_get_key @474
-	Z3_stats_is_uint @475
-	Z3_stats_is_double @476
-	Z3_stats_get_uint_value @477
-	Z3_stats_get_double_value @478
-	Z3_mk_injective_function @479
-	Z3_set_logic @480
-	Z3_push @481
-	Z3_pop @482
-	Z3_get_num_scopes @483
-	Z3_persist_ast @484
-	Z3_assert_cnstr @485
-	Z3_check_and_get_model @486
-	Z3_check @487
-	Z3_check_assumptions @488
-	Z3_get_implied_equalities @489
-	Z3_del_model @490
-	Z3_soft_check_cancel @491
-	Z3_get_search_failure @492
-	Z3_mk_label @493
-	Z3_get_relevant_labels @494
-	Z3_get_relevant_literals @495
-	Z3_get_guessed_literals @496
-	Z3_del_literals @497
-	Z3_get_num_literals @498
-	Z3_get_label_symbol @499
-	Z3_get_literal @500
-	Z3_disable_literal @501
-	Z3_block_literals @502
-	Z3_get_model_num_constants @503
-	Z3_get_model_constant @504
-	Z3_get_model_num_funcs @505
-	Z3_get_model_func_decl @506
-	Z3_eval_func_decl @507
-	Z3_is_array_value @508
-	Z3_get_array_value @509
-	Z3_get_model_func_else @510
-	Z3_get_model_func_num_entries @511
-	Z3_get_model_func_entry_num_args @512
-	Z3_get_model_func_entry_arg @513
-	Z3_get_model_func_entry_value @514
-	Z3_eval @515
-	Z3_eval_decl @516
-	Z3_context_to_string @517
-	Z3_statistics_to_string @518
-	Z3_get_context_assignment @519
+	Z3_param_descrs_to_string @26
+	Z3_mk_int_symbol @27
+	Z3_mk_string_symbol @28
+	Z3_mk_uninterpreted_sort @29
+	Z3_mk_bool_sort @30
+	Z3_mk_int_sort @31
+	Z3_mk_real_sort @32
+	Z3_mk_bv_sort @33
+	Z3_mk_finite_domain_sort @34
+	Z3_mk_array_sort @35
+	Z3_mk_tuple_sort @36
+	Z3_mk_enumeration_sort @37
+	Z3_mk_list_sort @38
+	Z3_mk_constructor @39
+	Z3_del_constructor @40
+	Z3_mk_datatype @41
+	Z3_mk_constructor_list @42
+	Z3_del_constructor_list @43
+	Z3_mk_datatypes @44
+	Z3_query_constructor @45
+	Z3_mk_func_decl @46
+	Z3_mk_app @47
+	Z3_mk_const @48
+	Z3_mk_fresh_func_decl @49
+	Z3_mk_fresh_const @50
+	Z3_mk_true @51
+	Z3_mk_false @52
+	Z3_mk_eq @53
+	Z3_mk_distinct @54
+	Z3_mk_not @55
+	Z3_mk_ite @56
+	Z3_mk_iff @57
+	Z3_mk_implies @58
+	Z3_mk_xor @59
+	Z3_mk_and @60
+	Z3_mk_or @61
+	Z3_mk_add @62
+	Z3_mk_mul @63
+	Z3_mk_sub @64
+	Z3_mk_unary_minus @65
+	Z3_mk_div @66
+	Z3_mk_mod @67
+	Z3_mk_rem @68
+	Z3_mk_power @69
+	Z3_mk_lt @70
+	Z3_mk_le @71
+	Z3_mk_gt @72
+	Z3_mk_ge @73
+	Z3_mk_int2real @74
+	Z3_mk_real2int @75
+	Z3_mk_is_int @76
+	Z3_mk_bvnot @77
+	Z3_mk_bvredand @78
+	Z3_mk_bvredor @79
+	Z3_mk_bvand @80
+	Z3_mk_bvor @81
+	Z3_mk_bvxor @82
+	Z3_mk_bvnand @83
+	Z3_mk_bvnor @84
+	Z3_mk_bvxnor @85
+	Z3_mk_bvneg @86
+	Z3_mk_bvadd @87
+	Z3_mk_bvsub @88
+	Z3_mk_bvmul @89
+	Z3_mk_bvudiv @90
+	Z3_mk_bvsdiv @91
+	Z3_mk_bvurem @92
+	Z3_mk_bvsrem @93
+	Z3_mk_bvsmod @94
+	Z3_mk_bvult @95
+	Z3_mk_bvslt @96
+	Z3_mk_bvule @97
+	Z3_mk_bvsle @98
+	Z3_mk_bvuge @99
+	Z3_mk_bvsge @100
+	Z3_mk_bvugt @101
+	Z3_mk_bvsgt @102
+	Z3_mk_concat @103
+	Z3_mk_extract @104
+	Z3_mk_sign_ext @105
+	Z3_mk_zero_ext @106
+	Z3_mk_repeat @107
+	Z3_mk_bvshl @108
+	Z3_mk_bvlshr @109
+	Z3_mk_bvashr @110
+	Z3_mk_rotate_left @111
+	Z3_mk_rotate_right @112
+	Z3_mk_ext_rotate_left @113
+	Z3_mk_ext_rotate_right @114
+	Z3_mk_int2bv @115
+	Z3_mk_bv2int @116
+	Z3_mk_bvadd_no_overflow @117
+	Z3_mk_bvadd_no_underflow @118
+	Z3_mk_bvsub_no_overflow @119
+	Z3_mk_bvsub_no_underflow @120
+	Z3_mk_bvsdiv_no_overflow @121
+	Z3_mk_bvneg_no_overflow @122
+	Z3_mk_bvmul_no_overflow @123
+	Z3_mk_bvmul_no_underflow @124
+	Z3_mk_select @125
+	Z3_mk_store @126
+	Z3_mk_const_array @127
+	Z3_mk_map @128
+	Z3_mk_array_default @129
+	Z3_mk_set_sort @130
+	Z3_mk_empty_set @131
+	Z3_mk_full_set @132
+	Z3_mk_set_add @133
+	Z3_mk_set_del @134
+	Z3_mk_set_union @135
+	Z3_mk_set_intersect @136
+	Z3_mk_set_difference @137
+	Z3_mk_set_complement @138
+	Z3_mk_set_member @139
+	Z3_mk_set_subset @140
+	Z3_mk_numeral @141
+	Z3_mk_real @142
+	Z3_mk_int @143
+	Z3_mk_unsigned_int @144
+	Z3_mk_int64 @145
+	Z3_mk_unsigned_int64 @146
+	Z3_mk_pattern @147
+	Z3_mk_bound @148
+	Z3_mk_forall @149
+	Z3_mk_exists @150
+	Z3_mk_quantifier @151
+	Z3_mk_quantifier_ex @152
+	Z3_mk_forall_const @153
+	Z3_mk_exists_const @154
+	Z3_mk_quantifier_const @155
+	Z3_mk_quantifier_const_ex @156
+	Z3_get_symbol_kind @157
+	Z3_get_symbol_int @158
+	Z3_get_symbol_string @159
+	Z3_get_sort_name @160
+	Z3_get_sort_id @161
+	Z3_sort_to_ast @162
+	Z3_is_eq_sort @163
+	Z3_get_sort_kind @164
+	Z3_get_bv_sort_size @165
+	Z3_get_finite_domain_sort_size @166
+	Z3_get_array_sort_domain @167
+	Z3_get_array_sort_range @168
+	Z3_get_tuple_sort_mk_decl @169
+	Z3_get_tuple_sort_num_fields @170
+	Z3_get_tuple_sort_field_decl @171
+	Z3_get_datatype_sort_num_constructors @172
+	Z3_get_datatype_sort_constructor @173
+	Z3_get_datatype_sort_recognizer @174
+	Z3_get_datatype_sort_constructor_accessor @175
+	Z3_get_relation_arity @176
+	Z3_get_relation_column @177
+	Z3_func_decl_to_ast @178
+	Z3_is_eq_func_decl @179
+	Z3_get_func_decl_id @180
+	Z3_get_decl_name @181
+	Z3_get_decl_kind @182
+	Z3_get_domain_size @183
+	Z3_get_arity @184
+	Z3_get_domain @185
+	Z3_get_range @186
+	Z3_get_decl_num_parameters @187
+	Z3_get_decl_parameter_kind @188
+	Z3_get_decl_int_parameter @189
+	Z3_get_decl_double_parameter @190
+	Z3_get_decl_symbol_parameter @191
+	Z3_get_decl_sort_parameter @192
+	Z3_get_decl_ast_parameter @193
+	Z3_get_decl_func_decl_parameter @194
+	Z3_get_decl_rational_parameter @195
+	Z3_app_to_ast @196
+	Z3_get_app_decl @197
+	Z3_get_app_num_args @198
+	Z3_get_app_arg @199
+	Z3_is_eq_ast @200
+	Z3_get_ast_id @201
+	Z3_get_ast_hash @202
+	Z3_get_sort @203
+	Z3_is_well_sorted @204
+	Z3_get_bool_value @205
+	Z3_get_ast_kind @206
+	Z3_is_app @207
+	Z3_is_numeral_ast @208
+	Z3_is_algebraic_number @209
+	Z3_to_app @210
+	Z3_to_func_decl @211
+	Z3_get_numeral_string @212
+	Z3_get_numeral_decimal_string @213
+	Z3_get_numerator @214
+	Z3_get_denominator @215
+	Z3_get_numeral_small @216
+	Z3_get_numeral_int @217
+	Z3_get_numeral_uint @218
+	Z3_get_numeral_uint64 @219
+	Z3_get_numeral_int64 @220
+	Z3_get_numeral_rational_int64 @221
+	Z3_get_algebraic_number_lower @222
+	Z3_get_algebraic_number_upper @223
+	Z3_pattern_to_ast @224
+	Z3_get_pattern_num_terms @225
+	Z3_get_pattern @226
+	Z3_get_index_value @227
+	Z3_is_quantifier_forall @228
+	Z3_get_quantifier_weight @229
+	Z3_get_quantifier_num_patterns @230
+	Z3_get_quantifier_pattern_ast @231
+	Z3_get_quantifier_num_no_patterns @232
+	Z3_get_quantifier_no_pattern_ast @233
+	Z3_get_quantifier_num_bound @234
+	Z3_get_quantifier_bound_name @235
+	Z3_get_quantifier_bound_sort @236
+	Z3_get_quantifier_body @237
+	Z3_simplify @238
+	Z3_simplify_ex @239
+	Z3_simplify_get_help @240
+	Z3_simplify_get_param_descrs @241
+	Z3_update_term @242
+	Z3_substitute @243
+	Z3_substitute_vars @244
+	Z3_translate @245
+	Z3_model_inc_ref @246
+	Z3_model_dec_ref @247
+	Z3_model_eval @248
+	Z3_model_get_const_interp @249
+	Z3_model_get_func_interp @250
+	Z3_model_get_num_consts @251
+	Z3_model_get_const_decl @252
+	Z3_model_get_num_funcs @253
+	Z3_model_get_func_decl @254
+	Z3_model_get_num_sorts @255
+	Z3_model_get_sort @256
+	Z3_model_get_sort_universe @257
+	Z3_is_as_array @258
+	Z3_get_as_array_func_decl @259
+	Z3_func_interp_inc_ref @260
+	Z3_func_interp_dec_ref @261
+	Z3_func_interp_get_num_entries @262
+	Z3_func_interp_get_entry @263
+	Z3_func_interp_get_else @264
+	Z3_func_interp_get_arity @265
+	Z3_func_entry_inc_ref @266
+	Z3_func_entry_dec_ref @267
+	Z3_func_entry_get_value @268
+	Z3_func_entry_get_num_args @269
+	Z3_func_entry_get_arg @270
+	Z3_open_log @271
+	Z3_append_log @272
+	Z3_close_log @273
+	Z3_toggle_warning_messages @274
+	Z3_set_ast_print_mode @275
+	Z3_ast_to_string @276
+	Z3_pattern_to_string @277
+	Z3_sort_to_string @278
+	Z3_func_decl_to_string @279
+	Z3_model_to_string @280
+	Z3_benchmark_to_smtlib_string @281
+	Z3_parse_smtlib2_string @282
+	Z3_parse_smtlib2_file @283
+	Z3_parse_smtlib_string @284
+	Z3_parse_smtlib_file @285
+	Z3_get_smtlib_num_formulas @286
+	Z3_get_smtlib_formula @287
+	Z3_get_smtlib_num_assumptions @288
+	Z3_get_smtlib_assumption @289
+	Z3_get_smtlib_num_decls @290
+	Z3_get_smtlib_decl @291
+	Z3_get_smtlib_num_sorts @292
+	Z3_get_smtlib_sort @293
+	Z3_get_smtlib_error @294
+	Z3_parse_z3_string @295
+	Z3_parse_z3_file @296
+	Z3_get_error_code @297
+	Z3_set_error_handler @298
+	Z3_set_error @299
+	Z3_get_error_msg @300
+	Z3_get_error_msg_ex @301
+	Z3_get_version @302
+	Z3_reset_memory @303
+	Z3_mk_theory @304
+	Z3_theory_get_ext_data @305
+	Z3_theory_mk_sort @306
+	Z3_theory_mk_value @307
+	Z3_theory_mk_constant @308
+	Z3_theory_mk_func_decl @309
+	Z3_theory_get_context @310
+	Z3_set_delete_callback @311
+	Z3_set_reduce_app_callback @312
+	Z3_set_reduce_eq_callback @313
+	Z3_set_reduce_distinct_callback @314
+	Z3_set_new_app_callback @315
+	Z3_set_new_elem_callback @316
+	Z3_set_init_search_callback @317
+	Z3_set_push_callback @318
+	Z3_set_pop_callback @319
+	Z3_set_restart_callback @320
+	Z3_set_reset_callback @321
+	Z3_set_final_check_callback @322
+	Z3_set_new_eq_callback @323
+	Z3_set_new_diseq_callback @324
+	Z3_set_new_assignment_callback @325
+	Z3_set_new_relevant_callback @326
+	Z3_theory_assert_axiom @327
+	Z3_theory_assume_eq @328
+	Z3_theory_enable_axiom_simplification @329
+	Z3_theory_get_eqc_root @330
+	Z3_theory_get_eqc_next @331
+	Z3_theory_get_num_parents @332
+	Z3_theory_get_parent @333
+	Z3_theory_is_value @334
+	Z3_theory_is_decl @335
+	Z3_theory_get_num_elems @336
+	Z3_theory_get_elem @337
+	Z3_theory_get_num_apps @338
+	Z3_theory_get_app @339
+	Z3_mk_fixedpoint @340
+	Z3_fixedpoint_inc_ref @341
+	Z3_fixedpoint_dec_ref @342
+	Z3_fixedpoint_add_rule @343
+	Z3_fixedpoint_add_fact @344
+	Z3_fixedpoint_assert @345
+	Z3_fixedpoint_query @346
+	Z3_fixedpoint_query_relations @347
+	Z3_fixedpoint_get_answer @348
+	Z3_fixedpoint_get_reason_unknown @349
+	Z3_fixedpoint_update_rule @350
+	Z3_fixedpoint_get_num_levels @351
+	Z3_fixedpoint_get_cover_delta @352
+	Z3_fixedpoint_add_cover @353
+	Z3_fixedpoint_get_statistics @354
+	Z3_fixedpoint_register_relation @355
+	Z3_fixedpoint_set_predicate_representation @356
+	Z3_fixedpoint_simplify_rules @357
+	Z3_fixedpoint_set_params @358
+	Z3_fixedpoint_get_help @359
+	Z3_fixedpoint_get_param_descrs @360
+	Z3_fixedpoint_to_string @361
+	Z3_fixedpoint_push @362
+	Z3_fixedpoint_pop @363
+	Z3_fixedpoint_init @364
+	Z3_fixedpoint_set_reduce_assign_callback @365
+	Z3_fixedpoint_set_reduce_app_callback @366
+	Z3_mk_ast_vector @367
+	Z3_ast_vector_inc_ref @368
+	Z3_ast_vector_dec_ref @369
+	Z3_ast_vector_size @370
+	Z3_ast_vector_get @371
+	Z3_ast_vector_set @372
+	Z3_ast_vector_resize @373
+	Z3_ast_vector_push @374
+	Z3_ast_vector_translate @375
+	Z3_ast_vector_to_string @376
+	Z3_mk_ast_map @377
+	Z3_ast_map_inc_ref @378
+	Z3_ast_map_dec_ref @379
+	Z3_ast_map_contains @380
+	Z3_ast_map_find @381
+	Z3_ast_map_insert @382
+	Z3_ast_map_erase @383
+	Z3_ast_map_reset @384
+	Z3_ast_map_size @385
+	Z3_ast_map_keys @386
+	Z3_ast_map_to_string @387
+	Z3_mk_goal @388
+	Z3_goal_inc_ref @389
+	Z3_goal_dec_ref @390
+	Z3_goal_precision @391
+	Z3_goal_assert @392
+	Z3_goal_inconsistent @393
+	Z3_goal_depth @394
+	Z3_goal_reset @395
+	Z3_goal_size @396
+	Z3_goal_formula @397
+	Z3_goal_num_exprs @398
+	Z3_goal_is_decided_sat @399
+	Z3_goal_is_decided_unsat @400
+	Z3_goal_translate @401
+	Z3_goal_to_string @402
+	Z3_mk_tactic @403
+	Z3_tactic_inc_ref @404
+	Z3_tactic_dec_ref @405
+	Z3_mk_probe @406
+	Z3_probe_inc_ref @407
+	Z3_probe_dec_ref @408
+	Z3_tactic_and_then @409
+	Z3_tactic_or_else @410
+	Z3_tactic_par_or @411
+	Z3_tactic_par_and_then @412
+	Z3_tactic_try_for @413
+	Z3_tactic_when @414
+	Z3_tactic_cond @415
+	Z3_tactic_repeat @416
+	Z3_tactic_skip @417
+	Z3_tactic_fail @418
+	Z3_tactic_fail_if @419
+	Z3_tactic_fail_if_not_decided @420
+	Z3_tactic_using_params @421
+	Z3_probe_const @422
+	Z3_probe_lt @423
+	Z3_probe_gt @424
+	Z3_probe_le @425
+	Z3_probe_ge @426
+	Z3_probe_eq @427
+	Z3_probe_and @428
+	Z3_probe_or @429
+	Z3_probe_not @430
+	Z3_get_num_tactics @431
+	Z3_get_tactic_name @432
+	Z3_get_num_probes @433
+	Z3_get_probe_name @434
+	Z3_tactic_get_help @435
+	Z3_tactic_get_param_descrs @436
+	Z3_tactic_get_descr @437
+	Z3_probe_get_descr @438
+	Z3_probe_apply @439
+	Z3_tactic_apply @440
+	Z3_tactic_apply_ex @441
+	Z3_apply_result_inc_ref @442
+	Z3_apply_result_dec_ref @443
+	Z3_apply_result_to_string @444
+	Z3_apply_result_get_num_subgoals @445
+	Z3_apply_result_get_subgoal @446
+	Z3_apply_result_convert_model @447
+	Z3_mk_solver @448
+	Z3_mk_simple_solver @449
+	Z3_mk_solver_for_logic @450
+	Z3_mk_solver_from_tactic @451
+	Z3_solver_get_help @452
+	Z3_solver_get_param_descrs @453
+	Z3_solver_set_params @454
+	Z3_solver_inc_ref @455
+	Z3_solver_dec_ref @456
+	Z3_solver_push @457
+	Z3_solver_pop @458
+	Z3_solver_reset @459
+	Z3_solver_get_num_scopes @460
+	Z3_solver_assert @461
+	Z3_solver_get_assertions @462
+	Z3_solver_check @463
+	Z3_solver_check_assumptions @464
+	Z3_solver_get_model @465
+	Z3_solver_get_proof @466
+	Z3_solver_get_unsat_core @467
+	Z3_solver_get_reason_unknown @468
+	Z3_solver_get_statistics @469
+	Z3_solver_to_string @470
+	Z3_stats_to_string @471
+	Z3_stats_inc_ref @472
+	Z3_stats_dec_ref @473
+	Z3_stats_size @474
+	Z3_stats_get_key @475
+	Z3_stats_is_uint @476
+	Z3_stats_is_double @477
+	Z3_stats_get_uint_value @478
+	Z3_stats_get_double_value @479
+	Z3_mk_injective_function @480
+	Z3_set_logic @481
+	Z3_push @482
+	Z3_pop @483
+	Z3_get_num_scopes @484
+	Z3_persist_ast @485
+	Z3_assert_cnstr @486
+	Z3_check_and_get_model @487
+	Z3_check @488
+	Z3_check_assumptions @489
+	Z3_get_implied_equalities @490
+	Z3_del_model @491
+	Z3_soft_check_cancel @492
+	Z3_get_search_failure @493
+	Z3_mk_label @494
+	Z3_get_relevant_labels @495
+	Z3_get_relevant_literals @496
+	Z3_get_guessed_literals @497
+	Z3_del_literals @498
+	Z3_get_num_literals @499
+	Z3_get_label_symbol @500
+	Z3_get_literal @501
+	Z3_disable_literal @502
+	Z3_block_literals @503
+	Z3_get_model_num_constants @504
+	Z3_get_model_constant @505
+	Z3_get_model_num_funcs @506
+	Z3_get_model_func_decl @507
+	Z3_eval_func_decl @508
+	Z3_is_array_value @509
+	Z3_get_array_value @510
+	Z3_get_model_func_else @511
+	Z3_get_model_func_num_entries @512
+	Z3_get_model_func_entry_num_args @513
+	Z3_get_model_func_entry_arg @514
+	Z3_get_model_func_entry_value @515
+	Z3_eval @516
+	Z3_eval_decl @517
+	Z3_context_to_string @518
+	Z3_statistics_to_string @519
+	Z3_get_context_assignment @520
diff --git a/lib/api.py b/lib/api.py
index 71449f43b..746d52cef 100644
--- a/lib/api.py
+++ b/lib/api.py
@@ -1100,6 +1100,7 @@ API('Z3_param_descrs_dec_ref', VOID, (_in(CONTEXT), _in(PARAM_DESCRS)))
 API('Z3_param_descrs_get_kind', UINT, (_in(CONTEXT), _in(PARAM_DESCRS), _in(SYMBOL)))
 API('Z3_param_descrs_size', UINT, (_in(CONTEXT), _in(PARAM_DESCRS)))
 API('Z3_param_descrs_get_name', SYMBOL, (_in(CONTEXT), _in(PARAM_DESCRS), _in(UINT)))
+API('Z3_param_descrs_to_string', STRING, (_in(CONTEXT), _in(PARAM_DESCRS)))
 # New APIs
 API('Z3_interrupt', VOID, (_in(CONTEXT),))
 API('Z3_get_error_msg_ex', STRING, (_in(CONTEXT), _in(ERROR_CODE)))
diff --git a/lib/api_commands.cpp b/lib/api_commands.cpp
index badb84ecf..342b25155 100644
--- a/lib/api_commands.cpp
+++ b/lib/api_commands.cpp
@@ -2328,6 +2328,11 @@ void exec_Z3_param_descrs_get_name(z3_replayer & in) {
     reinterpret_cast<Z3_param_descrs>(in.get_obj(1)),
     in.get_uint(2));
 }
+void exec_Z3_param_descrs_to_string(z3_replayer & in) {
+  Z3_param_descrs_to_string(
+    reinterpret_cast<Z3_context>(in.get_obj(0)),
+    reinterpret_cast<Z3_param_descrs>(in.get_obj(1)));
+}
 void exec_Z3_interrupt(z3_replayer & in) {
   Z3_interrupt(
     reinterpret_cast<Z3_context>(in.get_obj(0)));
@@ -3359,120 +3364,121 @@ void register_z3_replayer_cmds(z3_replayer & in) {
   in.register_cmd(357, exec_Z3_param_descrs_get_kind);
   in.register_cmd(358, exec_Z3_param_descrs_size);
   in.register_cmd(359, exec_Z3_param_descrs_get_name);
-  in.register_cmd(360, exec_Z3_interrupt);
-  in.register_cmd(361, exec_Z3_get_error_msg_ex);
-  in.register_cmd(362, exec_Z3_translate);
-  in.register_cmd(363, exec_Z3_mk_goal);
-  in.register_cmd(364, exec_Z3_goal_inc_ref);
-  in.register_cmd(365, exec_Z3_goal_dec_ref);
-  in.register_cmd(366, exec_Z3_goal_precision);
-  in.register_cmd(367, exec_Z3_goal_assert);
-  in.register_cmd(368, exec_Z3_goal_inconsistent);
-  in.register_cmd(369, exec_Z3_goal_depth);
-  in.register_cmd(370, exec_Z3_goal_reset);
-  in.register_cmd(371, exec_Z3_goal_size);
-  in.register_cmd(372, exec_Z3_goal_formula);
-  in.register_cmd(373, exec_Z3_goal_num_exprs);
-  in.register_cmd(374, exec_Z3_goal_is_decided_sat);
-  in.register_cmd(375, exec_Z3_goal_is_decided_unsat);
-  in.register_cmd(376, exec_Z3_goal_translate);
-  in.register_cmd(377, exec_Z3_goal_to_string);
-  in.register_cmd(378, exec_Z3_mk_tactic);
-  in.register_cmd(379, exec_Z3_mk_probe);
-  in.register_cmd(380, exec_Z3_tactic_inc_ref);
-  in.register_cmd(381, exec_Z3_tactic_dec_ref);
-  in.register_cmd(382, exec_Z3_probe_inc_ref);
-  in.register_cmd(383, exec_Z3_probe_dec_ref);
-  in.register_cmd(384, exec_Z3_tactic_and_then);
-  in.register_cmd(385, exec_Z3_tactic_or_else);
-  in.register_cmd(386, exec_Z3_tactic_par_or);
-  in.register_cmd(387, exec_Z3_tactic_par_and_then);
-  in.register_cmd(388, exec_Z3_tactic_try_for);
-  in.register_cmd(389, exec_Z3_tactic_when);
-  in.register_cmd(390, exec_Z3_tactic_cond);
-  in.register_cmd(391, exec_Z3_tactic_repeat);
-  in.register_cmd(392, exec_Z3_tactic_skip);
-  in.register_cmd(393, exec_Z3_tactic_fail);
-  in.register_cmd(394, exec_Z3_tactic_fail_if);
-  in.register_cmd(395, exec_Z3_tactic_fail_if_not_decided);
-  in.register_cmd(396, exec_Z3_tactic_using_params);
-  in.register_cmd(397, exec_Z3_probe_const);
-  in.register_cmd(398, exec_Z3_probe_lt);
-  in.register_cmd(399, exec_Z3_probe_le);
-  in.register_cmd(400, exec_Z3_probe_gt);
-  in.register_cmd(401, exec_Z3_probe_ge);
-  in.register_cmd(402, exec_Z3_probe_eq);
-  in.register_cmd(403, exec_Z3_probe_and);
-  in.register_cmd(404, exec_Z3_probe_or);
-  in.register_cmd(405, exec_Z3_probe_not);
-  in.register_cmd(406, exec_Z3_get_num_tactics);
-  in.register_cmd(407, exec_Z3_get_tactic_name);
-  in.register_cmd(408, exec_Z3_get_num_probes);
-  in.register_cmd(409, exec_Z3_get_probe_name);
-  in.register_cmd(410, exec_Z3_tactic_get_help);
-  in.register_cmd(411, exec_Z3_tactic_get_param_descrs);
-  in.register_cmd(412, exec_Z3_tactic_get_descr);
-  in.register_cmd(413, exec_Z3_probe_get_descr);
-  in.register_cmd(414, exec_Z3_probe_apply);
-  in.register_cmd(415, exec_Z3_tactic_apply);
-  in.register_cmd(416, exec_Z3_tactic_apply_ex);
-  in.register_cmd(417, exec_Z3_apply_result_inc_ref);
-  in.register_cmd(418, exec_Z3_apply_result_dec_ref);
-  in.register_cmd(419, exec_Z3_apply_result_to_string);
-  in.register_cmd(420, exec_Z3_apply_result_get_num_subgoals);
-  in.register_cmd(421, exec_Z3_apply_result_get_subgoal);
-  in.register_cmd(422, exec_Z3_apply_result_convert_model);
-  in.register_cmd(423, exec_Z3_mk_solver);
-  in.register_cmd(424, exec_Z3_mk_simple_solver);
-  in.register_cmd(425, exec_Z3_mk_solver_for_logic);
-  in.register_cmd(426, exec_Z3_mk_solver_from_tactic);
-  in.register_cmd(427, exec_Z3_solver_get_help);
-  in.register_cmd(428, exec_Z3_solver_get_param_descrs);
-  in.register_cmd(429, exec_Z3_solver_set_params);
-  in.register_cmd(430, exec_Z3_solver_inc_ref);
-  in.register_cmd(431, exec_Z3_solver_dec_ref);
-  in.register_cmd(432, exec_Z3_solver_push);
-  in.register_cmd(433, exec_Z3_solver_pop);
-  in.register_cmd(434, exec_Z3_solver_reset);
-  in.register_cmd(435, exec_Z3_solver_get_num_scopes);
-  in.register_cmd(436, exec_Z3_solver_assert);
-  in.register_cmd(437, exec_Z3_solver_get_assertions);
-  in.register_cmd(438, exec_Z3_solver_check);
-  in.register_cmd(439, exec_Z3_solver_check_assumptions);
-  in.register_cmd(440, exec_Z3_solver_get_model);
-  in.register_cmd(441, exec_Z3_solver_get_proof);
-  in.register_cmd(442, exec_Z3_solver_get_unsat_core);
-  in.register_cmd(443, exec_Z3_solver_get_reason_unknown);
-  in.register_cmd(444, exec_Z3_solver_get_statistics);
-  in.register_cmd(445, exec_Z3_solver_to_string);
-  in.register_cmd(446, exec_Z3_stats_to_string);
-  in.register_cmd(447, exec_Z3_stats_inc_ref);
-  in.register_cmd(448, exec_Z3_stats_dec_ref);
-  in.register_cmd(449, exec_Z3_stats_size);
-  in.register_cmd(450, exec_Z3_stats_get_key);
-  in.register_cmd(451, exec_Z3_stats_is_uint);
-  in.register_cmd(452, exec_Z3_stats_is_double);
-  in.register_cmd(453, exec_Z3_stats_get_uint_value);
-  in.register_cmd(454, exec_Z3_stats_get_double_value);
-  in.register_cmd(455, exec_Z3_mk_ast_vector);
-  in.register_cmd(456, exec_Z3_ast_vector_inc_ref);
-  in.register_cmd(457, exec_Z3_ast_vector_dec_ref);
-  in.register_cmd(458, exec_Z3_ast_vector_size);
-  in.register_cmd(459, exec_Z3_ast_vector_get);
-  in.register_cmd(460, exec_Z3_ast_vector_set);
-  in.register_cmd(461, exec_Z3_ast_vector_resize);
-  in.register_cmd(462, exec_Z3_ast_vector_push);
-  in.register_cmd(463, exec_Z3_ast_vector_translate);
-  in.register_cmd(464, exec_Z3_ast_vector_to_string);
-  in.register_cmd(465, exec_Z3_mk_ast_map);
-  in.register_cmd(466, exec_Z3_ast_map_inc_ref);
-  in.register_cmd(467, exec_Z3_ast_map_dec_ref);
-  in.register_cmd(468, exec_Z3_ast_map_contains);
-  in.register_cmd(469, exec_Z3_ast_map_find);
-  in.register_cmd(470, exec_Z3_ast_map_insert);
-  in.register_cmd(471, exec_Z3_ast_map_erase);
-  in.register_cmd(472, exec_Z3_ast_map_size);
-  in.register_cmd(473, exec_Z3_ast_map_reset);
-  in.register_cmd(474, exec_Z3_ast_map_keys);
-  in.register_cmd(475, exec_Z3_ast_map_to_string);
+  in.register_cmd(360, exec_Z3_param_descrs_to_string);
+  in.register_cmd(361, exec_Z3_interrupt);
+  in.register_cmd(362, exec_Z3_get_error_msg_ex);
+  in.register_cmd(363, exec_Z3_translate);
+  in.register_cmd(364, exec_Z3_mk_goal);
+  in.register_cmd(365, exec_Z3_goal_inc_ref);
+  in.register_cmd(366, exec_Z3_goal_dec_ref);
+  in.register_cmd(367, exec_Z3_goal_precision);
+  in.register_cmd(368, exec_Z3_goal_assert);
+  in.register_cmd(369, exec_Z3_goal_inconsistent);
+  in.register_cmd(370, exec_Z3_goal_depth);
+  in.register_cmd(371, exec_Z3_goal_reset);
+  in.register_cmd(372, exec_Z3_goal_size);
+  in.register_cmd(373, exec_Z3_goal_formula);
+  in.register_cmd(374, exec_Z3_goal_num_exprs);
+  in.register_cmd(375, exec_Z3_goal_is_decided_sat);
+  in.register_cmd(376, exec_Z3_goal_is_decided_unsat);
+  in.register_cmd(377, exec_Z3_goal_translate);
+  in.register_cmd(378, exec_Z3_goal_to_string);
+  in.register_cmd(379, exec_Z3_mk_tactic);
+  in.register_cmd(380, exec_Z3_mk_probe);
+  in.register_cmd(381, exec_Z3_tactic_inc_ref);
+  in.register_cmd(382, exec_Z3_tactic_dec_ref);
+  in.register_cmd(383, exec_Z3_probe_inc_ref);
+  in.register_cmd(384, exec_Z3_probe_dec_ref);
+  in.register_cmd(385, exec_Z3_tactic_and_then);
+  in.register_cmd(386, exec_Z3_tactic_or_else);
+  in.register_cmd(387, exec_Z3_tactic_par_or);
+  in.register_cmd(388, exec_Z3_tactic_par_and_then);
+  in.register_cmd(389, exec_Z3_tactic_try_for);
+  in.register_cmd(390, exec_Z3_tactic_when);
+  in.register_cmd(391, exec_Z3_tactic_cond);
+  in.register_cmd(392, exec_Z3_tactic_repeat);
+  in.register_cmd(393, exec_Z3_tactic_skip);
+  in.register_cmd(394, exec_Z3_tactic_fail);
+  in.register_cmd(395, exec_Z3_tactic_fail_if);
+  in.register_cmd(396, exec_Z3_tactic_fail_if_not_decided);
+  in.register_cmd(397, exec_Z3_tactic_using_params);
+  in.register_cmd(398, exec_Z3_probe_const);
+  in.register_cmd(399, exec_Z3_probe_lt);
+  in.register_cmd(400, exec_Z3_probe_le);
+  in.register_cmd(401, exec_Z3_probe_gt);
+  in.register_cmd(402, exec_Z3_probe_ge);
+  in.register_cmd(403, exec_Z3_probe_eq);
+  in.register_cmd(404, exec_Z3_probe_and);
+  in.register_cmd(405, exec_Z3_probe_or);
+  in.register_cmd(406, exec_Z3_probe_not);
+  in.register_cmd(407, exec_Z3_get_num_tactics);
+  in.register_cmd(408, exec_Z3_get_tactic_name);
+  in.register_cmd(409, exec_Z3_get_num_probes);
+  in.register_cmd(410, exec_Z3_get_probe_name);
+  in.register_cmd(411, exec_Z3_tactic_get_help);
+  in.register_cmd(412, exec_Z3_tactic_get_param_descrs);
+  in.register_cmd(413, exec_Z3_tactic_get_descr);
+  in.register_cmd(414, exec_Z3_probe_get_descr);
+  in.register_cmd(415, exec_Z3_probe_apply);
+  in.register_cmd(416, exec_Z3_tactic_apply);
+  in.register_cmd(417, exec_Z3_tactic_apply_ex);
+  in.register_cmd(418, exec_Z3_apply_result_inc_ref);
+  in.register_cmd(419, exec_Z3_apply_result_dec_ref);
+  in.register_cmd(420, exec_Z3_apply_result_to_string);
+  in.register_cmd(421, exec_Z3_apply_result_get_num_subgoals);
+  in.register_cmd(422, exec_Z3_apply_result_get_subgoal);
+  in.register_cmd(423, exec_Z3_apply_result_convert_model);
+  in.register_cmd(424, exec_Z3_mk_solver);
+  in.register_cmd(425, exec_Z3_mk_simple_solver);
+  in.register_cmd(426, exec_Z3_mk_solver_for_logic);
+  in.register_cmd(427, exec_Z3_mk_solver_from_tactic);
+  in.register_cmd(428, exec_Z3_solver_get_help);
+  in.register_cmd(429, exec_Z3_solver_get_param_descrs);
+  in.register_cmd(430, exec_Z3_solver_set_params);
+  in.register_cmd(431, exec_Z3_solver_inc_ref);
+  in.register_cmd(432, exec_Z3_solver_dec_ref);
+  in.register_cmd(433, exec_Z3_solver_push);
+  in.register_cmd(434, exec_Z3_solver_pop);
+  in.register_cmd(435, exec_Z3_solver_reset);
+  in.register_cmd(436, exec_Z3_solver_get_num_scopes);
+  in.register_cmd(437, exec_Z3_solver_assert);
+  in.register_cmd(438, exec_Z3_solver_get_assertions);
+  in.register_cmd(439, exec_Z3_solver_check);
+  in.register_cmd(440, exec_Z3_solver_check_assumptions);
+  in.register_cmd(441, exec_Z3_solver_get_model);
+  in.register_cmd(442, exec_Z3_solver_get_proof);
+  in.register_cmd(443, exec_Z3_solver_get_unsat_core);
+  in.register_cmd(444, exec_Z3_solver_get_reason_unknown);
+  in.register_cmd(445, exec_Z3_solver_get_statistics);
+  in.register_cmd(446, exec_Z3_solver_to_string);
+  in.register_cmd(447, exec_Z3_stats_to_string);
+  in.register_cmd(448, exec_Z3_stats_inc_ref);
+  in.register_cmd(449, exec_Z3_stats_dec_ref);
+  in.register_cmd(450, exec_Z3_stats_size);
+  in.register_cmd(451, exec_Z3_stats_get_key);
+  in.register_cmd(452, exec_Z3_stats_is_uint);
+  in.register_cmd(453, exec_Z3_stats_is_double);
+  in.register_cmd(454, exec_Z3_stats_get_uint_value);
+  in.register_cmd(455, exec_Z3_stats_get_double_value);
+  in.register_cmd(456, exec_Z3_mk_ast_vector);
+  in.register_cmd(457, exec_Z3_ast_vector_inc_ref);
+  in.register_cmd(458, exec_Z3_ast_vector_dec_ref);
+  in.register_cmd(459, exec_Z3_ast_vector_size);
+  in.register_cmd(460, exec_Z3_ast_vector_get);
+  in.register_cmd(461, exec_Z3_ast_vector_set);
+  in.register_cmd(462, exec_Z3_ast_vector_resize);
+  in.register_cmd(463, exec_Z3_ast_vector_push);
+  in.register_cmd(464, exec_Z3_ast_vector_translate);
+  in.register_cmd(465, exec_Z3_ast_vector_to_string);
+  in.register_cmd(466, exec_Z3_mk_ast_map);
+  in.register_cmd(467, exec_Z3_ast_map_inc_ref);
+  in.register_cmd(468, exec_Z3_ast_map_dec_ref);
+  in.register_cmd(469, exec_Z3_ast_map_contains);
+  in.register_cmd(470, exec_Z3_ast_map_find);
+  in.register_cmd(471, exec_Z3_ast_map_insert);
+  in.register_cmd(472, exec_Z3_ast_map_erase);
+  in.register_cmd(473, exec_Z3_ast_map_size);
+  in.register_cmd(474, exec_Z3_ast_map_reset);
+  in.register_cmd(475, exec_Z3_ast_map_keys);
+  in.register_cmd(476, exec_Z3_ast_map_to_string);
 }
diff --git a/lib/api_log_macros.cpp b/lib/api_log_macros.cpp
index 4358b3dc0..997978725 100644
--- a/lib/api_log_macros.cpp
+++ b/lib/api_log_macros.cpp
@@ -2570,23 +2570,29 @@ void log_Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, unsigned a2
   U(a2);
   C(359);
 }
+void log_Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1) {
+  R();
+  P(a0);
+  P(a1);
+  C(360);
+}
 void log_Z3_interrupt(Z3_context a0) {
   R();
   P(a0);
-  C(360);
+  C(361);
 }
 void log_Z3_get_error_msg_ex(Z3_context a0, Z3_error_code a1) {
   R();
   P(a0);
   U(static_cast<unsigned>(a1));
-  C(361);
+  C(362);
 }
 void log_Z3_translate(Z3_context a0, Z3_ast a1, Z3_context a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(362);
+  C(363);
 }
 void log_Z3_mk_goal(Z3_context a0, Z3_bool a1, Z3_bool a2, Z3_bool a3) {
   R();
@@ -2594,144 +2600,144 @@ void log_Z3_mk_goal(Z3_context a0, Z3_bool a1, Z3_bool a2, Z3_bool a3) {
   I(a1);
   I(a2);
   I(a3);
-  C(363);
+  C(364);
 }
 void log_Z3_goal_inc_ref(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(364);
+  C(365);
 }
 void log_Z3_goal_dec_ref(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(365);
+  C(366);
 }
 void log_Z3_goal_precision(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(366);
+  C(367);
 }
 void log_Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(367);
+  C(368);
 }
 void log_Z3_goal_inconsistent(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(368);
+  C(369);
 }
 void log_Z3_goal_depth(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(369);
+  C(370);
 }
 void log_Z3_goal_reset(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(370);
+  C(371);
 }
 void log_Z3_goal_size(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(371);
+  C(372);
 }
 void log_Z3_goal_formula(Z3_context a0, Z3_goal a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(372);
+  C(373);
 }
 void log_Z3_goal_num_exprs(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(373);
+  C(374);
 }
 void log_Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(374);
+  C(375);
 }
 void log_Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(375);
+  C(376);
 }
 void log_Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(376);
+  C(377);
 }
 void log_Z3_goal_to_string(Z3_context a0, Z3_goal a1) {
   R();
   P(a0);
   P(a1);
-  C(377);
+  C(378);
 }
 void log_Z3_mk_tactic(Z3_context a0, Z3_string a1) {
   R();
   P(a0);
   S(a1);
-  C(378);
+  C(379);
 }
 void log_Z3_mk_probe(Z3_context a0, Z3_string a1) {
   R();
   P(a0);
   S(a1);
-  C(379);
+  C(380);
 }
 void log_Z3_tactic_inc_ref(Z3_context a0, Z3_tactic a1) {
   R();
   P(a0);
   P(a1);
-  C(380);
+  C(381);
 }
 void log_Z3_tactic_dec_ref(Z3_context a0, Z3_tactic a1) {
   R();
   P(a0);
   P(a1);
-  C(381);
+  C(382);
 }
 void log_Z3_probe_inc_ref(Z3_context a0, Z3_probe a1) {
   R();
   P(a0);
   P(a1);
-  C(382);
+  C(383);
 }
 void log_Z3_probe_dec_ref(Z3_context a0, Z3_probe a1) {
   R();
   P(a0);
   P(a1);
-  C(383);
+  C(384);
 }
 void log_Z3_tactic_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(384);
+  C(385);
 }
 void log_Z3_tactic_or_else(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(385);
+  C(386);
 }
 void log_Z3_tactic_par_or(Z3_context a0, unsigned a1, Z3_tactic const * a2) {
   R();
@@ -2739,28 +2745,28 @@ void log_Z3_tactic_par_or(Z3_context a0, unsigned a1, Z3_tactic const * a2) {
   U(a1);
   for (unsigned i = 0; i < a1; i++) { P(a2[i]); }
   Ap(a1);
-  C(386);
+  C(387);
 }
 void log_Z3_tactic_par_and_then(Z3_context a0, Z3_tactic a1, Z3_tactic a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(387);
+  C(388);
 }
 void log_Z3_tactic_try_for(Z3_context a0, Z3_tactic a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(388);
+  C(389);
 }
 void log_Z3_tactic_when(Z3_context a0, Z3_probe a1, Z3_tactic a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(389);
+  C(390);
 }
 void log_Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3) {
   R();
@@ -2768,163 +2774,163 @@ void log_Z3_tactic_cond(Z3_context a0, Z3_probe a1, Z3_tactic a2, Z3_tactic a3)
   P(a1);
   P(a2);
   P(a3);
-  C(390);
+  C(391);
 }
 void log_Z3_tactic_repeat(Z3_context a0, Z3_tactic a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(391);
+  C(392);
 }
 void log_Z3_tactic_skip(Z3_context a0) {
   R();
   P(a0);
-  C(392);
+  C(393);
 }
 void log_Z3_tactic_fail(Z3_context a0) {
   R();
   P(a0);
-  C(393);
+  C(394);
 }
 void log_Z3_tactic_fail_if(Z3_context a0, Z3_probe a1) {
   R();
   P(a0);
   P(a1);
-  C(394);
+  C(395);
 }
 void log_Z3_tactic_fail_if_not_decided(Z3_context a0) {
   R();
   P(a0);
-  C(395);
+  C(396);
 }
 void log_Z3_tactic_using_params(Z3_context a0, Z3_tactic a1, Z3_params a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(396);
+  C(397);
 }
 void log_Z3_probe_const(Z3_context a0, double a1) {
   R();
   P(a0);
   D(a1);
-  C(397);
+  C(398);
 }
 void log_Z3_probe_lt(Z3_context a0, Z3_probe a1, Z3_probe a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(398);
+  C(399);
 }
 void log_Z3_probe_le(Z3_context a0, Z3_probe a1, Z3_probe a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(399);
+  C(400);
 }
 void log_Z3_probe_gt(Z3_context a0, Z3_probe a1, Z3_probe a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(400);
+  C(401);
 }
 void log_Z3_probe_ge(Z3_context a0, Z3_probe a1, Z3_probe a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(401);
+  C(402);
 }
 void log_Z3_probe_eq(Z3_context a0, Z3_probe a1, Z3_probe a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(402);
+  C(403);
 }
 void log_Z3_probe_and(Z3_context a0, Z3_probe a1, Z3_probe a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(403);
+  C(404);
 }
 void log_Z3_probe_or(Z3_context a0, Z3_probe a1, Z3_probe a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(404);
+  C(405);
 }
 void log_Z3_probe_not(Z3_context a0, Z3_probe a1) {
   R();
   P(a0);
   P(a1);
-  C(405);
+  C(406);
 }
 void log_Z3_get_num_tactics(Z3_context a0) {
   R();
   P(a0);
-  C(406);
+  C(407);
 }
 void log_Z3_get_tactic_name(Z3_context a0, unsigned a1) {
   R();
   P(a0);
   U(a1);
-  C(407);
+  C(408);
 }
 void log_Z3_get_num_probes(Z3_context a0) {
   R();
   P(a0);
-  C(408);
+  C(409);
 }
 void log_Z3_get_probe_name(Z3_context a0, unsigned a1) {
   R();
   P(a0);
   U(a1);
-  C(409);
+  C(410);
 }
 void log_Z3_tactic_get_help(Z3_context a0, Z3_tactic a1) {
   R();
   P(a0);
   P(a1);
-  C(410);
+  C(411);
 }
 void log_Z3_tactic_get_param_descrs(Z3_context a0, Z3_tactic a1) {
   R();
   P(a0);
   P(a1);
-  C(411);
+  C(412);
 }
 void log_Z3_tactic_get_descr(Z3_context a0, Z3_string a1) {
   R();
   P(a0);
   S(a1);
-  C(412);
+  C(413);
 }
 void log_Z3_probe_get_descr(Z3_context a0, Z3_string a1) {
   R();
   P(a0);
   S(a1);
-  C(413);
+  C(414);
 }
 void log_Z3_probe_apply(Z3_context a0, Z3_probe a1, Z3_goal a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(414);
+  C(415);
 }
 void log_Z3_tactic_apply(Z3_context a0, Z3_tactic a1, Z3_goal a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(415);
+  C(416);
 }
 void log_Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a3) {
   R();
@@ -2932,38 +2938,38 @@ void log_Z3_tactic_apply_ex(Z3_context a0, Z3_tactic a1, Z3_goal a2, Z3_params a
   P(a1);
   P(a2);
   P(a3);
-  C(416);
+  C(417);
 }
 void log_Z3_apply_result_inc_ref(Z3_context a0, Z3_apply_result a1) {
   R();
   P(a0);
   P(a1);
-  C(417);
+  C(418);
 }
 void log_Z3_apply_result_dec_ref(Z3_context a0, Z3_apply_result a1) {
   R();
   P(a0);
   P(a1);
-  C(418);
+  C(419);
 }
 void log_Z3_apply_result_to_string(Z3_context a0, Z3_apply_result a1) {
   R();
   P(a0);
   P(a1);
-  C(419);
+  C(420);
 }
 void log_Z3_apply_result_get_num_subgoals(Z3_context a0, Z3_apply_result a1) {
   R();
   P(a0);
   P(a1);
-  C(420);
+  C(421);
 }
 void log_Z3_apply_result_get_subgoal(Z3_context a0, Z3_apply_result a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(421);
+  C(422);
 }
 void log_Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, unsigned a2, Z3_model a3) {
   R();
@@ -2971,104 +2977,104 @@ void log_Z3_apply_result_convert_model(Z3_context a0, Z3_apply_result a1, unsign
   P(a1);
   U(a2);
   P(a3);
-  C(422);
+  C(423);
 }
 void log_Z3_mk_solver(Z3_context a0) {
   R();
   P(a0);
-  C(423);
+  C(424);
 }
 void log_Z3_mk_simple_solver(Z3_context a0) {
   R();
   P(a0);
-  C(424);
+  C(425);
 }
 void log_Z3_mk_solver_for_logic(Z3_context a0, Z3_symbol a1) {
   R();
   P(a0);
   Sy(a1);
-  C(425);
+  C(426);
 }
 void log_Z3_mk_solver_from_tactic(Z3_context a0, Z3_tactic a1) {
   R();
   P(a0);
   P(a1);
-  C(426);
+  C(427);
 }
 void log_Z3_solver_get_help(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(427);
+  C(428);
 }
 void log_Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(428);
+  C(429);
 }
 void log_Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(429);
+  C(430);
 }
 void log_Z3_solver_inc_ref(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(430);
+  C(431);
 }
 void log_Z3_solver_dec_ref(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(431);
+  C(432);
 }
 void log_Z3_solver_push(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(432);
+  C(433);
 }
 void log_Z3_solver_pop(Z3_context a0, Z3_solver a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(433);
+  C(434);
 }
 void log_Z3_solver_reset(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(434);
+  C(435);
 }
 void log_Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(435);
+  C(436);
 }
 void log_Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(436);
+  C(437);
 }
 void log_Z3_solver_get_assertions(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(437);
+  C(438);
 }
 void log_Z3_solver_check(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(438);
+  C(439);
 }
 void log_Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, unsigned a2, Z3_ast const * a3) {
   R();
@@ -3077,132 +3083,132 @@ void log_Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, unsigned a2, Z
   U(a2);
   for (unsigned i = 0; i < a2; i++) { P(a3[i]); }
   Ap(a2);
-  C(439);
+  C(440);
 }
 void log_Z3_solver_get_model(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(440);
+  C(441);
 }
 void log_Z3_solver_get_proof(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(441);
+  C(442);
 }
 void log_Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(442);
+  C(443);
 }
 void log_Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(443);
+  C(444);
 }
 void log_Z3_solver_get_statistics(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(444);
+  C(445);
 }
 void log_Z3_solver_to_string(Z3_context a0, Z3_solver a1) {
   R();
   P(a0);
   P(a1);
-  C(445);
+  C(446);
 }
 void log_Z3_stats_to_string(Z3_context a0, Z3_stats a1) {
   R();
   P(a0);
   P(a1);
-  C(446);
+  C(447);
 }
 void log_Z3_stats_inc_ref(Z3_context a0, Z3_stats a1) {
   R();
   P(a0);
   P(a1);
-  C(447);
+  C(448);
 }
 void log_Z3_stats_dec_ref(Z3_context a0, Z3_stats a1) {
   R();
   P(a0);
   P(a1);
-  C(448);
+  C(449);
 }
 void log_Z3_stats_size(Z3_context a0, Z3_stats a1) {
   R();
   P(a0);
   P(a1);
-  C(449);
+  C(450);
 }
 void log_Z3_stats_get_key(Z3_context a0, Z3_stats a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(450);
+  C(451);
 }
 void log_Z3_stats_is_uint(Z3_context a0, Z3_stats a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(451);
+  C(452);
 }
 void log_Z3_stats_is_double(Z3_context a0, Z3_stats a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(452);
+  C(453);
 }
 void log_Z3_stats_get_uint_value(Z3_context a0, Z3_stats a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(453);
+  C(454);
 }
 void log_Z3_stats_get_double_value(Z3_context a0, Z3_stats a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(454);
+  C(455);
 }
 void log_Z3_mk_ast_vector(Z3_context a0) {
   R();
   P(a0);
-  C(455);
+  C(456);
 }
 void log_Z3_ast_vector_inc_ref(Z3_context a0, Z3_ast_vector a1) {
   R();
   P(a0);
   P(a1);
-  C(456);
+  C(457);
 }
 void log_Z3_ast_vector_dec_ref(Z3_context a0, Z3_ast_vector a1) {
   R();
   P(a0);
   P(a1);
-  C(457);
+  C(458);
 }
 void log_Z3_ast_vector_size(Z3_context a0, Z3_ast_vector a1) {
   R();
   P(a0);
   P(a1);
-  C(458);
+  C(459);
 }
 void log_Z3_ast_vector_get(Z3_context a0, Z3_ast_vector a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(459);
+  C(460);
 }
 void log_Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, unsigned a2, Z3_ast a3) {
   R();
@@ -3210,65 +3216,65 @@ void log_Z3_ast_vector_set(Z3_context a0, Z3_ast_vector a1, unsigned a2, Z3_ast
   P(a1);
   U(a2);
   P(a3);
-  C(460);
+  C(461);
 }
 void log_Z3_ast_vector_resize(Z3_context a0, Z3_ast_vector a1, unsigned a2) {
   R();
   P(a0);
   P(a1);
   U(a2);
-  C(461);
+  C(462);
 }
 void log_Z3_ast_vector_push(Z3_context a0, Z3_ast_vector a1, Z3_ast a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(462);
+  C(463);
 }
 void log_Z3_ast_vector_translate(Z3_context a0, Z3_ast_vector a1, Z3_context a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(463);
+  C(464);
 }
 void log_Z3_ast_vector_to_string(Z3_context a0, Z3_ast_vector a1) {
   R();
   P(a0);
   P(a1);
-  C(464);
+  C(465);
 }
 void log_Z3_mk_ast_map(Z3_context a0) {
   R();
   P(a0);
-  C(465);
+  C(466);
 }
 void log_Z3_ast_map_inc_ref(Z3_context a0, Z3_ast_map a1) {
   R();
   P(a0);
   P(a1);
-  C(466);
+  C(467);
 }
 void log_Z3_ast_map_dec_ref(Z3_context a0, Z3_ast_map a1) {
   R();
   P(a0);
   P(a1);
-  C(467);
+  C(468);
 }
 void log_Z3_ast_map_contains(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(468);
+  C(469);
 }
 void log_Z3_ast_map_find(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(469);
+  C(470);
 }
 void log_Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3) {
   R();
@@ -3276,36 +3282,36 @@ void log_Z3_ast_map_insert(Z3_context a0, Z3_ast_map a1, Z3_ast a2, Z3_ast a3) {
   P(a1);
   P(a2);
   P(a3);
-  C(470);
+  C(471);
 }
 void log_Z3_ast_map_erase(Z3_context a0, Z3_ast_map a1, Z3_ast a2) {
   R();
   P(a0);
   P(a1);
   P(a2);
-  C(471);
+  C(472);
 }
 void log_Z3_ast_map_size(Z3_context a0, Z3_ast_map a1) {
   R();
   P(a0);
   P(a1);
-  C(472);
+  C(473);
 }
 void log_Z3_ast_map_reset(Z3_context a0, Z3_ast_map a1) {
   R();
   P(a0);
   P(a1);
-  C(473);
+  C(474);
 }
 void log_Z3_ast_map_keys(Z3_context a0, Z3_ast_map a1) {
   R();
   P(a0);
   P(a1);
-  C(474);
+  C(475);
 }
 void log_Z3_ast_map_to_string(Z3_context a0, Z3_ast_map a1) {
   R();
   P(a0);
   P(a1);
-  C(475);
+  C(476);
 }
diff --git a/lib/api_log_macros.h b/lib/api_log_macros.h
index ca2dde6d5..ac5e806c2 100644
--- a/lib/api_log_macros.h
+++ b/lib/api_log_macros.h
@@ -741,6 +741,8 @@ void log_Z3_param_descrs_size(Z3_context a0, Z3_param_descrs a1);
 #define LOG_Z3_param_descrs_size(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_size(_ARG0, _ARG1); }
 void log_Z3_param_descrs_get_name(Z3_context a0, Z3_param_descrs a1, unsigned a2);
 #define LOG_Z3_param_descrs_get_name(_ARG0, _ARG1, _ARG2) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_get_name(_ARG0, _ARG1, _ARG2); }
+void log_Z3_param_descrs_to_string(Z3_context a0, Z3_param_descrs a1);
+#define LOG_Z3_param_descrs_to_string(_ARG0, _ARG1) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_param_descrs_to_string(_ARG0, _ARG1); }
 void log_Z3_interrupt(Z3_context a0);
 #define LOG_Z3_interrupt(_ARG0) z3_log_ctx _LOG_CTX; if (_LOG_CTX.enabled()) { log_Z3_interrupt(_ARG0); }
 void log_Z3_get_error_msg_ex(Z3_context a0, Z3_error_code a1);
diff --git a/lib/api_params.cpp b/lib/api_params.cpp
index 2badef8d6..74899bc44 100644
--- a/lib/api_params.cpp
+++ b/lib/api_params.cpp
@@ -179,4 +179,21 @@ extern "C" {
         Z3_CATCH_RETURN(0);
     }
 
+    Z3_string Z3_API Z3_param_descrs_to_string(Z3_context c, Z3_param_descrs p) {
+        Z3_TRY;
+        LOG_Z3_param_descrs_to_string(c, p);
+        RESET_ERROR_CODE();
+        std::ostringstream buffer;
+        buffer << "(";
+        unsigned sz = to_param_descrs_ptr(p)->size();
+        for (unsigned i = 0; i < sz; i++) {
+            if (i > 0) 
+                buffer << ", ";
+            buffer << to_param_descrs_ptr(p)->get_param_name(i);
+        }
+        buffer << ")";
+        return mk_c(c)->mk_external_string(buffer.str());
+        Z3_CATCH_RETURN("");
+    }
+
 };
diff --git a/lib/z3_api.h b/lib/z3_api.h
index 6afcdcb49..f4c4e8260 100644
--- a/lib/z3_api.h
+++ b/lib/z3_api.h
@@ -1456,6 +1456,12 @@ extern "C" {
     */
     Z3_symbol Z3_API Z3_param_descrs_get_name(__in Z3_context c, __in Z3_param_descrs p, __in unsigned i);
 
+    /**
+       \brief Convert a parameter description set into a string. This function is mainly used for printing the
+       contents of a parameter description set.
+    */
+    Z3_string Z3_API Z3_param_descrs_to_string(__in Z3_context c, __in Z3_param_descrs p);
+
     /*@}*/
 #endif
 
diff --git a/python/z3.py b/python/z3.py
index dea752a87..011d63851 100644
--- a/python/z3.py
+++ b/python/z3.py
@@ -4421,18 +4421,7 @@ class ParamDescrsRef:
             return self.get_kind(arg)
 
     def __repr__(self):
-        r = io.StringIO()
-        first = True
-        r.write(u'(')
-        for i in range(self.size()):
-            if first:
-                first = False
-            else:
-                r.write(u' ')
-            r.write(u'%s' % self.get_name(i))
-        r.write(u')')
-        return r.getvalue()
-
+        return Z3_param_descrs_to_string(self.ctx.ref(), self.descr)
 
 #########################################
 #
diff --git a/python/z3core.py b/python/z3core.py
index 588e9fa86..5ae71a35d 100644
--- a/python/z3core.py
+++ b/python/z3core.py
@@ -696,6 +696,8 @@ def init(PATH):
   _lib.Z3_param_descrs_size.argtypes = [ContextObj, ParamDescrs]
   _lib.Z3_param_descrs_get_name.restype = Symbol
   _lib.Z3_param_descrs_get_name.argtypes = [ContextObj, ParamDescrs, ctypes.c_uint]
+  _lib.Z3_param_descrs_to_string.restype = ctypes.c_char_p
+  _lib.Z3_param_descrs_to_string.argtypes = [ContextObj, ParamDescrs]
   _lib.Z3_interrupt.argtypes = [ContextObj]
   _lib.Z3_get_error_msg_ex.restype = ctypes.c_char_p
   _lib.Z3_get_error_msg_ex.argtypes = [ContextObj, ctypes.c_uint]
@@ -3341,6 +3343,13 @@ def Z3_param_descrs_get_name(a0, a1, a2):
     raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
   return r
 
+def Z3_param_descrs_to_string(a0, a1):
+  r = lib().Z3_param_descrs_to_string(a0, a1)
+  err = lib().Z3_get_error_code(a0)
+  if err != Z3_OK:
+    raise Z3Exception(lib().Z3_get_error_msg_ex(a0, err))
+  return r
+
 def Z3_interrupt(a0):
   lib().Z3_interrupt(a0)
   err = lib().Z3_get_error_code(a0)