diff --git a/README-CMake.md b/README-CMake.md
index c004f5c7c..dc1f33ec6 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -292,6 +292,9 @@ The following useful options can be passed to CMake whilst configuring.
 * ``Z3_INSTALL_JAVA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JAVA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Java bindings.
 * ``Z3_JAVA_JAR_INSTALLDIR`` - STRING. The path to directory to install the Z3 Java ``.jar`` file. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
 * ``Z3_JAVA_JNI_LIB_INSTALLDIRR`` - STRING. The path to directory to install the Z3 Java JNI bridge library. This path should be relative to ``CMAKE_INSTALL_PREFIX``.
+* ``Z3_BUILD_OCAML_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's OCaml bindings will be built.
+* ``Z3_BUILD_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Julia bindings will be built.
+* ``Z3_INSTALL_JULIA_BINDINGS`` - BOOL. If set to ``TRUE`` and ``Z3_BUILD_JULIA_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Julia bindings.
 * ``Z3_INCLUDE_GIT_DESCRIBE`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the output of ``git describe`` will be included in the build.
 * ``Z3_INCLUDE_GIT_HASH`` - BOOL. If set to ``TRUE`` and the source tree of Z3 is a git repository then the git hash will be included in the build.
 * ``Z3_BUILD_DOCUMENTATION`` - BOOL. If set to ``TRUE`` then documentation for the API bindings can be built by invoking the ``api_docs`` target.
diff --git a/cmake/modules/AddOCaml.cmake b/cmake/modules/AddOCaml.cmake
new file mode 100644
index 000000000..e2993e79a
--- /dev/null
+++ b/cmake/modules/AddOCaml.cmake
@@ -0,0 +1,269 @@
+# Copied from https://github.com/llvm/llvm-project/tree/main/llvm/cmake/modules/AddOCaml.cmake
+# Modified by arbipher at 05/2024
+#
+# CMake build rules for the OCaml language.
+# Assumes FindOCaml is used.
+# http://ocaml.org/
+#
+# Example usage:
+#
+# add_ocaml_library(pkg_a OCAML mod_a OCAMLDEP pkg_b C mod_a_stubs PKG ctypes LLVM core)
+#
+# Unnamed parameters:
+#
+#   * Library name.
+#
+# Named parameters:
+#
+# OCAML     OCaml module names. Imply presence of a corresponding .ml and .mli files.
+# OCAMLDEP  Names of libraries this library depends on.
+# C         C stub sources. Imply presence of a corresponding .c file.
+# INCLUDES  Path for header files for C sources.
+# CFLAGS    Additional arguments passed when compiling C stubs.
+# PKG       Names of ocamlfind packages this library depends on.
+# LLVM      Names of LLVM libraries this library depends on.
+# GEN       Generated files. Do not need to copy.
+# NOCOPY    Do not automatically copy sources (.c, .ml, .mli) from the source directory,
+#           e.g. if they are generated.
+#
+
+function(add_ocaml_library name)
+  ## Argument Setting ##
+
+  # CMAKE_PARSE_ARGUMENTS(ARG "NOCOPY" "" "OCAML;OCAMLDEP;C;CFLAGS;PKG;LLVM" ${ARGN})
+  CMAKE_PARSE_ARGUMENTS(ARG "NOCOPY" "" "OCAML;OCAMLDEP;C;CFLAGS;PKG;GEN" ${ARGN})
+
+  set(src ${CMAKE_CURRENT_SOURCE_DIR})
+  set(bin ${CMAKE_CURRENT_BINARY_DIR})
+
+  # TODO: incorrect
+  set(ocaml_pkgs)
+  foreach( ocaml_pkg ${ARG_PKG} )
+    list(APPEND ocaml_pkgs "-package" "${ocaml_pkg}")
+  endforeach()
+
+  set(sources)
+
+  set(ocaml_inputs)
+
+  set(ocaml_outputs "${bin}/${name}.cma")
+  if( ARG_C )
+    list(APPEND ocaml_outputs
+         "${bin}/lib${name}${CMAKE_STATIC_LIBRARY_SUFFIX}")
+    if ( BUILD_SHARED_LIBS )
+      list(APPEND ocaml_outputs
+           "${bin}/dll${name}${CMAKE_SHARED_LIBRARY_SUFFIX}")
+    endif()
+  endif()
+  if( HAVE_OCAMLOPT )
+    list(APPEND ocaml_outputs
+         "${bin}/${name}.cmxa"
+         "${bin}/${name}${CMAKE_STATIC_LIBRARY_SUFFIX}")
+  endif()
+
+  set(ocaml_flags "-lstdc++" "-ldopt" "-L${LLVM_LIBRARY_DIR}"
+                  "-ccopt" "-L\\$CAMLORIGIN/../.."
+                  "-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.."
+                  ${ocaml_pkgs})
+
+  foreach( ocaml_dep ${ARG_OCAMLDEP} )
+    get_target_property(dep_ocaml_flags "ocaml_${ocaml_dep}" OCAML_FLAGS)
+    list(APPEND ocaml_flags ${dep_ocaml_flags})
+  endforeach()
+
+  if( NOT BUILD_SHARED_LIBS )
+    list(APPEND ocaml_flags "-custom")
+  endif()
+
+  # if(LLVM_LINK_LLVM_DYLIB)
+  #   list(APPEND ocaml_flags "-lLLVM")
+  # else()
+    # explicit_map_components_to_libraries(llvm_libs ${ARG_LLVM})
+    # foreach( llvm_lib ${llvm_libs} )
+    #   list(APPEND ocaml_flags "-l${llvm_lib}" )
+    # endforeach()
+
+    # get_property(system_libs TARGET LLVMSupport PROPERTY LLVM_SYSTEM_LIBS)
+    # foreach(system_lib ${system_libs})
+    #   if (system_lib MATCHES "^-")
+    #     # If it's an option, pass it without changes.
+    #     list(APPEND ocaml_flags "${system_lib}" )
+    #   else()
+    #     # Otherwise assume it's a library name we need to link with.
+    #     list(APPEND ocaml_flags "-l${system_lib}" )
+    #   endif()
+    # endforeach()
+  # endif()
+
+  string(REPLACE ";" " " ARG_CFLAGS "${ARG_CFLAGS}")
+  set(c_flags "${ARG_CFLAGS} ${LLVM_DEFINITIONS}")
+  foreach( include_dir ${LLVM_INCLUDE_DIR} ${LLVM_MAIN_INCLUDE_DIR} )
+    set(c_flags "${c_flags} -I${include_dir}")
+  endforeach()
+  # include -D/-UNDEBUG to match dump function visibility
+  # regex from HandleLLVMOptions.cmake
+  string(REGEX MATCH "(^| )[/-][UD] *NDEBUG($| )" flag_matches
+         "${CMAKE_C_FLAGS_${uppercase_CMAKE_BUILD_TYPE}} ${CMAKE_C_FLAGS}")
+  set(c_flags "${c_flags} ${flag_matches}")
+
+  foreach( ocaml_file ${ARG_OCAML} )
+    
+    if (EXISTS "${bin}/${ocaml_file}.mli")
+      list(APPEND sources "${ocaml_file}.mli")
+    else()
+      add_custom_command(
+        OUTPUT "${bin}/${ocaml_file}.mli"
+        COMMAND "${OCAMLFIND}" "ocamlc" "${ocaml_pkgs}" "-i" "-I" "${bin}" "-c" "${bin}/${ocaml_file}.ml" ">" "${bin}/${ocaml_file}.mli"
+        DEPENDS "${bin}/${ocaml_file}.ml"
+        COMMENT "Building OCaml mli file if non-exist"
+        VERBATIM)
+    endif()
+
+    list(APPEND sources "${ocaml_file}.ml")
+
+    list(APPEND ocaml_inputs "${bin}/${ocaml_file}.mli" "${bin}/${ocaml_file}.ml")
+
+    list(APPEND ocaml_outputs "${bin}/${ocaml_file}.cmi" "${bin}/${ocaml_file}.cmo")
+
+        list(APPEND ocaml_outputs "${bin}/${ocaml_file}.cmti" "${bin}/${ocaml_file}.cmt")
+
+    if( HAVE_OCAMLOPT )
+      list(APPEND ocaml_outputs
+           "${bin}/${ocaml_file}.cmx"
+          #  "${bin}/${ocaml_file}.o"
+           )
+    endif()
+
+  endforeach()
+
+
+  ## Compiling ML files ##
+
+  foreach( c_file ${ARG_C} )
+    list(APPEND sources "${c_file}.c")
+
+    list(APPEND c_inputs  "${bin}/${c_file}.c")
+    list(APPEND c_outputs "${bin}/${c_file}.o")
+  endforeach()
+
+  if( NOT ARG_NOCOPY )
+    foreach( source ${sources} )
+      if (NOT "${bin}/${source}" IN_LIST ARG_GEN)
+        add_custom_command(
+            OUTPUT "${bin}/${source}"
+            COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${src}/${source}" "${bin}"
+            DEPENDS "${src}/${source}"
+            COMMENT "Copying ${source} to build area")
+      endif()
+    endforeach()
+  endif()
+
+  ## Compiling C Stub ##
+
+  foreach( c_input ${c_inputs} )
+    get_filename_component(basename "${c_input}" NAME_WE)
+    add_custom_command(
+      OUTPUT "${bin}/${basename}.o"
+      COMMAND "${OCAMLFIND}" "ocamlc" "-o" "${bin}/${basename}.o" "-c" "${c_input}" -ccopt ${c_flags}
+      DEPENDS "${c_input}"
+      COMMENT "Building OCaml stub object file ${bin}/${basename}.o"
+      VERBATIM)
+  endforeach()
+
+  ## Setting linking argument and run mklib ##
+
+  set(ocaml_params)
+  foreach( ocaml_input ${ocaml_inputs} ${c_outputs})
+    get_filename_component(filename "${ocaml_input}" NAME)
+    list(APPEND ocaml_params "${filename}")
+  endforeach()
+
+  if( APPLE )
+    set(ocaml_rpath "@executable_path/../../../lib${LLVM_LIBDIR_SUFFIX}")
+  elseif( UNIX )
+    set(ocaml_rpath "\\$ORIGIN/../../../lib${LLVM_LIBDIR_SUFFIX}")
+  endif()
+  list(APPEND ocaml_flags "-ldopt" "-Wl,-rpath,${ocaml_rpath}")
+
+  add_custom_command(
+    OUTPUT ${ocaml_outputs}
+    COMMAND "${OCAMLFIND}" "ocamlmklib" "-ocamlcflags" "-bin-annot"
+      "-o" "${name}" ${ocaml_flags} ${ocaml_params}
+    DEPENDS ${ocaml_inputs} ${c_outputs}
+    COMMENT "Building OCaml library ${name}"
+    VERBATIM)
+
+  ## Build document
+
+  add_custom_command(
+    OUTPUT "${bin}/${name}.odoc"
+    COMMAND "${OCAMLFIND}" "ocamldoc"
+            "-I" "${bin}"
+            "-I" "${LLVM_LIBRARY_DIR}/ocaml/llvm/"
+            "-dump" "${bin}/${name}.odoc"
+            ${ocaml_pkgs} ${ocaml_inputs}
+    DEPENDS ${ocaml_inputs} ${ocaml_outputs}
+    COMMENT "Building OCaml documentation for ${name}"
+    VERBATIM)
+
+  add_custom_target("ocaml_${name}" ALL DEPENDS ${ocaml_outputs} "${bin}/${name}.odoc")
+
+  set_target_properties("ocaml_${name}" PROPERTIES
+    OCAML_FLAGS "-I;${bin}")
+  set_target_properties("ocaml_${name}" PROPERTIES
+    OCAML_ODOC "${bin}/${name}.odoc")
+
+  ## Setting dependencies
+
+  foreach( ocaml_dep ${ARG_OCAMLDEP} )
+    add_dependencies("ocaml_${name}" "ocaml_${ocaml_dep}")
+  endforeach()
+
+  if( NOT LLVM_OCAML_OUT_OF_TREE )
+    foreach( llvm_lib ${llvm_libs} )
+      add_dependencies("ocaml_${name}" "${llvm_lib}")
+    endforeach()
+  endif()
+
+  ## Configurating installation
+
+  set(install_files)
+  set(install_shlibs)
+  foreach( ocaml_output ${ocaml_inputs} ${ocaml_outputs} )
+    get_filename_component(ext "${ocaml_output}" EXT)
+
+    if( NOT (ext STREQUAL ".cmo" OR
+             ext STREQUAL ".ml" OR
+             ext STREQUAL ".o" OR
+             ext STREQUAL CMAKE_SHARED_LIBRARY_SUFFIX) )
+      list(APPEND install_files "${ocaml_output}")
+    elseif( ext STREQUAL CMAKE_SHARED_LIBRARY_SUFFIX)
+      list(APPEND install_shlibs "${ocaml_output}")
+    endif()
+  endforeach()
+
+  install(FILES ${install_files}
+          DESTINATION "${LLVM_OCAML_INSTALL_PATH}/llvm")
+  install(FILES ${install_shlibs}
+          PERMISSIONS OWNER_READ OWNER_WRITE OWNER_EXECUTE
+                      GROUP_READ GROUP_EXECUTE
+                      WORLD_READ WORLD_EXECUTE
+          DESTINATION "${LLVM_OCAML_INSTALL_PATH}/stublibs")
+
+  foreach( install_file ${install_files} ${install_shlibs} )
+    get_filename_component(filename "${install_file}" NAME)
+    add_custom_command(TARGET "ocaml_${name}" POST_BUILD
+      COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${install_file}"
+                                             "${LLVM_LIBRARY_DIR}/ocaml/llvm/"
+      COMMENT "Copying OCaml library component ${filename} to intermediate area"
+      VERBATIM)
+    add_dependencies("ocaml_${name}" ocaml_make_directory)
+  endforeach()
+endfunction()
+
+# add_custom_target(ocaml_make_directory
+#   COMMAND "${CMAKE_COMMAND}" "-E" "make_directory" "${LLVM_LIBRARY_DIR}/ocaml/llvm")
+add_custom_target("ocaml_make_directory")
+# add_custom_target("ocaml_all")
+# set_target_properties(ocaml_all PROPERTIES FOLDER "Misc")
+# set_target_properties(ocaml_make_directory PROPERTIES FOLDER "Misc")
diff --git a/cmake/modules/FindOCaml.cmake b/cmake/modules/FindOCaml.cmake
new file mode 100644
index 000000000..32f06790b
--- /dev/null
+++ b/cmake/modules/FindOCaml.cmake
@@ -0,0 +1,107 @@
+# Copied from https://github.com/llvm/llvm-project/tree/main/llvm/cmake/modules/FindOCaml.cmake
+# Modified by arbipher at 05/2024
+#
+# CMake find_package() module for the OCaml language.
+# Assumes ocamlfind will be used for compilation.
+# http://ocaml.org/
+#
+# Example usage:
+#
+# find_package(OCaml)
+#
+# If successful, the following variables will be defined:
+# OCAMLFIND
+# OCAML_VERSION
+# OCAML_STDLIB_PATH
+# HAVE_OCAMLOPT
+#
+# Also provides find_ocamlfind_package() macro.
+#
+# Example usage:
+#
+# find_ocamlfind_package(ctypes)
+#
+# In any case, the following variables are defined:
+#
+# HAVE_OCAML_${pkg}
+#
+# If successful, the following variables will be defined:
+#
+# OCAML_${pkg}_VERSION
+
+include( FindPackageHandleStandardArgs )
+include(AddOCaml)
+
+find_program(OCAMLFIND
+             NAMES ocamlfind)
+
+if( OCAMLFIND )
+  execute_process(
+    COMMAND ${OCAMLFIND} ocamlc -version
+    OUTPUT_VARIABLE OCAML_VERSION
+    OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+  execute_process(
+    COMMAND ${OCAMLFIND} ocamlc -where
+    OUTPUT_VARIABLE OCAML_STDLIB_PATH
+    OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+  execute_process(
+    COMMAND ${OCAMLFIND} ocamlc -version
+    OUTPUT_QUIET
+    RESULT_VARIABLE find_ocaml_result)
+  if( find_ocaml_result EQUAL 0 )
+    set(HAVE_OCAMLOPT TRUE)
+  else()
+    set(HAVE_OCAMLOPT FALSE)
+  endif()
+endif()
+
+find_package_handle_standard_args( OCaml DEFAULT_MSG
+  OCAMLFIND
+  OCAML_VERSION
+  OCAML_STDLIB_PATH)
+
+mark_as_advanced(
+  OCAMLFIND)
+
+function(find_ocamlfind_package pkg)
+  CMAKE_PARSE_ARGUMENTS(ARG "OPTIONAL" "VERSION" "" ${ARGN})
+
+  execute_process(
+    COMMAND "${OCAMLFIND}" "query" "${pkg}" "-format" "%v"
+    RESULT_VARIABLE result
+    OUTPUT_VARIABLE version
+    ERROR_VARIABLE error
+    OUTPUT_STRIP_TRAILING_WHITESPACE
+    ERROR_STRIP_TRAILING_WHITESPACE)
+
+  if( NOT result EQUAL 0 AND NOT ARG_OPTIONAL )
+    message(FATAL_ERROR ${error})
+  endif()
+
+  if( result EQUAL 0 )
+    set(found TRUE)
+  else()
+    set(found FALSE)
+  endif()
+
+  if( found AND ARG_VERSION )
+    if( version VERSION_LESS ARG_VERSION AND ARG_OPTIONAL )
+      # If it's optional and the constraint is not satisfied, pretend
+      # it wasn't found.
+      set(found FALSE)
+    elseif( version VERSION_LESS ARG_VERSION )
+      message(FATAL_ERROR
+              "ocamlfind package ${pkg} should have version ${ARG_VERSION} or newer")
+    endif()
+  endif()
+
+  string(TOUPPER ${pkg} pkg)
+
+  set(HAVE_OCAML_${pkg} ${found}
+      PARENT_SCOPE)
+
+  set(OCAML_${pkg}_VERSION ${version}
+      PARENT_SCOPE)
+endfunction()
diff --git a/makefile b/makefile
new file mode 100644
index 000000000..4bce3411d
--- /dev/null
+++ b/makefile
@@ -0,0 +1,400 @@
+# ${PROJECT_SOURCE_DIR}:       /vendor/z3
+# ${PROJECT_BINARY_DIR}:       /vendor/z3/build
+# ${CMAKE_CURRENT_SOURCE_DIR}: /vendor/z3/src/api/ml
+# ${CMAKE_CURRENT_BINARY_DIR}: /vendor/z3/build/src/api/ml
+
+# TODO: add `-bin-annot` to more `ocamlc`
+# Question: who will set `CAMLORIGIN`
+# - 	-dllpath $$CAMLORIGIN/../.. \
+# Q: is `ocamlmklib -ldopt -Lfoo` the same as `ocamlmklib -Lfoo`
+# it doesn't looks right (item 4)
+#    https://www.ocaml.org/manual/5.2/runtime.html#s:ocamlrun-dllpath
+#
+# if external libz3 is given, no files should be build
+# 
+# find_program(OCAMLFIND
+#              NAMES ocamlfind)
+# find_library(ocaml)
+# include(FindOCaml)
+# Todo: use DEPFILE in https://cmake.org/cmake/help/latest/command/add_custom_command.html
+# for rpath, see https://discourse.cmake.org/t/how-to-get-an-lc-rpath-and-rpath-prefix-on-a-dylib-on-macos/5540
+
+# Generate ``z3native.ml`` and ``z3native_stubs.c``
+
+# set(z3ml_generated_files
+#   "${z3ml_bin}/z3native.ml"
+#   "${z3ml_bin}/z3native_stubs.c"
+#   "${z3ml_enums_ml}"
+# )
+
+# add_custom_target(ocaml_generated DEPENDS
+#   ${z3ml_generated_files}
+# )
+
+# add_custom_command(
+#   OUTPUT "${z3ml_bin}/z3enums.mli"
+#   COMMAND "${OCAMLFIND}" "ocamlc" 
+#           "-package" "zarith"
+#           "-i" 
+#           "-I" "${z3ml_bin}"
+#           "-c" "${z3ml_bin}/z3enums.ml"
+#           ">" "${z3ml_bin}/z3enums.mli"
+#   DEPENDS "${z3ml_enums_ml}"
+#   COMMENT "Building z3enums.mli"
+#   VERBATIM)
+
+# "-ldopt"
+# "-ccopt" "-L\\$CAMLORIGIN/../.."
+# "-ccopt" "-Wl,-rpath,\\$CAMLORIGIN/../.."
+
+# add_custom_command(
+#   OUTPUT "${z3ml_bin}/z3native.cmx"
+#   COMMAND "${OCAMLFIND}" "ocamlopt" 
+#           "-package" "zarith"
+#           "-I" "${z3ml_bin}"
+#           "-c" "${z3ml_bin}/z3native.ml"
+#   DEPENDS "${z3ml_bin}/z3enums.cmo"
+#           "${z3ml_bin}/z3native.mli"
+#           "${z3ml_bin}/z3native.cmi"
+#           "${z3ml_bin}/z3native.ml"
+#   COMMENT "Building z3native.cmx"
+#   VERBATIM)
+
+# add_custom_command(
+#   OUTPUT "${z3ml_bin}/z3enums.cmo"
+#   COMMAND "${OCAMLFIND}" "ocamlc" 
+#           "-package" "zarith"
+#           "-I" "${z3ml_bin}"
+#           "-c" "${z3ml_bin}/z3enums.ml"
+#   DEPENDS "${z3ml_enums_ml}"
+#   COMMENT "Building z3enums.cmo"
+#   VERBATIM)
+
+# add_custom_command(
+#   OUTPUT "${z3ml_bin}/z3native.mli"
+#   COMMAND "${OCAMLFIND}" "ocamlc" 
+#           "-package" "zarith"
+#           "-i" 
+#           "-I" "${z3ml_bin}"
+#           "-c" "${z3ml_bin}/z3native.ml"
+#           ">" "${z3ml_bin}/z3native.mli"
+#   DEPENDS "${z3ml_enums_ml}"
+#           "${z3ml_bin}/z3enums.cmo"
+#           "${z3ml_bin}/z3native.ml"
+#   COMMENT "Building z3native.mli"
+#   VERBATIM)
+
+# add_custom_command(
+#   OUTPUT "${z3ml_bin}/z3.cmx"
+#   COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags}
+#           "-c" "${z3ml_bin}/z3.ml"  
+#   DEPENDS "${z3ml_bin}/z3enums.cmo"
+#           "${z3ml_bin}/z3native.cmo"
+#           "${z3ml_bin}/z3.ml"
+#           "${z3ml_bin}/z3.mli"
+#           "${z3ml_bin}/z3.cmi"
+#   COMMENT "Building z3.cmx"
+#   VERBATIM)
+
+# add_custom_command(
+#   OUTPUT "${z3ml_bin}/z3ml.cmxa"
+#   COMMAND "${OCAMLFIND}" "ocamlmklib"
+#     "-o" z3ml
+#     ${ocamlmklib_flags}
+#     "-I" "${z3ml_bin}"
+#     "${z3ml_bin}/z3enums.cmx"
+#     "${z3ml_bin}/z3native.cmx"
+#     "${z3ml_bin}/z3native_stubs.o"
+#     "${z3ml_bin}/z3.cmx"
+#   DEPENDS
+#     libz3
+#     "${z3ml_bin}/z3enums.cmx"
+#     "${z3ml_bin}/z3native.cmx"
+#     "${z3ml_bin}/z3native_stubs.o"
+#     "${z3ml_bin}/z3.cmx"
+#   COMMENT "Building OCaml library ${name}"
+#   VERBATIM)
+# add_custom_command(
+#   OUTPUT "${z3ml_bin}/z3ml.cmxs"
+#   COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared"
+#     "-o" "${z3ml_bin}/z3ml.cmxs"
+#     "-I" "."
+#     "-I" "${z3ml_bin}"
+#     "${z3ml_bin}/z3ml.cmxa"
+#   DEPENDS
+#     "${z3ml_bin}/z3ml.cmxa"
+#   COMMENT "Building OCaml library ${name}"
+#   VERBATIM)
+
+#          "${z3ml_bin}/z3enums.cmi"
+
+ML_LIB=/home/ex/.opam/5.2.0/lib
+ML_LIB=/Users/ex/.opam/5.2.0/lib
+ROOT=$$(pwd)
+MY_Z3=/home/ex/my_z3
+MY_Z3=/Users/ex/code/tmp/my-z3
+
+ml0:
+	mkdir -p build
+	cd build && cmake -G "Ninja" \
+	-DZ3_BUILD_LIBZ3_SHARED=TRUE \
+	-DZ3_BUILD_OCAML_BINDINGS=TRUE \
+	../
+
+# -DGRAPHVIZ_EXECUTABLES=FALSE \
+# -DGRAPHVIZ_INTERFACE_LIBS=FALSE \
+# --graphviz=deps.dot \
+
+ml-inner-mk:
+	mkdir -p build
+	cd build && cmake \
+	-DCMAKE_VERBOSE_MAKEFILE=TRUE \
+	-DZ3_BUILD_LIBZ3_SHARED=TRUE \
+	-DZ3_BUILD_OCAML_BINDINGS=TRUE \
+	-DZ3_BUILD_PYTHON_BINDINGS=TRUE \
+	--debug-trycompile \
+	../
+
+ml-mk:
+	mkdir -p build
+	cd build && cmake \
+	-DCMAKE_VERBOSE_MAKEFILE=TRUE \
+	-DZ3_BUILD_LIBZ3_SHARED=TRUE \
+	-DZ3_BUILD_OCAML_BINDINGS=TRUE \
+	-DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=$(MY_Z3) \
+	--debug-trycompile \
+	../
+
+ml-inner:
+	mkdir -p build
+	cd build && cmake \
+	-G "Ninja" \
+	-DCMAKE_VERBOSE_MAKEFILE=TRUE \
+	-DZ3_BUILD_LIBZ3_SHARED=TRUE \
+	-DZ3_BUILD_OCAML_BINDINGS=TRUE \
+	--debug-trycompile \
+	../
+
+ml:
+	mkdir -p build
+	cd build && cmake \
+	-G "Ninja" \
+	-DCMAKE_VERBOSE_MAKEFILE=TRUE \
+	-DZ3_BUILD_LIBZ3_SHARED=TRUE \
+	-DZ3_BUILD_OCAML_BINDINGS=TRUE \
+	--debug-trycompile \
+	../
+
+# -DZ3_BUILD_OCAML_EXTERNAL_LIBZ3=$(MY_Z3) \
+# -DZ3_USE_LIB_GMP=TRUE \
+
+# LD_LIBRARY_PATH=build ./build/src/api/ml/ml_example
+
+build-all:
+	cd build && make -j16
+
+build-mk:
+	cd build && make -j16 build_z3_ocaml_bindings
+.PHONY:build
+
+build-nj:
+	cd build && ninja
+.PHONY:build-nj
+
+build:
+	cd build && ninja build_z3_ocaml_bindings
+.PHONY:build
+
+dot:
+	cd build && dot -Tpng -o deps.png deps.dot
+
+clean:
+	rm -rf build
+
+MKLIB_FLAGS = \
+	ocamlfind ocamlmklib \
+	-ocamlcflags -bin-annot \
+	-package zarith \
+	-lz3 -lstdc++ -lpthread\
+	-lgmp \
+	-L$(ROOT)/build \
+	-dllpath $(ROOT)/build \
+	-L$(ML_LIB)/stublibs \
+	-dllpath $(ML_LIB)/stublibs \
+	-I build/src/api/ml \
+	-o build/src/api/ml/z3ml	
+
+om:
+	$(MKLIB_FLAGS) \
+	build/src/api/ml/z3enums.cmo \
+	build/src/api/ml/z3native.cmo \
+	build/src/api/ml/z3native_stubs.o \
+	build/src/api/ml/z3.cmo
+
+	$(MKLIB_FLAGS) \
+	build/src/api/ml/z3enums.cmx \
+	build/src/api/ml/z3native.cmx \
+	build/src/api/ml/z3native_stubs.o \
+	build/src/api/ml/z3.cmx
+
+# why?
+# DEPENDS "${z3ml_bin}/z3enums.cmo"
+# 	-I +threads \
+
+or1:
+	ocamlfind ocamlc -verbose \
+	-o ml_example.byte \
+	-package zarith \
+	-I $(ROOT)/build/src/api/ml \
+	-dllpath $(ROOT)/build/src/api/ml \
+	-I $(ML_LIB)/stublibs \
+	-dllpath $(ML_LIB)/stublibs \
+	$(ML_LIB)/zarith/zarith.cma \
+	$(ROOT)/build/src/api/ml/z3ml.cma \
+	$(ROOT)/build/src/api/ml/ml_example.ml \
+
+# 	-linkpkg \
+
+or2:
+	ocamlrun ml_example.byte
+
+# -I $(ML_LIB)/stublibs \
+    # "-cclib" "-L${PROJECT_BINARY_DIR}"
+    # "-cclib" [[-L. -lpthread -lstdc++ -lz3]]
+    # "-linkpkg"
+# "-cclib" "-L${PROJECT_BINARY_DIR}"
+# "-cclib" [[-L. -lpthread -lstdc++ -lz3]]
+    
+# 	-I +threads \
+
+oc1:
+	ocamlfind ocamlopt \
+	-o ml_example \
+	-package zarith \
+	-linkpkg \
+	-I $(ROOT)/build/src/api/ml \
+	z3ml.cmxa \
+	$(ROOT)/build/src/api/ml/ml_example.ml
+
+oc2:
+	./ml_example
+
+# must have
+# $(ML_LIB)/zarith/zarith.cma 
+# -I $(ROOT)/build/src/api/ml
+
+# can be removed
+# -cclib "-lstdc++ -lz3"
+# -cclib "-L. -L$(ML_LIB)/stublibs -L$(ML_LIB)/zarith "
+# -L$(ROOT)/build
+# -package zarith
+# -linkpkg
+# -lpthread
+# -package z3
+# -I $(ML_LIB)/zarith 
+
+# must not have
+# -custom
+
+# -o $(ROOT)/build/src/api/ml/ml_example.byte
+
+# CAML_LD_LIBRARY_PATH=$(ML_LIB)/stublibs:$(ROOT)/build:$(ROOT)/build/src/api/ml:$(ML_LIB)/zarith
+
+or3:
+	ocamlrun -I $(ML_LIB)/zarith -I $(ML_LIB)/stublibs -I $(ML_LIB)/zarith ml_example.byte
+
+# -I $(ML_LIB)/zarith 
+# -I $(ML_LIB)/stublibs
+# -I $(ROOT)/build
+# -I $(ROOT)/build/src/api/ml
+# -t -b
+
+
+# -cclib "-L. -lpthread -lstdc++ -lz3"
+
+# set (cc_flags "\"-L. -lpthread -lstdc++ -lz3\"")
+#"LD_LIBRARY_PATH=${PROJECT_BINARY_DIR}"
+
+# Link libz3 into the python directory so bindings work out of the box
+# add_custom_command(OUTPUT "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+#   COMMAND "${CMAKE_COMMAND}" "-E" "${LINK_COMMAND}"
+#     "${PROJECT_BINARY_DIR}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+#     "${z3py_bindings_build_dest}/libz3${CMAKE_SHARED_MODULE_SUFFIX}"
+#   DEPENDS libz3
+#   COMMENT "Linking libz3 into python directory"
+# )
+
+# add_ocaml_library(z3ml
+#   OCAML    z3enums z3native z3
+#   # OCAMLDEP llvm
+#   PKG      zarith
+#   C        z3native_stubs
+#   CFLAGS   "-I${Z3_C_API_PATH} -I${CMAKE_CURRENT_SOURCE_DIR} -I\$\(ocamlfind ocamlc -where\)"
+#   GEN      "${OCAML_GENERATED_FILES}"
+#   # -I${CMAKE_CURRENT_SOURCE_DIR}/../llvm
+#   # LLVM     IRReader)
+# )
+
+
+# set(z3_c_api_path "${PROJECT_SOURCE_DIR}/src/api")
+# target_sources(z3ml PRIVATE
+#                 z3native_stubs.h
+#                 ${z3_c_api_path})
+
+
+# message(heads "--${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}")
+# message(extra deps "--${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}")
+
+# add_custom_target(z3natives_stubs.c DEPENDS "${Z3_OCAML_NATIVE_STUB_PRE_FILE}")
+# target_sources(ocaml_z3 
+#               PRIVATE ${Z3_OCAML_NATIVE_FILE} ${Z3_OCAML_NATIVE_STUB_FILE})
+
+# target_include_directories(ocaml_z3
+#     PUBLIC ${CMAKE_CURRENT_BINARY_DIR}
+# )
+
+# add_custom_target (LibCoreBC DEPENDS libcore.bc)
+
+# target_sources(src/api/ml/z3natives_stubs.c
+#                 PUBLIC Z3_OCAML_NATIVE_STUB_FILE)
+
+# add_custom_target(${Z3_OCAML_NATIVE_STUB_FILE} DEPENDS 
+#                  ${Z3_OCAML_NATIVE_STUB_PRE_FILE})
+
+# target_precompile_headers(
+#   ocaml_z3 PRIVATE
+#   z3native_stubs.h
+# )
+
+# target_sources(ocaml_z3 PRIVATE
+#                 "${PROJECT_SOURCE_DIR}/src/api/ml/z3native.ml"
+#                 "${PROJECT_SOURCE_DIR}/src/api/ml/z3native_stubs.c")
+
+# add_dependencies(ocaml_z3
+#               "${PROJECT_SOURCE_DIR}/src/api"
+#               "${PROJECT_BINARY_DIR}/src/api"
+#             )
+
+# find_package(OCaml)
+# message("DDDebug ${OCAMLFIND}")
+# message("DDDebug ${pkg}")
+# find_ocamlfind_package(ctypes)
+# # find_ocamlfind_package("nonexist")
+# message(small " ${HAVE_OCAML_ctype}")
+# message(caps " ${HAVE_OCAML_CTYPES}")
+# message(small " ${OCAML_ctype_VERSION}")
+# message(caps " ${OCAML_CTYPES_VERSION}")
+# find_package(ocaml REQUIRED)
+
+# add_custom_target(ocaml_post_z3enums DEPENDS
+#   "${CMAKE_CURRENT_BINARY_DIR}/z3enums.ml"
+#   "${CMAKE_CURRENT_BINARY_DIR}/z3enums.mli"
+#   "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmo"
+#   "${CMAKE_CURRENT_BINARY_DIR}/z3enums.cmx"
+# )
+# add_custom_target(z3.ml DEPENDS
+#   ocaml_post_z3enums
+# )
+# add_custom_target(z3native.ml DEPENDS
+#   ocaml_post_z3enums
+# )
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 5faede21f..071436200 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -299,6 +299,18 @@ if (Z3_BUILD_JAVA_BINDINGS)
   add_subdirectory(api/java)
 endif()
 
+################################################################################
+# OCaml bindings
+################################################################################
+option(Z3_BUILD_OCAML_BINDINGS "Build OCaml bindings for Z3" OFF)
+if (Z3_BUILD_OCAML_BINDINGS)
+  if (NOT Z3_BUILD_LIBZ3_SHARED)
+    message(FATAL_ERROR "The OCaml bindings will not work with a static libz3. "
+      "You either need to disable Z3_BUILD_OCAML_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED")
+  endif()
+  add_subdirectory(api/ml)
+endif()
+
 ################################################################################
 # Julia bindings
 ################################################################################
diff --git a/src/api/ml/CMakeLists.txt b/src/api/ml/CMakeLists.txt
new file mode 100644
index 000000000..18ea6f15d
--- /dev/null
+++ b/src/api/ml/CMakeLists.txt
@@ -0,0 +1,320 @@
+find_package(OCaml REQUIRED)
+
+set(exe_ext ${CMAKE_EXECUTABLE_SUFFIX})
+set(so_ext ${CMAKE_SHARED_LIBRARY_SUFFIX})
+set(bc_ext ".byte")
+
+set(z3ml_src ${CMAKE_CURRENT_SOURCE_DIR})
+set(z3ml_bin ${CMAKE_CURRENT_BINARY_DIR})
+
+if (Z3_BUILD_OCAML_EXTERNAL_LIBZ3)
+  add_custom_target(libz3_z3ml
+    ALL
+    DEPENDS ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3}/libz3${so_ext}
+  )
+  set(libz3_path ${Z3_BUILD_OCAML_EXTERNAL_LIBZ3})
+else()
+  add_custom_target(libz3_z3ml
+    ALL
+    DEPENDS libz3
+  )
+  set(libz3_path ${PROJECT_BINARY_DIR})
+endif()
+
+add_custom_command(
+  OUTPUT
+    ${z3ml_bin}/z3native.ml
+    ${z3ml_bin}/z3native_stubs.c
+  COMMAND "${Python3_EXECUTABLE}"
+    "${PROJECT_SOURCE_DIR}/scripts/update_api.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--ml-src-dir"
+    "${CMAKE_CURRENT_SOURCE_DIR}"
+    "--ml-output-dir"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+  DEPENDS
+    ${PROJECT_SOURCE_DIR}/scripts/update_api.py
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+  COMMENT "Generatinging ${z3ml_bin}/z3native.ml and ${z3ml_bin}/z3native_stubs.c"
+  VERBATIM
+)
+
+add_custom_command(
+  OUTPUT 
+    ${z3ml_bin}/z3enums.ml
+  COMMAND "${Python3_EXECUTABLE}"
+    "${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py"
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    "--ml-output-dir"
+    "${CMAKE_CURRENT_BINARY_DIR}"
+  DEPENDS
+    ${PROJECT_SOURCE_DIR}/scripts/mk_consts_files.py
+    ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN}
+    ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES}
+  COMMENT "Generating ${z3ml_bin}/z3enums.ml"
+  VERBATIM
+)
+
+add_custom_command(
+  OUTPUT  ${z3ml_bin}/z3.ml
+          ${z3ml_bin}/z3.mli
+  COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.ml" "${z3ml_bin}/z3.ml"
+  COMMAND "${CMAKE_COMMAND}" "-E" "copy" "${z3ml_src}/z3.mli" "${z3ml_bin}/z3.mli"
+  DEPENDS ${z3ml_src}/z3.ml
+          ${z3ml_src}/z3.mli
+  COMMENT "Copying z3.ml and z3.mli to build area")
+
+set(z3ml_common_flags  "-package" "zarith"
+                       "-I" "${z3ml_bin}")
+
+# z3native_stubs.c depends on nothing
+execute_process(
+  COMMAND ${OCAMLFIND} ocamlc "-where"
+  OUTPUT_VARIABLE ocaml_stub_lib_path
+  OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+add_custom_command(
+  OUTPUT ${z3ml_bin}/z3native_stubs.o
+  COMMAND "${OCAMLFIND}" "ocamlc" ${z3ml_common_flags}
+          "-o" "${z3ml_bin}/z3native_stubs.o"
+          "-I" "${z3ml_src}"
+          "-I" "${PROJECT_SOURCE_DIR}/src/api"
+          "-I" "${ocaml_stub_lib_path}"
+          "-c" "${z3ml_bin}/z3native_stubs.c"
+  DEPENDS ${z3ml_bin}/z3native_stubs.c
+  COMMENT "Building z3native_stubs.o"
+  VERBATIM)
+
+# z3enum.ml depends on nothing
+add_custom_command(
+  OUTPUT ${z3ml_bin}/z3enums.mli
+         ${z3ml_bin}/z3enums.cmi
+         ${z3ml_bin}/z3enums.cmo
+         ${z3ml_bin}/z3enums.cmx
+  COMMAND "${OCAMLFIND}" "ocamlc"   ${z3ml_common_flags}
+         "-i" 
+         "-c" "${z3ml_bin}/z3enums.ml"
+         ">" "${z3ml_bin}/z3enums.mli"
+  COMMAND "${OCAMLFIND}" "ocamlc"   ${z3ml_common_flags}
+         "-c" "${z3ml_bin}/z3enums.mli"  
+  COMMAND "${OCAMLFIND}" "ocamlc"   ${z3ml_common_flags}
+         "-c" "${z3ml_bin}/z3enums.ml"
+  COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags}
+          "-c" "${z3ml_bin}/z3enums.ml"
+  DEPENDS ${z3ml_bin}/z3enums.ml
+  COMMENT "Building z3enums.{mli,cmi,cmo,cmx}"
+  VERBATIM)
+
+# z3native.ml depends on z3enums
+add_custom_command(
+  OUTPUT ${z3ml_bin}/z3native.mli
+         ${z3ml_bin}/z3native.cmi
+         ${z3ml_bin}/z3native.cmo
+         ${z3ml_bin}/z3native.cmx
+  COMMAND "${OCAMLFIND}" "ocamlc"   ${z3ml_common_flags}
+         "-i" 
+         "-c" "${z3ml_bin}/z3native.ml"
+         ">" "${z3ml_bin}/z3native.mli"
+  COMMAND "${OCAMLFIND}" "ocamlc"   ${z3ml_common_flags}
+         "-c" "${z3ml_bin}/z3native.mli"  
+  COMMAND "${OCAMLFIND}" "ocamlc"   ${z3ml_common_flags}
+          "-c" "${z3ml_bin}/z3native.ml"
+  COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags}
+          "-c" "${z3ml_bin}/z3native.ml"
+  DEPENDS ${z3ml_bin}/z3enums.cmo
+          ${z3ml_bin}/z3native.ml
+  COMMENT "Building z3native.{mli,cmi,cmo,cmx}"
+  VERBATIM)
+
+# z3.ml depends on z3enums and z3native
+add_custom_command(
+  OUTPUT ${z3ml_bin}/z3.cmi
+         ${z3ml_bin}/z3.cmo
+         ${z3ml_bin}/z3.cmx
+  COMMAND "${OCAMLFIND}" "ocamlc"   ${z3ml_common_flags}
+          "-c" "${z3ml_bin}/z3.mli"
+  COMMAND "${OCAMLFIND}" "ocamlc"   ${z3ml_common_flags}
+          "-c" "${z3ml_bin}/z3.ml"
+  COMMAND "${OCAMLFIND}" "ocamlopt" ${z3ml_common_flags}
+          "-c" "${z3ml_bin}/z3.ml" 
+  DEPENDS ${z3ml_bin}/z3enums.cmo
+          ${z3ml_bin}/z3native.cmo
+          ${z3ml_bin}/z3.ml
+          ${z3ml_bin}/z3.mli
+  COMMENT "Building z3.cmo"
+  VERBATIM)
+
+# making ocaml stublibs  
+execute_process(
+  COMMAND ${OCAMLFIND} printconf destdir
+  OUTPUT_VARIABLE ocaml_destdir_path
+  OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+set(ocaml_stublibs_path "${ocaml_destdir_path}/stublibs")
+
+set(c_lib_deps "-lz3" "-lstdc++" "-lpthread")
+if (Z3_USE_LIB_GMP)
+  list(APPEND c_lib_deps "-lgmp")
+endif()
+
+if( APPLE )
+  set(ocaml_rpath "@executable_path/../libz3${so_ext}")
+elseif( UNIX )
+  set(ocaml_rpath "\\$ORIGIN/../libz3${so_ext}")
+endif()
+list(APPEND c_lib_deps "-dllpath" ${ocaml_rpath})
+
+# We may not directly use CMake's BUILD_RPATH or INSTALL_RPATH since they don't set 
+# the ocaml stub libraries as a normal library target.
+
+set(ocamlmklib_flags "-o" "z3ml"
+                     "-ocamlcflags" "-bin-annot"
+                     "-package" "zarith"
+                     ${c_lib_deps}
+                     "-L${libz3_path}"
+                     "-dllpath" "${libz3_path}"
+                     "-L${ocaml_stublibs_path}"
+                     "-dllpath" "${ocaml_stublibs_path}"
+                     "-dllpath" "@rpath/dllz3ml.so"
+                     "-I" "${z3ml_bin}")
+
+# OCaml's dll stublib hava platform-independent name `dll<pkg>.so`
+
+add_custom_command(
+  OUTPUT ${z3ml_bin}/dllz3ml.so
+         ${z3ml_bin}/libz3ml.a
+         ${z3ml_bin}/z3ml.cma
+         ${z3ml_bin}/z3ml.cmxa
+         ${z3ml_bin}/z3ml.cmxs
+  COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags}
+          "${z3ml_bin}/z3enums.cmo"
+          "${z3ml_bin}/z3native.cmo"
+          "${z3ml_bin}/z3native_stubs.o"
+          "${z3ml_bin}/z3.cmo"
+  COMMAND "${OCAMLFIND}" "ocamlmklib" ${ocamlmklib_flags}
+          "${z3ml_bin}/z3enums.cmx"
+          "${z3ml_bin}/z3native.cmx"
+          "${z3ml_bin}/z3native_stubs.o"
+          "${z3ml_bin}/z3.cmx"
+  COMMAND "${OCAMLFIND}" "ocamlopt" "-linkall" "-shared"
+          "-o" "${z3ml_bin}/z3ml.cmxs"
+          "-I" "${z3ml_bin}"
+          "${z3ml_bin}/z3ml.cmxa"
+  DEPENDS
+          libz3_z3ml
+          ${z3ml_bin}/z3native_stubs.o
+          ${z3ml_bin}/z3enums.cmo
+          ${z3ml_bin}/z3native.cmo
+          ${z3ml_bin}/z3.cmo
+          ${z3ml_bin}/z3enums.cmx
+          ${z3ml_bin}/z3native.cmx
+          ${z3ml_bin}/z3.cmx
+  COMMENT "Building z3ml.{cma,cmxa,cmxs}, dllz3ml.so, and libz3ml.a"
+  VERBATIM)
+
+###############################################################################
+# Example
+###############################################################################
+ 
+add_custom_command(
+  OUTPUT  ${z3ml_bin}/ml_example.ml
+  COMMAND "${CMAKE_COMMAND}" "-E" 
+          "copy" "${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml" "${z3ml_bin}/ml_example.ml"
+  DEPENDS ${PROJECT_SOURCE_DIR}/examples/ml/ml_example.ml
+  COMMENT "Copying ml_example.ml to build area")
+
+execute_process(
+  COMMAND ${OCAMLFIND} query zarith
+  OUTPUT_VARIABLE ocaml_pkg_zarith_path
+  OUTPUT_STRIP_TRAILING_WHITESPACE)
+
+#     "-I" "+threads"
+
+add_custom_command(
+  OUTPUT ${z3ml_bin}/ml_example${bc_ext}
+         ${z3ml_bin}/ml_example.bc.log
+  COMMAND "${OCAMLFIND}" "ocamlc"
+    "-o" "${z3ml_bin}/ml_example${bc_ext}"
+    "-package" "zarith"
+    "-I" "${z3ml_bin}"
+    "-dllpath" "${z3ml_bin}"
+    "-I" ${ocaml_stublibs_path}
+    "-dllpath" ${ocaml_stublibs_path}
+    "${ocaml_pkg_zarith_path}/zarith.cma"
+    "${z3ml_bin}/z3ml.cma"
+    "${z3ml_bin}/ml_example.ml"
+  COMMAND 
+    "ocamlrun" "${z3ml_bin}/ml_example${bc_ext}"
+    ">" "${z3ml_bin}/ml_example.bc.log"
+  DEPENDS
+    ${z3ml_bin}/z3ml.cma
+    ${z3ml_bin}/dllz3ml.so
+    ${z3ml_bin}/ml_example.ml
+  COMMENT "Testing build and run ml_example bytecode"
+  VERBATIM)
+
+#     "-I" "+threads"
+
+add_custom_command(
+  OUTPUT ${z3ml_bin}/ml_example${exe_ext}
+         ${z3ml_bin}/ml_example.log
+  COMMAND "${OCAMLFIND}" "ocamlopt"
+    "-o" "${z3ml_bin}/ml_example${exe_ext}"
+    "-package" "zarith"
+    "-linkpkg"
+    "-I" "${z3ml_bin}"
+    "${z3ml_bin}/z3ml.cmxa"
+    "${z3ml_bin}/ml_example.ml"
+  COMMAND "${z3ml_bin}/ml_example${exe_ext}"
+    ">" "${z3ml_bin}/ml_example.log"
+  DEPENDS
+    ${z3ml_bin}/z3ml.cmxa
+    ${z3ml_bin}/dllz3ml.so
+    ${z3ml_bin}/ml_example.ml
+  COMMENT "Testing build and run ml_example natively"
+  VERBATIM)
+
+add_custom_target(build_ocaml_example
+  ALL
+  DEPENDS
+    ${z3ml_bin}/ml_example${bc_ext}
+    ${z3ml_bin}/ml_example${exe_ext}
+)
+
+add_custom_target(build_z3_ocaml_bindings
+  ALL
+  DEPENDS
+    ${z3ml_bin}/z3ml.cma
+    ${z3ml_bin}/z3ml.cmxa
+    ${z3ml_bin}/z3ml.cmxs
+    ${z3ml_bin}/dllz3ml.so
+    ${z3ml_bin}/libz3ml.a
+    build_ocaml_example
+)
+
+###############################################################################
+# Install
+###############################################################################
+
+# Hacky: When the os is APPLE, a fix command will mutate `libz3.dylib` and `dlllibz3.so` inplace.
+# I don't know how to use conditional `COMMAND` nor specify a file dependency for itself
+# Renaming it and back seems a simple solution.
+
+#   COMMAND mv "${z3ml_bin}/dllz3ml.so" "${z3ml_bin}/dllz3ml.pre.so"
+# if (NOT APPLE)
+#   add_custom_command(
+#     OUTPUT "${z3ml_bin}/dllz3ml.so"
+#     COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so}"
+#     DEPENDS "${z3ml_bin}/dllz3ml.pre.so"
+#   )
+# else()
+#   # if IS_OSX:
+#   # install_name_tool -id ${stubs_install_path}/libz3.dylib libz3.dylib
+#   # install_name_tool -change libz3.dylib ${stubs_install_path}/libz3.dylib api/ml/dllz3ml.so
+#   add_custom_command(
+#     OUTPUT "${z3ml_bin}/dllz3ml.so"
+#     COMMAND mv "${z3ml_bin}/dllz3ml.pre.so" "${z3ml_bin}/dllz3ml.so"
+#     DEPENDS "${z3ml_bin}/dllz3ml.so"
+#   )
+# endif()
\ No newline at end of file
diff --git a/src/api/ml/z3.mli b/src/api/ml/z3.mli
index 5320fc38e..0b31874e1 100644
--- a/src/api/ml/z3.mli
+++ b/src/api/ml/z3.mli
@@ -42,9 +42,10 @@ type context
     - timeout (unsigned)         default timeout (in milliseconds) used for solvers
     - well_sorted_check          type checker
     - auto_config                use heuristics to automatically select solver and configure it
-    - model                      model generation for solvers, this parameter can be overwritten when creating a solver
-    - model_validate             validate models produced by solvers
-    - unsat_core                 unsat-core generation for solvers, this parameter can be overwritten when creating a solver
+    - model  (Boolean)           model generation for solvers, this parameter can be overwritten when creating a solver
+    - model_validate  (Boolean)  validate models produced by solvers
+    - unsat_core  (Boolean)      unsat-core generation for solvers, this parameter can be overwritten when creating a solver
+    - encoding                   the string encoding used internally (must be either "unicode" - 18 bit, "bmp" - 16 bit or "ascii" - 8 bit)
 *)
 val mk_context : (string * string) list -> context
 
@@ -3712,6 +3713,31 @@ end
     For example:
     (set_global_param "pp.decimal" "true")
     will set the parameter "decimal" in the module "pp" to true.
+
+    Legal parameters are:
+        auto_config (bool) (default: true)
+        debug_ref_count (bool) (default: false)
+        dot_proof_file (string) (default: proof.dot)
+        dump_models (bool) (default: false)
+        encoding (string) (default: unicode)
+        memory_high_watermark (unsigned int) (default: 0)
+        memory_high_watermark_mb (unsigned int) (default: 0)
+        memory_max_alloc_count (unsigned int) (default: 0)
+        memory_max_size (unsigned int) (default: 0)
+        model (bool) (default: true)
+        model_validate (bool) (default: false)
+        proof (bool) (default: false)
+        rlimit (unsigned int) (default: 0)
+        smtlib2_compliant (bool) (default: false)
+        stats (bool) (default: false)
+        timeout (unsigned int) (default: 4294967295)
+        trace (bool) (default: false)
+        trace_file_name (string) (default: z3.log)
+        type_check (bool) (default: true)
+        unsat_core (bool) (default: false)
+        verbose (unsigned int) (default: 0)
+        warning (bool) (default: true)
+        well_sorted_check (bool) (default: false)
 *)
 val set_global_param : string -> string -> unit