Commits

Leonardo de Moura  committed fa6b2a7

finished binding auto gen for Python and DotNet

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>

  • Participants
  • Parent commits 639f66d

Comments (0)

Files changed (8)

File scripts/mk_make.py

 add_lib('api', ['portfolio', 'user_plugin'])
 add_exe('shell', ['api', 'sat', 'extra_cmds'], exe_name='z3')
 add_exe('test', ['api', 'fuzzing'], exe_name='test-z3')
-API_files = ['z3_api.h', 'z3_poly.h']
+API_files = ['z3_api.h', 'z3_poly.h', 'z3_internal_types.h']
 add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', dll_name='z3', export_files=API_files)
 add_dot_net_dll('dotnet', ['api_dll'], 'bindings/dotnet/Microsoft.Z3', dll_name='Microsoft.Z3', assembly_info_dir='Properties')
 add_dot_net_dll('dotnetV3', ['api_dll'], 'bindings/dotnet/Microsoft.Z3V3', dll_name='Microsoft.Z3V3')
 mk_auto_src()
 mk_bindings(API_files)
 
-# mk_makefile()
+mk_makefile()
 

File scripts/mk_util.py

     fout.close()
     shutil.move(tmp, assemblyinfo)
     if VERBOSE:
-        print "Updated %s" % assemblyinfo
+        print "Updated '%s'" % assemblyinfo
 
 ADD_TACTIC_DATA=[]
 ADD_PROBE_DATA=[]
                 mk_def_file(c)
 
 def mk_bindings(api_files):
-    mk_z3consts_py(api_files)
-    mk_z3consts_donet(api_files)
+    if not ONLY_MAKEFILES:
+        mk_z3consts_py(api_files)
+        mk_z3consts_donet(api_files)
+        new_api_files = []
+        api = get_component('api')
+        for api_file in api_files:
+            api_file_path = api.find_file(api_file, api.name)
+            new_api_files.append('%s/%s' % (api_file_path.src_dir, api_file))
+        g = {}
+        g["API_FILES"] = new_api_files
+        execfile('scripts/update_api.py', g) # HACK
 
 # Extract enumeration types from API files, and add python definitions.
 def mk_z3consts_py(api_files):
     if VERBOSE:
         print "Generated '%s'" % ('%s/Enumerations.cs' % dotnet.src_dir)
 
-
+# Return the Component object named name
 def get_component(name):
     return _Name2Component[name]
+
+# Return the directory where the python bindings are located.
+def get_python_dir():
+    return PYTHON_DIR
+
+# Return true if in verbose mode
+def is_verbose():
+    return VERBOSE

File scripts/update_api.py

 ############################################
 # Copyright (c) 2012 Microsoft Corporation
 # 
-# Scripts for generate API bindings and definitions
+# Scripts for generating Makefiles and Visual 
+# Studio project files.
 #
 # Author: Leonardo de Moura (leonardo)
 ############################################
-import re
-import sys
-import os
-
-API_FILES = []
-
-def add_api_file(dir, file):
-    API_FILES.append("%s%s%s" % (dir, os.sep, file))
-
-add_api_file('lib', 'z3_api.h')
-add_api_file('lib', 'z3_internal_types.h')
-add_api_file('lib', 'z3_poly.h')
-
+from mk_util import *
+from mk_exception import *
+
+##########################################################
+# TODO: rewrite this file without using global variables.
+# This file is a big HACK.
+# It started as small simple script.
+# Now, it is too big, and is invoked from mk_make.py
+# The communication uses 
+#
+##########################################################
 
 #
 # Generate logging support and bindings
 #
-
-log_h   = open('lib%sapi_log_macros.h' % os.sep, 'w')
-log_c   = open('lib%sapi_log_macros.cpp' % os.sep, 'w')
-exe_c   = open('lib%sapi_commands.cpp' % os.sep, 'w')
-core_py = open('python%sz3core.py' % os.sep, 'w')
-dotnet_fileout = 'Microsoft.Z3%sNative.cs' % os.sep
+api_dir     = get_component('api').src_dir
+dotnet_dir  = get_component('dotnet').src_dir
+
+log_h   = open('%s/api_log_macros.h' % api_dir, 'w')
+log_c   = open('%s/api_log_macros.cpp' % api_dir, 'w')
+exe_c   = open('%s/api_commands.cpp' % api_dir, 'w')
+core_py = open('%s/z3core.py' % get_python_dir(), 'w')
+dotnet_fileout = '%s/Native.cs' % dotnet_dir
 ##
-log_h.write('// Automatically generated file, generator: update_api.py\n')
+log_h.write('// Automatically generated file\n')
 log_h.write('#include\"z3.h\"\n')
 ##
-log_c.write('// Automatically generated file, generator: update_api.py\n')
+log_c.write('// Automatically generated file\n')
 log_c.write('#include<iostream>\n')
 log_c.write('#include\"z3.h\"\n')
 log_c.write('#include\"api_log_macros.h\"\n')
 log_c.write('#include\"z3_logger.h\"\n')
 ##
-exe_c.write('// Automatically generated file, generator: update_api.py\n')
+exe_c.write('// Automatically generated file\n')
 exe_c.write('#include\"z3.h\"\n')
 exe_c.write('#include\"z3_internal.h\"\n')
 exe_c.write('#include\"z3_replayer.h\"\n')
 ##
 exe_c.write('void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg_ex(ctx, c)); }\n')
 ##
-core_py.write('# Automatically generated file, generator: update_api.py\n')
+core_py.write('# Automatically generated file\n')
 core_py.write('import sys, os\n')
 core_py.write('import ctypes\n')
 core_py.write('from z3types import *\n')
         for line in api:
             m = pat1.match(line)
             if m:
