-
Notifications
You must be signed in to change notification settings - Fork 1
/
Copy pathapi_entries.sh
652 lines (652 loc) · 26.2 KB
/
api_entries.sh
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
Z3_API_FUNCS="'["
Z3_API_FUNCS+="\"_Z3_algebraic_add\","
Z3_API_FUNCS+="\"_Z3_algebraic_div\","
Z3_API_FUNCS+="\"_Z3_algebraic_eq\","
Z3_API_FUNCS+="\"_Z3_algebraic_eval\","
Z3_API_FUNCS+="\"_Z3_algebraic_ge\","
Z3_API_FUNCS+="\"_Z3_algebraic_gt\","
Z3_API_FUNCS+="\"_Z3_algebraic_is_neg\","
Z3_API_FUNCS+="\"_Z3_algebraic_is_pos\","
Z3_API_FUNCS+="\"_Z3_algebraic_is_value\","
Z3_API_FUNCS+="\"_Z3_algebraic_is_zero\","
Z3_API_FUNCS+="\"_Z3_algebraic_le\","
Z3_API_FUNCS+="\"_Z3_algebraic_lt\","
Z3_API_FUNCS+="\"_Z3_algebraic_mul\","
Z3_API_FUNCS+="\"_Z3_algebraic_neq\","
Z3_API_FUNCS+="\"_Z3_algebraic_power\","
Z3_API_FUNCS+="\"_Z3_algebraic_root\","
Z3_API_FUNCS+="\"_Z3_algebraic_roots\","
Z3_API_FUNCS+="\"_Z3_algebraic_sign\","
Z3_API_FUNCS+="\"_Z3_algebraic_sub\","
Z3_API_FUNCS+="\"_Z3_app_to_ast\","
Z3_API_FUNCS+="\"_Z3_append_log\","
Z3_API_FUNCS+="\"_Z3_apply_result_convert_model\","
Z3_API_FUNCS+="\"_Z3_apply_result_dec_ref\","
Z3_API_FUNCS+="\"_Z3_apply_result_get_num_subgoals\","
Z3_API_FUNCS+="\"_Z3_apply_result_get_subgoal\","
Z3_API_FUNCS+="\"_Z3_apply_result_inc_ref\","
Z3_API_FUNCS+="\"_Z3_apply_result_to_string\","
Z3_API_FUNCS+="\"_Z3_ast_map_contains\","
Z3_API_FUNCS+="\"_Z3_ast_map_dec_ref\","
Z3_API_FUNCS+="\"_Z3_ast_map_erase\","
Z3_API_FUNCS+="\"_Z3_ast_map_find\","
Z3_API_FUNCS+="\"_Z3_ast_map_inc_ref\","
Z3_API_FUNCS+="\"_Z3_ast_map_insert\","
Z3_API_FUNCS+="\"_Z3_ast_map_keys\","
Z3_API_FUNCS+="\"_Z3_ast_map_reset\","
Z3_API_FUNCS+="\"_Z3_ast_map_size\","
Z3_API_FUNCS+="\"_Z3_ast_map_to_string\","
Z3_API_FUNCS+="\"_Z3_ast_to_string\","
Z3_API_FUNCS+="\"_Z3_ast_vector_dec_ref\","
Z3_API_FUNCS+="\"_Z3_ast_vector_get\","
Z3_API_FUNCS+="\"_Z3_ast_vector_inc_ref\","
Z3_API_FUNCS+="\"_Z3_ast_vector_push\","
Z3_API_FUNCS+="\"_Z3_ast_vector_resize\","
Z3_API_FUNCS+="\"_Z3_ast_vector_set\","
Z3_API_FUNCS+="\"_Z3_ast_vector_size\","
Z3_API_FUNCS+="\"_Z3_ast_vector_to_string\","
Z3_API_FUNCS+="\"_Z3_ast_vector_translate\","
Z3_API_FUNCS+="\"_Z3_benchmark_to_smtlib_string\","
Z3_API_FUNCS+="\"_Z3_check_interpolant\","
Z3_API_FUNCS+="\"_Z3_close_log\","
Z3_API_FUNCS+="\"_Z3_compute_interpolant\","
Z3_API_FUNCS+="\"_Z3_datatype_update_field\","
Z3_API_FUNCS+="\"_Z3_dec_ref\","
Z3_API_FUNCS+="\"_Z3_del_config\","
Z3_API_FUNCS+="\"_Z3_del_constructor\","
Z3_API_FUNCS+="\"_Z3_del_constructor_list\","
Z3_API_FUNCS+="\"_Z3_del_context\","
Z3_API_FUNCS+="\"_Z3_disable_trace\","
Z3_API_FUNCS+="\"_Z3_enable_trace\","
Z3_API_FUNCS+="\"_Z3_finalize_memory\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_add_cover\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_add_fact\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_add_rule\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_assert\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_dec_ref\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_from_file\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_from_string\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_answer\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_assertions\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_cover_delta\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_help\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_num_levels\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_param_descrs\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_reason_unknown\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_rules\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_get_statistics\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_inc_ref\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_pop\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_push\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_query\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_query_relations\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_register_relation\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_set_params\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_set_predicate_representation\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_to_string\","
Z3_API_FUNCS+="\"_Z3_fixedpoint_update_rule\","
Z3_API_FUNCS+="\"_Z3_fpa_get_ebits\","
Z3_API_FUNCS+="\"_Z3_fpa_get_numeral_exponent_bv\","
Z3_API_FUNCS+="\"_Z3_fpa_get_numeral_exponent_int64\","
Z3_API_FUNCS+="\"_Z3_fpa_get_numeral_exponent_string\","
Z3_API_FUNCS+="\"_Z3_fpa_get_numeral_sign\","
Z3_API_FUNCS+="\"_Z3_fpa_get_numeral_sign_bv\","
Z3_API_FUNCS+="\"_Z3_fpa_get_numeral_significand_bv\","
Z3_API_FUNCS+="\"_Z3_fpa_get_numeral_significand_string\","
Z3_API_FUNCS+="\"_Z3_fpa_get_numeral_significand_uint64\","
Z3_API_FUNCS+="\"_Z3_fpa_get_sbits\","
Z3_API_FUNCS+="\"_Z3_fpa_is_numeral_inf\","
Z3_API_FUNCS+="\"_Z3_fpa_is_numeral_nan\","
Z3_API_FUNCS+="\"_Z3_fpa_is_numeral_negative\","
Z3_API_FUNCS+="\"_Z3_fpa_is_numeral_normal\","
Z3_API_FUNCS+="\"_Z3_fpa_is_numeral_positive\","
Z3_API_FUNCS+="\"_Z3_fpa_is_numeral_subnormal\","
Z3_API_FUNCS+="\"_Z3_fpa_is_numeral_zero\","
Z3_API_FUNCS+="\"_Z3_func_decl_to_ast\","
Z3_API_FUNCS+="\"_Z3_func_decl_to_string\","
Z3_API_FUNCS+="\"_Z3_func_entry_dec_ref\","
Z3_API_FUNCS+="\"_Z3_func_entry_get_arg\","
Z3_API_FUNCS+="\"_Z3_func_entry_get_num_args\","
Z3_API_FUNCS+="\"_Z3_func_entry_get_value\","
Z3_API_FUNCS+="\"_Z3_func_entry_inc_ref\","
Z3_API_FUNCS+="\"_Z3_func_interp_dec_ref\","
Z3_API_FUNCS+="\"_Z3_func_interp_get_arity\","
Z3_API_FUNCS+="\"_Z3_func_interp_get_else\","
Z3_API_FUNCS+="\"_Z3_func_interp_get_entry\","
Z3_API_FUNCS+="\"_Z3_func_interp_get_num_entries\","
Z3_API_FUNCS+="\"_Z3_func_interp_inc_ref\","
Z3_API_FUNCS+="\"_Z3_get_algebraic_number_lower\","
Z3_API_FUNCS+="\"_Z3_get_algebraic_number_upper\","
Z3_API_FUNCS+="\"_Z3_get_app_arg\","
Z3_API_FUNCS+="\"_Z3_get_app_decl\","
Z3_API_FUNCS+="\"_Z3_get_app_num_args\","
Z3_API_FUNCS+="\"_Z3_get_arity\","
Z3_API_FUNCS+="\"_Z3_get_array_sort_domain\","
Z3_API_FUNCS+="\"_Z3_get_array_sort_range\","
Z3_API_FUNCS+="\"_Z3_get_as_array_func_decl\","
Z3_API_FUNCS+="\"_Z3_get_ast_hash\","
Z3_API_FUNCS+="\"_Z3_get_ast_id\","
Z3_API_FUNCS+="\"_Z3_get_ast_kind\","
Z3_API_FUNCS+="\"_Z3_get_bool_value\","
Z3_API_FUNCS+="\"_Z3_get_bv_sort_size\","
Z3_API_FUNCS+="\"_Z3_get_datatype_sort_constructor\","
Z3_API_FUNCS+="\"_Z3_get_datatype_sort_constructor_accessor\","
Z3_API_FUNCS+="\"_Z3_get_datatype_sort_num_constructors\","
Z3_API_FUNCS+="\"_Z3_get_datatype_sort_recognizer\","
Z3_API_FUNCS+="\"_Z3_get_decl_ast_parameter\","
Z3_API_FUNCS+="\"_Z3_get_decl_double_parameter\","
Z3_API_FUNCS+="\"_Z3_get_decl_func_decl_parameter\","
Z3_API_FUNCS+="\"_Z3_get_decl_int_parameter\","
Z3_API_FUNCS+="\"_Z3_get_decl_kind\","
Z3_API_FUNCS+="\"_Z3_get_decl_name\","
Z3_API_FUNCS+="\"_Z3_get_decl_num_parameters\","
Z3_API_FUNCS+="\"_Z3_get_decl_parameter_kind\","
Z3_API_FUNCS+="\"_Z3_get_decl_rational_parameter\","
Z3_API_FUNCS+="\"_Z3_get_decl_sort_parameter\","
Z3_API_FUNCS+="\"_Z3_get_decl_symbol_parameter\","
Z3_API_FUNCS+="\"_Z3_get_denominator\","
Z3_API_FUNCS+="\"_Z3_get_domain\","
Z3_API_FUNCS+="\"_Z3_get_domain_size\","
Z3_API_FUNCS+="\"_Z3_get_error_code\","
Z3_API_FUNCS+="\"_Z3_get_error_msg\","
Z3_API_FUNCS+="\"_Z3_get_estimated_alloc_size\","
Z3_API_FUNCS+="\"_Z3_get_finite_domain_sort_size\","
Z3_API_FUNCS+="\"_Z3_get_full_version\","
Z3_API_FUNCS+="\"_Z3_get_func_decl_id\","
Z3_API_FUNCS+="\"_Z3_get_implied_equalities\","
Z3_API_FUNCS+="\"_Z3_get_index_value\","
Z3_API_FUNCS+="\"_Z3_get_interpolant\","
Z3_API_FUNCS+="\"_Z3_get_num_probes\","
Z3_API_FUNCS+="\"_Z3_get_num_tactics\","
Z3_API_FUNCS+="\"_Z3_get_numeral_decimal_string\","
Z3_API_FUNCS+="\"_Z3_get_numeral_int\","
Z3_API_FUNCS+="\"_Z3_get_numeral_int64\","
Z3_API_FUNCS+="\"_Z3_get_numeral_rational_int64\","
Z3_API_FUNCS+="\"_Z3_get_numeral_small\","
Z3_API_FUNCS+="\"_Z3_get_numeral_string\","
Z3_API_FUNCS+="\"_Z3_get_numeral_uint\","
Z3_API_FUNCS+="\"_Z3_get_numeral_uint64\","
Z3_API_FUNCS+="\"_Z3_get_numerator\","
Z3_API_FUNCS+="\"_Z3_get_pattern\","
Z3_API_FUNCS+="\"_Z3_get_pattern_num_terms\","
Z3_API_FUNCS+="\"_Z3_get_probe_name\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_body\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_bound_name\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_bound_sort\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_no_pattern_ast\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_num_bound\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_num_no_patterns\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_num_patterns\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_pattern_ast\","
Z3_API_FUNCS+="\"_Z3_get_quantifier_weight\","
Z3_API_FUNCS+="\"_Z3_get_range\","
Z3_API_FUNCS+="\"_Z3_get_relation_arity\","
Z3_API_FUNCS+="\"_Z3_get_relation_column\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_assumption\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_decl\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_error\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_formula\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_num_assumptions\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_num_decls\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_num_formulas\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_num_sorts\","
Z3_API_FUNCS+="\"_Z3_get_smtlib_sort\","
Z3_API_FUNCS+="\"_Z3_get_sort\","
Z3_API_FUNCS+="\"_Z3_get_sort_id\","
Z3_API_FUNCS+="\"_Z3_get_sort_kind\","
Z3_API_FUNCS+="\"_Z3_get_sort_name\","
Z3_API_FUNCS+="\"_Z3_get_string\","
Z3_API_FUNCS+="\"_Z3_get_symbol_int\","
Z3_API_FUNCS+="\"_Z3_get_symbol_kind\","
Z3_API_FUNCS+="\"_Z3_get_symbol_string\","
Z3_API_FUNCS+="\"_Z3_get_tactic_name\","
Z3_API_FUNCS+="\"_Z3_get_tuple_sort_field_decl\","
Z3_API_FUNCS+="\"_Z3_get_tuple_sort_mk_decl\","
Z3_API_FUNCS+="\"_Z3_get_tuple_sort_num_fields\","
Z3_API_FUNCS+="\"_Z3_get_version\","
Z3_API_FUNCS+="\"_Z3_global_param_get\","
Z3_API_FUNCS+="\"_Z3_global_param_reset_all\","
Z3_API_FUNCS+="\"_Z3_global_param_set\","
Z3_API_FUNCS+="\"_Z3_goal_assert\","
Z3_API_FUNCS+="\"_Z3_goal_dec_ref\","
Z3_API_FUNCS+="\"_Z3_goal_depth\","
Z3_API_FUNCS+="\"_Z3_goal_formula\","
Z3_API_FUNCS+="\"_Z3_goal_inc_ref\","
Z3_API_FUNCS+="\"_Z3_goal_inconsistent\","
Z3_API_FUNCS+="\"_Z3_goal_is_decided_sat\","
Z3_API_FUNCS+="\"_Z3_goal_is_decided_unsat\","
Z3_API_FUNCS+="\"_Z3_goal_num_exprs\","
Z3_API_FUNCS+="\"_Z3_goal_precision\","
Z3_API_FUNCS+="\"_Z3_goal_reset\","
Z3_API_FUNCS+="\"_Z3_goal_size\","
Z3_API_FUNCS+="\"_Z3_goal_to_string\","
Z3_API_FUNCS+="\"_Z3_goal_translate\","
Z3_API_FUNCS+="\"_Z3_inc_ref\","
Z3_API_FUNCS+="\"_Z3_interpolation_profile\","
Z3_API_FUNCS+="\"_Z3_interrupt\","
Z3_API_FUNCS+="\"_Z3_is_algebraic_number\","
Z3_API_FUNCS+="\"_Z3_is_app\","
Z3_API_FUNCS+="\"_Z3_is_as_array\","
Z3_API_FUNCS+="\"_Z3_is_eq_ast\","
Z3_API_FUNCS+="\"_Z3_is_eq_func_decl\","
Z3_API_FUNCS+="\"_Z3_is_eq_sort\","
Z3_API_FUNCS+="\"_Z3_is_numeral_ast\","
Z3_API_FUNCS+="\"_Z3_is_quantifier_forall\","
Z3_API_FUNCS+="\"_Z3_is_re_sort\","
Z3_API_FUNCS+="\"_Z3_is_seq_sort\","
Z3_API_FUNCS+="\"_Z3_is_string\","
Z3_API_FUNCS+="\"_Z3_is_string_sort\","
Z3_API_FUNCS+="\"_Z3_is_well_sorted\","
Z3_API_FUNCS+="\"_Z3_mk_add\","
Z3_API_FUNCS+="\"_Z3_mk_and\","
Z3_API_FUNCS+="\"_Z3_mk_app\","
Z3_API_FUNCS+="\"_Z3_mk_array_default\","
Z3_API_FUNCS+="\"_Z3_mk_array_ext\","
Z3_API_FUNCS+="\"_Z3_mk_array_sort\","
Z3_API_FUNCS+="\"_Z3_mk_ast_map\","
Z3_API_FUNCS+="\"_Z3_mk_ast_vector\","
Z3_API_FUNCS+="\"_Z3_mk_atleast\","
Z3_API_FUNCS+="\"_Z3_mk_atmost\","
Z3_API_FUNCS+="\"_Z3_mk_bool_sort\","
Z3_API_FUNCS+="\"_Z3_mk_bound\","
Z3_API_FUNCS+="\"_Z3_mk_bv2int\","
Z3_API_FUNCS+="\"_Z3_mk_bv_sort\","
Z3_API_FUNCS+="\"_Z3_mk_bvadd\","
Z3_API_FUNCS+="\"_Z3_mk_bvadd_no_overflow\","
Z3_API_FUNCS+="\"_Z3_mk_bvadd_no_underflow\","
Z3_API_FUNCS+="\"_Z3_mk_bvand\","
Z3_API_FUNCS+="\"_Z3_mk_bvashr\","
Z3_API_FUNCS+="\"_Z3_mk_bvlshr\","
Z3_API_FUNCS+="\"_Z3_mk_bvmul\","
Z3_API_FUNCS+="\"_Z3_mk_bvmul_no_overflow\","
Z3_API_FUNCS+="\"_Z3_mk_bvmul_no_underflow\","
Z3_API_FUNCS+="\"_Z3_mk_bvnand\","
Z3_API_FUNCS+="\"_Z3_mk_bvneg\","
Z3_API_FUNCS+="\"_Z3_mk_bvneg_no_overflow\","
Z3_API_FUNCS+="\"_Z3_mk_bvnor\","
Z3_API_FUNCS+="\"_Z3_mk_bvnot\","
Z3_API_FUNCS+="\"_Z3_mk_bvor\","
Z3_API_FUNCS+="\"_Z3_mk_bvredand\","
Z3_API_FUNCS+="\"_Z3_mk_bvredor\","
Z3_API_FUNCS+="\"_Z3_mk_bvsdiv\","
Z3_API_FUNCS+="\"_Z3_mk_bvsdiv_no_overflow\","
Z3_API_FUNCS+="\"_Z3_mk_bvsge\","
Z3_API_FUNCS+="\"_Z3_mk_bvsgt\","
Z3_API_FUNCS+="\"_Z3_mk_bvshl\","
Z3_API_FUNCS+="\"_Z3_mk_bvsle\","
Z3_API_FUNCS+="\"_Z3_mk_bvslt\","
Z3_API_FUNCS+="\"_Z3_mk_bvsmod\","
Z3_API_FUNCS+="\"_Z3_mk_bvsrem\","
Z3_API_FUNCS+="\"_Z3_mk_bvsub\","
Z3_API_FUNCS+="\"_Z3_mk_bvsub_no_overflow\","
Z3_API_FUNCS+="\"_Z3_mk_bvsub_no_underflow\","
Z3_API_FUNCS+="\"_Z3_mk_bvudiv\","
Z3_API_FUNCS+="\"_Z3_mk_bvuge\","
Z3_API_FUNCS+="\"_Z3_mk_bvugt\","
Z3_API_FUNCS+="\"_Z3_mk_bvule\","
Z3_API_FUNCS+="\"_Z3_mk_bvult\","
Z3_API_FUNCS+="\"_Z3_mk_bvurem\","
Z3_API_FUNCS+="\"_Z3_mk_bvxnor\","
Z3_API_FUNCS+="\"_Z3_mk_bvxor\","
Z3_API_FUNCS+="\"_Z3_mk_concat\","
Z3_API_FUNCS+="\"_Z3_mk_config\","
Z3_API_FUNCS+="\"_Z3_mk_const\","
Z3_API_FUNCS+="\"_Z3_mk_const_array\","
Z3_API_FUNCS+="\"_Z3_mk_constructor\","
Z3_API_FUNCS+="\"_Z3_mk_constructor_list\","
Z3_API_FUNCS+="\"_Z3_mk_context\","
Z3_API_FUNCS+="\"_Z3_mk_context_rc\","
Z3_API_FUNCS+="\"_Z3_mk_datatype\","
Z3_API_FUNCS+="\"_Z3_mk_datatypes\","
Z3_API_FUNCS+="\"_Z3_mk_distinct\","
Z3_API_FUNCS+="\"_Z3_mk_div\","
Z3_API_FUNCS+="\"_Z3_mk_empty_set\","
Z3_API_FUNCS+="\"_Z3_mk_enumeration_sort\","
Z3_API_FUNCS+="\"_Z3_mk_eq\","
Z3_API_FUNCS+="\"_Z3_mk_exists\","
Z3_API_FUNCS+="\"_Z3_mk_exists_const\","
Z3_API_FUNCS+="\"_Z3_mk_ext_rotate_left\","
Z3_API_FUNCS+="\"_Z3_mk_ext_rotate_right\","
Z3_API_FUNCS+="\"_Z3_mk_extract\","
Z3_API_FUNCS+="\"_Z3_mk_false\","
Z3_API_FUNCS+="\"_Z3_mk_finite_domain_sort\","
Z3_API_FUNCS+="\"_Z3_mk_fixedpoint\","
Z3_API_FUNCS+="\"_Z3_mk_forall\","
Z3_API_FUNCS+="\"_Z3_mk_forall_const\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_abs\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_add\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_div\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_eq\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_fma\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_fp\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_geq\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_gt\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_inf\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_is_infinite\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_is_nan\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_is_negative\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_is_normal\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_is_positive\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_is_subnormal\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_is_zero\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_leq\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_lt\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_max\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_min\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_mul\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_nan\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_neg\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_numeral_double\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_numeral_float\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_numeral_int\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_numeral_int64_uint64\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_numeral_int_uint\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_rem\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_rna\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_rne\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_round_nearest_ties_to_away\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_round_nearest_ties_to_even\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_round_to_integral\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_round_toward_negative\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_round_toward_positive\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_round_toward_zero\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_rounding_mode_sort\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_rtn\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_rtp\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_rtz\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort_128\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort_16\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort_32\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort_64\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort_double\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort_half\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort_quadruple\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sort_single\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sqrt\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_sub\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_fp_bv\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_fp_float\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_fp_int_real\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_fp_real\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_fp_signed\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_fp_unsigned\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_ieee_bv\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_real\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_sbv\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_to_ubv\","
Z3_API_FUNCS+="\"_Z3_mk_fpa_zero\","
Z3_API_FUNCS+="\"_Z3_mk_fresh_const\","
Z3_API_FUNCS+="\"_Z3_mk_fresh_func_decl\","
Z3_API_FUNCS+="\"_Z3_mk_full_set\","
Z3_API_FUNCS+="\"_Z3_mk_func_decl\","
Z3_API_FUNCS+="\"_Z3_mk_ge\","
Z3_API_FUNCS+="\"_Z3_mk_goal\","
Z3_API_FUNCS+="\"_Z3_mk_gt\","
Z3_API_FUNCS+="\"_Z3_mk_iff\","
Z3_API_FUNCS+="\"_Z3_mk_implies\","
Z3_API_FUNCS+="\"_Z3_mk_int\","
Z3_API_FUNCS+="\"_Z3_mk_int2bv\","
Z3_API_FUNCS+="\"_Z3_mk_int2real\","
Z3_API_FUNCS+="\"_Z3_mk_int64\","
Z3_API_FUNCS+="\"_Z3_mk_int_sort\","
Z3_API_FUNCS+="\"_Z3_mk_int_symbol\","
Z3_API_FUNCS+="\"_Z3_mk_int_to_str\","
Z3_API_FUNCS+="\"_Z3_mk_interpolant\","
Z3_API_FUNCS+="\"_Z3_mk_interpolation_context\","
Z3_API_FUNCS+="\"_Z3_mk_is_int\","
Z3_API_FUNCS+="\"_Z3_mk_ite\","
Z3_API_FUNCS+="\"_Z3_mk_le\","
Z3_API_FUNCS+="\"_Z3_mk_list_sort\","
Z3_API_FUNCS+="\"_Z3_mk_lt\","
Z3_API_FUNCS+="\"_Z3_mk_map\","
Z3_API_FUNCS+="\"_Z3_mk_mod\","
Z3_API_FUNCS+="\"_Z3_mk_mul\","
Z3_API_FUNCS+="\"_Z3_mk_not\","
Z3_API_FUNCS+="\"_Z3_mk_numeral\","
Z3_API_FUNCS+="\"_Z3_mk_optimize\","
Z3_API_FUNCS+="\"_Z3_mk_or\","
Z3_API_FUNCS+="\"_Z3_mk_params\","
Z3_API_FUNCS+="\"_Z3_mk_pattern\","
Z3_API_FUNCS+="\"_Z3_mk_pbeq\","
Z3_API_FUNCS+="\"_Z3_mk_pbge\","
Z3_API_FUNCS+="\"_Z3_mk_pble\","
Z3_API_FUNCS+="\"_Z3_mk_power\","
Z3_API_FUNCS+="\"_Z3_mk_probe\","
Z3_API_FUNCS+="\"_Z3_mk_quantifier\","
Z3_API_FUNCS+="\"_Z3_mk_quantifier_const\","
Z3_API_FUNCS+="\"_Z3_mk_quantifier_const_ex\","
Z3_API_FUNCS+="\"_Z3_mk_quantifier_ex\","
Z3_API_FUNCS+="\"_Z3_mk_re_complement\","
Z3_API_FUNCS+="\"_Z3_mk_re_concat\","
Z3_API_FUNCS+="\"_Z3_mk_re_empty\","
Z3_API_FUNCS+="\"_Z3_mk_re_full\","
Z3_API_FUNCS+="\"_Z3_mk_re_intersect\","
Z3_API_FUNCS+="\"_Z3_mk_re_loop\","
Z3_API_FUNCS+="\"_Z3_mk_re_option\","
Z3_API_FUNCS+="\"_Z3_mk_re_plus\","
Z3_API_FUNCS+="\"_Z3_mk_re_range\","
Z3_API_FUNCS+="\"_Z3_mk_re_sort\","
Z3_API_FUNCS+="\"_Z3_mk_re_star\","
Z3_API_FUNCS+="\"_Z3_mk_re_union\","
Z3_API_FUNCS+="\"_Z3_mk_real\","
Z3_API_FUNCS+="\"_Z3_mk_real2int\","
Z3_API_FUNCS+="\"_Z3_mk_real_sort\","
Z3_API_FUNCS+="\"_Z3_mk_rem\","
Z3_API_FUNCS+="\"_Z3_mk_repeat\","
Z3_API_FUNCS+="\"_Z3_mk_rotate_left\","
Z3_API_FUNCS+="\"_Z3_mk_rotate_right\","
Z3_API_FUNCS+="\"_Z3_mk_select\","
Z3_API_FUNCS+="\"_Z3_mk_seq_at\","
Z3_API_FUNCS+="\"_Z3_mk_seq_concat\","
Z3_API_FUNCS+="\"_Z3_mk_seq_contains\","
Z3_API_FUNCS+="\"_Z3_mk_seq_empty\","
Z3_API_FUNCS+="\"_Z3_mk_seq_extract\","
Z3_API_FUNCS+="\"_Z3_mk_seq_in_re\","
Z3_API_FUNCS+="\"_Z3_mk_seq_index\","
Z3_API_FUNCS+="\"_Z3_mk_seq_length\","
Z3_API_FUNCS+="\"_Z3_mk_seq_prefix\","
Z3_API_FUNCS+="\"_Z3_mk_seq_replace\","
Z3_API_FUNCS+="\"_Z3_mk_seq_sort\","
Z3_API_FUNCS+="\"_Z3_mk_seq_suffix\","
Z3_API_FUNCS+="\"_Z3_mk_seq_to_re\","
Z3_API_FUNCS+="\"_Z3_mk_seq_unit\","
Z3_API_FUNCS+="\"_Z3_mk_set_add\","
Z3_API_FUNCS+="\"_Z3_mk_set_complement\","
Z3_API_FUNCS+="\"_Z3_mk_set_del\","
Z3_API_FUNCS+="\"_Z3_mk_set_difference\","
Z3_API_FUNCS+="\"_Z3_mk_set_intersect\","
Z3_API_FUNCS+="\"_Z3_mk_set_member\","
Z3_API_FUNCS+="\"_Z3_mk_set_sort\","
Z3_API_FUNCS+="\"_Z3_mk_set_subset\","
Z3_API_FUNCS+="\"_Z3_mk_set_union\","
Z3_API_FUNCS+="\"_Z3_mk_sign_ext\","
Z3_API_FUNCS+="\"_Z3_mk_simple_solver\","
Z3_API_FUNCS+="\"_Z3_mk_solver\","
Z3_API_FUNCS+="\"_Z3_mk_solver_for_logic\","
Z3_API_FUNCS+="\"_Z3_mk_solver_from_tactic\","
Z3_API_FUNCS+="\"_Z3_mk_store\","
Z3_API_FUNCS+="\"_Z3_mk_str_to_int\","
Z3_API_FUNCS+="\"_Z3_mk_string\","
Z3_API_FUNCS+="\"_Z3_mk_string_sort\","
Z3_API_FUNCS+="\"_Z3_mk_string_symbol\","
Z3_API_FUNCS+="\"_Z3_mk_sub\","
Z3_API_FUNCS+="\"_Z3_mk_tactic\","
Z3_API_FUNCS+="\"_Z3_mk_true\","
Z3_API_FUNCS+="\"_Z3_mk_tuple_sort\","
Z3_API_FUNCS+="\"_Z3_mk_unary_minus\","
Z3_API_FUNCS+="\"_Z3_mk_uninterpreted_sort\","
Z3_API_FUNCS+="\"_Z3_mk_unsigned_int\","
Z3_API_FUNCS+="\"_Z3_mk_unsigned_int64\","
Z3_API_FUNCS+="\"_Z3_mk_xor\","
Z3_API_FUNCS+="\"_Z3_mk_zero_ext\","
Z3_API_FUNCS+="\"_Z3_model_dec_ref\","
Z3_API_FUNCS+="\"_Z3_model_eval\","
Z3_API_FUNCS+="\"_Z3_model_get_const_decl\","
Z3_API_FUNCS+="\"_Z3_model_get_const_interp\","
Z3_API_FUNCS+="\"_Z3_model_get_func_decl\","
Z3_API_FUNCS+="\"_Z3_model_get_func_interp\","
Z3_API_FUNCS+="\"_Z3_model_get_num_consts\","
Z3_API_FUNCS+="\"_Z3_model_get_num_funcs\","
Z3_API_FUNCS+="\"_Z3_model_get_num_sorts\","
Z3_API_FUNCS+="\"_Z3_model_get_sort\","
Z3_API_FUNCS+="\"_Z3_model_get_sort_universe\","
Z3_API_FUNCS+="\"_Z3_model_has_interp\","
Z3_API_FUNCS+="\"_Z3_model_inc_ref\","
Z3_API_FUNCS+="\"_Z3_model_to_string\","
Z3_API_FUNCS+="\"_Z3_open_log\","
Z3_API_FUNCS+="\"_Z3_optimize_assert\","
Z3_API_FUNCS+="\"_Z3_optimize_assert_soft\","
Z3_API_FUNCS+="\"_Z3_optimize_check\","
Z3_API_FUNCS+="\"_Z3_optimize_dec_ref\","
Z3_API_FUNCS+="\"_Z3_optimize_from_file\","
Z3_API_FUNCS+="\"_Z3_optimize_from_string\","
Z3_API_FUNCS+="\"_Z3_optimize_get_assertions\","
Z3_API_FUNCS+="\"_Z3_optimize_get_help\","
Z3_API_FUNCS+="\"_Z3_optimize_get_lower\","
Z3_API_FUNCS+="\"_Z3_optimize_get_lower_as_vector\","
Z3_API_FUNCS+="\"_Z3_optimize_get_model\","
Z3_API_FUNCS+="\"_Z3_optimize_get_objectives\","
Z3_API_FUNCS+="\"_Z3_optimize_get_param_descrs\","
Z3_API_FUNCS+="\"_Z3_optimize_get_reason_unknown\","
Z3_API_FUNCS+="\"_Z3_optimize_get_statistics\","
Z3_API_FUNCS+="\"_Z3_optimize_get_upper\","
Z3_API_FUNCS+="\"_Z3_optimize_get_upper_as_vector\","
Z3_API_FUNCS+="\"_Z3_optimize_inc_ref\","
Z3_API_FUNCS+="\"_Z3_optimize_maximize\","
Z3_API_FUNCS+="\"_Z3_optimize_minimize\","
Z3_API_FUNCS+="\"_Z3_optimize_pop\","
Z3_API_FUNCS+="\"_Z3_optimize_push\","
Z3_API_FUNCS+="\"_Z3_optimize_set_params\","
Z3_API_FUNCS+="\"_Z3_optimize_to_string\","
Z3_API_FUNCS+="\"_Z3_param_descrs_dec_ref\","
Z3_API_FUNCS+="\"_Z3_param_descrs_get_documentation\","
Z3_API_FUNCS+="\"_Z3_param_descrs_get_kind\","
Z3_API_FUNCS+="\"_Z3_param_descrs_get_name\","
Z3_API_FUNCS+="\"_Z3_param_descrs_inc_ref\","
Z3_API_FUNCS+="\"_Z3_param_descrs_size\","
Z3_API_FUNCS+="\"_Z3_param_descrs_to_string\","
Z3_API_FUNCS+="\"_Z3_params_dec_ref\","
Z3_API_FUNCS+="\"_Z3_params_inc_ref\","
Z3_API_FUNCS+="\"_Z3_params_set_bool\","
Z3_API_FUNCS+="\"_Z3_params_set_double\","
Z3_API_FUNCS+="\"_Z3_params_set_symbol\","
Z3_API_FUNCS+="\"_Z3_params_set_uint\","
Z3_API_FUNCS+="\"_Z3_params_to_string\","
Z3_API_FUNCS+="\"_Z3_params_validate\","
Z3_API_FUNCS+="\"_Z3_parse_smtlib2_file\","
Z3_API_FUNCS+="\"_Z3_parse_smtlib2_string\","
Z3_API_FUNCS+="\"_Z3_parse_smtlib_file\","
Z3_API_FUNCS+="\"_Z3_parse_smtlib_string\","
Z3_API_FUNCS+="\"_Z3_pattern_to_ast\","
Z3_API_FUNCS+="\"_Z3_pattern_to_string\","
Z3_API_FUNCS+="\"_Z3_polynomial_subresultants\","
Z3_API_FUNCS+="\"_Z3_probe_and\","
Z3_API_FUNCS+="\"_Z3_probe_apply\","
Z3_API_FUNCS+="\"_Z3_probe_const\","
Z3_API_FUNCS+="\"_Z3_probe_dec_ref\","
Z3_API_FUNCS+="\"_Z3_probe_eq\","
Z3_API_FUNCS+="\"_Z3_probe_ge\","
Z3_API_FUNCS+="\"_Z3_probe_get_descr\","
Z3_API_FUNCS+="\"_Z3_probe_gt\","
Z3_API_FUNCS+="\"_Z3_probe_inc_ref\","
Z3_API_FUNCS+="\"_Z3_probe_le\","
Z3_API_FUNCS+="\"_Z3_probe_lt\","
Z3_API_FUNCS+="\"_Z3_probe_not\","
Z3_API_FUNCS+="\"_Z3_probe_or\","
Z3_API_FUNCS+="\"_Z3_query_constructor\","
Z3_API_FUNCS+="\"_Z3_rcf_add\","
Z3_API_FUNCS+="\"_Z3_rcf_del\","
Z3_API_FUNCS+="\"_Z3_rcf_div\","
Z3_API_FUNCS+="\"_Z3_rcf_eq\","
Z3_API_FUNCS+="\"_Z3_rcf_ge\","
Z3_API_FUNCS+="\"_Z3_rcf_get_numerator_denominator\","
Z3_API_FUNCS+="\"_Z3_rcf_gt\","
Z3_API_FUNCS+="\"_Z3_rcf_inv\","
Z3_API_FUNCS+="\"_Z3_rcf_le\","
Z3_API_FUNCS+="\"_Z3_rcf_lt\","
Z3_API_FUNCS+="\"_Z3_rcf_mk_e\","
Z3_API_FUNCS+="\"_Z3_rcf_mk_infinitesimal\","
Z3_API_FUNCS+="\"_Z3_rcf_mk_pi\","
Z3_API_FUNCS+="\"_Z3_rcf_mk_rational\","
Z3_API_FUNCS+="\"_Z3_rcf_mk_roots\","
Z3_API_FUNCS+="\"_Z3_rcf_mk_small_int\","
Z3_API_FUNCS+="\"_Z3_rcf_mul\","
Z3_API_FUNCS+="\"_Z3_rcf_neg\","
Z3_API_FUNCS+="\"_Z3_rcf_neq\","
Z3_API_FUNCS+="\"_Z3_rcf_num_to_decimal_string\","
Z3_API_FUNCS+="\"_Z3_rcf_num_to_string\","
Z3_API_FUNCS+="\"_Z3_rcf_power\","
Z3_API_FUNCS+="\"_Z3_rcf_sub\","
Z3_API_FUNCS+="\"_Z3_read_interpolation_problem\","
Z3_API_FUNCS+="\"_Z3_reset_memory\","
Z3_API_FUNCS+="\"_Z3_set_ast_print_mode\","
Z3_API_FUNCS+="\"_Z3_set_error\","
Z3_API_FUNCS+="\"_Z3_set_param_value\","
Z3_API_FUNCS+="\"_Z3_simplify\","
Z3_API_FUNCS+="\"_Z3_simplify_ex\","
Z3_API_FUNCS+="\"_Z3_simplify_get_help\","
Z3_API_FUNCS+="\"_Z3_simplify_get_param_descrs\","
Z3_API_FUNCS+="\"_Z3_solver_assert\","
Z3_API_FUNCS+="\"_Z3_solver_assert_and_track\","
Z3_API_FUNCS+="\"_Z3_solver_check\","
Z3_API_FUNCS+="\"_Z3_solver_check_assumptions\","
Z3_API_FUNCS+="\"_Z3_solver_dec_ref\","
Z3_API_FUNCS+="\"_Z3_solver_get_assertions\","
Z3_API_FUNCS+="\"_Z3_solver_get_consequences\","
Z3_API_FUNCS+="\"_Z3_solver_get_help\","
Z3_API_FUNCS+="\"_Z3_solver_get_model\","
Z3_API_FUNCS+="\"_Z3_solver_get_num_scopes\","
Z3_API_FUNCS+="\"_Z3_solver_get_param_descrs\","
Z3_API_FUNCS+="\"_Z3_solver_get_proof\","
Z3_API_FUNCS+="\"_Z3_solver_get_reason_unknown\","
Z3_API_FUNCS+="\"_Z3_solver_get_statistics\","
Z3_API_FUNCS+="\"_Z3_solver_get_unsat_core\","
Z3_API_FUNCS+="\"_Z3_solver_inc_ref\","
Z3_API_FUNCS+="\"_Z3_solver_pop\","
Z3_API_FUNCS+="\"_Z3_solver_push\","
Z3_API_FUNCS+="\"_Z3_solver_reset\","
Z3_API_FUNCS+="\"_Z3_solver_set_params\","
Z3_API_FUNCS+="\"_Z3_solver_to_string\","
Z3_API_FUNCS+="\"_Z3_solver_translate\","
Z3_API_FUNCS+="\"_Z3_sort_to_ast\","
Z3_API_FUNCS+="\"_Z3_sort_to_string\","
Z3_API_FUNCS+="\"_Z3_stats_dec_ref\","
Z3_API_FUNCS+="\"_Z3_stats_get_double_value\","
Z3_API_FUNCS+="\"_Z3_stats_get_key\","
Z3_API_FUNCS+="\"_Z3_stats_get_uint_value\","
Z3_API_FUNCS+="\"_Z3_stats_inc_ref\","
Z3_API_FUNCS+="\"_Z3_stats_is_double\","
Z3_API_FUNCS+="\"_Z3_stats_is_uint\","
Z3_API_FUNCS+="\"_Z3_stats_size\","
Z3_API_FUNCS+="\"_Z3_stats_to_string\","
Z3_API_FUNCS+="\"_Z3_substitute\","
Z3_API_FUNCS+="\"_Z3_substitute_vars\","
Z3_API_FUNCS+="\"_Z3_tactic_and_then\","
Z3_API_FUNCS+="\"_Z3_tactic_apply\","
Z3_API_FUNCS+="\"_Z3_tactic_apply_ex\","
Z3_API_FUNCS+="\"_Z3_tactic_cond\","
Z3_API_FUNCS+="\"_Z3_tactic_dec_ref\","
Z3_API_FUNCS+="\"_Z3_tactic_fail\","
Z3_API_FUNCS+="\"_Z3_tactic_fail_if\","
Z3_API_FUNCS+="\"_Z3_tactic_fail_if_not_decided\","
Z3_API_FUNCS+="\"_Z3_tactic_get_descr\","
Z3_API_FUNCS+="\"_Z3_tactic_get_help\","
Z3_API_FUNCS+="\"_Z3_tactic_get_param_descrs\","
Z3_API_FUNCS+="\"_Z3_tactic_inc_ref\","
Z3_API_FUNCS+="\"_Z3_tactic_or_else\","
Z3_API_FUNCS+="\"_Z3_tactic_par_and_then\","
Z3_API_FUNCS+="\"_Z3_tactic_par_or\","
Z3_API_FUNCS+="\"_Z3_tactic_repeat\","
Z3_API_FUNCS+="\"_Z3_tactic_skip\","
Z3_API_FUNCS+="\"_Z3_tactic_try_for\","
Z3_API_FUNCS+="\"_Z3_tactic_using_params\","
Z3_API_FUNCS+="\"_Z3_tactic_when\","
Z3_API_FUNCS+="\"_Z3_to_app\","
Z3_API_FUNCS+="\"_Z3_to_func_decl\","
Z3_API_FUNCS+="\"_Z3_toggle_warning_messages\","
Z3_API_FUNCS+="\"_Z3_translate\","
Z3_API_FUNCS+="\"_Z3_update_param_value\","
Z3_API_FUNCS+="\"_Z3_update_term\","
Z3_API_FUNCS+="\"_Z3_write_interpolation_problem\""
Z3_API_FUNCS+="]'"