-                print line.strip()
                 eval(line)
     for k, v in Type2Str.iteritems():
         if is_obj(k):
     core_py.write("]\n")
 
 def extra_API(name, result, params):
-    print 'extra_API(%s)' % name
     mk_py_binding(name, result, params)
     reg_dotnet(name, result, params)
 
     global Type2Str
     global dotnet_fileout
     dotnet = open(dotnet_fileout, 'w')
-    dotnet.write('// Automatically generated file, generator: api.py\n')
+    dotnet.write('// Automatically generated file\n')
     dotnet.write('using System;\n')
     dotnet.write('using System.Collections.Generic;\n')
     dotnet.write('using System.Text;\n')
         file.write("_ARG%s" % i)
         i = i + 1
     file.write(") z3_log_ctx _LOG_CTX; ")
-    auxs = Set([])
+    auxs = set()
     i = 0
     for p in params:
         if log_param(p):
         file.write("_ARG%s" %i)
         i = i + 1
     file.write("); ")
-    auxs = Set([])
+    auxs = set()
     i = 0
     for p in params:
         if log_param(p):
 def def_API(name, result, params):
     global API2Id, next_id
     global log_h, log_c
-    print 'def_API(%s)' % name
-    # print "generating ", name
     mk_py_binding(name, result, params)
     reg_dotnet(name, result, params)
     API2Id[next_id] = name
     for api_file in API_FILES:
         api = open(api_file, 'r')
         for line in api:
-            m = pat1.match(line)
-            if m:
-                eval(line)
-            m = pat2.match(line)
-            if m:
-                eval(line)
-
-mk_z3consts_donet()
-mk_z3consts_py()
-mk_z3tactics_py()
+            try:
+                m = pat1.match(line)
+                if m:
+                    eval(line)
+                m = pat2.match(line)
+                if m:
+                    eval(line)
+            except Exception as ex:
+                print ex
+                raise MKException("Failed to process API definition: %s" % line)
 def_Types()
 def_APIs()
 mk_bindings()
 mk_dotnet()
 mk_dotnet_wrappers()
 
+if is_verbose():
+    print "Generated '%s'" % ('%s/api_log_macros.h' % api_dir)
+    print "Generated '%s'" % ('%s/api_log_macros.cpp' % api_dir)
+    print "Generated '%s'" % ('%s/api_commands.cpp' % api_dir)
+    print "Generated '%s'" % ('%s/z3core.py' % get_python_dir())
+    print "Generated '%s'" % ('%s/Native.cs' % dotnet_dir)

File src/api/api_commands.cpp

-// Automatically generated file, generator: update_api.py
-#include"z3.h"
-#include"z3_internal.h"
-#include"z3_replayer.h"
-void Z3_replacer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\n", Z3_get_error_msg_ex(ctx, c)); }
-void exec_Z3_mk_config(z3_replayer & in) {
-  Z3_config result = Z3_mk_config(
-    );
-  in.store_result(result);
-}
-void exec_Z3_del_config(z3_replayer & in) {
-  Z3_del_config(
-    reinterpret_cast<Z3_config>(in.get_obj(0)));
-}
-void exec_Z3_set_param_value(z3_replayer & in) {
-  Z3_set_param_value(
-    reinterpret_cast<Z3_config>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_str(2));
-}
-void exec_Z3_mk_context(z3_replayer & in) {
-  Z3_context result = Z3_mk_context(
-    reinterpret_cast<Z3_config>(in.get_obj(0)));
-  in.store_result(result);
-  Z3_set_error_handler(result, Z3_replacer_error_handler);}
-void exec_Z3_mk_context_rc(z3_replayer & in) {
-  Z3_context result = Z3_mk_context_rc(
-    reinterpret_cast<Z3_config>(in.get_obj(0)));
-  in.store_result(result);
-  Z3_set_error_handler(result, Z3_replacer_error_handler);}
-void exec_Z3_del_context(z3_replayer & in) {
-  Z3_del_context(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-}
-void exec_Z3_inc_ref(z3_replayer & in) {
-  Z3_inc_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_dec_ref(z3_replayer & in) {
-  Z3_dec_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_update_param_value(z3_replayer & in) {
-  Z3_update_param_value(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_str(2));
-}
-void exec_Z3_get_param_value(z3_replayer & in) {
-  Z3_get_param_value(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_str_addr(2));
-}
-void exec_Z3_interrupt(z3_replayer & in) {
-  Z3_interrupt(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-}
-void exec_Z3_mk_params(z3_replayer & in) {
-  Z3_params result = Z3_mk_params(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-  in.store_result(result);
-}
-void exec_Z3_params_inc_ref(z3_replayer & in) {
-  Z3_params_inc_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_params>(in.get_obj(1)));
-}
-void exec_Z3_params_dec_ref(z3_replayer & in) {
-  Z3_params_dec_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_params>(in.get_obj(1)));
-}
-void exec_Z3_params_set_bool(z3_replayer & in) {
-  Z3_params_set_bool(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_params>(in.get_obj(1)),
-    in.get_symbol(2),
-    in.get_bool(3));
-}
-void exec_Z3_params_set_uint(z3_replayer & in) {
-  Z3_params_set_uint(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_params>(in.get_obj(1)),
-    in.get_symbol(2),
-    in.get_uint(3));
-}
-void exec_Z3_params_set_double(z3_replayer & in) {
-  Z3_params_set_double(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_params>(in.get_obj(1)),
-    in.get_symbol(2),
-    in.get_double(3));
-}
-void exec_Z3_params_set_symbol(z3_replayer & in) {
-  Z3_params_set_symbol(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_params>(in.get_obj(1)),
-    in.get_symbol(2),
-    in.get_symbol(3));
-}
-void exec_Z3_params_to_string(z3_replayer & in) {
-  Z3_params_to_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_params>(in.get_obj(1)));
-}
-void exec_Z3_params_validate(z3_replayer & in) {
-  Z3_params_validate(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_params>(in.get_obj(1)),
-    reinterpret_cast<Z3_param_descrs>(in.get_obj(2)));
-}
-void exec_Z3_param_descrs_inc_ref(z3_replayer & in) {
-  Z3_param_descrs_inc_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_param_descrs>(in.get_obj(1)));
-}
-void exec_Z3_param_descrs_dec_ref(z3_replayer & in) {
-  Z3_param_descrs_dec_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_param_descrs>(in.get_obj(1)));
-}
-void exec_Z3_param_descrs_get_kind(z3_replayer & in) {
-  Z3_param_descrs_get_kind(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_param_descrs>(in.get_obj(1)),
-    in.get_symbol(2));
-}
-void exec_Z3_param_descrs_size(z3_replayer & in) {
-  Z3_param_descrs_size(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_param_descrs>(in.get_obj(1)));
-}
-void exec_Z3_param_descrs_get_name(z3_replayer & in) {
-  Z3_param_descrs_get_name(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    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_mk_int_symbol(z3_replayer & in) {
-  Z3_mk_int_symbol(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_int(1));
-}
-void exec_Z3_mk_string_symbol(z3_replayer & in) {
-  Z3_mk_string_symbol(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1));
-}
-void exec_Z3_mk_uninterpreted_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_uninterpreted_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1));
-  in.store_result(result);
-}
-void exec_Z3_mk_bool_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_bool_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-  in.store_result(result);
-}
-void exec_Z3_mk_int_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_int_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-  in.store_result(result);
-}
-void exec_Z3_mk_real_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_real_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bv_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_bv_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1));
-  in.store_result(result);
-}
-void exec_Z3_mk_finite_domain_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_finite_domain_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1),
-    in.get_uint64(2));
-  in.store_result(result);
-}
-void exec_Z3_mk_array_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_array_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_tuple_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_tuple_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1),
-    in.get_uint(2),
-    in.get_symbol_array(3),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(4)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(5)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_array(6)));
-  in.store_result(result);
-}
-void exec_Z3_mk_enumeration_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_enumeration_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1),
-    in.get_uint(2),
-    in.get_symbol_array(3),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_array(4)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_array(5)));
-  in.store_result(result);
-}
-void exec_Z3_mk_list_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_list_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(3)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(4)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(5)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(6)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(7)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(8)));
-  in.store_result(result);
-}
-void exec_Z3_mk_constructor(z3_replayer & in) {
-  Z3_constructor result = Z3_mk_constructor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1),
-    in.get_symbol(2),
-    in.get_uint(3),
-    in.get_symbol_array(4),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(5)),
-    in.get_uint_array(6));
-  in.store_result(result);
-}
-void exec_Z3_del_constructor(z3_replayer & in) {
-  Z3_del_constructor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_constructor>(in.get_obj(1)));
-}
-void exec_Z3_mk_datatype(z3_replayer & in) {
-  Z3_sort result = Z3_mk_datatype(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1),
-    in.get_uint(2),
-    reinterpret_cast<Z3_constructor*>(in.get_obj_array(3)));
-  in.store_result(result);
-}
-void exec_Z3_mk_constructor_list(z3_replayer & in) {
-  Z3_constructor_list result = Z3_mk_constructor_list(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_constructor*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_del_constructor_list(z3_replayer & in) {
-  Z3_del_constructor_list(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_constructor_list>(in.get_obj(1)));
-}
-void exec_Z3_mk_datatypes(z3_replayer & in) {
-  Z3_mk_datatypes(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    in.get_symbol_array(2),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(3)),
-    reinterpret_cast<Z3_constructor_list*>(in.get_obj_array(4)));
-}
-void exec_Z3_query_constructor(z3_replayer & in) {
-  Z3_query_constructor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_constructor>(in.get_obj(1)),
-    in.get_uint(2),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(3)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_addr(4)),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_array(5)));
-}
-void exec_Z3_mk_func_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_mk_func_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1),
-    in.get_uint(2),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(3)),
-    reinterpret_cast<Z3_sort>(in.get_obj(4)));
-  in.store_result(result);
-}
-void exec_Z3_mk_app(z3_replayer & in) {
-  Z3_ast result = Z3_mk_app(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(3)));
-  in.store_result(result);
-}
-void exec_Z3_mk_const(z3_replayer & in) {
-  Z3_ast result = Z3_mk_const(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_fresh_func_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_mk_fresh_func_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_uint(2),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(3)),
-    reinterpret_cast<Z3_sort>(in.get_obj(4)));
-  in.store_result(result);
-}
-void exec_Z3_mk_fresh_const(z3_replayer & in) {
-  Z3_ast result = Z3_mk_fresh_const(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_true(z3_replayer & in) {
-  Z3_ast result = Z3_mk_true(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-  in.store_result(result);
-}
-void exec_Z3_mk_false(z3_replayer & in) {
-  Z3_ast result = Z3_mk_false(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-  in.store_result(result);
-}
-void exec_Z3_mk_eq(z3_replayer & in) {
-  Z3_ast result = Z3_mk_eq(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_distinct(z3_replayer & in) {
-  Z3_ast result = Z3_mk_distinct(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_not(z3_replayer & in) {
-  Z3_ast result = Z3_mk_not(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_ite(z3_replayer & in) {
-  Z3_ast result = Z3_mk_ite(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)),
-    reinterpret_cast<Z3_ast>(in.get_obj(3)));
-  in.store_result(result);
-}
-void exec_Z3_mk_iff(z3_replayer & in) {
-  Z3_ast result = Z3_mk_iff(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_implies(z3_replayer & in) {
-  Z3_ast result = Z3_mk_implies(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_xor(z3_replayer & in) {
-  Z3_ast result = Z3_mk_xor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_and(z3_replayer & in) {
-  Z3_ast result = Z3_mk_and(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_or(z3_replayer & in) {
-  Z3_ast result = Z3_mk_or(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_add(z3_replayer & in) {
-  Z3_ast result = Z3_mk_add(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_mul(z3_replayer & in) {
-  Z3_ast result = Z3_mk_mul(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_sub(z3_replayer & in) {
-  Z3_ast result = Z3_mk_sub(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_unary_minus(z3_replayer & in) {
-  Z3_ast result = Z3_mk_unary_minus(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_div(z3_replayer & in) {
-  Z3_ast result = Z3_mk_div(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_mod(z3_replayer & in) {
-  Z3_ast result = Z3_mk_mod(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_rem(z3_replayer & in) {
-  Z3_ast result = Z3_mk_rem(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_power(z3_replayer & in) {
-  Z3_ast result = Z3_mk_power(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_lt(z3_replayer & in) {
-  Z3_ast result = Z3_mk_lt(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_le(z3_replayer & in) {
-  Z3_ast result = Z3_mk_le(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_gt(z3_replayer & in) {
-  Z3_ast result = Z3_mk_gt(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_ge(z3_replayer & in) {
-  Z3_ast result = Z3_mk_ge(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_int2real(z3_replayer & in) {
-  Z3_ast result = Z3_mk_int2real(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_real2int(z3_replayer & in) {
-  Z3_ast result = Z3_mk_real2int(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_is_int(z3_replayer & in) {
-  Z3_ast result = Z3_mk_is_int(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvnot(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvnot(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvredand(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvredand(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvredor(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvredor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvand(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvand(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvor(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvxor(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvxor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvnand(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvnand(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvnor(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvnor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvxnor(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvxnor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvneg(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvneg(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvadd(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvadd(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsub(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsub(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvmul(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvmul(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvudiv(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvudiv(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsdiv(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsdiv(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvurem(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvurem(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsrem(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsrem(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsmod(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsmod(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvult(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvult(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvslt(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvslt(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvule(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvule(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsle(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsle(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvuge(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvuge(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsge(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsge(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvugt(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvugt(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsgt(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsgt(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_concat(z3_replayer & in) {
-  Z3_ast result = Z3_mk_concat(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_extract(z3_replayer & in) {
-  Z3_ast result = Z3_mk_extract(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    in.get_uint(2),
-    reinterpret_cast<Z3_ast>(in.get_obj(3)));
-  in.store_result(result);
-}
-void exec_Z3_mk_sign_ext(z3_replayer & in) {
-  Z3_ast result = Z3_mk_sign_ext(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_zero_ext(z3_replayer & in) {
-  Z3_ast result = Z3_mk_zero_ext(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_repeat(z3_replayer & in) {
-  Z3_ast result = Z3_mk_repeat(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvshl(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvshl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvlshr(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvlshr(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvashr(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvashr(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_rotate_left(z3_replayer & in) {
-  Z3_ast result = Z3_mk_rotate_left(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_rotate_right(z3_replayer & in) {
-  Z3_ast result = Z3_mk_rotate_right(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_ext_rotate_left(z3_replayer & in) {
-  Z3_ast result = Z3_mk_ext_rotate_left(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_ext_rotate_right(z3_replayer & in) {
-  Z3_ast result = Z3_mk_ext_rotate_right(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_int2bv(z3_replayer & in) {
-  Z3_ast result = Z3_mk_int2bv(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bv2int(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bv2int(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_bool(2));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvadd_no_overflow(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvadd_no_overflow(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)),
-    in.get_bool(3));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvadd_no_underflow(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvadd_no_underflow(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsub_no_overflow(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsub_no_overflow(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsub_no_underflow(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsub_no_underflow(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)),
-    in.get_bool(3));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvsdiv_no_overflow(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvsdiv_no_overflow(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvneg_no_overflow(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvneg_no_overflow(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvmul_no_overflow(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvmul_no_overflow(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)),
-    in.get_bool(3));
-  in.store_result(result);
-}
-void exec_Z3_mk_bvmul_no_underflow(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bvmul_no_underflow(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_select(z3_replayer & in) {
-  Z3_ast result = Z3_mk_select(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_store(z3_replayer & in) {
-  Z3_ast result = Z3_mk_store(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)),
-    reinterpret_cast<Z3_ast>(in.get_obj(3)));
-  in.store_result(result);
-}
-void exec_Z3_mk_const_array(z3_replayer & in) {
-  Z3_ast result = Z3_mk_const_array(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_map(z3_replayer & in) {
-  Z3_ast result = Z3_mk_map(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(3)));
-  in.store_result(result);
-}
-void exec_Z3_mk_array_default(z3_replayer & in) {
-  Z3_ast result = Z3_mk_array_default(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_sort(z3_replayer & in) {
-  Z3_sort result = Z3_mk_set_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_empty_set(z3_replayer & in) {
-  Z3_ast result = Z3_mk_empty_set(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_full_set(z3_replayer & in) {
-  Z3_ast result = Z3_mk_full_set(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_add(z3_replayer & in) {
-  Z3_ast result = Z3_mk_set_add(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_del(z3_replayer & in) {
-  Z3_ast result = Z3_mk_set_del(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_union(z3_replayer & in) {
-  Z3_ast result = Z3_mk_set_union(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_intersect(z3_replayer & in) {
-  Z3_ast result = Z3_mk_set_intersect(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_difference(z3_replayer & in) {
-  Z3_ast result = Z3_mk_set_difference(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_complement(z3_replayer & in) {
-  Z3_ast result = Z3_mk_set_complement(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_member(z3_replayer & in) {
-  Z3_ast result = Z3_mk_set_member(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_set_subset(z3_replayer & in) {
-  Z3_ast result = Z3_mk_set_subset(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_numeral(z3_replayer & in) {
-  Z3_ast result = Z3_mk_numeral(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_real(z3_replayer & in) {
-  Z3_ast result = Z3_mk_real(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_int(1),
-    in.get_int(2));
-  in.store_result(result);
-}
-void exec_Z3_mk_int(z3_replayer & in) {
-  Z3_ast result = Z3_mk_int(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_int(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_unsigned_int(z3_replayer & in) {
-  Z3_ast result = Z3_mk_unsigned_int(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_int64(z3_replayer & in) {
-  Z3_ast result = Z3_mk_int64(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_int64(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_unsigned_int64(z3_replayer & in) {
-  Z3_ast result = Z3_mk_unsigned_int64(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint64(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_pattern(z3_replayer & in) {
-  Z3_pattern result = Z3_mk_pattern(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_bound(z3_replayer & in) {
-  Z3_ast result = Z3_mk_bound(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_mk_forall(z3_replayer & in) {
-  Z3_ast result = Z3_mk_forall(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    in.get_uint(2),
-    reinterpret_cast<Z3_pattern*>(in.get_obj_array(3)),
-    in.get_uint(4),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(5)),
-    in.get_symbol_array(6),
-    reinterpret_cast<Z3_ast>(in.get_obj(7)));
-  in.store_result(result);
-}
-void exec_Z3_mk_exists(z3_replayer & in) {
-  Z3_ast result = Z3_mk_exists(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    in.get_uint(2),
-    reinterpret_cast<Z3_pattern*>(in.get_obj_array(3)),
-    in.get_uint(4),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(5)),
-    in.get_symbol_array(6),
-    reinterpret_cast<Z3_ast>(in.get_obj(7)));
-  in.store_result(result);
-}
-void exec_Z3_mk_quantifier(z3_replayer & in) {
-  Z3_ast result = Z3_mk_quantifier(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_bool(1),
-    in.get_uint(2),
-    in.get_uint(3),
-    reinterpret_cast<Z3_pattern*>(in.get_obj_array(4)),
-    in.get_uint(5),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(6)),
-    in.get_symbol_array(7),
-    reinterpret_cast<Z3_ast>(in.get_obj(8)));
-  in.store_result(result);
-}
-void exec_Z3_mk_quantifier_ex(z3_replayer & in) {
-  Z3_ast result = Z3_mk_quantifier_ex(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_bool(1),
-    in.get_uint(2),
-    in.get_symbol(3),
-    in.get_symbol(4),
-    in.get_uint(5),
-    reinterpret_cast<Z3_pattern*>(in.get_obj_array(6)),
-    in.get_uint(7),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(8)),
-    in.get_uint(9),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(10)),
-    in.get_symbol_array(11),
-    reinterpret_cast<Z3_ast>(in.get_obj(12)));
-  in.store_result(result);
-}
-void exec_Z3_mk_forall_const(z3_replayer & in) {
-  Z3_ast result = Z3_mk_forall_const(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    in.get_uint(2),
-    reinterpret_cast<Z3_app*>(in.get_obj_array(3)),
-    in.get_uint(4),
-    reinterpret_cast<Z3_pattern*>(in.get_obj_array(5)),
-    reinterpret_cast<Z3_ast>(in.get_obj(6)));
-  in.store_result(result);
-}
-void exec_Z3_mk_exists_const(z3_replayer & in) {
-  Z3_ast result = Z3_mk_exists_const(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1),
-    in.get_uint(2),
-    reinterpret_cast<Z3_app*>(in.get_obj_array(3)),
-    in.get_uint(4),
-    reinterpret_cast<Z3_pattern*>(in.get_obj_array(5)),
-    reinterpret_cast<Z3_ast>(in.get_obj(6)));
-  in.store_result(result);
-}
-void exec_Z3_mk_quantifier_const(z3_replayer & in) {
-  Z3_ast result = Z3_mk_quantifier_const(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_bool(1),
-    in.get_uint(2),
-    in.get_uint(3),
-    reinterpret_cast<Z3_app*>(in.get_obj_array(4)),
-    in.get_uint(5),
-    reinterpret_cast<Z3_pattern*>(in.get_obj_array(6)),
-    reinterpret_cast<Z3_ast>(in.get_obj(7)));
-  in.store_result(result);
-}
-void exec_Z3_mk_quantifier_const_ex(z3_replayer & in) {
-  Z3_ast result = Z3_mk_quantifier_const_ex(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_bool(1),
-    in.get_uint(2),
-    in.get_symbol(3),
-    in.get_symbol(4),
-    in.get_uint(5),
-    reinterpret_cast<Z3_app*>(in.get_obj_array(6)),
-    in.get_uint(7),
-    reinterpret_cast<Z3_pattern*>(in.get_obj_array(8)),
-    in.get_uint(9),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(10)),
-    reinterpret_cast<Z3_ast>(in.get_obj(11)));
-  in.store_result(result);
-}
-void exec_Z3_get_symbol_kind(z3_replayer & in) {
-  Z3_get_symbol_kind(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1));
-}
-void exec_Z3_get_symbol_int(z3_replayer & in) {
-  Z3_get_symbol_int(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1));
-}
-void exec_Z3_get_symbol_string(z3_replayer & in) {
-  Z3_get_symbol_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_symbol(1));
-}
-void exec_Z3_get_sort_name(z3_replayer & in) {
-  Z3_get_sort_name(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-}
-void exec_Z3_get_sort_id(z3_replayer & in) {
-  Z3_get_sort_id(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-}
-void exec_Z3_sort_to_ast(z3_replayer & in) {
-  Z3_ast result = Z3_sort_to_ast(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_is_eq_sort(z3_replayer & in) {
-  Z3_is_eq_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-}
-void exec_Z3_get_sort_kind(z3_replayer & in) {
-  Z3_get_sort_kind(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-}
-void exec_Z3_get_bv_sort_size(z3_replayer & in) {
-  Z3_get_bv_sort_size(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-}
-void exec_Z3_get_finite_domain_sort_size(z3_replayer & in) {
-  Z3_get_finite_domain_sort_size(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    in.get_uint64_addr(2));
-}
-void exec_Z3_get_array_sort_domain(z3_replayer & in) {
-  Z3_sort result = Z3_get_array_sort_domain(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_array_sort_range(z3_replayer & in) {
-  Z3_sort result = Z3_get_array_sort_range(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_tuple_sort_mk_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_get_tuple_sort_mk_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_tuple_sort_num_fields(z3_replayer & in) {
-  Z3_get_tuple_sort_num_fields(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-}
-void exec_Z3_get_tuple_sort_field_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_get_tuple_sort_field_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_datatype_sort_num_constructors(z3_replayer & in) {
-  Z3_get_datatype_sort_num_constructors(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-}
-void exec_Z3_get_datatype_sort_constructor(z3_replayer & in) {
-  Z3_func_decl result = Z3_get_datatype_sort_constructor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_datatype_sort_recognizer(z3_replayer & in) {
-  Z3_func_decl result = Z3_get_datatype_sort_recognizer(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_datatype_sort_constructor_accessor(z3_replayer & in) {
-  Z3_func_decl result = Z3_get_datatype_sort_constructor_accessor(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    in.get_uint(2),
-    in.get_uint(3));
-  in.store_result(result);
-}
-void exec_Z3_get_relation_arity(z3_replayer & in) {
-  Z3_get_relation_arity(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-}
-void exec_Z3_get_relation_column(z3_replayer & in) {
-  Z3_sort result = Z3_get_relation_column(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_func_decl_to_ast(z3_replayer & in) {
-  Z3_ast result = Z3_func_decl_to_ast(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_is_eq_func_decl(z3_replayer & in) {
-  Z3_is_eq_func_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(2)));
-}
-void exec_Z3_get_func_decl_id(z3_replayer & in) {
-  Z3_get_func_decl_id(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-}
-void exec_Z3_get_decl_name(z3_replayer & in) {
-  Z3_get_decl_name(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-}
-void exec_Z3_get_decl_kind(z3_replayer & in) {
-  Z3_get_decl_kind(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-}
-void exec_Z3_get_domain_size(z3_replayer & in) {
-  Z3_get_domain_size(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-}
-void exec_Z3_get_arity(z3_replayer & in) {
-  Z3_get_arity(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-}
-void exec_Z3_get_domain(z3_replayer & in) {
-  Z3_sort result = Z3_get_domain(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_range(z3_replayer & in) {
-  Z3_sort result = Z3_get_range(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_decl_num_parameters(z3_replayer & in) {
-  Z3_get_decl_num_parameters(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-}
-void exec_Z3_get_decl_parameter_kind(z3_replayer & in) {
-  Z3_get_decl_parameter_kind(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-}
-void exec_Z3_get_decl_int_parameter(z3_replayer & in) {
-  Z3_get_decl_int_parameter(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-}
-void exec_Z3_get_decl_double_parameter(z3_replayer & in) {
-  Z3_get_decl_double_parameter(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-}
-void exec_Z3_get_decl_symbol_parameter(z3_replayer & in) {
-  Z3_get_decl_symbol_parameter(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-}
-void exec_Z3_get_decl_sort_parameter(z3_replayer & in) {
-  Z3_sort result = Z3_get_decl_sort_parameter(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_decl_ast_parameter(z3_replayer & in) {
-  Z3_ast result = Z3_get_decl_ast_parameter(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_decl_func_decl_parameter(z3_replayer & in) {
-  Z3_func_decl result = Z3_get_decl_func_decl_parameter(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_decl_rational_parameter(z3_replayer & in) {
-  Z3_get_decl_rational_parameter(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)),
-    in.get_uint(2));
-}
-void exec_Z3_app_to_ast(z3_replayer & in) {
-  Z3_ast result = Z3_app_to_ast(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_app>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_app_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_get_app_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_app>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_app_num_args(z3_replayer & in) {
-  Z3_get_app_num_args(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_app>(in.get_obj(1)));
-}
-void exec_Z3_get_app_arg(z3_replayer & in) {
-  Z3_ast result = Z3_get_app_arg(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_app>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_is_eq_ast(z3_replayer & in) {
-  Z3_is_eq_ast(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)));
-}
-void exec_Z3_get_ast_id(z3_replayer & in) {
-  Z3_get_ast_id(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_ast_hash(z3_replayer & in) {
-  Z3_get_ast_hash(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_sort(z3_replayer & in) {
-  Z3_sort result = Z3_get_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_is_well_sorted(z3_replayer & in) {
-  Z3_is_well_sorted(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_bool_value(z3_replayer & in) {
-  Z3_get_bool_value(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_ast_kind(z3_replayer & in) {
-  Z3_get_ast_kind(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_is_app(z3_replayer & in) {
-  Z3_is_app(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_is_numeral_ast(z3_replayer & in) {
-  Z3_is_numeral_ast(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_is_algebraic_number(z3_replayer & in) {
-  Z3_is_algebraic_number(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_to_app(z3_replayer & in) {
-  Z3_app result = Z3_to_app(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_to_func_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_to_func_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_numeral_string(z3_replayer & in) {
-  Z3_get_numeral_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_numeral_decimal_string(z3_replayer & in) {
-  Z3_get_numeral_decimal_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2));
-}
-void exec_Z3_get_numerator(z3_replayer & in) {
-  Z3_ast result = Z3_get_numerator(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_denominator(z3_replayer & in) {
-  Z3_ast result = Z3_get_denominator(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_numeral_small(z3_replayer & in) {
-  Z3_get_numeral_small(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_int64_addr(2),
-    in.get_int64_addr(3));
-}
-void exec_Z3_get_numeral_int(z3_replayer & in) {
-  Z3_get_numeral_int(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_int_addr(2));
-}
-void exec_Z3_get_numeral_uint(z3_replayer & in) {
-  Z3_get_numeral_uint(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint_addr(2));
-}
-void exec_Z3_get_numeral_uint64(z3_replayer & in) {
-  Z3_get_numeral_uint64(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint64_addr(2));
-}
-void exec_Z3_get_numeral_int64(z3_replayer & in) {
-  Z3_get_numeral_int64(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_int64_addr(2));
-}
-void exec_Z3_get_numeral_rational_int64(z3_replayer & in) {
-  Z3_get_numeral_rational_int64(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_int64_addr(2),
-    in.get_int64_addr(3));
-}
-void exec_Z3_get_algebraic_number_lower(z3_replayer & in) {
-  Z3_ast result = Z3_get_algebraic_number_lower(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_algebraic_number_upper(z3_replayer & in) {
-  Z3_ast result = Z3_get_algebraic_number_upper(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_pattern_to_ast(z3_replayer & in) {
-  Z3_ast result = Z3_pattern_to_ast(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_pattern>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_get_pattern_num_terms(z3_replayer & in) {
-  Z3_get_pattern_num_terms(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_pattern>(in.get_obj(1)));
-}
-void exec_Z3_get_pattern(z3_replayer & in) {
-  Z3_ast result = Z3_get_pattern(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_pattern>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_index_value(z3_replayer & in) {
-  Z3_get_index_value(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_is_quantifier_forall(z3_replayer & in) {
-  Z3_is_quantifier_forall(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_quantifier_weight(z3_replayer & in) {
-  Z3_get_quantifier_weight(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_quantifier_num_patterns(z3_replayer & in) {
-  Z3_get_quantifier_num_patterns(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_quantifier_pattern_ast(z3_replayer & in) {
-  Z3_pattern result = Z3_get_quantifier_pattern_ast(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_quantifier_num_no_patterns(z3_replayer & in) {
-  Z3_get_quantifier_num_no_patterns(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_quantifier_no_pattern_ast(z3_replayer & in) {
-  Z3_ast result = Z3_get_quantifier_no_pattern_ast(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_quantifier_num_bound(z3_replayer & in) {
-  Z3_get_quantifier_num_bound(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_quantifier_bound_name(z3_replayer & in) {
-  Z3_get_quantifier_bound_name(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2));
-}
-void exec_Z3_get_quantifier_bound_sort(z3_replayer & in) {
-  Z3_sort result = Z3_get_quantifier_bound_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_get_quantifier_body(z3_replayer & in) {
-  Z3_ast result = Z3_get_quantifier_body(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_simplify(z3_replayer & in) {
-  Z3_ast result = Z3_simplify(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_simplify_ex(z3_replayer & in) {
-  Z3_ast result = Z3_simplify_ex(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_params>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_simplify_get_help(z3_replayer & in) {
-  Z3_simplify_get_help(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-}
-void exec_Z3_simplify_get_param_descrs(z3_replayer & in) {
-  Z3_param_descrs result = Z3_simplify_get_param_descrs(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-  in.store_result(result);
-}
-void exec_Z3_update_term(z3_replayer & in) {
-  Z3_ast result = Z3_update_term(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(3)));
-  in.store_result(result);
-}
-void exec_Z3_substitute(z3_replayer & in) {
-  Z3_ast result = Z3_substitute(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(3)),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(4)));
-  in.store_result(result);
-}
-void exec_Z3_substitute_vars(z3_replayer & in) {
-  Z3_ast result = Z3_substitute_vars(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    in.get_uint(2),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(3)));
-  in.store_result(result);
-}
-void exec_Z3_translate(z3_replayer & in) {
-  Z3_ast result = Z3_translate(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)),
-    reinterpret_cast<Z3_context>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_model_inc_ref(z3_replayer & in) {
-  Z3_model_inc_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)));
-}
-void exec_Z3_model_dec_ref(z3_replayer & in) {
-  Z3_model_dec_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)));
-}
-void exec_Z3_model_eval(z3_replayer & in) {
-  Z3_model_eval(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)),
-    reinterpret_cast<Z3_ast>(in.get_obj(2)),
-    in.get_bool(3),
-    reinterpret_cast<Z3_ast*>(in.get_obj_addr(4)));
-}
-void exec_Z3_model_get_const_interp(z3_replayer & in) {
-  Z3_ast result = Z3_model_get_const_interp(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_model_get_func_interp(z3_replayer & in) {
-  Z3_func_interp result = Z3_model_get_func_interp(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_model_get_num_consts(z3_replayer & in) {
-  Z3_model_get_num_consts(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)));
-}
-void exec_Z3_model_get_const_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_model_get_const_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_model_get_num_funcs(z3_replayer & in) {
-  Z3_model_get_num_funcs(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)));
-}
-void exec_Z3_model_get_func_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_model_get_func_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_model_get_num_sorts(z3_replayer & in) {
-  Z3_model_get_num_sorts(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)));
-}
-void exec_Z3_model_get_sort(z3_replayer & in) {
-  Z3_sort result = Z3_model_get_sort(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_model_get_sort_universe(z3_replayer & in) {
-  Z3_ast_vector result = Z3_model_get_sort_universe(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)),
-    reinterpret_cast<Z3_sort>(in.get_obj(2)));
-  in.store_result(result);
-}
-void exec_Z3_is_as_array(z3_replayer & in) {
-  Z3_is_as_array(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_get_as_array_func_decl(z3_replayer & in) {
-  Z3_func_decl result = Z3_get_as_array_func_decl(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_func_interp_inc_ref(z3_replayer & in) {
-  Z3_func_interp_inc_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_interp>(in.get_obj(1)));
-}
-void exec_Z3_func_interp_dec_ref(z3_replayer & in) {
-  Z3_func_interp_dec_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_interp>(in.get_obj(1)));
-}
-void exec_Z3_func_interp_get_num_entries(z3_replayer & in) {
-  Z3_func_interp_get_num_entries(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_interp>(in.get_obj(1)));
-}
-void exec_Z3_func_interp_get_entry(z3_replayer & in) {
-  Z3_func_entry result = Z3_func_interp_get_entry(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_interp>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_func_interp_get_else(z3_replayer & in) {
-  Z3_ast result = Z3_func_interp_get_else(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_interp>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_func_interp_get_arity(z3_replayer & in) {
-  Z3_func_interp_get_arity(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_interp>(in.get_obj(1)));
-}
-void exec_Z3_func_entry_inc_ref(z3_replayer & in) {
-  Z3_func_entry_inc_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_entry>(in.get_obj(1)));
-}
-void exec_Z3_func_entry_dec_ref(z3_replayer & in) {
-  Z3_func_entry_dec_ref(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_entry>(in.get_obj(1)));
-}
-void exec_Z3_func_entry_get_value(z3_replayer & in) {
-  Z3_ast result = Z3_func_entry_get_value(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_entry>(in.get_obj(1)));
-  in.store_result(result);
-}
-void exec_Z3_func_entry_get_num_args(z3_replayer & in) {
-  Z3_func_entry_get_num_args(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_entry>(in.get_obj(1)));
-}
-void exec_Z3_func_entry_get_arg(z3_replayer & in) {
-  Z3_ast result = Z3_func_entry_get_arg(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_entry>(in.get_obj(1)),
-    in.get_uint(2));
-  in.store_result(result);
-}
-void exec_Z3_toggle_warning_messages(z3_replayer & in) {
-  Z3_toggle_warning_messages(
-    in.get_bool(0));
-}
-void exec_Z3_set_ast_print_mode(z3_replayer & in) {
-  Z3_set_ast_print_mode(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    static_cast<Z3_ast_print_mode>(in.get_uint(1)));
-}
-void exec_Z3_ast_to_string(z3_replayer & in) {
-  Z3_ast_to_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_ast>(in.get_obj(1)));
-}
-void exec_Z3_pattern_to_string(z3_replayer & in) {
-  Z3_pattern_to_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_pattern>(in.get_obj(1)));
-}
-void exec_Z3_sort_to_string(z3_replayer & in) {
-  Z3_sort_to_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_sort>(in.get_obj(1)));
-}
-void exec_Z3_func_decl_to_string(z3_replayer & in) {
-  Z3_func_decl_to_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_func_decl>(in.get_obj(1)));
-}
-void exec_Z3_model_to_string(z3_replayer & in) {
-  Z3_model_to_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    reinterpret_cast<Z3_model>(in.get_obj(1)));
-}
-void exec_Z3_benchmark_to_smtlib_string(z3_replayer & in) {
-  Z3_benchmark_to_smtlib_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_str(2),
-    in.get_str(3),
-    in.get_str(4),
-    in.get_uint(5),
-    reinterpret_cast<Z3_ast*>(in.get_obj_array(6)),
-    reinterpret_cast<Z3_ast>(in.get_obj(7)));
-}
-void exec_Z3_parse_smtlib2_string(z3_replayer & in) {
-  Z3_ast result = Z3_parse_smtlib2_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_uint(2),
-    in.get_symbol_array(3),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(4)),
-    in.get_uint(5),
-    in.get_symbol_array(6),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_array(7)));
-  in.store_result(result);
-}
-void exec_Z3_parse_smtlib2_file(z3_replayer & in) {
-  Z3_ast result = Z3_parse_smtlib2_file(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_uint(2),
-    in.get_symbol_array(3),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(4)),
-    in.get_uint(5),
-    in.get_symbol_array(6),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_array(7)));
-  in.store_result(result);
-}
-void exec_Z3_parse_smtlib_string(z3_replayer & in) {
-  Z3_parse_smtlib_string(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_uint(2),
-    in.get_symbol_array(3),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(4)),
-    in.get_uint(5),
-    in.get_symbol_array(6),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_array(7)));
-}
-void exec_Z3_parse_smtlib_file(z3_replayer & in) {
-  Z3_parse_smtlib_file(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_str(1),
-    in.get_uint(2),
-    in.get_symbol_array(3),
-    reinterpret_cast<Z3_sort*>(in.get_obj_array(4)),
-    in.get_uint(5),
-    in.get_symbol_array(6),
-    reinterpret_cast<Z3_func_decl*>(in.get_obj_array(7)));
-}
-void exec_Z3_get_smtlib_num_formulas(z3_replayer & in) {
-  Z3_get_smtlib_num_formulas(
-    reinterpret_cast<Z3_context>(in.get_obj(0)));
-}
-void exec_Z3_get_smtlib_formula(z3_replayer & in) {
-  Z3_ast result = Z3_get_smtlib_formula(
-    reinterpret_cast<Z3_context>(in.get_obj(0)),
-    in.get_uint(1));
-  in.store_result(result);
-}