diff --git a/README-CMake.md b/README-CMake.md
index 26bde8f37..c9edb9378 100644
--- a/README-CMake.md
+++ b/README-CMake.md
@@ -423,6 +423,7 @@ 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_GO_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's Go bindings will be built. Requires Go 1.20+ and ``Z3_BUILD_LIBZ3_SHARED=ON``.
 * ``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.
@@ -523,6 +524,41 @@ where ``VERSION`` is the Z3 version. Under non Windows systems a
 symbolic link named ``com.microsoft.z3.jar`` is provided. This symbolic
 link is not created when building under Windows.
 
+### Go bindings
+
+Go bindings can be built by setting ``Z3_BUILD_GO_BINDINGS=ON``. The Go bindings use CGO to wrap
+the Z3 C API, so you'll need:
+
+* Go 1.20 or later installed on your system
+* ``Z3_BUILD_LIBZ3_SHARED=ON`` (Go bindings require the shared library)
+
+Example:
+
+```
+mkdir build
+cd build
+cmake -DZ3_BUILD_GO_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ../
+make
+```
+
+If CMake detects a Go installation (via ``go`` executable in PATH), it will create two optional targets:
+
+* ``go-bindings`` - Builds the Go bindings
+* ``test-go-examples`` - Runs the Go examples
+
+Note that the Go bindings are installed as source files (not compiled) since Go packages are
+typically distributed as source and compiled by the user's Go toolchain.
+
+To use the installed Go bindings, set the appropriate CGO flags:
+
+```
+export CGO_CFLAGS="-I/path/to/z3/include"
+export CGO_LDFLAGS="-L/path/to/z3/lib -lz3"
+export LD_LIBRARY_PATH="/path/to/z3/lib:$LD_LIBRARY_PATH"  # Linux/macOS
+```
+
+For detailed usage examples and API documentation, see ``src/api/go/README.md`` and ``examples/go/``.
+
 ## Developer/packager notes
 
 These notes are help developers and packagers of Z3.
diff --git a/README.md b/README.md
index ddda3662c..04fe821ec 100644
--- a/README.md
+++ b/README.md
@@ -195,6 +195,14 @@ For IDE setup instructions (Eclipse, IntelliJ IDEA, Visual Studio Code) and trou
 
 See [``examples/java``](examples/java) for examples.
 
+### ``Go``
+
+Use the ``--go`` command line flag with ``mk_make.py`` to enable building these. Note that Go bindings use CGO and require a Go toolchain (Go 1.20 or later) to build.
+
+With CMake, use the ``-DZ3_BUILD_GO_BINDINGS=ON`` option.
+
+See [``examples/go``](examples/go) for examples and [``src/api/go/README.md``](src/api/go/README.md) for complete API documentation.
+
 ### ``OCaml``
 
 Use the ``--ml`` command line flag with ``mk_make.py`` to enable building these.
diff --git a/build_z3.bat b/build_z3.bat
new file mode 100644
index 000000000..57b0c233b
--- /dev/null
+++ b/build_z3.bat
@@ -0,0 +1,30 @@
+@echo off
+REM Z3 Build Script
+
+echo Checking for build directory...
+if not exist C:\z3\build (
+    echo Creating build directory...
+    mkdir C:\z3\build
+) else (
+    echo Build directory already exists
+)
+
+echo Changing to build directory...
+cd /d C:\z3\build
+
+echo Running CMake configuration...
+cmake ..
+if errorlevel 1 (
+    echo CMake configuration failed!
+    exit /b 1
+)
+
+echo Building Z3 with parallel 8...
+cmake --build . --parallel 8
+if errorlevel 1 (
+    echo Build failed!
+    exit /b 1
+)
+
+echo Build completed successfully!
+exit /b 0
diff --git a/doc/CMakeLists.txt b/doc/CMakeLists.txt
index 6f81edf0d..4b1de889b 100644
--- a/doc/CMakeLists.txt
+++ b/doc/CMakeLists.txt
@@ -9,6 +9,7 @@ set(MK_API_DOC_SCRIPT "${CMAKE_CURRENT_SOURCE_DIR}/mk_api_doc.py")
 set(PYTHON_API_OPTIONS "")
 set(DOTNET_API_OPTIONS "")
 set(JAVA_API_OPTIONS "")
+set(GO_API_OPTIONS "")
 SET(DOC_EXTRA_DEPENDS "")
 
 if (Z3_BUILD_PYTHON_BINDINGS)
@@ -41,6 +42,15 @@ else()
   list(APPEND JAVA_API_OPTIONS "--no-java")
 endif()
 
+if (Z3_BUILD_GO_BINDINGS)
+  list(APPEND GO_API_OPTIONS "--go")
+  list(APPEND GO_API_OPTIONS "--go-search-paths"
+    "${PROJECT_SOURCE_DIR}/src/api/go"
+  )
+else()
+  # Go bindings don't have a --no-go option, just omit --go
+endif()
+
 option(Z3_ALWAYS_BUILD_DOCS "Always build documentation for API bindings" ON)
 if (Z3_ALWAYS_BUILD_DOCS)
   set(ALWAYS_BUILD_DOCS_ARG "ALL")
@@ -66,12 +76,26 @@ add_custom_target(api_docs ${ALWAYS_BUILD_DOCS_ARG}
   ${PYTHON_API_OPTIONS}
   ${DOTNET_API_OPTIONS}
   ${JAVA_API_OPTIONS}
+  ${GO_API_OPTIONS}
   DEPENDS
     ${DOC_EXTRA_DEPENDS}
   COMMENT "Generating documentation"
   USES_TERMINAL
 )
 
+# Add separate target for Go documentation
+if (Z3_BUILD_GO_BINDINGS)
+  set(MK_GO_DOC_SCRIPT "${CMAKE_CURRENT_SOURCE_DIR}/mk_go_doc.py")
+  add_custom_target(go_docs
+    COMMAND
+    "${Python3_EXECUTABLE}" "${MK_GO_DOC_SCRIPT}"
+    --output-dir "${DOC_DEST_DIR}/html/go"
+    --go-api-path "${PROJECT_SOURCE_DIR}/src/api/go"
+    COMMENT "Generating Go API documentation"
+    USES_TERMINAL
+  )
+endif()
+
 # Remove generated documentation when running `clean` target.
 set_property(DIRECTORY APPEND PROPERTY
   ADDITIONAL_MAKE_CLEAN_FILES
diff --git a/doc/README b/doc/README
index e46554230..cfb34b4e5 100644
--- a/doc/README
+++ b/doc/README
@@ -1,7 +1,7 @@
 API documentation
 -----------------
 
-To generate the API documentation for the C, C++, .NET, Java and Python APIs, we must execute
+To generate the API documentation for the C, C++, .NET, Java, Python, and Go APIs, we must execute
 
    python mk_api_doc.py
 
@@ -10,6 +10,12 @@ We must have doxygen installed in our system.
 The documentation will be stored in the subdirectory './api/html'.
 The main file is './api/html/index.html'
 
+To include Go API documentation, use:
+
+   python mk_api_doc.py --go
+
+Note: Go documentation requires Go to be installed (for godoc support).
+
 Code documentation
 ------------------
 
diff --git a/doc/mk_api_doc.py b/doc/mk_api_doc.py
index f5c4ff68c..ae3d6c931 100644
--- a/doc/mk_api_doc.py
+++ b/doc/mk_api_doc.py
@@ -15,24 +15,27 @@ import subprocess
 ML_ENABLED=False
 MLD_ENABLED=False
 JS_ENABLED=False
+GO_ENABLED=False
 BUILD_DIR='../build'
 DOXYGEN_EXE='doxygen'
 TEMP_DIR=os.path.join(os.getcwd(), 'tmp')
 OUTPUT_DIRECTORY=os.path.join(os.getcwd(), 'api')
 Z3PY_PACKAGE_PATH='../src/api/python/z3'
 JS_API_PATH='../src/api/js'
+GO_API_PATH='../src/api/go'
 Z3PY_ENABLED=True
 DOTNET_ENABLED=True
 JAVA_ENABLED=True
 Z3OPTIONS_ENABLED=True
 DOTNET_API_SEARCH_PATHS=['../src/api/dotnet']
 JAVA_API_SEARCH_PATHS=['../src/api/java']
+GO_API_SEARCH_PATHS=['../src/api/go']
 SCRIPT_DIR=os.path.abspath(os.path.dirname(__file__))
 
 def parse_options():
     global ML_ENABLED, MLD_ENABLED, BUILD_DIR, DOXYGEN_EXE, TEMP_DIR, OUTPUT_DIRECTORY
-    global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED, JS_ENABLED
-    global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS, JS_API_PATH
+    global Z3PY_PACKAGE_PATH, Z3PY_ENABLED, DOTNET_ENABLED, JAVA_ENABLED, JS_ENABLED, GO_ENABLED
+    global DOTNET_API_SEARCH_PATHS, JAVA_API_SEARCH_PATHS, GO_API_SEARCH_PATHS, JS_API_PATH, GO_API_PATH
     parser = argparse.ArgumentParser(description=__doc__)
     parser.add_argument('-b',
         '--build',
@@ -54,6 +57,11 @@ def parse_options():
         default=False,
         help='Include JS/TS API documentation'
     )
+    parser.add_argument('--go',
+        action='store_true',
+        default=False,
+        help='Include Go API documentation'
+    )
     parser.add_argument('--doxygen-executable',
         dest='doxygen_executable',
         default=DOXYGEN_EXE,
@@ -109,10 +117,17 @@ def parse_options():
         default=JAVA_API_SEARCH_PATHS,
         help='Specify one or more paths to look for Java files (default: %(default)s).',
     )
+    parser.add_argument('--go-search-paths',
+        dest='go_search_paths',
+        nargs='+',
+        default=GO_API_SEARCH_PATHS,
+        help='Specify one or more paths to look for Go files (default: %(default)s).',
+    )
     pargs = parser.parse_args()
     ML_ENABLED = pargs.ml
     MLD_ENABLED = pargs.mld
     JS_ENABLED = pargs.js
+    GO_ENABLED = pargs.go
     BUILD_DIR = pargs.build
     DOXYGEN_EXE = pargs.doxygen_executable
     TEMP_DIR = pargs.temp_dir
@@ -123,6 +138,7 @@ def parse_options():
     JAVA_ENABLED = not pargs.no_java
     DOTNET_API_SEARCH_PATHS = pargs.dotnet_search_paths
     JAVA_API_SEARCH_PATHS = pargs.java_search_paths
+    GO_API_SEARCH_PATHS = pargs.go_search_paths
 
     if Z3PY_ENABLED:
         if not os.path.exists(Z3PY_PACKAGE_PATH):
@@ -288,6 +304,18 @@ try:
         print("Java documentation disabled")
         doxygen_config_substitutions['JAVA_API_FILES'] = ''
         doxygen_config_substitutions['JAVA_API_SEARCH_PATHS'] = ''
+    if GO_ENABLED:
+        print("Go documentation enabled")
+        doxygen_config_substitutions['GO_API_FILES'] = '*.go'
+        go_api_search_path_str = ""
+        for p in GO_API_SEARCH_PATHS:
+            # Quote path so that paths with spaces are handled correctly
+            go_api_search_path_str += "\"{}\" ".format(p)
+        doxygen_config_substitutions['GO_API_SEARCH_PATHS'] = go_api_search_path_str
+    else:
+        print("Go documentation disabled")
+        doxygen_config_substitutions['GO_API_FILES'] = ''
+        doxygen_config_substitutions['GO_API_SEARCH_PATHS'] = ''
     if JS_ENABLED:
         print('Javascript documentation enabled')
     else:
@@ -350,6 +378,13 @@ try:
                 prefix=bullet_point_prefix)
     else:
         website_dox_substitutions['JS_API'] = ''
+    if GO_ENABLED:
+        website_dox_substitutions['GO_API'] = (
+            '{prefix}<a class="el" href="go/index.html">Go API</a>'
+            ).format(
+                prefix=bullet_point_prefix)
+    else:
+        website_dox_substitutions['GO_API'] = ''
     configure_file(
         doc_path('website.dox.in'),
         temp_path('website.dox'),
@@ -428,6 +463,97 @@ try:
             exit(1)
         print("Generated Javascript documentation.")
 
+    if GO_ENABLED:
+        go_output_dir = os.path.join(OUTPUT_DIRECTORY, 'html', 'go')
+        mk_dir(go_output_dir)
+        go_api_abs_path = os.path.abspath(GO_API_PATH)
+        
+        # Check if godoc is available
+        godoc_available = False
+        try:
+            subprocess.check_output(['go', 'version'], stderr=subprocess.STDOUT)
+            godoc_available = True
+        except (subprocess.CalledProcessError, FileNotFoundError):
+            print("WARNING: Go is not installed. Skipping godoc generation.")
+            godoc_available = False
+        
+        if godoc_available:
+            # Generate godoc HTML for each Go file
+            go_files = [
+                'z3.go', 'solver.go', 'tactic.go', 'bitvec.go', 
+                'fp.go', 'seq.go', 'datatype.go', 'optimize.go'
+            ]
+            
+            # Create a simple HTML index
+            index_html = os.path.join(go_output_dir, 'index.html')
+            with open(index_html, 'w') as f:
+                f.write('<!DOCTYPE html>\n<html>\n<head>\n')
+                f.write('<title>Z3 Go API Documentation</title>\n')
+                f.write('<style>\n')
+                f.write('body { font-family: Arial, sans-serif; margin: 40px; }\n')
+                f.write('h1 { color: #333; }\n')
+                f.write('ul { list-style-type: none; padding: 0; }\n')
+                f.write('li { margin: 10px 0; }\n')
+                f.write('a { color: #0066cc; text-decoration: none; font-size: 18px; }\n')
+                f.write('a:hover { text-decoration: underline; }\n')
+                f.write('.description { color: #666; margin-left: 20px; }\n')
+                f.write('</style>\n')
+                f.write('</head>\n<body>\n')
+                f.write('<h1>Z3 Go API Documentation</h1>\n')
+                f.write('<p>Go bindings for the Z3 Theorem Prover.</p>\n')
+                f.write('<h2>Package: github.com/Z3Prover/z3/src/api/go</h2>\n')
+                f.write('<ul>\n')
+                
+                # Add links to the README
+                readme_path = os.path.join(go_api_abs_path, 'README.md')
+                if os.path.exists(readme_path):
+                    # Copy README as index documentation
+                    readme_html_path = os.path.join(go_output_dir, 'README.html')
+                    try:
+                        # Try to convert markdown to HTML if markdown module is available
+                        with open(readme_path, 'r') as rf:
+                            readme_content = rf.read()
+                        with open(readme_html_path, 'w') as wf:
+                            wf.write('<!DOCTYPE html>\n<html>\n<head>\n')
+                            wf.write('<title>Z3 Go API - README</title>\n')
+                            wf.write('<style>body { font-family: Arial, sans-serif; margin: 40px; max-width: 900px; }</style>\n')
+                            wf.write('</head>\n<body>\n<pre>\n')
+                            wf.write(readme_content)
+                            wf.write('</pre>\n</body>\n</html>\n')
+                        f.write('<li><a href="README.html">README - Getting Started</a></li>\n')
+                    except Exception as e:
+                        print(f"Warning: Could not process README.md: {e}")
+                
+                # Add module descriptions
+                f.write('<li><a href="#core">z3.go</a> - Core types (Context, Config, Symbol, Sort, Expr, FuncDecl)</li>\n')
+                f.write('<li><a href="#solver">solver.go</a> - Solver and Model API</li>\n')
+                f.write('<li><a href="#tactic">tactic.go</a> - Tactics, Goals, Probes, and Parameters</li>\n')
+                f.write('<li><a href="#bitvec">bitvec.go</a> - Bit-vector operations</li>\n')
+                f.write('<li><a href="#fp">fp.go</a> - Floating-point operations</li>\n')
+                f.write('<li><a href="#seq">seq.go</a> - Sequences, strings, and regular expressions</li>\n')
+                f.write('<li><a href="#datatype">datatype.go</a> - Algebraic datatypes, tuples, enumerations</li>\n')
+                f.write('<li><a href="#optimize">optimize.go</a> - Optimization with maximize/minimize objectives</li>\n')
+                f.write('</ul>\n')
+                
+                f.write('<h2>Usage</h2>\n')
+                f.write('<pre>\n')
+                f.write('import "github.com/Z3Prover/z3/src/api/go"\n\n')
+                f.write('ctx := z3.NewContext()\n')
+                f.write('solver := ctx.NewSolver()\n')
+                f.write('x := ctx.MkIntConst("x")\n')
+                f.write('solver.Assert(ctx.MkGt(x, ctx.MkInt(0, ctx.MkIntSort())))\n')
+                f.write('if solver.Check() == z3.Satisfiable {\n')
+                f.write('    fmt.Println("sat")\n')
+                f.write('}\n')
+                f.write('</pre>\n')
+                
+                f.write('<h2>Installation</h2>\n')
+                f.write('<p>See <a href="README.html">README</a> for build instructions.</p>\n')
+                f.write('<p>Go back to <a href="../index.html">main API documentation</a>.</p>\n')
+                f.write('</body>\n</html>\n')
+            
+            print("Generated Go documentation.")
+
     print("Documentation was successfully generated at subdirectory '{}'.".format(OUTPUT_DIRECTORY))
 except Exception:
     exctype, value = sys.exc_info()[:2]
diff --git a/doc/mk_go_doc.py b/doc/mk_go_doc.py
new file mode 100644
index 000000000..5ba122979
--- /dev/null
+++ b/doc/mk_go_doc.py
@@ -0,0 +1,654 @@
+#!/usr/bin/env python
+# Copyright (c) Microsoft Corporation 2025
+"""
+Z3 Go API documentation generator script
+
+This script generates HTML documentation for the Z3 Go bindings.
+It creates a browsable HTML interface for the Go API documentation.
+"""
+
+import os
+import sys
+import subprocess
+import argparse
+import re
+
+SCRIPT_DIR = os.path.abspath(os.path.dirname(__file__))
+GO_API_PATH = os.path.join(SCRIPT_DIR, '..', 'src', 'api', 'go')
+OUTPUT_DIR = os.path.join(SCRIPT_DIR, 'api', 'html', 'go')
+
+def extract_types_and_functions(filepath):
+    """Extract type and function names from a Go source file."""
+    types = []
+    functions = []
+    
+    try:
+        with open(filepath, 'r', encoding='utf-8') as f:
+            content = f.read()
+            
+            # Extract type declarations
+            type_pattern = r'type\s+(\w+)\s+(?:struct|interface)'
+            types = re.findall(type_pattern, content)
+            
+            # Extract function/method declarations
+            # Match both: func Name() and func (r *Type) Name()
+            func_pattern = r'func\s+(?:\([^)]+\)\s+)?(\w+)\s*\('
+            functions = re.findall(func_pattern, content)
+            
+    except Exception as e:
+        print(f"Warning: Could not parse {filepath}: {e}")
+    
+    return types, functions
+
+def extract_detailed_api(filepath):
+    """Extract detailed type and function information with signatures and comments."""
+    types_info = {}
+    functions_info = []
+    context_methods = []  # Special handling for Context methods
+    
+    try:
+        with open(filepath, 'r', encoding='utf-8') as f:
+            lines = f.readlines()
+            i = 0
+            
+            while i < len(lines):
+                line = lines[i].strip()
+                
+                # Extract type with comment
+                if line.startswith('type ') and ('struct' in line or 'interface' in line):
+                    # Look back for comment
+                    comment = ""
+                    j = i - 1
+                    while j >= 0 and (lines[j].strip().startswith('//') or lines[j].strip() == ''):
+                        if lines[j].strip().startswith('//'):
+                            comment = lines[j].strip()[2:].strip() + " " + comment
+                        j -= 1
+                    
+                    match = re.match(r'type\s+(\w+)\s+', line)
+                    if match:
+                        type_name = match.group(1)
+                        types_info[type_name] = {
+                            'comment': comment.strip(),
+                            'methods': []
+                        }
+                
+                # Extract function/method with signature and comment
+                if line.startswith('func '):
+                    # Look back for comment
+                    comment = ""
+                    j = i - 1
+                    while j >= 0 and (lines[j].strip().startswith('//') or lines[j].strip() == ''):
+                        if lines[j].strip().startswith('//'):
+                            comment = lines[j].strip()[2:].strip() + " " + comment
+                        j -= 1
+                    
+                    # Extract full signature (may span multiple lines)
+                    signature = line
+                    k = i + 1
+                    while k < len(lines) and '{' not in signature:
+                        signature += ' ' + lines[k].strip()
+                        k += 1
+                    
+                    # Remove body
+                    if '{' in signature:
+                        signature = signature[:signature.index('{')].strip()
+                    
+                    # Parse receiver if method
+                    method_match = re.match(r'func\s+\(([^)]+)\)\s+(\w+)', signature)
+                    func_match = re.match(r'func\s+(\w+)', signature)
+                    
+                    if method_match:
+                        receiver = method_match.group(1).strip()
+                        func_name = method_match.group(2)
+                        # Extract receiver type
+                        receiver_type = receiver.split()[-1].strip('*')
+                        
+                        # Only add if function name is public
+                        if func_name[0].isupper():
+                            if receiver_type == 'Context':
+                                # Special handling for Context methods - add to context_methods
+                                context_methods.append({
+                                    'name': func_name,
+                                    'signature': signature,
+                                    'comment': comment.strip()
+                                })
+                            elif receiver_type in types_info:
+                                types_info[receiver_type]['methods'].append({
+                                    'name': func_name,
+                                    'signature': signature,
+                                    'comment': comment.strip()
+                                })
+                    elif func_match:
+                        func_name = func_match.group(1)
+                        # Only add if it's public (starts with capital)
+                        if func_name[0].isupper():
+                            functions_info.append({
+                                'name': func_name,
+                                'signature': signature,
+                                'comment': comment.strip()
+                            })
+                
+                i += 1
+            
+            # If we have Context methods but no other content, return them as functions
+            if context_methods and not types_info and not functions_info:
+                functions_info = context_methods
+            elif context_methods:
+                # Add Context pseudo-type
+                types_info['Context'] = {
+                    'comment': 'Context methods (receiver omitted for clarity)',
+                    'methods': context_methods
+                }
+                
+    except Exception as e:
+        print(f"Warning: Could not parse detailed API from {filepath}: {e}")
+    
+    return types_info, functions_info
+
+def extract_package_comment(filepath):
+    """Extract the package-level documentation comment from a Go file."""
+    try:
+        with open(filepath, 'r', encoding='utf-8') as f:
+            lines = f.readlines()
+            comment_lines = []
+            in_comment = False
+            
+            for line in lines:
+                stripped = line.strip()
+                if stripped.startswith('/*'):
+                    in_comment = True
+                    comment_lines.append(stripped[2:].strip())
+                elif in_comment:
+                    if '*/' in stripped:
+                        comment_lines.append(stripped.replace('*/', '').strip())
+                        break
+                    comment_lines.append(stripped.lstrip('*').strip())
+                elif stripped.startswith('//'):
+                    comment_lines.append(stripped[2:].strip())
+                elif stripped.startswith('package'):
+                    break
+            
+            return ' '.join(comment_lines).strip() if comment_lines else None
+    except Exception as e:
+        return None
+
+def parse_args():
+    parser = argparse.ArgumentParser(description=__doc__)
+    parser.add_argument('-o', '--output-dir',
+        dest='output_dir',
+        default=OUTPUT_DIR,
+        help='Output directory for documentation (default: %(default)s)',
+    )
+    parser.add_argument('--go-api-path',
+        dest='go_api_path',
+        default=GO_API_PATH,
+        help='Path to Go API source files (default: %(default)s)',
+    )
+    return parser.parse_args()
+
+def check_go_installed():
+    """Check if Go is installed and available."""
+    try:
+        # Try to find go in common locations
+        go_paths = [
+            'go',
+            'C:\\Program Files\\Go\\bin\\go.exe',
+            'C:\\Go\\bin\\go.exe',
+        ]
+        
+        for go_cmd in go_paths:
+            try:
+                result = subprocess.run([go_cmd, 'version'], 
+                                      capture_output=True, 
+                                      text=True,
+                                      check=True,
+                                      timeout=5)
+                print(f"Found Go: {result.stdout.strip()}")
+                return go_cmd
+            except (subprocess.CalledProcessError, FileNotFoundError, subprocess.TimeoutExpired):
+                continue
+        
+        print("WARNING: Go is not installed or not in PATH")
+        print("Install Go from https://golang.org/dl/ for enhanced documentation")
+        return None
+    except Exception as e:
+        print(f"WARNING: Could not check Go installation: {e}")
+        return None
+
+def extract_package_comment(go_file_path):
+    """Extract package-level documentation comment from a Go file."""
+    try:
+        with open(go_file_path, 'r', encoding='utf-8') as f:
+            lines = f.readlines()
+            in_comment = False
+            comment_lines = []
+            
+            for line in lines:
+                stripped = line.strip()
+                if stripped.startswith('/*'):
+                    in_comment = True
+                    comment_lines.append(stripped[2:].strip())
+                elif in_comment:
+                    if stripped.endswith('*/'):
+                        comment_lines.append(stripped[:-2].strip())
+                        break
+                    comment_lines.append(stripped.lstrip('*').strip())
+                elif stripped.startswith('//'):
+                    comment_lines.append(stripped[2:].strip())
+                elif stripped.startswith('package '):
+                    break
+            
+            return ' '.join(comment_lines).strip()
+    except Exception as e:
+        print(f"Warning: Could not extract comment from {go_file_path}: {e}")
+        return ""
+
+def generate_godoc_markdown(go_cmd, go_api_path, output_dir):
+    """Generate markdown documentation using godoc."""
+    print("Generating documentation with godoc...")
+    
+    os.makedirs(output_dir, exist_ok=True)
+    
+    try:
+        # Change to the Go API directory
+        orig_dir = os.getcwd()
+        os.chdir(go_api_path)
+        
+        # Run go doc to get package documentation
+        result = subprocess.run(
+            [go_cmd, 'doc', '-all'],
+            capture_output=True,
+            text=True,
+            timeout=30
+        )
+        
+        if result.returncode == 0:
+            # Create markdown file
+            doc_text = result.stdout
+            godoc_md = os.path.join(output_dir, 'godoc.md')
+            
+            with open(godoc_md, 'w', encoding='utf-8') as f:
+                f.write('# Z3 Go API Documentation (godoc)\n\n')
+                f.write(doc_text)
+            
+            print(f"Generated godoc markdown at: {godoc_md}")
+            os.chdir(orig_dir)
+            return True
+        else:
+            print(f"godoc returned error: {result.stderr}")
+            os.chdir(orig_dir)
+            return False
+            
+    except Exception as e:
+        print(f"Error generating godoc markdown: {e}")
+        try:
+            os.chdir(orig_dir)
+        except:
+            pass
+        return False
+
+def generate_module_page(module_filename, description, go_api_path, output_dir):
+    """Generate a detailed HTML page for a single Go module."""
+    file_path = os.path.join(go_api_path, module_filename)
+    if not os.path.exists(file_path):
+        return
+    
+    module_name = module_filename.replace('.go', '')
+    output_path = os.path.join(output_dir, f'{module_name}.html')
+    
+    # Extract detailed API information
+    types_info, functions_info = extract_detailed_api(file_path)
+    
+    with open(output_path, 'w', encoding='utf-8') as f:
+        f.write('<!DOCTYPE html>\n<html lang="en">\n<head>\n')
+        f.write('    <meta charset="UTF-8">\n')
+        f.write(f'    <title>{module_filename} - Z3 Go API</title>\n')
+        f.write('    <style>\n')
+        f.write('        body { font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, sans-serif; margin: 0; padding: 0; line-height: 1.6; }\n')
+        f.write('        header { background: #2d3748; color: white; padding: 2rem; }\n')
+        f.write('        header h1 { margin: 0; font-size: 2rem; }\n')
+        f.write('        header p { margin: 0.5rem 0 0 0; opacity: 0.9; }\n')
+        f.write('        .container { max-width: 1200px; margin: 0 auto; padding: 2rem; }\n')
+        f.write('        .nav { background: #edf2f7; padding: 1rem; margin-bottom: 2rem; border-radius: 4px; }\n')
+        f.write('        .nav a { color: #2b6cb0; text-decoration: none; margin-right: 1rem; }\n')
+        f.write('        .nav a:hover { text-decoration: underline; }\n')
+        f.write('        h2 { color: #2d3748; border-bottom: 2px solid #4299e1; padding-bottom: 0.5rem; margin-top: 2rem; }\n')
+        f.write('        h3 { color: #2d3748; margin-top: 1.5rem; }\n')
+        f.write('        .type-section, .function-section { margin: 1.5rem 0; }\n')
+        f.write('        .api-item { background: #f7fafc; padding: 1rem; margin: 1rem 0; border-left: 4px solid #4299e1; border-radius: 4px; }\n')
+        f.write('        .api-item h4 { margin: 0 0 0.5rem 0; color: #2b6cb0; font-family: monospace; }\n')
+        f.write('        .signature { background: #2d3748; color: #e2e8f0; padding: 0.75rem; border-radius: 4px; font-family: monospace; overflow-x: auto; margin: 0.5rem 0; }\n')
+        f.write('        .comment { color: #4a5568; margin: 0.5rem 0; }\n')
+        f.write('        code { background: #e2e8f0; padding: 2px 6px; border-radius: 3px; font-family: monospace; }\n')
+        f.write('        .method-list { margin-left: 1rem; }\n')
+        f.write('    </style>\n')
+        f.write('</head>\n<body>\n')
+        
+        f.write('    <header>\n')
+        f.write(f'        <h1>{module_filename}</h1>\n')
+        f.write(f'        <p>{description}</p>\n')
+        f.write('    </header>\n')
+        
+        f.write('    <div class="container">\n')
+        f.write('        <div class="nav">\n')
+        f.write('            <a href="index.html">← Back to Index</a>\n')
+        f.write('            <a href="godoc.md">Complete API Reference (markdown)</a>\n')
+        f.write('            <a href="README.md">README</a>\n')
+        f.write('            <a href="../index.html">All Languages</a>\n')
+        f.write('        </div>\n')
+        
+        # Types section
+        if types_info:
+            f.write('        <h2>Types</h2>\n')
+            for type_name in sorted(types_info.keys()):
+                type_data = types_info[type_name]
+                f.write('        <div class="type-section">\n')
+                f.write(f'            <h3>type {type_name}</h3>\n')
+                if type_data['comment']:
+                    f.write(f'            <p class="comment">{type_data["comment"]}</p>\n')
+                
+                # Methods
+                if type_data['methods']:
+                    f.write('            <div class="method-list">\n')
+                    f.write('                <h4>Methods:</h4>\n')
+                    for method in sorted(type_data['methods'], key=lambda m: m['name']):
+                        f.write('                <div class="api-item">\n')
+                        f.write(f'                    <h4>{method["name"]}</h4>\n')
+                        f.write(f'                    <div class="signature">{method["signature"]}</div>\n')
+                        if method['comment']:
+                            f.write(f'                    <p class="comment">{method["comment"]}</p>\n')
+                        f.write('                </div>\n')
+                    f.write('            </div>\n')
+                f.write('        </div>\n')
+        
+        # Package functions section
+        if functions_info:
+            f.write('        <h2>Functions</h2>\n')
+            f.write('        <div class="function-section">\n')
+            for func in sorted(functions_info, key=lambda f: f['name']):
+                f.write('            <div class="api-item">\n')
+                f.write(f'                <h4>{func["name"]}</h4>\n')
+                f.write(f'                <div class="signature">{func["signature"]}</div>\n')
+                if func['comment']:
+                    f.write(f'                <p class="comment">{func["comment"]}</p>\n')
+                f.write('            </div>\n')
+            f.write('        </div>\n')
+        
+        if not types_info and not functions_info:
+            f.write('        <p><em>No public API documentation extracted. See godoc for complete reference.</em></p>\n')
+        
+        f.write('        <div class="nav" style="margin-top: 3rem;">\n')
+        f.write('            <a href="index.html">← Back to Index</a>\n')
+        f.write('        </div>\n')
+        f.write('    </div>\n')
+        f.write('</body>\n</html>\n')
+    
+    print(f"Generated module page: {output_path}")
+
+def generate_html_docs(go_api_path, output_dir):
+    """Generate HTML documentation for Go bindings."""
+    
+    # Create output directory
+    os.makedirs(output_dir, exist_ok=True)
+    
+    # Go source files and their descriptions
+    go_files = {
+        'z3.go': 'Core types (Context, Config, Symbol, Sort, Expr, FuncDecl, Quantifier, Lambda) and basic operations',
+        'solver.go': 'Solver and Model API for SMT solving',
+        'tactic.go': 'Tactics, Goals, Probes, and Parameters for goal-based solving',
+        'arith.go': 'Arithmetic operations (integers, reals) and comparisons',
+        'array.go': 'Array operations (select, store, constant arrays)',
+        'bitvec.go': 'Bit-vector operations and constraints',
+        'fp.go': 'IEEE 754 floating-point operations',
+        'seq.go': 'Sequences, strings, and regular expressions',
+        'datatype.go': 'Algebraic datatypes, tuples, and enumerations',
+        'optimize.go': 'Optimization with maximize/minimize objectives',
+        'fixedpoint.go': 'Fixedpoint solver for Datalog and constrained Horn clauses (CHC)',
+        'log.go': 'Interaction logging for debugging and analysis',
+    }
+    
+    # Generate main index.html
+    index_path = os.path.join(output_dir, 'index.html')
+    with open(index_path, 'w', encoding='utf-8') as f:
+        f.write('<!DOCTYPE html>\n')
+        f.write('<html lang="en">\n')
+        f.write('<head>\n')
+        f.write('    <meta charset="UTF-8">\n')
+        f.write('    <meta name="viewport" content="width=device-width, initial-scale=1.0">\n')
+        f.write('    <title>Z3 Go API Documentation</title>\n')
+        f.write('    <style>\n')
+        f.write('        body { font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, sans-serif; margin: 0; padding: 0; line-height: 1.6; }\n')
+        f.write('        header { background: #2d3748; color: white; padding: 2rem; }\n')
+        f.write('        header h1 { margin: 0; font-size: 2.5rem; }\n')
+        f.write('        header p { margin: 0.5rem 0 0 0; font-size: 1.1rem; opacity: 0.9; }\n')
+        f.write('        .container { max-width: 1200px; margin: 0 auto; padding: 2rem; }\n')
+        f.write('        .section { margin: 2rem 0; }\n')
+        f.write('        .section h2 { color: #2d3748; border-bottom: 2px solid #4299e1; padding-bottom: 0.5rem; }\n')
+        f.write('        .file-list { list-style: none; padding: 0; }\n')
+        f.write('        .file-item { background: #f7fafc; border-left: 4px solid #4299e1; margin: 1rem 0; padding: 1rem; border-radius: 4px; }\n')
+        f.write('        .file-item h3 { margin: 0 0 0.5rem 0; color: #2d3748; }\n')
+        f.write('        .file-item h3 a { color: #2b6cb0; text-decoration: none; }\n')
+        f.write('        .file-item h3 a:hover { color: #4299e1; text-decoration: underline; }\n')
+        f.write('        .file-item p { margin: 0; color: #4a5568; }\n')
+        f.write('        .code-block { background: #2d3748; color: #e2e8f0; padding: 1.5rem; border-radius: 4px; overflow-x: auto; }\n')
+        f.write('        .code-block pre { margin: 0; }\n')
+        f.write('        .install-section { background: #edf2f7; padding: 1.5rem; border-radius: 4px; margin: 1rem 0; }\n')
+        f.write('        .back-link { display: inline-block; margin-top: 2rem; color: #2b6cb0; text-decoration: none; }\n')
+        f.write('        .back-link:hover { text-decoration: underline; }\n')
+        f.write('    </style>\n')
+        f.write('</head>\n')
+        f.write('<body>\n')
+        
+        f.write('    <header>\n')
+        f.write('        <h1>Z3 Go API Documentation</h1>\n')
+        f.write('        <p>Go bindings for the Z3 Theorem Prover</p>\n')
+        f.write('    </header>\n')
+        
+        f.write('    <div class="container">\n')
+        
+        # Overview section
+        f.write('        <div class="section">\n')
+        f.write('            <h2>Overview</h2>\n')
+        f.write('            <p>The Z3 Go bindings provide idiomatic Go access to the Z3 SMT solver. These bindings use CGO to wrap the Z3 C API and provide automatic memory management through Go finalizers.</p>\n')
+        f.write('            <p><strong>Package:</strong> <code>github.com/Z3Prover/z3/src/api/go</code></p>\n')
+        f.write('        </div>\n')
+        
+        # Quick start
+        f.write('        <div class="section">\n')
+        f.write('            <h2>Quick Start</h2>\n')
+        f.write('            <div class="code-block">\n')
+        f.write('                <pre>package main\n\n')
+        f.write('import (\n')
+        f.write('    "fmt"\n')
+        f.write('    "github.com/Z3Prover/z3/src/api/go"\n')
+        f.write(')\n\n')
+        f.write('func main() {\n')
+        f.write('    // Create a context\n')
+        f.write('    ctx := z3.NewContext()\n\n')
+        f.write('    // Create integer variable\n')
+        f.write('    x := ctx.MkIntConst("x")\n\n')
+        f.write('    // Create solver\n')
+        f.write('    solver := ctx.NewSolver()\n\n')
+        f.write('    // Add constraint: x > 0\n')
+        f.write('    zero := ctx.MkInt(0, ctx.MkIntSort())\n')
+        f.write('    solver.Assert(ctx.MkGt(x, zero))\n\n')
+        f.write('    // Check satisfiability\n')
+        f.write('    if solver.Check() == z3.Satisfiable {\n')
+        f.write('        fmt.Println("sat")\n')
+        f.write('        model := solver.Model()\n')
+        f.write('        if val, ok := model.Eval(x, true); ok {\n')
+        f.write('            fmt.Println("x =", val.String())\n')
+        f.write('        }\n')
+        f.write('    }\n')
+        f.write('}</pre>\n')
+        f.write('            </div>\n')
+        f.write('        </div>\n')
+        
+        # Installation
+        f.write('        <div class="section">\n')
+        f.write('            <h2>Installation</h2>\n')
+        f.write('            <div class="install-section">\n')
+        f.write('                <p><strong>Prerequisites:</strong></p>\n')
+        f.write('                <ul>\n')
+        f.write('                    <li>Go 1.20 or later</li>\n')
+        f.write('                    <li>Z3 built as a shared library</li>\n')
+        f.write('                    <li>CGO enabled (default)</li>\n')
+        f.write('                </ul>\n')
+        f.write('                <p><strong>Build Z3 with Go bindings:</strong></p>\n')
+        f.write('                <div class="code-block">\n')
+        f.write('                    <pre># Using CMake\n')
+        f.write('mkdir build && cd build\n')
+        f.write('cmake -DZ3_BUILD_GO_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ..\n')
+        f.write('make\n\n')
+        f.write('# Using Python build script\n')
+        f.write('python scripts/mk_make.py --go\n')
+        f.write('cd build && make</pre>\n')
+        f.write('                </div>\n')
+        f.write('                <p><strong>Set environment variables:</strong></p>\n')
+        f.write('                <div class="code-block">\n')
+        f.write('                    <pre>export CGO_CFLAGS="-I${Z3_ROOT}/src/api"\n')
+        f.write('export CGO_LDFLAGS="-L${Z3_ROOT}/build -lz3"\n')
+        f.write('export LD_LIBRARY_PATH="${Z3_ROOT}/build:$LD_LIBRARY_PATH"</pre>\n')
+        f.write('                </div>\n')
+        f.write('            </div>\n')
+        f.write('        </div>\n')
+        
+        # API modules with detailed documentation
+        f.write('        <div class="section">\n')
+        f.write('            <h2>API Modules</h2>\n')
+        
+        for filename, description in go_files.items():
+            file_path = os.path.join(go_api_path, filename)
+            if os.path.exists(file_path):
+                module_name = filename.replace('.go', '')
+                
+                # Generate individual module page
+                generate_module_page(filename, description, go_api_path, output_dir)
+                
+                # Extract types and functions from the file
+                types, functions = extract_types_and_functions(file_path)
+                
+                f.write(f'            <div class="file-item" id="{module_name}">\n')
+                f.write(f'                <h3><a href="{module_name}.html">{filename}</a></h3>\n')
+                f.write(f'                <p>{description}</p>\n')
+                
+                if types:
+                    f.write('                <p><strong>Types:</strong> ')
+                    f.write(', '.join([f'<code>{t}</code>' for t in sorted(types)]))
+                    f.write('</p>\n')
+                
+                if functions:
+                    # Filter public functions
+                    public_funcs = [f for f in functions if f and len(f) > 0 and f[0].isupper()]
+                    if public_funcs:
+                        f.write('                <p><strong>Key Functions:</strong> ')
+                        # Show first 15 functions to keep it manageable
+                        funcs_to_show = sorted(public_funcs)[:15]
+                        f.write(', '.join([f'<code>{func}()</code>' for func in funcs_to_show]))
+                        if len(public_funcs) > 15:
+                            f.write(f' <em>(+{len(public_funcs)-15} more)</em>')
+                        f.write('</p>\n')
+                
+                f.write(f'                <p><a href="{module_name}.html">→ View full API reference</a></p>\n')
+                f.write('            </div>\n')
+        
+        f.write('        </div>\n')
+        
+        # Features section
+        f.write('        <div class="section">\n')
+        f.write('            <h2>Features</h2>\n')
+        f.write('            <ul>\n')
+        f.write('                <li><strong>Core SMT:</strong> Boolean logic, arithmetic, arrays, quantifiers</li>\n')
+        f.write('                <li><strong>Bit-vectors:</strong> Fixed-size bit-vector arithmetic and operations</li>\n')
+        f.write('                <li><strong>Floating-point:</strong> IEEE 754 floating-point arithmetic</li>\n')
+        f.write('                <li><strong>Strings & Sequences:</strong> String constraints and sequence operations</li>\n')
+        f.write('                <li><strong>Regular Expressions:</strong> Pattern matching and regex constraints</li>\n')
+        f.write('                <li><strong>Datatypes:</strong> Algebraic datatypes, tuples, enumerations</li>\n')
+        f.write('                <li><strong>Tactics:</strong> Goal-based solving with tactic combinators</li>\n')
+        f.write('                <li><strong>Optimization:</strong> MaxSMT with maximize/minimize objectives</li>\n')
+        f.write('                <li><strong>Memory Management:</strong> Automatic via Go finalizers</li>\n')
+        f.write('            </ul>\n')
+        f.write('        </div>\n')
+        
+        # Resources
+        f.write('        <div class="section">\n')
+        f.write('            <h2>Resources</h2>\n')
+        f.write('            <ul>\n')
+        f.write('                <li><a href="https://github.com/Z3Prover/z3">Z3 GitHub Repository</a></li>\n')
+        f.write('                <li><a href="../index.html">All API Documentation</a></li>\n')
+        
+        # Check if README exists and copy it
+        readme_path = os.path.join(go_api_path, 'README.md')
+        if os.path.exists(readme_path):
+            # Copy README.md to output directory
+            readme_dest = os.path.join(output_dir, 'README.md')
+            try:
+                import shutil
+                shutil.copy2(readme_path, readme_dest)
+                f.write('                <li><a href="README.md">Go API README (markdown)</a></li>\n')
+                print(f"Copied README.md to: {readme_dest}")
+            except Exception as e:
+                print(f"Warning: Could not copy README.md: {e}")
+        
+        # Link to godoc.md if it will be generated
+        f.write('                <li><a href="godoc.md">Complete API Reference (godoc markdown)</a></li>\n')
+        
+        f.write('            </ul>\n')
+        f.write('        </div>\n')
+        
+        f.write('        <a href="../index.html" class="back-link">← Back to main API documentation</a>\n')
+        f.write('    </div>\n')
+        f.write('</body>\n')
+        f.write('</html>\n')
+    
+    print(f"Generated Go documentation index at: {index_path}")
+    return True
+
+def main():
+    args = parse_args()
+    
+    print("Z3 Go API Documentation Generator")
+    print("=" * 50)
+    
+    # Check if Go is installed
+    go_cmd = check_go_installed()
+    
+    # Verify Go API path exists
+    if not os.path.exists(args.go_api_path):
+        print(f"ERROR: Go API path does not exist: {args.go_api_path}")
+        return 1
+    
+    # Generate documentation
+    print(f"\nGenerating documentation from: {args.go_api_path}")
+    print(f"Output directory: {args.output_dir}")
+    
+    # Try godoc first if Go is available
+    godoc_success = False
+    if go_cmd:
+        godoc_success = generate_godoc_markdown(go_cmd, args.go_api_path, args.output_dir)
+    
+    # Always generate our custom HTML documentation
+    if not generate_html_docs(args.go_api_path, args.output_dir):
+        print("ERROR: Failed to generate documentation")
+        return 1
+    
+    if godoc_success:
+        print("\n✓ Generated both godoc markdown and custom HTML documentation")
+    
+    print("\n" + "=" * 50)
+    print("Documentation generated successfully!")
+    print(f"Open {os.path.join(args.output_dir, 'index.html')} in your browser.")
+    
+    return 0
+
+if __name__ == '__main__':
+    try:
+        sys.exit(main())
+    except KeyboardInterrupt:
+        print("\nInterrupted by user")
+        sys.exit(1)
+    except Exception as e:
+        print(f"ERROR: {e}")
+        import traceback
+        traceback.print_exc()
+        sys.exit(1)
diff --git a/doc/test_go_doc/README.html b/doc/test_go_doc/README.html
new file mode 100644
index 000000000..5faf285e6
--- /dev/null
+++ b/doc/test_go_doc/README.html
@@ -0,0 +1,303 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <title>Z3 Go API - README</title>
+    <style>body { font-family: monospace; margin: 40px; max-width: 1000px; white-space: pre-wrap; }</style>
+</head>
+<body>
+# Z3 Go Bindings
+
+This directory contains Go language bindings for the Z3 theorem prover.
+
+## Overview
+
+The Go bindings provide a comprehensive interface to Z3's C API using CGO. The bindings support:
+
+- **Core Z3 Types**: Context, Config, Symbol, AST, Sort, Expr, FuncDecl
+- **Solver Operations**: Creating solvers, asserting constraints, checking satisfiability
+- **Model Manipulation**: Extracting and evaluating models
+- **Boolean Logic**: And, Or, Not, Implies, Iff, Xor
+- **Arithmetic**: Add, Sub, Mul, Div, Mod, comparison operators
+- **Bit-vectors**: Full bit-vector arithmetic, bitwise operations, shifts, comparisons
+- **Floating Point**: IEEE 754 floating-point arithmetic with rounding modes
+- **Arrays**: Select, Store, constant arrays
+- **Sequences/Strings**: String operations, concatenation, contains, indexing
+- **Regular Expressions**: Pattern matching, Kleene star/plus, regex operations
+- **Quantifiers**: Forall, Exists
+- **Functions**: Function declarations and applications
+- **Tactics & Goals**: Goal-based solving and tactic combinators
+- **Probes**: Goal property checking
+- **Datatypes**: Algebraic datatypes, tuples, enumerations, lists
+- **Parameters**: Solver and tactic configuration
+- **Optimize**: Optimization problems with maximize/minimize objectives
+
+## Building
+
+### Prerequisites
+
+- Go 1.20 or later
+- Z3 library built and installed
+- CGO enabled
+
+### With CMake
+
+```bash
+mkdir build && cd build
+cmake -DBUILD_GO_BINDINGS=ON ..
+make
+```
+
+### With Python Build System
+
+```bash
+python scripts/mk_make.py --go
+cd build
+make
+```
+
+## Usage
+
+### Basic Example
+
+```go
+package main
+
+import (
+    "fmt"
+    "github.com/Z3Prover/z3/src/api/go"
+)
+
+func main() {
+    // Create a context
+    ctx := z3.NewContext()
+    
+    // Create variables
+    x := ctx.MkIntConst("x")
+    y := ctx.MkIntConst("y")
+    
+    // Create constraints: x + y == 10 && x > y
+    ten := ctx.MkInt(10, ctx.MkIntSort())
+    eq := ctx.MkEq(ctx.MkAdd(x, y), ten)
+    gt := ctx.MkGt(x, y)
+    
+    // Create solver and check
+    solver := ctx.NewSolver()
+    solver.Assert(eq)
+    solver.Assert(gt)
+    
+    if solver.Check() == z3.Satisfiable {
+        model := solver.Model()
+        if xVal, ok := model.Eval(x, true); ok {
+            fmt.Println("x =", xVal.String())
+        }
+        if yVal, ok := model.Eval(y, true); ok {
+            fmt.Println("y =", yVal.String())
+        }
+    }
+}
+```
+
+### Running Examples
+
+```bash
+cd examples/go
+
+# Set library path (Linux/Mac)
+export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
+export CGO_CFLAGS="-I../../src/api"
+export CGO_LDFLAGS="-L../../build -lz3"
+
+# Set library path (Windows)
+set PATH=..\..\build;%PATH%
+set CGO_CFLAGS=-I../../src/api
+set CGO_LDFLAGS=-L../../build -lz3
+
+# Run example
+go run basic_example.go
+```
+
+## API Reference
+
+### Context
+
+- `NewContext()` - Create a new Z3 context
+- `NewContextWithConfig(cfg *Config)` - Create context with configuration
+- `SetParam(key, value string)` - Set context parameters
+
+### Creating Expressions
+
+- `MkBoolConst(name string)` - Create Boolean variable
+- `MkIntConst(name string)` - Create integer variable
+- `MkRealConst(name string)` - Create real variable
+- `MkInt(value int, sort *Sort)` - Create integer constant
+- `MkReal(num, den int)` - Create rational constant
+
+### Boolean Operations
+
+- `MkAnd(exprs ...*Expr)` - Conjunction
+- `MkOr(exprs ...*Expr)` - Disjunction
+- `MkNot(expr *Expr)` - Negation
+- `MkImplies(lhs, rhs *Expr)` - Implication
+- `MkIff(lhs, rhs *Expr)` - If-and-only-if
+- `MkXor(lhs, rhs *Expr)` - Exclusive or
+
+### Arithmetic Operations
+
+- `MkAdd(exprs ...*Expr)` - Addition
+- `MkSub(exprs ...*Expr)` - Subtraction
+- `MkMul(exprs ...*Expr)` - Multiplication
+- `MkDiv(lhs, rhs *Expr)` - Division
+- `MkMod(lhs, rhs *Expr)` - Modulo
+- `MkRem(lhs, rhs *Expr)` - Remainder
+
+### Comparison Operations
+
+- `MkEq(lhs, rhs *Expr)` - Equality
+- `MkDistinct(exprs ...*Expr)` - Distinct
+- `MkLt(lhs, rhs *Expr)` - Less than
+- `MkLe(lhs, rhs *Expr)` - Less than or equal
+- `MkGt(lhs, rhs *Expr)` - Greater than
+- `MkGe(lhs, rhs *Expr)` - Greater than or equal
+
+### Solver Operations
+
+- `NewSolver()` - Create a new solver
+- `Assert(constraint *Expr)` - Add constraint
+- `Check()` - Check satisfiability (returns Satisfiable, Unsatisfiable, or Unknown)
+- `Model()` - Get model (if satisfiable)
+- `Push()` - Create backtracking point
+- `Pop(n uint)` - Remove backtracking points
+- `Reset()` - Remove all assertions
+
+### Model Operations
+
+- `Eval(expr *Expr, modelCompletion bool)` - Evaluate expression in model
+- `NumConsts()` - Number of constants in model
+- `NumFuncs()` - Number of functions in model
+- `String()` - Get string representation
+
+### Bit-vector Operations
+
+- `MkBvSort(sz uint)` - Create bit-vector sort
+- `MkBVConst(name string, size uint)` - Create bit-vector variable
+- `MkBVAdd/Sub/Mul/UDiv/SDiv(lhs, rhs *Expr)` - Arithmetic operations
+- `MkBVAnd/Or/Xor/Not(...)` - Bitwise operations
+- `MkBVShl/LShr/AShr(lhs, rhs *Expr)` - Shift operations
+- `MkBVULT/SLT/ULE/SLE/UGE/SGE/UGT/SGT(...)` - Comparisons
+- `MkConcat(lhs, rhs *Expr)` - Bit-vector concatenation
+- `MkExtract(high, low uint, expr *Expr)` - Extract bits
+- `MkSignExt/ZeroExt(i uint, expr *Expr)` - Extend bit-vectors
+
+### Floating-Point Operations
+
+- `MkFPSort(ebits, sbits uint)` - Create floating-point sort
+- `MkFPSort16/32/64/128()` - Standard IEEE 754 sorts
+- `MkFPInf/NaN/Zero(sort *Sort, ...)` - Special values
+- `MkFPAdd/Sub/Mul/Div(rm, lhs, rhs *Expr)` - Arithmetic with rounding
+- `MkFPNeg/Abs/Sqrt(...)` - Unary operations
+- `MkFPLT/GT/LE/GE/Eq(lhs, rhs *Expr)` - Comparisons
+- `MkFPIsNaN/IsInf/IsZero(expr *Expr)` - Predicates
+
+### Sequence/String Operations
+
+- `MkStringSort()` - Create string sort
+- `MkSeqSort(elemSort *Sort)` - Create sequence sort
+- `MkString(value string)` - Create string constant
+- `MkSeqConcat(exprs ...*Expr)` - Concatenation
+- `MkSeqLength(seq *Expr)` - Length
+- `MkSeqPrefix/Suffix/Contains(...)` - Predicates
+- `MkSeqAt(seq, index *Expr)` - Element access
+- `MkSeqExtract(seq, offset, length *Expr)` - Substring
+- `MkStrToInt/IntToStr(...)` - Conversions
+
+### Regular Expression Operations
+
+- `MkReSort(seqSort *Sort)` - Create regex sort
+- `MkToRe(seq *Expr)` - Convert string to regex
+- `MkInRe(seq, re *Expr)` - String matches regex predicate
+- `MkReStar(re *Expr)` - Kleene star (zero or more)
+- `MkRePlus(re *Expr)` - Kleene plus (one or more)
+- `MkReOption(re *Expr)` - Optional (zero or one)
+- `MkRePower(re *Expr, n uint)` - Exactly n repetitions
+- `MkReLoop(re *Expr, lo, hi uint)` - Bounded repetition
+- `MkReConcat(regexes ...*Expr)` - Concatenation
+- `MkReUnion(regexes ...*Expr)` - Alternation (OR)
+- `MkReIntersect(regexes ...*Expr)` - Intersection
+- `MkReComplement(re *Expr)` - Complement
+- `MkReDiff(a, b *Expr)` - Difference
+- `MkReEmpty/Full/Allchar(sort *Sort)` - Special regexes
+- `MkReRange(lo, hi *Expr)` - Character range
+- `MkSeqReplaceRe/ReAll(seq, re, replacement *Expr)` - Regex replace
+
+### Datatype Operations
+
+- `MkConstructor(name, recognizer string, ...)` - Create constructor
+- `MkDatatypeSort(name string, constructors []*Constructor)` - Create datatype
+- `MkDatatypeSorts(names []string, ...)` - Mutually recursive datatypes
+- `MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort)` - Tuples
+- `MkEnumSort(name string, enumNames []string)` - Enumerations
+- `MkListSort(name string, elemSort *Sort)` - Lists
+
+### Tactic Operations
+
+- `MkTactic(name string)` - Create tactic by name
+- `MkGoal(models, unsatCores, proofs bool)` - Create goal
+- `Apply(g *Goal)` - Apply tactic to goal
+- `AndThen(t2 *Tactic)` - Sequential composition
+- `OrElse(t2 *Tactic)` - Try first, fallback to second
+- `Repeat(max uint)` - Repeat tactic
+- `TacticWhen/Cond(...)` - Conditional tactics
+
+### Probe Operations
+
+- `MkProbe(name string)` - Create probe by name
+- `Apply(g *Goal)` - Evaluate probe on goal
+- `Lt/Gt/Le/Ge/Eq(p2 *Probe)` - Probe comparisons
+- `And/Or/Not(...)` - Probe combinators
+
+### Parameter Operations
+
+- `MkParams()` - Create parameter set
+- `SetBool/Uint/Double/Symbol(key string, value ...)` - Set parameters
+
+### Optimize Operations
+
+- `NewOptimize()` - Create optimization context
+- `Assert(constraint *Expr)` - Add constraint
+- `AssertSoft(constraint *Expr, weight, group string)` - Add soft constraint
+- `Maximize(expr *Expr)` - Add maximization objective
+- `Minimize(expr *Expr)` - Add minimization objective
+- `Check(assumptions ...*Expr)` - Check and optimize
+- `Model()` - Get optimal model
+- `GetLower/Upper(index uint)` - Get objective bounds
+- `Push/Pop()` - Backtracking
+- `Assertions/Objectives()` - Get assertions and objectives
+- `UnsatCore()` - Get unsat core
+
+## Memory Management
+
+The Go bindings use `runtime.SetFinalizer` to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately.
+
+## Thread Safety
+
+Z3 contexts are not thread-safe. Each goroutine should use its own context, or use appropriate synchronization when sharing a context.
+
+## License
+
+Z3 is licensed under the MIT License. See LICENSE.txt in the repository root.
+
+## Contributing
+
+Bug reports and contributions are welcome! Please submit issues and pull requests to the main Z3 repository.
+
+## References
+
+- [Z3 GitHub Repository](https://github.com/Z3Prover/z3)
+- [Z3 API Documentation](https://z3prover.github.io/api/html/index.html)
+- [Z3 Guide](https://microsoft.github.io/z3guide/)
+
+<hr>
+<p><a href="index.html">Back to Go API Documentation</a></p>
+</body>
+</html>
diff --git a/doc/test_go_doc/index.html b/doc/test_go_doc/index.html
new file mode 100644
index 000000000..f9fb2a9f0
--- /dev/null
+++ b/doc/test_go_doc/index.html
@@ -0,0 +1,164 @@
+<!DOCTYPE html>
+<html lang="en">
+<head>
+    <meta charset="UTF-8">
+    <meta name="viewport" content="width=device-width, initial-scale=1.0">
+    <title>Z3 Go API Documentation</title>
+    <style>
+        body { font-family: -apple-system, BlinkMacSystemFont, "Segoe UI", Roboto, sans-serif; margin: 0; padding: 0; line-height: 1.6; }
+        header { background: #2d3748; color: white; padding: 2rem; }
+        header h1 { margin: 0; font-size: 2.5rem; }
+        header p { margin: 0.5rem 0 0 0; font-size: 1.1rem; opacity: 0.9; }
+        .container { max-width: 1200px; margin: 0 auto; padding: 2rem; }
+        .section { margin: 2rem 0; }
+        .section h2 { color: #2d3748; border-bottom: 2px solid #4299e1; padding-bottom: 0.5rem; }
+        .file-list { list-style: none; padding: 0; }
+        .file-item { background: #f7fafc; border-left: 4px solid #4299e1; margin: 1rem 0; padding: 1rem; border-radius: 4px; }
+        .file-item h3 { margin: 0 0 0.5rem 0; color: #2d3748; }
+        .file-item h3 a { color: #2b6cb0; text-decoration: none; }
+        .file-item h3 a:hover { color: #4299e1; text-decoration: underline; }
+        .file-item p { margin: 0; color: #4a5568; }
+        .code-block { background: #2d3748; color: #e2e8f0; padding: 1.5rem; border-radius: 4px; overflow-x: auto; }
+        .code-block pre { margin: 0; }
+        .install-section { background: #edf2f7; padding: 1.5rem; border-radius: 4px; margin: 1rem 0; }
+        .back-link { display: inline-block; margin-top: 2rem; color: #2b6cb0; text-decoration: none; }
+        .back-link:hover { text-decoration: underline; }
+    </style>
+</head>
+<body>
+    <header>
+        <h1>Z3 Go API Documentation</h1>
+        <p>Go bindings for the Z3 Theorem Prover</p>
+    </header>
+    <div class="container">
+        <div class="section">
+            <h2>Overview</h2>
+            <p>The Z3 Go bindings provide idiomatic Go access to the Z3 SMT solver. These bindings use CGO to wrap the Z3 C API and provide automatic memory management through Go finalizers.</p>
+            <p><strong>Package:</strong> <code>github.com/Z3Prover/z3/src/api/go</code></p>
+        </div>
+        <div class="section">
+            <h2>Quick Start</h2>
+            <div class="code-block">
+                <pre>package main
+
+import (
+    "fmt"
+    "github.com/Z3Prover/z3/src/api/go"
+)
+
+func main() {
+    // Create a context
+    ctx := z3.NewContext()
+
+    // Create integer variable
+    x := ctx.MkIntConst("x")
+
+    // Create solver
+    solver := ctx.NewSolver()
+
+    // Add constraint: x > 0
+    zero := ctx.MkInt(0, ctx.MkIntSort())
+    solver.Assert(ctx.MkGt(x, zero))
+
+    // Check satisfiability
+    if solver.Check() == z3.Satisfiable {
+        fmt.Println("sat")
+        model := solver.Model()
+        if val, ok := model.Eval(x, true); ok {
+            fmt.Println("x =", val.String())
+        }
+    }
+}</pre>
+            </div>
+        </div>
+        <div class="section">
+            <h2>Installation</h2>
+            <div class="install-section">
+                <p><strong>Prerequisites:</strong></p>
+                <ul>
+                    <li>Go 1.20 or later</li>
+                    <li>Z3 built as a shared library</li>
+                    <li>CGO enabled (default)</li>
+                </ul>
+                <p><strong>Build Z3 with Go bindings:</strong></p>
+                <div class="code-block">
+                    <pre># Using CMake
+mkdir build && cd build
+cmake -DZ3_BUILD_GO_BINDINGS=ON -DZ3_BUILD_LIBZ3_SHARED=ON ..
+make
+
+# Using Python build script
+python scripts/mk_make.py --go
+cd build && make</pre>
+                </div>
+                <p><strong>Set environment variables:</strong></p>
+                <div class="code-block">
+                    <pre>export CGO_CFLAGS="-I${Z3_ROOT}/src/api"
+export CGO_LDFLAGS="-L${Z3_ROOT}/build -lz3"
+export LD_LIBRARY_PATH="${Z3_ROOT}/build:$LD_LIBRARY_PATH"</pre>
+                </div>
+            </div>
+        </div>
+        <div class="section">
+            <h2>API Modules</h2>
+            <ul class="file-list">
+                <li class="file-item">
+                    <h3><a href="#z3.go">z3.go</a></h3>
+                    <p>Package z3 provides Go bindings for the Z3 theorem prover. It wraps the Z3 C API using CGO.</p>
+                </li>
+                <li class="file-item">
+                    <h3><a href="#solver.go">solver.go</a></h3>
+                    <p>Solver and Model API for SMT solving</p>
+                </li>
+                <li class="file-item">
+                    <h3><a href="#tactic.go">tactic.go</a></h3>
+                    <p>Tactics, Goals, Probes, and Parameters for goal-based solving</p>
+                </li>
+                <li class="file-item">
+                    <h3><a href="#bitvec.go">bitvec.go</a></h3>
+                    <p>Bit-vector operations and constraints</p>
+                </li>
+                <li class="file-item">
+                    <h3><a href="#fp.go">fp.go</a></h3>
+                    <p>IEEE 754 floating-point operations</p>
+                </li>
+                <li class="file-item">
+                    <h3><a href="#seq.go">seq.go</a></h3>
+                    <p>Sequences, strings, and regular expressions</p>
+                </li>
+                <li class="file-item">
+                    <h3><a href="#datatype.go">datatype.go</a></h3>
+                    <p>Algebraic datatypes, tuples, and enumerations</p>
+                </li>
+                <li class="file-item">
+                    <h3><a href="#optimize.go">optimize.go</a></h3>
+                    <p>Optimization with maximize/minimize objectives</p>
+                </li>
+            </ul>
+        </div>
+        <div class="section">
+            <h2>Features</h2>
+            <ul>
+                <li><strong>Core SMT:</strong> Boolean logic, arithmetic, arrays, quantifiers</li>
+                <li><strong>Bit-vectors:</strong> Fixed-size bit-vector arithmetic and operations</li>
+                <li><strong>Floating-point:</strong> IEEE 754 floating-point arithmetic</li>
+                <li><strong>Strings & Sequences:</strong> String constraints and sequence operations</li>
+                <li><strong>Regular Expressions:</strong> Pattern matching and regex constraints</li>
+                <li><strong>Datatypes:</strong> Algebraic datatypes, tuples, enumerations</li>
+                <li><strong>Tactics:</strong> Goal-based solving with tactic combinators</li>
+                <li><strong>Optimization:</strong> MaxSMT with maximize/minimize objectives</li>
+                <li><strong>Memory Management:</strong> Automatic via Go finalizers</li>
+            </ul>
+        </div>
+        <div class="section">
+            <h2>Resources</h2>
+            <ul>
+                <li><a href="https://github.com/Z3Prover/z3">Z3 GitHub Repository</a></li>
+                <li><a href="../index.html">All API Documentation</a></li>
+                <li><a href="README.html">Go API README</a></li>
+            </ul>
+        </div>
+        <a href="../index.html" class="back-link">← Back to main API documentation</a>
+    </div>
+</body>
+</html>
diff --git a/doc/website.dox.in b/doc/website.dox.in
index 651652ce4..be9e1b093 100644
--- a/doc/website.dox.in
+++ b/doc/website.dox.in
@@ -8,5 +8,5 @@
 
    This website hosts the automatically generated documentation for the Z3 APIs.
 
-   @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@
+   @C_API@ @CPP_API@ @DOTNET_API@ @JAVA_API@ @PYTHON_API@ @OCAML_API@ @JS_API@ @GO_API@
 */
diff --git a/doc/z3api.cfg.in b/doc/z3api.cfg.in
index 1c367e141..cc238b01f 100644
--- a/doc/z3api.cfg.in
+++ b/doc/z3api.cfg.in
@@ -841,7 +841,8 @@ WARN_LOGFILE           =
 INPUT                  = "@TEMP_DIR@" \
                          "@CXX_API_SEARCH_PATHS@" \
                          @DOTNET_API_SEARCH_PATHS@ \
-                         @JAVA_API_SEARCH_PATHS@
+                         @JAVA_API_SEARCH_PATHS@ \
+                         @GO_API_SEARCH_PATHS@
 
 # This tag can be used to specify the character encoding of the source files
 # that doxygen parses. Internally doxygen uses the UTF-8 encoding. Doxygen uses
@@ -879,7 +880,8 @@ FILE_PATTERNS          = website.dox \
                          z3++.h \
                          @PYTHON_API_FILES@ \
                          @DOTNET_API_FILES@ \
-                         @JAVA_API_FILES@
+                         @JAVA_API_FILES@ \
+                         @GO_API_FILES@
 
 # The RECURSIVE tag can be used to specify whether or not subdirectories should
 # be searched for input files as well.
diff --git a/examples/go/README.md b/examples/go/README.md
new file mode 100644
index 000000000..011f08579
--- /dev/null
+++ b/examples/go/README.md
@@ -0,0 +1,145 @@
+# Z3 Go Examples
+
+This directory contains examples demonstrating how to use the Z3 Go bindings.
+
+## Examples
+
+### basic_example.go
+
+Demonstrates fundamental Z3 operations:
+- Creating contexts and solvers
+- Defining integer and boolean variables
+- Adding constraints
+- Checking satisfiability
+- Extracting models
+
+## Building and Running
+
+### Prerequisites
+
+1. Build Z3 with Go bindings enabled
+2. Ensure Z3 library is in your library path
+3. Go 1.20 or later
+
+### Linux/macOS
+
+```bash
+# Build Z3 first
+cd ../..
+mkdir build && cd build
+cmake ..
+make -j$(nproc)
+
+# Set up environment
+cd ../examples/go
+export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
+export CGO_CFLAGS="-I../../src/api"
+export CGO_LDFLAGS="-L../../build -lz3"
+
+# Run examples
+go run basic_example.go
+```
+
+### Windows
+
+```cmd
+REM Build Z3 first
+cd ..\..
+mkdir build
+cd build
+cmake ..
+cmake --build . --config Release
+
+REM Set up environment
+cd ..\examples\go
+set PATH=..\..\build\Release;%PATH%
+set CGO_CFLAGS=-I..\..\src\api
+set CGO_LDFLAGS=-L..\..\build\Release -lz3
+
+REM Run examples
+go run basic_example.go
+```
+
+## Expected Output
+
+When you run `basic_example.go`, you should see output similar to:
+
+```
+Z3 Go Bindings - Basic Example
+================================
+
+Example 1: Solving x > 0
+Satisfiable!
+Model: ...
+x = 1
+
+Example 2: Solving x + y = 10 ∧ x - y = 2
+Satisfiable!
+x = 6
+y = 4
+
+Example 3: Boolean satisfiability
+Satisfiable!
+p = false
+q = true
+
+Example 4: Checking unsatisfiability
+Status: unsat
+The constraints are unsatisfiable (as expected)
+
+All examples completed successfully!
+```
+
+## Creating Your Own Examples
+
+1. Import the Z3 package:
+   ```go
+   import "github.com/Z3Prover/z3/src/api/go"
+   ```
+
+2. Create a context:
+   ```go
+   ctx := z3.NewContext()
+   ```
+
+3. Create variables and constraints:
+   ```go
+   x := ctx.MkIntConst("x")
+   constraint := ctx.MkGt(x, ctx.MkInt(0, ctx.MkIntSort()))
+   ```
+
+4. Solve:
+   ```go
+   solver := ctx.NewSolver()
+   solver.Assert(constraint)
+   if solver.Check() == z3.Satisfiable {
+       model := solver.Model()
+       // Use model...
+   }
+   ```
+
+## Troubleshooting
+
+### "undefined reference to Z3_*" errors
+
+Make sure:
+- Z3 is built and the library is in your library path
+- CGO_LDFLAGS includes the correct library path
+- On Windows, the DLL is in your PATH
+
+### "cannot find package" errors
+
+Make sure:
+- CGO_CFLAGS includes the Z3 API header directory
+- The go.mod file exists in src/api/go
+
+### CGO compilation errors
+
+Ensure:
+- CGO is enabled (set CGO_ENABLED=1 if needed)
+- You have a C compiler installed (gcc, clang, or MSVC)
+- The Z3 headers are accessible
+
+## More Information
+
+See the README.md in src/api/go for complete API documentation.
diff --git a/examples/go/advanced_example.go b/examples/go/advanced_example.go
new file mode 100644
index 000000000..0db4b6daf
--- /dev/null
+++ b/examples/go/advanced_example.go
@@ -0,0 +1,313 @@
+package main
+
+import (
+	"fmt"
+	"github.com/Z3Prover/z3/src/api/go"
+)
+
+func main() {
+	ctx := z3.NewContext()
+	fmt.Println("Z3 Go Bindings - Advanced Features Example")
+	fmt.Println("==========================================")
+
+	// Example 1: Bit-vectors
+	fmt.Println("\nExample 1: Bit-vector operations")
+	x := ctx.MkBVConst("x", 8)
+	y := ctx.MkBVConst("y", 8)
+	
+	// x + y == 255 && x > y
+	sum := ctx.MkBVAdd(x, y)
+	ff := ctx.MkBV(255, 8)
+	
+	solver := ctx.NewSolver()
+	solver.Assert(ctx.MkEq(sum, ff))
+	solver.Assert(ctx.MkBVUGT(x, y))
+	
+	if solver.Check() == z3.Satisfiable {
+		model := solver.Model()
+		fmt.Println("Satisfiable!")
+		if xVal, ok := model.Eval(x, true); ok {
+			fmt.Println("x =", xVal.String())
+		}
+		if yVal, ok := model.Eval(y, true); ok {
+			fmt.Println("y =", yVal.String())
+		}
+	}
+
+	// Example 2: Floating-point arithmetic
+	fmt.Println("\nExample 2: Floating-point arithmetic")
+	solver.Reset()
+	
+	fpSort := ctx.MkFPSort32()
+	a := ctx.MkConst(ctx.MkStringSymbol("a"), fpSort)
+	b := ctx.MkConst(ctx.MkStringSymbol("b"), fpSort)
+	
+	// a + b > 0.0 (with rounding mode)
+	rm := ctx.MkConst(ctx.MkStringSymbol("rm"), ctx.MkFPRoundingModeSort())
+	fpSum := ctx.MkFPAdd(rm, a, b)
+	zero := ctx.MkFPZero(fpSort, false)
+	
+	solver.Assert(ctx.MkFPGT(fpSum, zero))
+	solver.Assert(ctx.MkFPGT(a, ctx.MkFPZero(fpSort, false)))
+	
+	if solver.Check() == z3.Satisfiable {
+		fmt.Println("Satisfiable! (Floating-point constraint satisfied)")
+	}
+
+	// Example 3: Strings
+	fmt.Println("\nExample 3: String operations")
+	solver.Reset()
+	
+	s1 := ctx.MkConst(ctx.MkStringSymbol("s1"), ctx.MkStringSort())
+	s2 := ctx.MkConst(ctx.MkStringSymbol("s2"), ctx.MkStringSort())
+	
+	// s1 contains "hello" && length(s1) < 20
+	hello := ctx.MkString("hello")
+	solver.Assert(ctx.MkSeqContains(s1, hello))
+	
+	len1 := ctx.MkSeqLength(s1)
+	twenty := ctx.MkInt(20, ctx.MkIntSort())
+	solver.Assert(ctx.MkLt(len1, twenty))
+	
+	// s2 is s1 concatenated with "world"
+	world := ctx.MkString(" world")
+	solver.Assert(ctx.MkEq(s2, ctx.MkSeqConcat(s1, world)))
+	
+	if solver.Check() == z3.Satisfiable {
+		model := solver.Model()
+		fmt.Println("Satisfiable!")
+		if s1Val, ok := model.Eval(s1, true); ok {
+			fmt.Println("s1 =", s1Val.String())
+		}
+		if s2Val, ok := model.Eval(s2, true); ok {
+			fmt.Println("s2 =", s2Val.String())
+		}
+	}
+
+	// Example 4: Datatypes (List)
+	fmt.Println("\nExample 4: List datatype")
+	solver.Reset()
+	
+	intSort := ctx.MkIntSort()
+	listSort, nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl := 
+		ctx.MkListSort("IntList", intSort)
+	
+	// Create list: cons(1, cons(2, nil))
+	nilList := ctx.MkApp(nilDecl)
+	one := ctx.MkInt(1, intSort)
+	two := ctx.MkInt(2, intSort)
+	list2 := ctx.MkApp(consDecl, two, nilList)
+	list12 := ctx.MkApp(consDecl, one, list2)
+	
+	// Check that head(list12) == 1
+	listVar := ctx.MkConst(ctx.MkStringSymbol("mylist"), listSort)
+	solver.Assert(ctx.MkEq(listVar, list12))
+	
+	headOfList := ctx.MkApp(headDecl, listVar)
+	solver.Assert(ctx.MkEq(headOfList, one))
+	
+	if solver.Check() == z3.Satisfiable {
+		fmt.Println("Satisfiable! List head is 1")
+	}
+
+	// Example 5: Tactics and Goals
+	fmt.Println("\nExample 5: Using tactics")
+	
+	goal := ctx.MkGoal(true, false, false)
+	p := ctx.MkIntConst("p")
+	q := ctx.MkIntConst("q")
+	
+	// Add constraint: p > 0 && q > 0 && p + q == 10
+	goal.Assert(ctx.MkGt(p, ctx.MkInt(0, ctx.MkIntSort())))
+	goal.Assert(ctx.MkGt(q, ctx.MkInt(0, ctx.MkIntSort())))
+	goal.Assert(ctx.MkEq(ctx.MkAdd(p, q), ctx.MkInt(10, ctx.MkIntSort())))
+	
+	// Apply simplify tactic
+	tactic := ctx.MkTactic("simplify")
+	result := tactic.Apply(goal)
+	
+	fmt.Printf("Tactic produced %d subgoals\n", result.NumSubgoals())
+	if result.NumSubgoals() > 0 {
+		subgoal := result.Subgoal(0)
+		fmt.Println("Simplified goal:", subgoal.String())
+	}
+
+	// Example 6: Enumerations
+	fmt.Println("\nExample 6: Enumeration types")
+	solver.Reset()
+	
+	colorSort, colorConsts, colorTesters := ctx.MkEnumSort(
+		"Color",
+		[]string{"Red", "Green", "Blue"},
+	)
+	
+	red := ctx.MkApp(colorConsts[0])
+	green := ctx.MkApp(colorConsts[1])
+	blue := ctx.MkApp(colorConsts[2])
+	
+	c1 := ctx.MkConst(ctx.MkStringSymbol("c1"), colorSort)
+	c2 := ctx.MkConst(ctx.MkStringSymbol("c2"), colorSort)
+	
+	// c1 != c2 && c1 != Red
+	solver.Assert(ctx.MkDistinct(c1, c2))
+	solver.Assert(ctx.MkNot(ctx.MkEq(c1, red)))
+	
+	if solver.Check() == z3.Satisfiable {
+		model := solver.Model()
+		fmt.Println("Satisfiable!")
+		if c1Val, ok := model.Eval(c1, true); ok {
+			fmt.Println("c1 =", c1Val.String())
+		}
+		if c2Val, ok := model.Eval(c2, true); ok {
+			fmt.Println("c2 =", c2Val.String())
+		}
+	}
+
+	// Example 7: Tuples
+	fmt.Println("\nExample 7: Tuple types")
+	solver.Reset()
+	
+	tupleSort, mkTuple, projections := ctx.MkTupleSort(
+		"Point",
+		[]string{"x", "y"},
+		[]*z3.Sort{ctx.MkIntSort(), ctx.MkIntSort()},
+	)
+	
+	// Create point (3, 4)
+	three := ctx.MkInt(3, ctx.MkIntSort())
+	four := ctx.MkInt(4, ctx.MkIntSort())
+	point := ctx.MkApp(mkTuple, three, four)
+	
+	p1 := ctx.MkConst(ctx.MkStringSymbol("p1"), tupleSort)
+	solver.Assert(ctx.MkEq(p1, point))
+	
+	// Extract x coordinate
+	xCoord := ctx.MkApp(projections[0], p1)
+	solver.Assert(ctx.MkEq(xCoord, three))
+	
+	if solver.Check() == z3.Satisfiable {
+		fmt.Println("Satisfiable! Tuple point created")
+		model := solver.Model()
+		if p1Val, ok := model.Eval(p1, true); ok {
+			fmt.Println("p1 =", p1Val.String())
+		}
+	}
+
+	// Example 8: Regular expressions  
+	fmt.Println("\nExample 8: Regular expressions")
+	solver.Reset()
+	
+	// Create a string variable
+	str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort())
+	
+	// Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c')
+	a := ctx.MkToRe(ctx.MkString("a"))
+	b := ctx.MkToRe(ctx.MkString("b"))
+	c := ctx.MkToRe(ctx.MkString("c"))
+	
+	// (a|b)
+	aOrB := ctx.MkReUnion(a, b)
+	
+	// (a|b)*
+	aOrBStar := ctx.MkReStar(aOrB)
+	
+	// c+
+	cPlus := ctx.MkRePlus(c)
+	
+	// (a|b)*c+
+	regex := ctx.MkReConcat(aOrBStar, cPlus)
+	
+	// Assert that string matches the regex
+	solver.Assert(ctx.MkInRe(str, regex))
+	
+	// Also assert that length is less than 10
+	strLen := ctx.MkSeqLength(str)
+	ten := ctx.MkInt(10, ctx.MkIntSort())
+	solver.Assert(ctx.MkLt(strLen, ten))
+	
+	if solver.Check() == z3.Satisfiable {
+		model := solver.Model()
+		fmt.Println("Satisfiable!")
+		if strVal, ok := model.Eval(str, true); ok {
+			fmt.Println("String matching (a|b)*c+:", strVal.String())
+		}
+	}
+
+	// Example 8: Regular expressions
+	fmt.Println("\nExample 8: Regular expressions")
+	solver.Reset()
+	
+	// Create a string variable
+	str := ctx.MkConst(ctx.MkStringSymbol("str"), ctx.MkStringSort())
+	
+	// Create regex: (a|b)*c+ (zero or more 'a' or 'b', followed by one or more 'c')
+	a := ctx.MkToRe(ctx.MkString("a"))
+	b := ctx.MkToRe(ctx.MkString("b"))
+	c := ctx.MkToRe(ctx.MkString("c"))
+	
+	// (a|b)*
+	aOrB := ctx.MkReUnion(a, b)
+	aOrBStar := ctx.MkReStar(aOrB)
+	
+	// c+
+	cPlus := ctx.MkRePlus(c)
+	
+	// (a|b)*c+
+	regex := ctx.MkReConcat(aOrBStar, cPlus)
+	
+	// Assert that string matches the regex
+	solver.Assert(ctx.MkInRe(str, regex))
+	
+	// Also assert that length is less than 10
+	strLen := ctx.MkSeqLength(str)
+	tenStr := ctx.MkInt(10, ctx.MkIntSort())
+	solver.Assert(ctx.MkLt(strLen, tenStr))
+	
+	if solver.Check() == z3.Satisfiable {
+		model := solver.Model()
+		fmt.Println("Satisfiable!")
+		if strVal, ok := model.Eval(str, true); ok {
+			fmt.Println("String matching (a|b)*c+:", strVal.String())
+		}
+	}
+
+	// Example 9: Optimization
+	fmt.Println("\nExample 9: Optimization (maximize/minimize)")
+	
+	opt := ctx.NewOptimize()
+	
+	// Variables
+	xOpt := ctx.MkIntConst("x_opt")
+	yOpt := ctx.MkIntConst("y_opt")
+	
+	// Constraints: x + y <= 10, x >= 0, y >= 0
+	tenOpt := ctx.MkInt(10, ctx.MkIntSort())
+	zeroOpt := ctx.MkInt(0, ctx.MkIntSort())
+	
+	opt.Assert(ctx.MkLe(ctx.MkAdd(xOpt, yOpt), tenOpt))
+	opt.Assert(ctx.MkGe(xOpt, zeroOpt))
+	opt.Assert(ctx.MkGe(yOpt, zeroOpt))
+	
+	// Objective: maximize x + 2*y
+	twoOpt := ctx.MkInt(2, ctx.MkIntSort())
+	objective := ctx.MkAdd(xOpt, ctx.MkMul(twoOpt, yOpt))
+	objHandle := opt.Maximize(objective)
+	
+	if opt.Check() == z3.Satisfiable {
+		model := opt.Model()
+		fmt.Println("Optimal solution found!")
+		if xVal, ok := model.Eval(xOpt, true); ok {
+			fmt.Println("x =", xVal.String())
+		}
+		if yVal, ok := model.Eval(yOpt, true); ok {
+			fmt.Println("y =", yVal.String())
+		}
+		upper := opt.GetUpper(objHandle)
+		if upper != nil {
+			fmt.Println("Maximum value of x + 2*y =", upper.String())
+		}
+	}
+
+	fmt.Println("\nAll advanced examples completed successfully!")
+}
+
diff --git a/examples/go/basic_example.go b/examples/go/basic_example.go
new file mode 100644
index 000000000..73bcf84df
--- /dev/null
+++ b/examples/go/basic_example.go
@@ -0,0 +1,98 @@
+package main
+
+import (
+	"fmt"
+	"github.com/Z3Prover/z3/src/api/go"
+)
+
+func main() {
+	// Create a new Z3 context
+	ctx := z3.NewContext()
+	fmt.Println("Z3 Go Bindings - Basic Example")
+	fmt.Println("================================")
+
+	// Example 1: Simple integer constraint
+	fmt.Println("\nExample 1: Solving x > 0")
+	x := ctx.MkIntConst("x")
+	zero := ctx.MkInt(0, ctx.MkIntSort())
+	constraint := ctx.MkGt(x, zero)
+	
+	solver := ctx.NewSolver()
+	solver.Assert(constraint)
+	
+	if solver.Check() == z3.Satisfiable {
+		model := solver.Model()
+		fmt.Println("Satisfiable!")
+		fmt.Println("Model:", model.String())
+		if val, ok := model.Eval(x, true); ok {
+			fmt.Println("x =", val.String())
+		}
+	}
+
+	// Example 2: System of equations
+	fmt.Println("\nExample 2: Solving x + y = 10 ∧ x - y = 2")
+	solver.Reset()
+	y := ctx.MkIntConst("y")
+	ten := ctx.MkInt(10, ctx.MkIntSort())
+	two := ctx.MkInt(2, ctx.MkIntSort())
+	
+	eq1 := ctx.MkEq(ctx.MkAdd(x, y), ten)
+	eq2 := ctx.MkEq(ctx.MkSub(x, y), two)
+	
+	solver.Assert(eq1)
+	solver.Assert(eq2)
+	
+	if solver.Check() == z3.Satisfiable {
+		model := solver.Model()
+		fmt.Println("Satisfiable!")
+		if xVal, ok := model.Eval(x, true); ok {
+			fmt.Println("x =", xVal.String())
+		}
+		if yVal, ok := model.Eval(y, true); ok {
+			fmt.Println("y =", yVal.String())
+		}
+	}
+
+	// Example 3: Boolean logic
+	fmt.Println("\nExample 3: Boolean satisfiability")
+	solver.Reset()
+	p := ctx.MkBoolConst("p")
+	q := ctx.MkBoolConst("q")
+	
+	// (p ∨ q) ∧ (¬p ∨ ¬q)
+	formula := ctx.MkAnd(
+		ctx.MkOr(p, q),
+		ctx.MkOr(ctx.MkNot(p), ctx.MkNot(q)),
+	)
+	
+	solver.Assert(formula)
+	
+	if solver.Check() == z3.Satisfiable {
+		model := solver.Model()
+		fmt.Println("Satisfiable!")
+		if pVal, ok := model.Eval(p, true); ok {
+			fmt.Println("p =", pVal.String())
+		}
+		if qVal, ok := model.Eval(q, true); ok {
+			fmt.Println("q =", qVal.String())
+		}
+	}
+
+	// Example 4: Unsatisfiable constraint
+	fmt.Println("\nExample 4: Checking unsatisfiability")
+	solver.Reset()
+	a := ctx.MkIntConst("a")
+	one := ctx.MkInt(1, ctx.MkIntSort())
+	
+	// a > 0 ∧ a < 0 (unsatisfiable)
+	solver.Assert(ctx.MkGt(a, zero))
+	solver.Assert(ctx.MkLt(a, zero))
+	
+	status := solver.Check()
+	fmt.Println("Status:", status.String())
+	if status == z3.Unsatisfiable {
+		fmt.Println("The constraints are unsatisfiable (as expected)")
+	}
+
+	fmt.Println("\nAll examples completed successfully!")
+}
diff --git a/examples/go/go.mod b/examples/go/go.mod
new file mode 100644
index 000000000..7ee4bbce2
--- /dev/null
+++ b/examples/go/go.mod
@@ -0,0 +1,8 @@
+module z3-examples
+
+go 1.20
+
+require github.com/Z3Prover/z3/src/api/go v0.0.0
+
+replace github.com/Z3Prover/z3/src/api/go => ../../src/api/go
+
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 163056099..aa1069a5e 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -93,6 +93,7 @@ DOTNET_CORE_ENABLED=False
 DOTNET_KEY_FILE=getenv("Z3_DOTNET_KEY_FILE", None)
 ASSEMBLY_VERSION=getenv("Z2_ASSEMBLY_VERSION", None)
 JAVA_ENABLED=False
+GO_ENABLED=False
 ML_ENABLED=False
 PYTHON_INSTALL_ENABLED=False
 STATIC_LIB=False
@@ -712,6 +713,7 @@ def display_help(exit_code):
     print("  --dotnet-key=<file>           sign the .NET assembly using the private key in <file>.")
     print("  --assembly-version=<x.x.x.x>  provide version number for build")
     print("  --java                        generate Java bindings.")
+    print("  --go                          generate Go bindings.")
     print("  --ml                          generate OCaml bindings.")
     print("  --js                          generate JScript bindings.")
     print("  --python                      generate Python bindings.")
@@ -745,7 +747,7 @@ def display_help(exit_code):
 # Parse configuration option for mk_make script
 def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
-    global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, ASSEMBLY_VERSION, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
+    global DOTNET_CORE_ENABLED, DOTNET_KEY_FILE, ASSEMBLY_VERSION, JAVA_ENABLED, GO_ENABLED, ML_ENABLED, STATIC_LIB, STATIC_BIN, PREFIX, GMP, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH, GIT_DESCRIBE, PYTHON_INSTALL_ENABLED, PYTHON_ENABLED
     global LINUX_X64, SLOW_OPTIMIZE, LOG_SYNC, SINGLE_THREADED
     global GUARD_CF, ALWAYS_DYNAMIC_BASE, IS_ARCH_ARM64
     try:
@@ -809,6 +811,8 @@ def parse_options():
             GMP = True
         elif opt in ('-j', '--java'):
             JAVA_ENABLED = True
+        elif opt in ('--go',):
+            GO_ENABLED = True
         elif opt == '--gprof':
             GPROF = True
         elif opt == '--githash':
@@ -953,6 +957,9 @@ def is_verbose():
 def is_java_enabled():
     return JAVA_ENABLED
 
+def is_go_enabled():
+    return GO_ENABLED
+
 def is_ml_enabled():
     return ML_ENABLED
 
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 65420484e..1a6608849 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -355,4 +355,16 @@ if (Z3_BUILD_JULIA_BINDINGS)
   add_subdirectory(api/julia)
 endif()
 
+################################################################################
+# Go bindings
+################################################################################
+option(Z3_BUILD_GO_BINDINGS "Build Go bindings for Z3" OFF)
+if (Z3_BUILD_GO_BINDINGS)
+  if (NOT Z3_BUILD_LIBZ3_SHARED)
+    message(FATAL_ERROR "The Go bindings will not work with a static libz3. "
+      "You either need to disable Z3_BUILD_GO_BINDINGS or enable Z3_BUILD_LIBZ3_SHARED")
+  endif()
+  add_subdirectory(api/go)
+endif()
+
 # TODO: Implement support for other bindigns
diff --git a/src/api/go/CMakeLists.txt b/src/api/go/CMakeLists.txt
new file mode 100644
index 000000000..f21bb4e37
--- /dev/null
+++ b/src/api/go/CMakeLists.txt
@@ -0,0 +1,54 @@
+# Z3 Go API
+
+# Note: This CMakeLists.txt is a placeholder for Go binding integration.
+# Go bindings use CGO and are typically built using the Go toolchain directly.
+# However, we can set up installation targets here.
+
+if(BUILD_GO_BINDINGS)
+    message(STATUS "Z3 Go bindings will be installed")
+    
+    # Install Go source files
+    install(FILES
+        ${CMAKE_CURRENT_SOURCE_DIR}/z3.go
+        ${CMAKE_CURRENT_SOURCE_DIR}/solver.go
+        ${CMAKE_CURRENT_SOURCE_DIR}/go.mod
+        ${CMAKE_CURRENT_SOURCE_DIR}/README.md
+        DESTINATION "${CMAKE_INSTALL_LIBDIR}/go/src/github.com/Z3Prover/z3/go"
+    )
+    
+    # On Windows, we need to ensure the DLL is accessible
+    if(WIN32)
+        message(STATUS "Go bindings on Windows require libz3.dll in PATH")
+    endif()
+    
+    # Add a custom target to test Go bindings if Go is available
+    find_program(GO_EXECUTABLE go)
+    if(GO_EXECUTABLE)
+        message(STATUS "Found Go: ${GO_EXECUTABLE}")
+        
+        # Custom target to build Go bindings
+        add_custom_target(go-bindings
+            COMMAND ${CMAKE_COMMAND} -E env
+                CGO_CFLAGS=-I${CMAKE_SOURCE_DIR}/src/api
+                CGO_LDFLAGS=-L${CMAKE_BINARY_DIR} -lz3
+                ${GO_EXECUTABLE} build -v
+            WORKING_DIRECTORY ${CMAKE_CURRENT_SOURCE_DIR}
+            COMMENT "Building Go bindings"
+            DEPENDS libz3
+        )
+        
+        # Custom target to test Go examples
+        add_custom_target(test-go-examples
+            COMMAND ${CMAKE_COMMAND} -E env
+                CGO_CFLAGS=-I${CMAKE_SOURCE_DIR}/src/api
+                CGO_LDFLAGS=-L${CMAKE_BINARY_DIR} -lz3
+                LD_LIBRARY_PATH=${CMAKE_BINARY_DIR}:$ENV{LD_LIBRARY_PATH}
+                PATH=${CMAKE_BINARY_DIR}\;$ENV{PATH}
+                ${GO_EXECUTABLE} run ${CMAKE_SOURCE_DIR}/examples/go/basic_example.go
+            COMMENT "Running Go examples"
+            DEPENDS libz3
+        )
+    else()
+        message(STATUS "Go not found - Go bindings can be built manually")
+    endif()
+endif()
diff --git a/src/api/go/README.md b/src/api/go/README.md
new file mode 100644
index 000000000..8814b72a1
--- /dev/null
+++ b/src/api/go/README.md
@@ -0,0 +1,331 @@
+# Z3 Go Bindings
+
+This directory contains Go language bindings for the Z3 theorem prover.
+
+## Overview
+
+The Go bindings provide a comprehensive interface to Z3's C API using CGO. The bindings support:
+
+- **Core Z3 Types**: Context, Config, Symbol, AST, Sort, Expr, FuncDecl
+- **Solver Operations**: Creating solvers, asserting constraints, checking satisfiability
+- **Model Manipulation**: Extracting and evaluating models
+- **Boolean Logic**: And, Or, Not, Implies, Iff, Xor
+- **Arithmetic**: Add, Sub, Mul, Div, Mod, comparison operators
+- **Bit-vectors**: Full bit-vector arithmetic, bitwise operations, shifts, comparisons
+- **Floating Point**: IEEE 754 floating-point arithmetic with rounding modes
+- **Arrays**: Select, Store, constant arrays
+- **Sequences/Strings**: String operations, concatenation, contains, indexing
+- **Regular Expressions**: Pattern matching, Kleene star/plus, regex operations
+- **Quantifiers**: Forall, Exists
+- **Functions**: Function declarations and applications
+- **Tactics & Goals**: Goal-based solving and tactic combinators
+- **Probes**: Goal property checking
+- **Datatypes**: Algebraic datatypes, tuples, enumerations, lists
+- **Parameters**: Solver and tactic configuration
+- **Optimize**: Optimization problems with maximize/minimize objectives
+
+## Building
+
+### Prerequisites
+
+- Go 1.20 or later
+- Z3 library built and installed
+- CGO enabled
+
+### With CMake
+
+```bash
+mkdir build && cd build
+cmake -DBUILD_GO_BINDINGS=ON ..
+make
+```
+
+### With Python Build System
+
+```bash
+python scripts/mk_make.py --go
+cd build
+make
+```
+
+## Usage
+
+### Basic Example
+
+```go
+package main
+
+import (
+    "fmt"
+    "github.com/Z3Prover/z3/src/api/go"
+)
+
+func main() {
+    // Create a context
+    ctx := z3.NewContext()
+    
+    // Create variables
+    x := ctx.MkIntConst("x")
+    y := ctx.MkIntConst("y")
+    
+    // Create constraints: x + y == 10 && x > y
+    ten := ctx.MkInt(10, ctx.MkIntSort())
+    eq := ctx.MkEq(ctx.MkAdd(x, y), ten)
+    gt := ctx.MkGt(x, y)
+    
+    // Create solver and check
+    solver := ctx.NewSolver()
+    solver.Assert(eq)
+    solver.Assert(gt)
+    
+    if solver.Check() == z3.Satisfiable {
+        model := solver.Model()
+        if xVal, ok := model.Eval(x, true); ok {
+            fmt.Println("x =", xVal.String())
+        }
+        if yVal, ok := model.Eval(y, true); ok {
+            fmt.Println("y =", yVal.String())
+        }
+    }
+}
+```
+
+### Running Examples
+
+```bash
+cd examples/go
+
+# Set library path (Linux/Mac)
+export LD_LIBRARY_PATH=../../build:$LD_LIBRARY_PATH
+export CGO_CFLAGS="-I../../src/api"
+export CGO_LDFLAGS="-L../../build -lz3"
+
+# Set library path (Windows)
+set PATH=..\..\build;%PATH%
+set CGO_CFLAGS=-I../../src/api
+set CGO_LDFLAGS=-L../../build -lz3
+
+# Run example
+go run basic_example.go
+```
+
+## API Reference
+
+### Context
+
+- `NewContext()` - Create a new Z3 context
+- `NewContextWithConfig(cfg *Config)` - Create context with configuration
+- `SetParam(key, value string)` - Set context parameters
+
+### Creating Expressions
+
+- `MkBoolConst(name string)` - Create Boolean variable
+- `MkIntConst(name string)` - Create integer variable
+- `MkRealConst(name string)` - Create real variable
+- `MkInt(value int, sort *Sort)` - Create integer constant
+- `MkReal(num, den int)` - Create rational constant
+
+### Boolean Operations
+
+- `MkAnd(exprs ...*Expr)` - Conjunction
+- `MkOr(exprs ...*Expr)` - Disjunction
+- `MkNot(expr *Expr)` - Negation
+- `MkImplies(lhs, rhs *Expr)` - Implication
+- `MkIff(lhs, rhs *Expr)` - If-and-only-if
+- `MkXor(lhs, rhs *Expr)` - Exclusive or
+
+### Arithmetic Operations
+
+- `MkAdd(exprs ...*Expr)` - Addition
+- `MkSub(exprs ...*Expr)` - Subtraction
+- `MkMul(exprs ...*Expr)` - Multiplication
+- `MkDiv(lhs, rhs *Expr)` - Division
+- `MkMod(lhs, rhs *Expr)` - Modulo
+- `MkRem(lhs, rhs *Expr)` - Remainder
+
+### Comparison Operations
+
+- `MkEq(lhs, rhs *Expr)` - Equality
+- `MkDistinct(exprs ...*Expr)` - Distinct
+- `MkLt(lhs, rhs *Expr)` - Less than
+- `MkLe(lhs, rhs *Expr)` - Less than or equal
+- `MkGt(lhs, rhs *Expr)` - Greater than
+- `MkGe(lhs, rhs *Expr)` - Greater than or equal
+
+### Solver Operations
+
+- `NewSolver()` - Create a new solver
+- `Assert(constraint *Expr)` - Add constraint
+- `Check()` - Check satisfiability (returns Satisfiable, Unsatisfiable, or Unknown)
+- `Model()` - Get model (if satisfiable)
+- `Push()` - Create backtracking point
+- `Pop(n uint)` - Remove backtracking points
+- `Reset()` - Remove all assertions
+
+### Model Operations
+
+- `Eval(expr *Expr, modelCompletion bool)` - Evaluate expression in model
+- `NumConsts()` - Number of constants in model
+- `NumFuncs()` - Number of functions in model
+- `String()` - Get string representation
+
+### Bit-vector Operations
+
+- `MkBvSort(sz uint)` - Create bit-vector sort
+- `MkBVConst(name string, size uint)` - Create bit-vector variable
+- `MkBVAdd/Sub/Mul/UDiv/SDiv(lhs, rhs *Expr)` - Arithmetic operations
+- `MkBVAnd/Or/Xor/Not(...)` - Bitwise operations
+- `MkBVShl/LShr/AShr(lhs, rhs *Expr)` - Shift operations
+- `MkBVULT/SLT/ULE/SLE/UGE/SGE/UGT/SGT(...)` - Comparisons
+- `MkConcat(lhs, rhs *Expr)` - Bit-vector concatenation
+- `MkExtract(high, low uint, expr *Expr)` - Extract bits
+- `MkSignExt/ZeroExt(i uint, expr *Expr)` - Extend bit-vectors
+
+### Floating-Point Operations
+
+- `MkFPSort(ebits, sbits uint)` - Create floating-point sort
+- `MkFPSort16/32/64/128()` - Standard IEEE 754 sorts
+- `MkFPInf/NaN/Zero(sort *Sort, ...)` - Special values
+- `MkFPAdd/Sub/Mul/Div(rm, lhs, rhs *Expr)` - Arithmetic with rounding
+- `MkFPNeg/Abs/Sqrt(...)` - Unary operations
+- `MkFPLT/GT/LE/GE/Eq(lhs, rhs *Expr)` - Comparisons
+- `MkFPIsNaN/IsInf/IsZero(expr *Expr)` - Predicates
+
+### Sequence/String Operations
+
+- `MkStringSort()` - Create string sort
+- `MkSeqSort(elemSort *Sort)` - Create sequence sort
+- `MkString(value string)` - Create string constant
+- `MkSeqConcat(exprs ...*Expr)` - Concatenation
+- `MkSeqLength(seq *Expr)` - Length
+- `MkSeqPrefix/Suffix/Contains(...)` - Predicates
+- `MkSeqAt(seq, index *Expr)` - Element access
+- `MkSeqExtract(seq, offset, length *Expr)` - Substring
+- `MkStrToInt/IntToStr(...)` - Conversions
+
+### Regular Expression Operations
+
+- `MkReSort(seqSort *Sort)` - Create regex sort
+- `MkToRe(seq *Expr)` - Convert string to regex
+- `MkInRe(seq, re *Expr)` - String matches regex predicate
+- `MkReStar(re *Expr)` - Kleene star (zero or more)
+- `MkRePlus(re *Expr)` - Kleene plus (one or more)
+- `MkReOption(re *Expr)` - Optional (zero or one)
+- `MkRePower(re *Expr, n uint)` - Exactly n repetitions
+- `MkReLoop(re *Expr, lo, hi uint)` - Bounded repetition
+- `MkReConcat(regexes ...*Expr)` - Concatenation
+- `MkReUnion(regexes ...*Expr)` - Alternation (OR)
+- `MkReIntersect(regexes ...*Expr)` - Intersection
+- `MkReComplement(re *Expr)` - Complement
+- `MkReDiff(a, b *Expr)` - Difference
+- `MkReEmpty/Full/Allchar(sort *Sort)` - Special regexes
+- `MkReRange(lo, hi *Expr)` - Character range
+- `MkSeqReplaceRe/ReAll(seq, re, replacement *Expr)` - Regex replace
+
+### Datatype Operations
+
+- `MkConstructor(name, recognizer string, ...)` - Create constructor
+- `MkDatatypeSort(name string, constructors []*Constructor)` - Create datatype
+- `MkDatatypeSorts(names []string, ...)` - Mutually recursive datatypes
+- `MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort)` - Tuples
+- `MkEnumSort(name string, enumNames []string)` - Enumerations
+- `MkListSort(name string, elemSort *Sort)` - Lists
+
+### Tactic Operations
+
+- `MkTactic(name string)` - Create tactic by name
+- `MkGoal(models, unsatCores, proofs bool)` - Create goal
+- `Apply(g *Goal)` - Apply tactic to goal
+- `AndThen(t2 *Tactic)` - Sequential composition
+- `OrElse(t2 *Tactic)` - Try first, fallback to second
+- `Repeat(max uint)` - Repeat tactic
+- `TacticWhen/Cond(...)` - Conditional tactics
+
+### Probe Operations
+
+- `MkProbe(name string)` - Create probe by name
+- `Apply(g *Goal)` - Evaluate probe on goal
+- `Lt/Gt/Le/Ge/Eq(p2 *Probe)` - Probe comparisons
+- `And/Or/Not(...)` - Probe combinators
+
+### Parameter Operations
+
+- `MkParams()` - Create parameter set
+- `SetBool/Uint/Double/Symbol(key string, value ...)` - Set parameters
+
+### Optimize Operations
+
+- `NewOptimize()` - Create optimization context
+- `Assert(constraint *Expr)` - Add constraint
+- `AssertSoft(constraint *Expr, weight, group string)` - Add soft constraint
+- `Maximize(expr *Expr)` - Add maximization objective
+- `Minimize(expr *Expr)` - Add minimization objective
+- `Check(assumptions ...*Expr)` - Check and optimize
+- `Model()` - Get optimal model
+- `GetLower/Upper(index uint)` - Get objective bounds
+- `Push/Pop()` - Backtracking
+- `Assertions/Objectives()` - Get assertions and objectives
+- `UnsatCore()` - Get unsat core
+
+### Fixedpoint Operations (Datalog/CHC)
+
+- `NewFixedpoint()` - Create fixedpoint solver
+- `RegisterRelation(funcDecl *FuncDecl)` - Register predicate
+- `AddRule(rule *Expr, name *Symbol)` - Add Horn clause
+- `AddFact(pred *FuncDecl, args []int)` - Add table fact
+- `Query(query *Expr)` - Query constraints
+- `QueryRelations(relations []*FuncDecl)` - Query relations
+- `GetAnswer()` - Get satisfying instance or proof
+- `Push/Pop()` - Backtracking
+
+### Quantifier Operations
+
+- `MkQuantifier(isForall bool, weight int, sorts, names, body, patterns)` - Create quantifier
+- `MkQuantifierConst(isForall bool, weight int, bound, body, patterns)` - Create with bound vars
+- `IsUniversal/IsExistential()` - Check quantifier type
+- `GetNumBound()` - Number of bound variables
+- `GetBoundName/Sort(idx int)` - Get bound variable info
+- `GetBody()` - Get quantifier body
+- `GetNumPatterns()` - Number of patterns
+- `GetPattern(idx int)` - Get pattern
+
+### Lambda Operations
+
+- `MkLambda(sorts, names, body)` - Create lambda expression
+- `MkLambdaConst(bound, body)` - Create lambda with bound variables
+- `GetNumBound()` - Number of bound variables
+- `GetBoundName/Sort(idx int)` - Get bound variable info
+- `GetBody()` - Get lambda body
+
+### Type Variables
+
+- `MkTypeVariable(name *Symbol)` - Create polymorphic type variable sort
+
+### Logging
+
+- `OpenLog(filename string)` - Open interaction log
+- `CloseLog()` - Close log
+- `AppendLog(s string)` - Append to log
+- `IsLogOpen()` - Check if log is open
+
+## Memory Management
+
+The Go bindings use `runtime.SetFinalizer` to automatically manage Z3 reference counts. You don't need to manually call inc_ref/dec_ref. However, be aware that finalizers run during garbage collection, so resources may not be freed immediately.
+
+## Thread Safety
+
+Z3 contexts are not thread-safe. Each goroutine should use its own context, or use appropriate synchronization when sharing a context.
+
+## License
+
+Z3 is licensed under the MIT License. See LICENSE.txt in the repository root.
+
+## Contributing
+
+Bug reports and contributions are welcome! Please submit issues and pull requests to the main Z3 repository.
+
+## References
+
+- [Z3 GitHub Repository](https://github.com/Z3Prover/z3)
+- [Z3 API Documentation](https://z3prover.github.io/api/html/index.html)
+- [Z3 Guide](https://microsoft.github.io/z3guide/)
diff --git a/src/api/go/add_godoc.py b/src/api/go/add_godoc.py
new file mode 100644
index 000000000..62bab03f1
--- /dev/null
+++ b/src/api/go/add_godoc.py
@@ -0,0 +1,89 @@
+#!/usr/bin/env python3
+"""
+Add godoc comments to Z3 Go bindings systematically.
+This script adds proper godoc documentation to all exported types and functions.
+"""
+
+import os
+import re
+
+# Godoc comment templates for common patterns
+TYPE_COMMENTS = {
+    'Config': '// Config represents a Z3 configuration object used to customize solver behavior.\n// Create with NewConfig and configure using SetParamValue before creating a Context.',
+    'Context': '// Context represents a Z3 logical context.\n// All Z3 objects (sorts, expressions, solvers) are tied to the context that created them.\n// Contexts are not thread-safe - use separate contexts for concurrent operations.',
+    'Symbol': '// Symbol represents a Z3 symbol, which can be either a string or integer identifier.\n// Symbols are used to name sorts, constants, and functions.',
+    'AST': '// AST represents an Abstract Syntax Tree node in Z3.\n// This is the base type for all Z3 expressions, sorts, and function declarations.',
+    'Sort': '// Sort represents a type in Z3\'s type system.\n// Common sorts include Bool, Int, Real, BitVec, Array, and user-defined datatypes.',
+    'Expr': '// Expr represents a Z3 expression (term).\n// Expressions are typed AST nodes that can be evaluated, simplified, or used in constraints.',
+    'FuncDecl': '// FuncDecl represents a function declaration in Z3.\n// Function declarations define the signature (domain and range sorts) of functions.',
+    'Pattern': '// Pattern represents a pattern for quantifier instantiation.\n// Patterns guide Z3\'s E-matching algorithm for quantifier instantiation.',
+    'Quantifier': '// Quantifier represents a quantified formula (forall or exists).\n// Quantifiers bind variables and include optional patterns for instantiation.',
+    'Lambda': '// Lambda represents a lambda expression (anonymous function).\n// Lambda expressions can be used as array values or in higher-order reasoning.',
+    'Statistics': '// Statistics holds performance and diagnostic information from Z3 solvers.\n// Use GetKey, GetUintValue, and GetDoubleValue to access individual statistics.',
+}
+
+FUNCTION_COMMENTS = {
+    'NewConfig': '// NewConfig creates a new Z3 configuration object.\n// Use SetParamValue to configure parameters before creating a context.',
+    'NewContext': '// NewContext creates a new Z3 context with default configuration.\n// The context manages memory for all Z3 objects and must outlive any objects it creates.',
+    'NewContextWithConfig': '// NewContextWithConfig creates a new Z3 context with the given configuration.\n// The configuration is consumed and should not be reused.',
+}
+
+def add_godoc_comment(content, pattern, comment):
+    """Add godoc comment before a type or function declaration."""
+    # Check if comment already exists
+    lines = content.split('\n')
+    result = []
+    i = 0
+    
+    while i < len(lines):
+        line = lines[i]
+        
+        # Check if this line matches our pattern
+        if re.match(pattern, line):
+            # Check if previous line is already a comment
+            if i > 0 and (result[-1].strip().startswith('//') or result[-1].strip().startswith('/*')):
+                # Comment exists, skip
+                result.append(line)
+            else:
+                # Add comment
+                result.append(comment)
+                result.append(line)
+        else:
+            result.append(line)
+        
+        i += 1
+    
+    return '\n'.join(result)
+
+def process_file(filepath, type_comments, func_comments):
+    """Process a single Go file and add godoc comments."""
+    print(f"Processing {filepath}...")
+    
+    with open(filepath, 'r', encoding='utf-8') as f:
+        content = f.read()
+    
+    # Add type comments
+    for type_name, comment in type_comments.items():
+        pattern = f'^type {type_name} struct'
+        content = add_godoc_comment(content, pattern, comment)
+    
+    # Add function comments
+    for func_name, comment in func_comments.items():
+        pattern = f'^func (\\([^)]+\\) )?{func_name}\\('
+        content = add_godoc_comment(content, pattern, comment)
+    
+    with open(filepath, 'w', encoding='utf-8') as f:
+        f.write(content)
+    
+    print(f"Updated {filepath}")
+
+if __name__ == '__main__':
+    go_api_dir = os.path.dirname(os.path.abspath(__file__))
+    
+    # Process z3.go with core types
+    z3_go = os.path.join(go_api_dir, 'z3.go')
+    if os.path.exists(z3_go):
+        process_file(z3_go, TYPE_COMMENTS, FUNCTION_COMMENTS)
+    
+    print("\nGodoc comments added successfully!")
+    print("Run 'go doc' to verify documentation.")
diff --git a/src/api/go/arith.go b/src/api/go/arith.go
new file mode 100644
index 000000000..12c01e195
--- /dev/null
+++ b/src/api/go/arith.go
@@ -0,0 +1,126 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+
+// Arithmetic operations and sorts
+
+// MkIntSort creates the integer sort.
+func (c *Context) MkIntSort() *Sort {
+	return newSort(c, C.Z3_mk_int_sort(c.ptr))
+}
+
+// MkRealSort creates the real number sort.
+func (c *Context) MkRealSort() *Sort {
+	return newSort(c, C.Z3_mk_real_sort(c.ptr))
+}
+
+// MkInt creates an integer constant from an int.
+func (c *Context) MkInt(value int, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_int(c.ptr, C.int(value), sort.ptr))
+}
+
+// MkInt64 creates an integer constant from an int64.
+func (c *Context) MkInt64(value int64, sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_int64(c.ptr, C.int64_t(value), sort.ptr))
+}
+
+// MkReal creates a real constant from numerator and denominator.
+func (c *Context) MkReal(num, den int) *Expr {
+	return newExpr(c, C.Z3_mk_real(c.ptr, C.int(num), C.int(den)))
+}
+
+// MkIntConst creates an integer constant (variable) with the given name.
+func (c *Context) MkIntConst(name string) *Expr {
+	sym := c.MkStringSymbol(name)
+	return c.MkConst(sym, c.MkIntSort())
+}
+
+// MkRealConst creates a real constant (variable) with the given name.
+func (c *Context) MkRealConst(name string) *Expr {
+	sym := c.MkStringSymbol(name)
+	return c.MkConst(sym, c.MkRealSort())
+}
+
+// MkAdd creates an addition.
+func (c *Context) MkAdd(exprs ...*Expr) *Expr {
+	if len(exprs) == 0 {
+		return c.MkInt(0, c.MkIntSort())
+	}
+	if len(exprs) == 1 {
+		return exprs[0]
+	}
+	cExprs := make([]C.Z3_ast, len(exprs))
+	for i, e := range exprs {
+		cExprs[i] = e.ptr
+	}
+	return newExpr(c, C.Z3_mk_add(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+// MkSub creates a subtraction.
+func (c *Context) MkSub(exprs ...*Expr) *Expr {
+	if len(exprs) == 0 {
+		return c.MkInt(0, c.MkIntSort())
+	}
+	if len(exprs) == 1 {
+		return newExpr(c, C.Z3_mk_unary_minus(c.ptr, exprs[0].ptr))
+	}
+	cExprs := make([]C.Z3_ast, len(exprs))
+	for i, e := range exprs {
+		cExprs[i] = e.ptr
+	}
+	return newExpr(c, C.Z3_mk_sub(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+// MkMul creates a multiplication.
+func (c *Context) MkMul(exprs ...*Expr) *Expr {
+	if len(exprs) == 0 {
+		return c.MkInt(1, c.MkIntSort())
+	}
+	if len(exprs) == 1 {
+		return exprs[0]
+	}
+	cExprs := make([]C.Z3_ast, len(exprs))
+	for i, e := range exprs {
+		cExprs[i] = e.ptr
+	}
+	return newExpr(c, C.Z3_mk_mul(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+// MkDiv creates a division.
+func (c *Context) MkDiv(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_div(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkMod creates a modulo operation.
+func (c *Context) MkMod(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_mod(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkRem creates a remainder operation.
+func (c *Context) MkRem(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_rem(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkLt creates a less-than constraint.
+func (c *Context) MkLt(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_lt(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkLe creates a less-than-or-equal constraint.
+func (c *Context) MkLe(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_le(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkGt creates a greater-than constraint.
+func (c *Context) MkGt(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_gt(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkGe creates a greater-than-or-equal constraint.
+func (c *Context) MkGe(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_ge(c.ptr, lhs.ptr, rhs.ptr))
+}
diff --git a/src/api/go/array.go b/src/api/go/array.go
new file mode 100644
index 000000000..98e947301
--- /dev/null
+++ b/src/api/go/array.go
@@ -0,0 +1,29 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+
+// Array operations and sorts
+
+// MkArraySort creates an array sort.
+func (c *Context) MkArraySort(domain, range_ *Sort) *Sort {
+	return newSort(c, C.Z3_mk_array_sort(c.ptr, domain.ptr, range_.ptr))
+}
+
+// MkSelect creates an array read (select) operation.
+func (c *Context) MkSelect(array, index *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_select(c.ptr, array.ptr, index.ptr))
+}
+
+// MkStore creates an array write (store) operation.
+func (c *Context) MkStore(array, index, value *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_store(c.ptr, array.ptr, index.ptr, value.ptr))
+}
+
+// MkConstArray creates a constant array.
+func (c *Context) MkConstArray(sort *Sort, value *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_const_array(c.ptr, sort.ptr, value.ptr))
+}
diff --git a/src/api/go/bitvec.go b/src/api/go/bitvec.go
new file mode 100644
index 000000000..9ffd220ac
--- /dev/null
+++ b/src/api/go/bitvec.go
@@ -0,0 +1,160 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+
+// Bit-vector operations
+
+// MkBVConst creates a bit-vector constant with the given name and size.
+func (c *Context) MkBVConst(name string, size uint) *Expr {
+	sym := c.MkStringSymbol(name)
+	return c.MkConst(sym, c.MkBvSort(size))
+}
+
+// MkBV creates a bit-vector numeral from an integer.
+func (c *Context) MkBV(value int, size uint) *Expr {
+	return newExpr(c, C.Z3_mk_int(c.ptr, C.int(value), c.MkBvSort(size).ptr))
+}
+
+// MkBVFromInt64 creates a bit-vector from an int64.
+func (c *Context) MkBVFromInt64(value int64, size uint) *Expr {
+	return newExpr(c, C.Z3_mk_int64(c.ptr, C.int64_t(value), c.MkBvSort(size).ptr))
+}
+
+// MkBVAdd creates a bit-vector addition.
+func (c *Context) MkBVAdd(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvadd(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVSub creates a bit-vector subtraction.
+func (c *Context) MkBVSub(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsub(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVMul creates a bit-vector multiplication.
+func (c *Context) MkBVMul(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvmul(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVUDiv creates an unsigned bit-vector division.
+func (c *Context) MkBVUDiv(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvudiv(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVSDiv creates a signed bit-vector division.
+func (c *Context) MkBVSDiv(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsdiv(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVURem creates an unsigned bit-vector remainder.
+func (c *Context) MkBVURem(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvurem(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVSRem creates a signed bit-vector remainder.
+func (c *Context) MkBVSRem(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsrem(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVNeg creates a bit-vector negation.
+func (c *Context) MkBVNeg(expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvneg(c.ptr, expr.ptr))
+}
+
+// MkBVAnd creates a bit-vector bitwise AND.
+func (c *Context) MkBVAnd(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvand(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVOr creates a bit-vector bitwise OR.
+func (c *Context) MkBVOr(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvor(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVXor creates a bit-vector bitwise XOR.
+func (c *Context) MkBVXor(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvxor(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVNot creates a bit-vector bitwise NOT.
+func (c *Context) MkBVNot(expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvnot(c.ptr, expr.ptr))
+}
+
+// MkBVShl creates a bit-vector shift left.
+func (c *Context) MkBVShl(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvshl(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVLShr creates a bit-vector logical shift right.
+func (c *Context) MkBVLShr(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvlshr(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVAShr creates a bit-vector arithmetic shift right.
+func (c *Context) MkBVAShr(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvashr(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVULT creates an unsigned bit-vector less-than.
+func (c *Context) MkBVULT(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvult(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVSLT creates a signed bit-vector less-than.
+func (c *Context) MkBVSLT(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvslt(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVULE creates an unsigned bit-vector less-than-or-equal.
+func (c *Context) MkBVULE(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvule(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVSLE creates a signed bit-vector less-than-or-equal.
+func (c *Context) MkBVSLE(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsle(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVUGE creates an unsigned bit-vector greater-than-or-equal.
+func (c *Context) MkBVUGE(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvuge(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVSGE creates a signed bit-vector greater-than-or-equal.
+func (c *Context) MkBVSGE(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsge(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVUGT creates an unsigned bit-vector greater-than.
+func (c *Context) MkBVUGT(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvugt(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkBVSGT creates a signed bit-vector greater-than.
+func (c *Context) MkBVSGT(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_bvsgt(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkConcat creates a bit-vector concatenation.
+func (c *Context) MkConcat(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_concat(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkExtract creates a bit-vector extraction.
+func (c *Context) MkExtract(high, low uint, expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_extract(c.ptr, C.uint(high), C.uint(low), expr.ptr))
+}
+
+// MkSignExt creates a bit-vector sign extension.
+func (c *Context) MkSignExt(i uint, expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_sign_ext(c.ptr, C.uint(i), expr.ptr))
+}
+
+// MkZeroExt creates a bit-vector zero extension.
+func (c *Context) MkZeroExt(i uint, expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_zero_ext(c.ptr, C.uint(i), expr.ptr))
+}
diff --git a/src/api/go/datatype.go b/src/api/go/datatype.go
new file mode 100644
index 000000000..2dd9d8555
--- /dev/null
+++ b/src/api/go/datatype.go
@@ -0,0 +1,293 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"runtime"
+	"unsafe"
+)
+
+// Constructor represents a datatype constructor.
+type Constructor struct {
+	ctx *Context
+	ptr C.Z3_constructor
+}
+
+// newConstructor creates a new Constructor and manages its reference count.
+func newConstructor(ctx *Context, ptr C.Z3_constructor) *Constructor {
+	c := &Constructor{ctx: ctx, ptr: ptr}
+	C.Z3_constructor_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(c, func(cons *Constructor) {
+		C.Z3_constructor_dec_ref(cons.ctx.ptr, cons.ptr)
+	})
+	return c
+}
+
+// MkConstructor creates a constructor for a datatype.
+// name is the constructor name, recognizer is the recognizer name,
+// fieldNames are the names of the fields, and fieldSorts are the sorts of the fields.
+// fieldSortRefs can be 0 for non-recursive fields or the datatype index for recursive fields.
+func (c *Context) MkConstructor(name, recognizer string, fieldNames []string, fieldSorts []*Sort, fieldSortRefs []uint) *Constructor {
+	cName := C.CString(name)
+	cRecognizer := C.CString(recognizer)
+	defer C.free(unsafe.Pointer(cName))
+	defer C.free(unsafe.Pointer(cRecognizer))
+
+	numFields := uint(len(fieldNames))
+	if numFields != uint(len(fieldSorts)) || numFields != uint(len(fieldSortRefs)) {
+		panic("fieldNames, fieldSorts, and fieldSortRefs must have the same length")
+	}
+
+	var cFieldNames *C.Z3_symbol
+	var cSorts *C.Z3_sort
+	var cSortRefs *C.uint
+	
+	if numFields > 0 {
+		fieldSyms := make([]C.Z3_symbol, numFields)
+		for i, fname := range fieldNames {
+			fieldSyms[i] = c.MkStringSymbol(fname).ptr
+		}
+		cFieldNames = &fieldSyms[0]
+
+		sorts := make([]C.Z3_sort, numFields)
+		for i, s := range fieldSorts {
+			if s != nil {
+				sorts[i] = s.ptr
+			}
+		}
+		cSorts = &sorts[0]
+
+		refs := make([]C.uint, numFields)
+		for i, r := range fieldSortRefs {
+			refs[i] = C.uint(r)
+		}
+		cSortRefs = &refs[0]
+	}
+
+	sym := c.MkStringSymbol(name)
+	recSym := c.MkStringSymbol(recognizer)
+	
+	return newConstructor(c, C.Z3_mk_constructor(
+		c.ptr,
+		sym.ptr,
+		recSym.ptr,
+		C.uint(numFields),
+		cFieldNames,
+		cSorts,
+		cSortRefs,
+	))
+}
+
+// ConstructorList represents a list of datatype constructors.
+type ConstructorList struct {
+	ctx *Context
+	ptr C.Z3_constructor_list
+}
+
+// newConstructorList creates a new ConstructorList and manages its reference count.
+func newConstructorList(ctx *Context, ptr C.Z3_constructor_list) *ConstructorList {
+	cl := &ConstructorList{ctx: ctx, ptr: ptr}
+	C.Z3_constructor_list_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(cl, func(list *ConstructorList) {
+		C.Z3_constructor_list_dec_ref(list.ctx.ptr, list.ptr)
+	})
+	return cl
+}
+
+// MkConstructorList creates a list of constructors for a datatype.
+func (c *Context) MkConstructorList(constructors []*Constructor) *ConstructorList {
+	numCons := uint(len(constructors))
+	if numCons == 0 {
+		return nil
+	}
+
+	cons := make([]C.Z3_constructor, numCons)
+	for i, constr := range constructors {
+		cons[i] = constr.ptr
+	}
+
+	return newConstructorList(c, C.Z3_mk_constructor_list(c.ptr, C.uint(numCons), &cons[0]))
+}
+
+// MkDatatypeSort creates a datatype sort from a constructor list.
+func (c *Context) MkDatatypeSort(name string, constructors []*Constructor) *Sort {
+	sym := c.MkStringSymbol(name)
+	
+	numCons := uint(len(constructors))
+	cons := make([]C.Z3_constructor, numCons)
+	for i, constr := range constructors {
+		cons[i] = constr.ptr
+	}
+
+	return newSort(c, C.Z3_mk_datatype(c.ptr, sym.ptr, C.uint(numCons), &cons[0]))
+}
+
+// MkDatatypeSorts creates multiple mutually recursive datatype sorts.
+func (c *Context) MkDatatypeSorts(names []string, constructorLists [][]*Constructor) []*Sort {
+	numTypes := uint(len(names))
+	if numTypes != uint(len(constructorLists)) {
+		panic("names and constructorLists must have the same length")
+	}
+
+	syms := make([]C.Z3_symbol, numTypes)
+	for i, name := range names {
+		syms[i] = c.MkStringSymbol(name).ptr
+	}
+
+	cLists := make([]C.Z3_constructor_list, numTypes)
+	for i, constrs := range constructorLists {
+		cons := make([]C.Z3_constructor, len(constrs))
+		for j, constr := range constrs {
+			cons[j] = constr.ptr
+		}
+		cLists[i] = C.Z3_mk_constructor_list(c.ptr, C.uint(len(constrs)), &cons[0])
+	}
+
+	resultSorts := make([]C.Z3_sort, numTypes)
+	
+	C.Z3_mk_datatypes(c.ptr, C.uint(numTypes), &syms[0], &resultSorts[0], &cLists[0])
+
+	// Clean up constructor lists
+	for i := range cLists {
+		C.Z3_constructor_list_dec_ref(c.ptr, cLists[i])
+	}
+
+	sorts := make([]*Sort, numTypes)
+	for i := range resultSorts {
+		sorts[i] = newSort(c, resultSorts[i])
+	}
+
+	return sorts
+}
+
+// GetDatatypeSortConstructor returns the i-th constructor of a datatype sort.
+func (c *Context) GetDatatypeSortConstructor(sort *Sort, i uint) *FuncDecl {
+	return newFuncDecl(c, C.Z3_get_datatype_sort_constructor(c.ptr, sort.ptr, C.uint(i)))
+}
+
+// GetDatatypeSortRecognizer returns the i-th recognizer of a datatype sort.
+func (c *Context) GetDatatypeSortRecognizer(sort *Sort, i uint) *FuncDecl {
+	return newFuncDecl(c, C.Z3_get_datatype_sort_recognizer(c.ptr, sort.ptr, C.uint(i)))
+}
+
+// GetDatatypeSortConstructorAccessor returns the accessor for the i-th field of the j-th constructor.
+func (c *Context) GetDatatypeSortConstructorAccessor(sort *Sort, constructorIdx, accessorIdx uint) *FuncDecl {
+	return newFuncDecl(c, C.Z3_get_datatype_sort_constructor_accessor(
+		c.ptr, sort.ptr, C.uint(constructorIdx), C.uint(accessorIdx)))
+}
+
+// GetDatatypeSortNumConstructors returns the number of constructors in a datatype sort.
+func (c *Context) GetDatatypeSortNumConstructors(sort *Sort) uint {
+	return uint(C.Z3_get_datatype_sort_num_constructors(c.ptr, sort.ptr))
+}
+
+// Tuple sorts (special case of datatypes)
+
+// MkTupleSort creates a tuple sort with the given field sorts.
+func (c *Context) MkTupleSort(name string, fieldNames []string, fieldSorts []*Sort) (*Sort, *FuncDecl, []*FuncDecl) {
+	sym := c.MkStringSymbol(name)
+	
+	numFields := uint(len(fieldNames))
+	if numFields != uint(len(fieldSorts)) {
+		panic("fieldNames and fieldSorts must have the same length")
+	}
+
+	fieldSyms := make([]C.Z3_symbol, numFields)
+	for i, fname := range fieldNames {
+		fieldSyms[i] = c.MkStringSymbol(fname).ptr
+	}
+
+	sorts := make([]C.Z3_sort, numFields)
+	for i, s := range fieldSorts {
+		sorts[i] = s.ptr
+	}
+
+	var mkTupleDecl C.Z3_func_decl
+	projDecls := make([]C.Z3_func_decl, numFields)
+
+	tupleSort := C.Z3_mk_tuple_sort(
+		c.ptr,
+		sym.ptr,
+		C.uint(numFields),
+		&fieldSyms[0],
+		&sorts[0],
+		&mkTupleDecl,
+		&projDecls[0],
+	)
+
+	projections := make([]*FuncDecl, numFields)
+	for i := range projDecls {
+		projections[i] = newFuncDecl(c, projDecls[i])
+	}
+
+	return newSort(c, tupleSort), newFuncDecl(c, mkTupleDecl), projections
+}
+
+// Enumeration sorts (special case of datatypes)
+
+// MkEnumSort creates an enumeration sort with the given constants.
+func (c *Context) MkEnumSort(name string, enumNames []string) (*Sort, []*FuncDecl, []*FuncDecl) {
+	sym := c.MkStringSymbol(name)
+	
+	numEnums := uint(len(enumNames))
+	enumSyms := make([]C.Z3_symbol, numEnums)
+	for i, ename := range enumNames {
+		enumSyms[i] = c.MkStringSymbol(ename).ptr
+	}
+
+	enumConsts := make([]C.Z3_func_decl, numEnums)
+	enumTesters := make([]C.Z3_func_decl, numEnums)
+
+	enumSort := C.Z3_mk_enumeration_sort(
+		c.ptr,
+		sym.ptr,
+		C.uint(numEnums),
+		&enumSyms[0],
+		&enumConsts[0],
+		&enumTesters[0],
+	)
+
+	consts := make([]*FuncDecl, numEnums)
+	for i := range enumConsts {
+		consts[i] = newFuncDecl(c, enumConsts[i])
+	}
+
+	testers := make([]*FuncDecl, numEnums)
+	for i := range enumTesters {
+		testers[i] = newFuncDecl(c, enumTesters[i])
+	}
+
+	return newSort(c, enumSort), consts, testers
+}
+
+// List sorts (special case of datatypes)
+
+// MkListSort creates a list sort with the given element sort.
+func (c *Context) MkListSort(name string, elemSort *Sort) (*Sort, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl, *FuncDecl) {
+	sym := c.MkStringSymbol(name)
+
+	var nilDecl, consDecl, isNilDecl, isConsDecl, headDecl, tailDecl C.Z3_func_decl
+
+	listSort := C.Z3_mk_list_sort(
+		c.ptr,
+		sym.ptr,
+		elemSort.ptr,
+		&nilDecl,
+		&isNilDecl,
+		&consDecl,
+		&isConsDecl,
+		&headDecl,
+		&tailDecl,
+	)
+
+	return newSort(c, listSort),
+		newFuncDecl(c, nilDecl),
+		newFuncDecl(c, consDecl),
+		newFuncDecl(c, isNilDecl),
+		newFuncDecl(c, isConsDecl),
+		newFuncDecl(c, headDecl),
+		newFuncDecl(c, tailDecl)
+}
diff --git a/src/api/go/fixedpoint.go b/src/api/go/fixedpoint.go
new file mode 100644
index 000000000..c22926467
--- /dev/null
+++ b/src/api/go/fixedpoint.go
@@ -0,0 +1,282 @@
+// Copyright (c) Microsoft Corporation 2025
+// Z3 Go API: Fixedpoint solver for Datalog and CHC (Constrained Horn Clauses)
+
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"runtime"
+	"unsafe"
+)
+
+// Fixedpoint represents a fixedpoint solver for Datalog/CHC queries
+type Fixedpoint struct {
+	ctx *Context
+	ptr C.Z3_fixedpoint
+}
+
+// newFixedpoint creates a new Fixedpoint solver with proper memory management
+func newFixedpoint(ctx *Context, ptr C.Z3_fixedpoint) *Fixedpoint {
+	fp := &Fixedpoint{ctx: ctx, ptr: ptr}
+	C.Z3_fixedpoint_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(fp, func(f *Fixedpoint) {
+		C.Z3_fixedpoint_dec_ref(f.ctx.ptr, f.ptr)
+	})
+	return fp
+}
+
+// NewFixedpoint creates a new fixedpoint solver
+func (ctx *Context) NewFixedpoint() *Fixedpoint {
+	ptr := C.Z3_mk_fixedpoint(ctx.ptr)
+	return newFixedpoint(ctx, ptr)
+}
+
+// GetHelp returns a string describing all available fixedpoint solver parameters
+func (f *Fixedpoint) GetHelp() string {
+	cstr := C.Z3_fixedpoint_get_help(f.ctx.ptr, f.ptr)
+	return C.GoString(cstr)
+}
+
+// SetParams sets the fixedpoint solver parameters
+func (f *Fixedpoint) SetParams(params *Params) {
+	C.Z3_fixedpoint_set_params(f.ctx.ptr, f.ptr, params.ptr)
+}
+
+// GetParamDescrs retrieves parameter descriptions for the fixedpoint solver
+func (f *Fixedpoint) GetParamDescrs() *ParamDescrs {
+	ptr := C.Z3_fixedpoint_get_param_descrs(f.ctx.ptr, f.ptr)
+	return newParamDescrs(f.ctx, ptr)
+}
+
+// Assert adds a constraint into the fixedpoint solver
+func (f *Fixedpoint) Assert(constraint *Expr) {
+	C.Z3_fixedpoint_assert(f.ctx.ptr, f.ptr, constraint.ptr)
+}
+
+// RegisterRelation registers a predicate as a recursive relation
+func (f *Fixedpoint) RegisterRelation(funcDecl *FuncDecl) {
+	C.Z3_fixedpoint_register_relation(f.ctx.ptr, f.ptr, funcDecl.ptr)
+}
+
+// AddRule adds a rule (Horn clause) to the fixedpoint solver
+// The rule should be an implication of the form body => head
+// where head is a relation and body is a conjunction of relations
+func (f *Fixedpoint) AddRule(rule *Expr, name *Symbol) {
+	var namePtr C.Z3_symbol
+	if name != nil {
+		namePtr = name.ptr
+	} else {
+		namePtr = 0
+	}
+	C.Z3_fixedpoint_add_rule(f.ctx.ptr, f.ptr, rule.ptr, namePtr)
+}
+
+// AddFact adds a table fact to the fixedpoint solver
+func (f *Fixedpoint) AddFact(pred *FuncDecl, args []int) {
+	if len(args) == 0 {
+		C.Z3_fixedpoint_add_fact(f.ctx.ptr, f.ptr, pred.ptr, 0, nil)
+		return
+	}
+	
+	cArgs := make([]C.uint, len(args))
+	for i, arg := range args {
+		cArgs[i] = C.uint(arg)
+	}
+	C.Z3_fixedpoint_add_fact(f.ctx.ptr, f.ptr, pred.ptr, C.uint(len(args)), &cArgs[0])
+}
+
+// Query queries the fixedpoint solver with a constraint
+// Returns Satisfiable if there is a derivation, Unsatisfiable if not
+func (f *Fixedpoint) Query(query *Expr) Status {
+	result := C.Z3_fixedpoint_query(f.ctx.ptr, f.ptr, query.ptr)
+	switch result {
+	case C.Z3_L_TRUE:
+		return Satisfiable
+	case C.Z3_L_FALSE:
+		return Unsatisfiable
+	default:
+		return Unknown
+	}
+}
+
+// QueryRelations queries the fixedpoint solver with an array of relations
+// Returns Satisfiable if any relation is non-empty, Unsatisfiable otherwise
+func (f *Fixedpoint) QueryRelations(relations []*FuncDecl) Status {
+	if len(relations) == 0 {
+		return Unknown
+	}
+	
+	cRelations := make([]C.Z3_func_decl, len(relations))
+	for i, rel := range relations {
+		cRelations[i] = rel.ptr
+	}
+	
+	result := C.Z3_fixedpoint_query_relations(f.ctx.ptr, f.ptr, C.uint(len(relations)), &cRelations[0])
+	switch result {
+	case C.Z3_L_TRUE:
+		return Satisfiable
+	case C.Z3_L_FALSE:
+		return Unsatisfiable
+	default:
+		return Unknown
+	}
+}
+
+// UpdateRule updates a named rule in the fixedpoint solver
+func (f *Fixedpoint) UpdateRule(rule *Expr, name *Symbol) {
+	var namePtr C.Z3_symbol
+	if name != nil {
+		namePtr = name.ptr
+	} else {
+		namePtr = 0
+	}
+	C.Z3_fixedpoint_update_rule(f.ctx.ptr, f.ptr, rule.ptr, namePtr)
+}
+
+// GetAnswer retrieves the satisfying instance or instances of solver,
+// or definitions for the recursive predicates that show unsatisfiability
+func (f *Fixedpoint) GetAnswer() *Expr {
+	ptr := C.Z3_fixedpoint_get_answer(f.ctx.ptr, f.ptr)
+	if ptr == nil {
+		return nil
+	}
+	return newExpr(f.ctx, ptr)
+}
+
+// GetReasonUnknown retrieves explanation why fixedpoint engine returned status Unknown
+func (f *Fixedpoint) GetReasonUnknown() string {
+	cstr := C.Z3_fixedpoint_get_reason_unknown(f.ctx.ptr, f.ptr)
+	return C.GoString(cstr)
+}
+
+// GetNumLevels retrieves the number of levels explored for a given predicate
+func (f *Fixedpoint) GetNumLevels(predicate *FuncDecl) int {
+	return int(C.Z3_fixedpoint_get_num_levels(f.ctx.ptr, f.ptr, predicate.ptr))
+}
+
+// GetCoverDelta retrieves the cover delta for a given predicate and level
+func (f *Fixedpoint) GetCoverDelta(level int, predicate *FuncDecl) *Expr {
+	ptr := C.Z3_fixedpoint_get_cover_delta(f.ctx.ptr, f.ptr, C.int(level), predicate.ptr)
+	if ptr == nil {
+		return nil
+	}
+	return newExpr(f.ctx, ptr)
+}
+
+// AddCover adds a cover constraint to a predicate at a given level
+func (f *Fixedpoint) AddCover(level int, predicate *FuncDecl, property *Expr) {
+	C.Z3_fixedpoint_add_cover(f.ctx.ptr, f.ptr, C.int(level), predicate.ptr, property.ptr)
+}
+
+// String returns the string representation of the fixedpoint solver
+func (f *Fixedpoint) String() string {
+	cstr := C.Z3_fixedpoint_to_string(f.ctx.ptr, f.ptr, 0, nil)
+	return C.GoString(cstr)
+}
+
+// GetStatistics retrieves statistics for the fixedpoint solver
+func (f *Fixedpoint) GetStatistics() *Statistics {
+	ptr := C.Z3_fixedpoint_get_statistics(f.ctx.ptr, f.ptr)
+	return newStatistics(f.ctx, ptr)
+}
+
+// GetRules retrieves the current rules as a string
+func (f *Fixedpoint) GetRules() string {
+	return f.String()
+}
+
+// GetAssertions retrieves the fixedpoint assertions as an AST vector
+func (f *Fixedpoint) GetAssertions() *ASTVector {
+	ptr := C.Z3_fixedpoint_get_assertions(f.ctx.ptr, f.ptr)
+	return newASTVector(f.ctx, ptr)
+}
+
+// Push creates a backtracking point
+func (f *Fixedpoint) Push() {
+	C.Z3_fixedpoint_push(f.ctx.ptr, f.ptr)
+}
+
+// Pop backtracks one backtracking point
+func (f *Fixedpoint) Pop() {
+	C.Z3_fixedpoint_pop(f.ctx.ptr, f.ptr)
+}
+
+// SetPredicateRepresentation sets the predicate representation for a given relation
+func (f *Fixedpoint) SetPredicateRepresentation(funcDecl *FuncDecl, kinds []C.Z3_symbol) {
+	if len(kinds) == 0 {
+		C.Z3_fixedpoint_set_predicate_representation(f.ctx.ptr, f.ptr, funcDecl.ptr, 0, nil)
+		return
+	}
+	C.Z3_fixedpoint_set_predicate_representation(f.ctx.ptr, f.ptr, funcDecl.ptr, C.uint(len(kinds)), &kinds[0])
+}
+
+// FromString parses a Datalog program from a string
+func (f *Fixedpoint) FromString(s string) {
+	cstr := C.CString(s)
+	defer C.free(unsafe.Pointer(cstr))
+	C.Z3_fixedpoint_from_string(f.ctx.ptr, f.ptr, cstr)
+}
+
+// FromFile parses a Datalog program from a file
+func (f *Fixedpoint) FromFile(filename string) {
+	cstr := C.CString(filename)
+	defer C.free(unsafe.Pointer(cstr))
+	C.Z3_fixedpoint_from_file(f.ctx.ptr, f.ptr, cstr)
+}
+
+// Statistics represents statistics for Z3 solvers
+type Statistics struct {
+	ctx *Context
+	ptr C.Z3_stats
+}
+
+// newStatistics creates a new Statistics object with proper memory management
+func newStatistics(ctx *Context, ptr C.Z3_stats) *Statistics {
+	stats := &Statistics{ctx: ctx, ptr: ptr}
+	C.Z3_stats_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(stats, func(s *Statistics) {
+		C.Z3_stats_dec_ref(s.ctx.ptr, s.ptr)
+	})
+	return stats
+}
+
+// String returns the string representation of statistics
+func (s *Statistics) String() string {
+	cstr := C.Z3_stats_to_string(s.ctx.ptr, s.ptr)
+	return C.GoString(cstr)
+}
+
+// Size returns the number of statistical data entries
+func (s *Statistics) Size() int {
+	return int(C.Z3_stats_size(s.ctx.ptr, s.ptr))
+}
+
+// GetKey returns the key (name) of a statistical data entry at the given index
+func (s *Statistics) GetKey(idx int) string {
+	cstr := C.Z3_stats_get_key(s.ctx.ptr, s.ptr, C.uint(idx))
+	return C.GoString(cstr)
+}
+
+// IsUint returns true if the statistical data at the given index is unsigned integer
+func (s *Statistics) IsUint(idx int) bool {
+	return C.Z3_stats_is_uint(s.ctx.ptr, s.ptr, C.uint(idx)) != 0
+}
+
+// IsDouble returns true if the statistical data at the given index is double
+func (s *Statistics) IsDouble(idx int) bool {
+	return C.Z3_stats_is_double(s.ctx.ptr, s.ptr, C.uint(idx)) != 0
+}
+
+// GetUintValue returns the unsigned integer value at the given index
+func (s *Statistics) GetUintValue(idx int) uint64 {
+	return uint64(C.Z3_stats_get_uint_value(s.ctx.ptr, s.ptr, C.uint(idx)))
+}
+
+// GetDoubleValue returns the double value at the given index
+func (s *Statistics) GetDoubleValue(idx int) float64 {
+	return float64(C.Z3_stats_get_double_value(s.ctx.ptr, s.ptr, C.uint(idx)))
+}
diff --git a/src/api/go/fp.go b/src/api/go/fp.go
new file mode 100644
index 000000000..116d681aa
--- /dev/null
+++ b/src/api/go/fp.go
@@ -0,0 +1,139 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"unsafe"
+)
+
+// Floating-point operations
+
+// MkFPSort creates a floating-point sort.
+func (c *Context) MkFPSort(ebits, sbits uint) *Sort {
+	return newSort(c, C.Z3_mk_fpa_sort(c.ptr, C.uint(ebits), C.uint(sbits)))
+}
+
+// MkFPSort16 creates a 16-bit floating-point sort.
+func (c *Context) MkFPSort16() *Sort {
+	return newSort(c, C.Z3_mk_fpa_sort_16(c.ptr))
+}
+
+// MkFPSort32 creates a 32-bit floating-point sort (single precision).
+func (c *Context) MkFPSort32() *Sort {
+	return newSort(c, C.Z3_mk_fpa_sort_32(c.ptr))
+}
+
+// MkFPSort64 creates a 64-bit floating-point sort (double precision).
+func (c *Context) MkFPSort64() *Sort {
+	return newSort(c, C.Z3_mk_fpa_sort_64(c.ptr))
+}
+
+// MkFPSort128 creates a 128-bit floating-point sort (quadruple precision).
+func (c *Context) MkFPSort128() *Sort {
+	return newSort(c, C.Z3_mk_fpa_sort_128(c.ptr))
+}
+
+// MkFPRoundingModeSort creates the rounding mode sort.
+func (c *Context) MkFPRoundingModeSort() *Sort {
+	return newSort(c, C.Z3_mk_fpa_rounding_mode_sort(c.ptr))
+}
+
+// MkFPNumeral creates a floating-point numeral from a string.
+func (c *Context) MkFPNumeral(value string, sort *Sort) *Expr {
+	cStr := C.CString(value)
+	defer C.free(unsafe.Pointer(cStr))
+	return newExpr(c, C.Z3_mk_numeral(c.ptr, cStr, sort.ptr))
+}
+
+// MkFPInf creates a floating-point infinity.
+func (c *Context) MkFPInf(sort *Sort, negative bool) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_inf(c.ptr, sort.ptr, C.bool(negative)))
+}
+
+// MkFPNaN creates a floating-point NaN.
+func (c *Context) MkFPNaN(sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_nan(c.ptr, sort.ptr))
+}
+
+// MkFPZero creates a floating-point zero.
+func (c *Context) MkFPZero(sort *Sort, negative bool) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_zero(c.ptr, sort.ptr, C.bool(negative)))
+}
+
+// MkFPAdd creates a floating-point addition.
+func (c *Context) MkFPAdd(rm, lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_add(c.ptr, rm.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPSub creates a floating-point subtraction.
+func (c *Context) MkFPSub(rm, lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_sub(c.ptr, rm.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPMul creates a floating-point multiplication.
+func (c *Context) MkFPMul(rm, lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_mul(c.ptr, rm.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPDiv creates a floating-point division.
+func (c *Context) MkFPDiv(rm, lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_div(c.ptr, rm.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPNeg creates a floating-point negation.
+func (c *Context) MkFPNeg(expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_neg(c.ptr, expr.ptr))
+}
+
+// MkFPAbs creates a floating-point absolute value.
+func (c *Context) MkFPAbs(expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_abs(c.ptr, expr.ptr))
+}
+
+// MkFPSqrt creates a floating-point square root.
+func (c *Context) MkFPSqrt(rm, expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_sqrt(c.ptr, rm.ptr, expr.ptr))
+}
+
+// MkFPLT creates a floating-point less-than.
+func (c *Context) MkFPLT(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_lt(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPGT creates a floating-point greater-than.
+func (c *Context) MkFPGT(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_gt(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPLE creates a floating-point less-than-or-equal.
+func (c *Context) MkFPLE(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_leq(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPGE creates a floating-point greater-than-or-equal.
+func (c *Context) MkFPGE(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_geq(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPEq creates a floating-point equality.
+func (c *Context) MkFPEq(lhs, rhs *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_eq(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkFPIsNaN creates a predicate checking if a floating-point number is NaN.
+func (c *Context) MkFPIsNaN(expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_is_nan(c.ptr, expr.ptr))
+}
+
+// MkFPIsInf creates a predicate checking if a floating-point number is infinite.
+func (c *Context) MkFPIsInf(expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_is_infinite(c.ptr, expr.ptr))
+}
+
+// MkFPIsZero creates a predicate checking if a floating-point number is zero.
+func (c *Context) MkFPIsZero(expr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_fpa_is_zero(c.ptr, expr.ptr))
+}
diff --git a/src/api/go/go.mod b/src/api/go/go.mod
new file mode 100644
index 000000000..f3372382b
--- /dev/null
+++ b/src/api/go/go.mod
@@ -0,0 +1,6 @@
+module github.com/Z3Prover/z3/src/api/go
+
+go 1.20
+
+// This package provides Go bindings for the Z3 theorem prover.
+// It uses CGO to wrap the Z3 C API.
diff --git a/src/api/go/log.go b/src/api/go/log.go
new file mode 100644
index 000000000..dc43419ae
--- /dev/null
+++ b/src/api/go/log.go
@@ -0,0 +1,67 @@
+// Copyright (c) Microsoft Corporation 2025
+// Z3 Go API: Logging functionality
+
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"sync"
+	"unsafe"
+)
+
+var (
+	logMutex  sync.Mutex
+	isLogOpen bool
+)
+
+// OpenLog opens an interaction log file
+// Returns true if successful, false otherwise
+func OpenLog(filename string) bool {
+	logMutex.Lock()
+	defer logMutex.Unlock()
+	
+	cFilename := C.CString(filename)
+	defer C.free(unsafe.Pointer(cFilename))
+	
+	result := C.Z3_open_log(cFilename)
+	if result != 0 {
+		isLogOpen = true
+		return true
+	}
+	return false
+}
+
+// CloseLog closes the interaction log
+func CloseLog() {
+	logMutex.Lock()
+	defer logMutex.Unlock()
+	
+	C.Z3_close_log()
+	isLogOpen = false
+}
+
+// AppendLog appends a user-provided string to the interaction log
+// Panics if the log is not open
+func AppendLog(s string) {
+	logMutex.Lock()
+	defer logMutex.Unlock()
+	
+	if !isLogOpen {
+		panic("Log is not open")
+	}
+	
+	cStr := C.CString(s)
+	defer C.free(unsafe.Pointer(cStr))
+	C.Z3_append_log(cStr)
+}
+
+// IsLogOpen returns true if the interaction log is open
+func IsLogOpen() bool {
+	logMutex.Lock()
+	defer logMutex.Unlock()
+	return isLogOpen
+}
diff --git a/src/api/go/optimize.go b/src/api/go/optimize.go
new file mode 100644
index 000000000..bc6940a22
--- /dev/null
+++ b/src/api/go/optimize.go
@@ -0,0 +1,218 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"runtime"
+	"unsafe"
+)
+
+// Optimize represents a Z3 optimization context for solving optimization problems.
+// Unlike Solver which only checks satisfiability, Optimize can find optimal solutions
+// with respect to objective functions.
+type Optimize struct {
+	ctx *Context
+	ptr C.Z3_optimize
+}
+
+// NewOptimize creates a new optimization context.
+func (c *Context) NewOptimize() *Optimize {
+	opt := &Optimize{
+		ctx: c,
+		ptr: C.Z3_mk_optimize(c.ptr),
+	}
+	C.Z3_optimize_inc_ref(c.ptr, opt.ptr)
+	runtime.SetFinalizer(opt, func(o *Optimize) {
+		C.Z3_optimize_dec_ref(o.ctx.ptr, o.ptr)
+	})
+	return opt
+}
+
+// String returns the string representation of the optimize context.
+func (o *Optimize) String() string {
+	return C.GoString(C.Z3_optimize_to_string(o.ctx.ptr, o.ptr))
+}
+
+// Assert adds a constraint to the optimizer.
+func (o *Optimize) Assert(constraint *Expr) {
+	C.Z3_optimize_assert(o.ctx.ptr, o.ptr, constraint.ptr)
+}
+
+// AssertAndTrack adds a constraint with a tracking literal for unsat core extraction.
+func (o *Optimize) AssertAndTrack(constraint, track *Expr) {
+	C.Z3_optimize_assert_and_track(o.ctx.ptr, o.ptr, constraint.ptr, track.ptr)
+}
+
+// AssertSoft adds a soft constraint with a weight.
+// Soft constraints are used for MaxSMT problems.
+// Returns a handle to the objective.
+func (o *Optimize) AssertSoft(constraint *Expr, weight string, group string) uint {
+	cWeight := C.CString(weight)
+	cGroup := C.CString(group)
+	defer C.free(unsafe.Pointer(cWeight))
+	defer C.free(unsafe.Pointer(cGroup))
+	
+	sym := o.ctx.MkStringSymbol(group)
+	return uint(C.Z3_optimize_assert_soft(o.ctx.ptr, o.ptr, constraint.ptr, cWeight, sym.ptr))
+}
+
+// Maximize adds a maximization objective.
+// Returns a handle to the objective that can be used to retrieve bounds.
+func (o *Optimize) Maximize(expr *Expr) uint {
+	return uint(C.Z3_optimize_maximize(o.ctx.ptr, o.ptr, expr.ptr))
+}
+
+// Minimize adds a minimization objective.
+// Returns a handle to the objective that can be used to retrieve bounds.
+func (o *Optimize) Minimize(expr *Expr) uint {
+	return uint(C.Z3_optimize_minimize(o.ctx.ptr, o.ptr, expr.ptr))
+}
+
+// Check checks the satisfiability of the constraints and optimizes objectives.
+func (o *Optimize) Check(assumptions ...*Expr) Status {
+	var result C.Z3_lbool
+	if len(assumptions) == 0 {
+		result = C.Z3_optimize_check(o.ctx.ptr, o.ptr, 0, nil)
+	} else {
+		cAssumptions := make([]C.Z3_ast, len(assumptions))
+		for i, a := range assumptions {
+			cAssumptions[i] = a.ptr
+		}
+		result = C.Z3_optimize_check(o.ctx.ptr, o.ptr, C.uint(len(assumptions)), &cAssumptions[0])
+	}
+	return Status(result)
+}
+
+// Model returns the model if the constraints are satisfiable.
+func (o *Optimize) Model() *Model {
+	modelPtr := C.Z3_optimize_get_model(o.ctx.ptr, o.ptr)
+	if modelPtr == nil {
+		return nil
+	}
+	return newModel(o.ctx, modelPtr)
+}
+
+// Push creates a backtracking point.
+func (o *Optimize) Push() {
+	C.Z3_optimize_push(o.ctx.ptr, o.ptr)
+}
+
+// Pop removes a backtracking point.
+func (o *Optimize) Pop() {
+	C.Z3_optimize_pop(o.ctx.ptr, o.ptr)
+}
+
+// GetLower retrieves a lower bound for the objective at the given index.
+func (o *Optimize) GetLower(index uint) *Expr {
+	result := C.Z3_optimize_get_lower(o.ctx.ptr, o.ptr, C.uint(index))
+	if result == nil {
+		return nil
+	}
+	return newExpr(o.ctx, result)
+}
+
+// GetUpper retrieves an upper bound for the objective at the given index.
+func (o *Optimize) GetUpper(index uint) *Expr {
+	result := C.Z3_optimize_get_upper(o.ctx.ptr, o.ptr, C.uint(index))
+	if result == nil {
+		return nil
+	}
+	return newExpr(o.ctx, result)
+}
+
+// GetLowerAsVector retrieves a lower bound as a vector (inf, value, eps).
+// The objective value is unbounded if inf is non-zero,
+// otherwise it's represented as value + eps * EPSILON.
+func (o *Optimize) GetLowerAsVector(index uint) []*Expr {
+	vec := C.Z3_optimize_get_lower_as_vector(o.ctx.ptr, o.ptr, C.uint(index))
+	size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec))
+	if size != 3 {
+		return nil
+	}
+	return []*Expr{
+		newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 0)),
+		newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 1)),
+		newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 2)),
+	}
+}
+
+// GetUpperAsVector retrieves an upper bound as a vector (inf, value, eps).
+// The objective value is unbounded if inf is non-zero,
+// otherwise it's represented as value + eps * EPSILON.
+func (o *Optimize) GetUpperAsVector(index uint) []*Expr {
+	vec := C.Z3_optimize_get_upper_as_vector(o.ctx.ptr, o.ptr, C.uint(index))
+	size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec))
+	if size != 3 {
+		return nil
+	}
+	return []*Expr{
+		newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 0)),
+		newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 1)),
+		newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, 2)),
+	}
+}
+
+// ReasonUnknown returns the reason why the result is unknown.
+func (o *Optimize) ReasonUnknown() string {
+	return C.GoString(C.Z3_optimize_get_reason_unknown(o.ctx.ptr, o.ptr))
+}
+
+// GetHelp returns help information for the optimizer.
+func (o *Optimize) GetHelp() string {
+	return C.GoString(C.Z3_optimize_get_help(o.ctx.ptr, o.ptr))
+}
+
+// SetParams sets parameters for the optimizer.
+func (o *Optimize) SetParams(params *Params) {
+	C.Z3_optimize_set_params(o.ctx.ptr, o.ptr, params.ptr)
+}
+
+// Assertions returns the assertions in the optimizer.
+func (o *Optimize) Assertions() []*Expr {
+	vec := C.Z3_optimize_get_assertions(o.ctx.ptr, o.ptr)
+	size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec))
+	result := make([]*Expr, size)
+	for i := uint(0); i < size; i++ {
+		result[i] = newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, C.uint(i)))
+	}
+	return result
+}
+
+// Objectives returns the objectives in the optimizer.
+func (o *Optimize) Objectives() []*Expr {
+	vec := C.Z3_optimize_get_objectives(o.ctx.ptr, o.ptr)
+	size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec))
+	result := make([]*Expr, size)
+	for i := uint(0); i < size; i++ {
+		result[i] = newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, C.uint(i)))
+	}
+	return result
+}
+
+// UnsatCore returns the unsat core if the constraints are unsatisfiable.
+func (o *Optimize) UnsatCore() []*Expr {
+	vec := C.Z3_optimize_get_unsat_core(o.ctx.ptr, o.ptr)
+	size := uint(C.Z3_ast_vector_size(o.ctx.ptr, vec))
+	result := make([]*Expr, size)
+	for i := uint(0); i < size; i++ {
+		result[i] = newExpr(o.ctx, C.Z3_ast_vector_get(o.ctx.ptr, vec, C.uint(i)))
+	}
+	return result
+}
+
+// FromFile parses an SMT-LIB2 file with optimization objectives and constraints.
+func (o *Optimize) FromFile(filename string) {
+	cFilename := C.CString(filename)
+	defer C.free(unsafe.Pointer(cFilename))
+	C.Z3_optimize_from_file(o.ctx.ptr, o.ptr, cFilename)
+}
+
+// FromString parses an SMT-LIB2 string with optimization objectives and constraints.
+func (o *Optimize) FromString(s string) {
+	cStr := C.CString(s)
+	defer C.free(unsafe.Pointer(cStr))
+	C.Z3_optimize_from_string(o.ctx.ptr, o.ptr, cStr)
+}
diff --git a/src/api/go/seq.go b/src/api/go/seq.go
new file mode 100644
index 000000000..3da8a716a
--- /dev/null
+++ b/src/api/go/seq.go
@@ -0,0 +1,232 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"unsafe"
+)
+
+// Sequence and string operations
+
+// MkSeqSort creates a sequence sort.
+func (c *Context) MkSeqSort(elemSort *Sort) *Sort {
+	return newSort(c, C.Z3_mk_seq_sort(c.ptr, elemSort.ptr))
+}
+
+// MkStringSort creates a string sort (sequence of characters).
+func (c *Context) MkStringSort() *Sort {
+	return newSort(c, C.Z3_mk_string_sort(c.ptr))
+}
+
+// MkString creates a string constant.
+func (c *Context) MkString(value string) *Expr {
+	cStr := C.CString(value)
+	defer C.free(unsafe.Pointer(cStr))
+	return newExpr(c, C.Z3_mk_string(c.ptr, cStr))
+}
+
+// MkEmptySeq creates an empty sequence.
+func (c *Context) MkEmptySeq(sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_seq_empty(c.ptr, sort.ptr))
+}
+
+// MkSeqUnit creates a unit sequence containing a single element.
+func (c *Context) MkSeqUnit(elem *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_unit(c.ptr, elem.ptr))
+}
+
+// MkSeqConcat creates a sequence concatenation.
+func (c *Context) MkSeqConcat(exprs ...*Expr) *Expr {
+	if len(exprs) == 0 {
+		return nil
+	}
+	if len(exprs) == 1 {
+		return exprs[0]
+	}
+	cExprs := make([]C.Z3_ast, len(exprs))
+	for i, e := range exprs {
+		cExprs[i] = e.ptr
+	}
+	return newExpr(c, C.Z3_mk_seq_concat(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+// MkSeqLength creates a sequence length operation.
+func (c *Context) MkSeqLength(seq *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_length(c.ptr, seq.ptr))
+}
+
+// MkSeqPrefix creates a sequence prefix predicate.
+func (c *Context) MkSeqPrefix(prefix, seq *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_prefix(c.ptr, prefix.ptr, seq.ptr))
+}
+
+// MkSeqSuffix creates a sequence suffix predicate.
+func (c *Context) MkSeqSuffix(suffix, seq *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_suffix(c.ptr, suffix.ptr, seq.ptr))
+}
+
+// MkSeqContains creates a sequence contains predicate.
+func (c *Context) MkSeqContains(seq, substr *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_contains(c.ptr, seq.ptr, substr.ptr))
+}
+
+// MkSeqAt creates a sequence element access operation.
+func (c *Context) MkSeqAt(seq, index *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_at(c.ptr, seq.ptr, index.ptr))
+}
+
+// MkSeqExtract creates a sequence extract (substring) operation.
+func (c *Context) MkSeqExtract(seq, offset, length *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_extract(c.ptr, seq.ptr, offset.ptr, length.ptr))
+}
+
+// MkSeqReplace creates a sequence replace operation.
+func (c *Context) MkSeqReplace(seq, src, dst *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_replace(c.ptr, seq.ptr, src.ptr, dst.ptr))
+}
+
+// MkSeqIndexOf creates a sequence index-of operation.
+func (c *Context) MkSeqIndexOf(seq, substr, offset *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_index(c.ptr, seq.ptr, substr.ptr, offset.ptr))
+}
+
+// MkStrToInt creates a string-to-integer conversion.
+func (c *Context) MkStrToInt(str *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_str_to_int(c.ptr, str.ptr))
+}
+
+// MkIntToStr creates an integer-to-string conversion.
+func (c *Context) MkIntToStr(num *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_int_to_str(c.ptr, num.ptr))
+}
+
+// Regular expression operations
+
+// MkReSort creates a regular expression sort.
+func (c *Context) MkReSort(seqSort *Sort) *Sort {
+	return newSort(c, C.Z3_mk_re_sort(c.ptr, seqSort.ptr))
+}
+
+// MkToRe converts a sequence to a regular expression that accepts exactly that sequence.
+func (c *Context) MkToRe(seq *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_to_re(c.ptr, seq.ptr))
+}
+
+// MkInRe creates a membership predicate for a sequence in a regular expression.
+func (c *Context) MkInRe(seq, re *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_in_re(c.ptr, seq.ptr, re.ptr))
+}
+
+// MkReStar creates a Kleene star (zero or more repetitions) of a regular expression.
+func (c *Context) MkReStar(re *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_re_star(c.ptr, re.ptr))
+}
+
+// MkRePlus creates a Kleene plus (one or more repetitions) of a regular expression.
+func (c *Context) MkRePlus(re *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_re_plus(c.ptr, re.ptr))
+}
+
+// MkReOption creates an optional regular expression (zero or one repetition).
+func (c *Context) MkReOption(re *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_re_option(c.ptr, re.ptr))
+}
+
+// MkRePower creates a regular expression that matches exactly n repetitions.
+func (c *Context) MkRePower(re *Expr, n uint) *Expr {
+	return newExpr(c, C.Z3_mk_re_power(c.ptr, re.ptr, C.uint(n)))
+}
+
+// MkReLoop creates a regular expression with bounded repetition (between lo and hi times).
+// If hi is 0, it means unbounded (at least lo times).
+func (c *Context) MkReLoop(re *Expr, lo, hi uint) *Expr {
+	return newExpr(c, C.Z3_mk_re_loop(c.ptr, re.ptr, C.uint(lo), C.uint(hi)))
+}
+
+// MkReConcat creates a concatenation of regular expressions.
+func (c *Context) MkReConcat(regexes ...*Expr) *Expr {
+	if len(regexes) == 0 {
+		return nil
+	}
+	if len(regexes) == 1 {
+		return regexes[0]
+	}
+	cRegexes := make([]C.Z3_ast, len(regexes))
+	for i, re := range regexes {
+		cRegexes[i] = re.ptr
+	}
+	return newExpr(c, C.Z3_mk_re_concat(c.ptr, C.uint(len(regexes)), &cRegexes[0]))
+}
+
+// MkReUnion creates a union (alternation) of regular expressions.
+func (c *Context) MkReUnion(regexes ...*Expr) *Expr {
+	if len(regexes) == 0 {
+		return nil
+	}
+	if len(regexes) == 1 {
+		return regexes[0]
+	}
+	cRegexes := make([]C.Z3_ast, len(regexes))
+	for i, re := range regexes {
+		cRegexes[i] = re.ptr
+	}
+	return newExpr(c, C.Z3_mk_re_union(c.ptr, C.uint(len(regexes)), &cRegexes[0]))
+}
+
+// MkReIntersect creates an intersection of regular expressions.
+func (c *Context) MkReIntersect(regexes ...*Expr) *Expr {
+	if len(regexes) == 0 {
+		return nil
+	}
+	if len(regexes) == 1 {
+		return regexes[0]
+	}
+	cRegexes := make([]C.Z3_ast, len(regexes))
+	for i, re := range regexes {
+		cRegexes[i] = re.ptr
+	}
+	return newExpr(c, C.Z3_mk_re_intersect(c.ptr, C.uint(len(regexes)), &cRegexes[0]))
+}
+
+// MkReComplement creates the complement of a regular expression.
+func (c *Context) MkReComplement(re *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_re_complement(c.ptr, re.ptr))
+}
+
+// MkReDiff creates the difference of two regular expressions (a - b).
+func (c *Context) MkReDiff(a, b *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_re_diff(c.ptr, a.ptr, b.ptr))
+}
+
+// MkReEmpty creates an empty regular expression (accepts no strings).
+func (c *Context) MkReEmpty(sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_re_empty(c.ptr, sort.ptr))
+}
+
+// MkReFull creates a full regular expression (accepts all strings).
+func (c *Context) MkReFull(sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_re_full(c.ptr, sort.ptr))
+}
+
+// MkReAllchar creates a regular expression that accepts all single characters.
+func (c *Context) MkReAllchar(sort *Sort) *Expr {
+	return newExpr(c, C.Z3_mk_re_allchar(c.ptr, sort.ptr))
+}
+
+// MkReRange creates a regular expression for a character range [lo, hi].
+func (c *Context) MkReRange(lo, hi *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_re_range(c.ptr, lo.ptr, hi.ptr))
+}
+
+// MkSeqReplaceRe replaces the first occurrence matching a regular expression.
+func (c *Context) MkSeqReplaceRe(seq, re, replacement *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_replace_re(c.ptr, seq.ptr, re.ptr, replacement.ptr))
+}
+
+// MkSeqReplaceReAll replaces all occurrences matching a regular expression.
+func (c *Context) MkSeqReplaceReAll(seq, re, replacement *Expr) *Expr {
+	return newExpr(c, C.Z3_mk_seq_replace_re_all(c.ptr, seq.ptr, re.ptr, replacement.ptr))
+}
diff --git a/src/api/go/solver.go b/src/api/go/solver.go
new file mode 100644
index 000000000..3dec5cc70
--- /dev/null
+++ b/src/api/go/solver.go
@@ -0,0 +1,263 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"runtime"
+	"unsafe"
+)
+
+// Status represents the result of a satisfiability check.
+type Status int
+
+const (
+	// Unsatisfiable means the constraints are unsatisfiable.
+	Unsatisfiable Status = -1
+	// Unknown means Z3 could not determine satisfiability.
+	Unknown Status = 0
+	// Satisfiable means the constraints are satisfiable.
+	Satisfiable Status = 1
+)
+
+// String returns the string representation of the status.
+func (s Status) String() string {
+	switch s {
+	case Unsatisfiable:
+		return "unsat"
+	case Unknown:
+		return "unknown"
+	case Satisfiable:
+		return "sat"
+	default:
+		return "unknown"
+	}
+}
+
+// Solver represents a Z3 solver.
+type Solver struct {
+	ctx *Context
+	ptr C.Z3_solver
+}
+
+// NewSolver creates a new solver for the given context.
+func (c *Context) NewSolver() *Solver {
+	s := &Solver{
+		ctx: c,
+		ptr: C.Z3_mk_solver(c.ptr),
+	}
+	C.Z3_solver_inc_ref(c.ptr, s.ptr)
+	runtime.SetFinalizer(s, func(solver *Solver) {
+		C.Z3_solver_dec_ref(solver.ctx.ptr, solver.ptr)
+	})
+	return s
+}
+
+// NewSolverForLogic creates a solver for a specific logic.
+func (c *Context) NewSolverForLogic(logic string) *Solver {
+	sym := c.MkStringSymbol(logic)
+	s := &Solver{
+		ctx: c,
+		ptr: C.Z3_mk_solver_for_logic(c.ptr, sym.ptr),
+	}
+	C.Z3_solver_inc_ref(c.ptr, s.ptr)
+	runtime.SetFinalizer(s, func(solver *Solver) {
+		C.Z3_solver_dec_ref(solver.ctx.ptr, solver.ptr)
+	})
+	return s
+}
+
+// String returns the string representation of the solver.
+func (s *Solver) String() string {
+	return C.GoString(C.Z3_solver_to_string(s.ctx.ptr, s.ptr))
+}
+
+// Assert adds a constraint to the solver.
+func (s *Solver) Assert(constraint *Expr) {
+	C.Z3_solver_assert(s.ctx.ptr, s.ptr, constraint.ptr)
+}
+
+// AssertAndTrack adds a constraint with a tracking literal.
+func (s *Solver) AssertAndTrack(constraint, track *Expr) {
+	C.Z3_solver_assert_and_track(s.ctx.ptr, s.ptr, constraint.ptr, track.ptr)
+}
+
+// Check checks the satisfiability of the constraints.
+func (s *Solver) Check() Status {
+	result := C.Z3_solver_check(s.ctx.ptr, s.ptr)
+	return Status(result)
+}
+
+// CheckAssumptions checks satisfiability under assumptions.
+func (s *Solver) CheckAssumptions(assumptions ...*Expr) Status {
+	if len(assumptions) == 0 {
+		return s.Check()
+	}
+	cAssumptions := make([]C.Z3_ast, len(assumptions))
+	for i, a := range assumptions {
+		cAssumptions[i] = a.ptr
+	}
+	result := C.Z3_solver_check_assumptions(s.ctx.ptr, s.ptr, C.uint(len(assumptions)), &cAssumptions[0])
+	return Status(result)
+}
+
+// Model returns the model if the constraints are satisfiable.
+func (s *Solver) Model() *Model {
+	modelPtr := C.Z3_solver_get_model(s.ctx.ptr, s.ptr)
+	if modelPtr == nil {
+		return nil
+	}
+	return newModel(s.ctx, modelPtr)
+}
+
+// Push creates a backtracking point.
+func (s *Solver) Push() {
+	C.Z3_solver_push(s.ctx.ptr, s.ptr)
+}
+
+// Pop removes backtracking points.
+func (s *Solver) Pop(n uint) {
+	C.Z3_solver_pop(s.ctx.ptr, s.ptr, C.uint(n))
+}
+
+// Reset removes all assertions from the solver.
+func (s *Solver) Reset() {
+	C.Z3_solver_reset(s.ctx.ptr, s.ptr)
+}
+
+// NumScopes returns the number of backtracking points.
+func (s *Solver) NumScopes() uint {
+	return uint(C.Z3_solver_get_num_scopes(s.ctx.ptr, s.ptr))
+}
+
+// Assertions returns the assertions in the solver.
+func (s *Solver) Assertions() []*Expr {
+	vec := C.Z3_solver_get_assertions(s.ctx.ptr, s.ptr)
+	size := uint(C.Z3_ast_vector_size(s.ctx.ptr, vec))
+	result := make([]*Expr, size)
+	for i := uint(0); i < size; i++ {
+		result[i] = newExpr(s.ctx, C.Z3_ast_vector_get(s.ctx.ptr, vec, C.uint(i)))
+	}
+	return result
+}
+
+// UnsatCore returns the unsat core if the constraints are unsatisfiable.
+func (s *Solver) UnsatCore() []*Expr {
+	vec := C.Z3_solver_get_unsat_core(s.ctx.ptr, s.ptr)
+	size := uint(C.Z3_ast_vector_size(s.ctx.ptr, vec))
+	result := make([]*Expr, size)
+	for i := uint(0); i < size; i++ {
+		result[i] = newExpr(s.ctx, C.Z3_ast_vector_get(s.ctx.ptr, vec, C.uint(i)))
+	}
+	return result
+}
+
+// ReasonUnknown returns the reason why the result is unknown.
+func (s *Solver) ReasonUnknown() string {
+	return C.GoString(C.Z3_solver_get_reason_unknown(s.ctx.ptr, s.ptr))
+}
+
+// Model represents a Z3 model (satisfying assignment).
+type Model struct {
+	ctx *Context
+	ptr C.Z3_model
+}
+
+// newModel creates a new Model and manages its reference count.
+func newModel(ctx *Context, ptr C.Z3_model) *Model {
+	m := &Model{ctx: ctx, ptr: ptr}
+	C.Z3_model_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(m, func(model *Model) {
+		C.Z3_model_dec_ref(model.ctx.ptr, model.ptr)
+	})
+	return m
+}
+
+// String returns the string representation of the model.
+func (m *Model) String() string {
+	return C.GoString(C.Z3_model_to_string(m.ctx.ptr, m.ptr))
+}
+
+// NumConsts returns the number of constants in the model.
+func (m *Model) NumConsts() uint {
+	return uint(C.Z3_model_get_num_consts(m.ctx.ptr, m.ptr))
+}
+
+// NumFuncs returns the number of function interpretations in the model.
+func (m *Model) NumFuncs() uint {
+	return uint(C.Z3_model_get_num_funcs(m.ctx.ptr, m.ptr))
+}
+
+// GetConstDecl returns the i-th constant declaration in the model.
+func (m *Model) GetConstDecl(i uint) *FuncDecl {
+	return newFuncDecl(m.ctx, C.Z3_model_get_const_decl(m.ctx.ptr, m.ptr, C.uint(i)))
+}
+
+// GetFuncDecl returns the i-th function declaration in the model.
+func (m *Model) GetFuncDecl(i uint) *FuncDecl {
+	return newFuncDecl(m.ctx, C.Z3_model_get_func_decl(m.ctx.ptr, m.ptr, C.uint(i)))
+}
+
+// Eval evaluates an expression in the model.
+// If modelCompletion is true, Z3 will assign an interpretation for uninterpreted constants.
+func (m *Model) Eval(expr *Expr, modelCompletion bool) (*Expr, bool) {
+	var result C.Z3_ast
+	var completion C.bool
+	if modelCompletion {
+		completion = C.bool(true)
+	} else {
+		completion = C.bool(false)
+	}
+	success := C.Z3_model_eval(m.ctx.ptr, m.ptr, expr.ptr, completion, &result)
+	if success == C.bool(false) {
+		return nil, false
+	}
+	return newExpr(m.ctx, result), true
+}
+
+// GetConstInterp returns the interpretation of a constant.
+func (m *Model) GetConstInterp(decl *FuncDecl) *Expr {
+	result := C.Z3_model_get_const_interp(m.ctx.ptr, m.ptr, decl.ptr)
+	if result == nil {
+		return nil
+	}
+	return newExpr(m.ctx, result)
+}
+
+// FuncInterp represents a function interpretation in a model.
+type FuncInterp struct {
+	ctx *Context
+	ptr C.Z3_func_interp
+}
+
+// GetFuncInterp returns the interpretation of a function.
+func (m *Model) GetFuncInterp(decl *FuncDecl) *FuncInterp {
+	result := C.Z3_model_get_func_interp(m.ctx.ptr, m.ptr, decl.ptr)
+	if result == nil {
+		return nil
+	}
+	fi := &FuncInterp{ctx: m.ctx, ptr: result}
+	C.Z3_func_interp_inc_ref(m.ctx.ptr, result)
+	runtime.SetFinalizer(fi, func(f *FuncInterp) {
+		C.Z3_func_interp_dec_ref(f.ctx.ptr, f.ptr)
+	})
+	return fi
+}
+
+// NumEntries returns the number of entries in the function interpretation.
+func (fi *FuncInterp) NumEntries() uint {
+	return uint(C.Z3_func_interp_get_num_entries(fi.ctx.ptr, fi.ptr))
+}
+
+// GetElse returns the else value of the function interpretation.
+func (fi *FuncInterp) GetElse() *Expr {
+	result := C.Z3_func_interp_get_else(fi.ctx.ptr, fi.ptr)
+	return newExpr(fi.ctx, result)
+}
+
+// GetArity returns the arity of the function interpretation.
+func (fi *FuncInterp) GetArity() uint {
+	return uint(C.Z3_func_interp_get_arity(fi.ctx.ptr, fi.ptr))
+}
diff --git a/src/api/go/tactic.go b/src/api/go/tactic.go
new file mode 100644
index 000000000..167850146
--- /dev/null
+++ b/src/api/go/tactic.go
@@ -0,0 +1,294 @@
+package z3
+
+/*
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+	"runtime"
+	"unsafe"
+)
+
+// Tactic represents a Z3 tactic for transforming goals.
+type Tactic struct {
+	ctx *Context
+	ptr C.Z3_tactic
+}
+
+// newTactic creates a new Tactic and manages its reference count.
+func newTactic(ctx *Context, ptr C.Z3_tactic) *Tactic {
+	t := &Tactic{ctx: ctx, ptr: ptr}
+	C.Z3_tactic_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(t, func(tactic *Tactic) {
+		C.Z3_tactic_dec_ref(tactic.ctx.ptr, tactic.ptr)
+	})
+	return t
+}
+
+// MkTactic creates a tactic with the given name.
+func (c *Context) MkTactic(name string) *Tactic {
+	cName := C.CString(name)
+	defer C.free(unsafe.Pointer(cName))
+	return newTactic(c, C.Z3_mk_tactic(c.ptr, cName))
+}
+
+// Apply applies the tactic to a goal.
+func (t *Tactic) Apply(g *Goal) *ApplyResult {
+	return newApplyResult(t.ctx, C.Z3_tactic_apply(t.ctx.ptr, t.ptr, g.ptr))
+}
+
+// GetHelp returns help information for the tactic.
+func (t *Tactic) GetHelp() string {
+	return C.GoString(C.Z3_tactic_get_help(t.ctx.ptr, t.ptr))
+}
+
+// AndThen creates a tactic that applies t1 and then t2.
+func (t *Tactic) AndThen(t2 *Tactic) *Tactic {
+	return newTactic(t.ctx, C.Z3_tactic_and_then(t.ctx.ptr, t.ptr, t2.ptr))
+}
+
+// OrElse creates a tactic that applies t1, and if it fails, applies t2.
+func (t *Tactic) OrElse(t2 *Tactic) *Tactic {
+	return newTactic(t.ctx, C.Z3_tactic_or_else(t.ctx.ptr, t.ptr, t2.ptr))
+}
+
+// Repeat creates a tactic that applies t repeatedly (at most max times).
+func (t *Tactic) Repeat(max uint) *Tactic {
+	return newTactic(t.ctx, C.Z3_tactic_repeat(t.ctx.ptr, t.ptr, C.uint(max)))
+}
+
+// When creates a conditional tactic that applies t only if probe p evaluates to true.
+func (c *Context) TacticWhen(p *Probe, t *Tactic) *Tactic {
+	return newTactic(c, C.Z3_tactic_when(c.ptr, p.ptr, t.ptr))
+}
+
+// TacticCond creates a conditional tactic: if p then t1 else t2.
+func (c *Context) TacticCond(p *Probe, t1, t2 *Tactic) *Tactic {
+	return newTactic(c, C.Z3_tactic_cond(c.ptr, p.ptr, t1.ptr, t2.ptr))
+}
+
+// TacticFail creates a tactic that always fails.
+func (c *Context) TacticFail() *Tactic {
+	return newTactic(c, C.Z3_tactic_fail(c.ptr))
+}
+
+// TacticSkip creates a tactic that always succeeds.
+func (c *Context) TacticSkip() *Tactic {
+	return newTactic(c, C.Z3_tactic_skip(c.ptr))
+}
+
+// Goal represents a set of formulas that can be solved or transformed.
+type Goal struct {
+	ctx *Context
+	ptr C.Z3_goal
+}
+
+// newGoal creates a new Goal and manages its reference count.
+func newGoal(ctx *Context, ptr C.Z3_goal) *Goal {
+	g := &Goal{ctx: ctx, ptr: ptr}
+	C.Z3_goal_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(g, func(goal *Goal) {
+		C.Z3_goal_dec_ref(goal.ctx.ptr, goal.ptr)
+	})
+	return g
+}
+
+// MkGoal creates a new goal.
+func (c *Context) MkGoal(models, unsatCores, proofs bool) *Goal {
+	return newGoal(c, C.Z3_mk_goal(c.ptr, C.bool(models), C.bool(unsatCores), C.bool(proofs)))
+}
+
+// Assert adds a constraint to the goal.
+func (g *Goal) Assert(constraint *Expr) {
+	C.Z3_goal_assert(g.ctx.ptr, g.ptr, constraint.ptr)
+}
+
+// Size returns the number of formulas in the goal.
+func (g *Goal) Size() uint {
+	return uint(C.Z3_goal_size(g.ctx.ptr, g.ptr))
+}
+
+// Formula returns the i-th formula in the goal.
+func (g *Goal) Formula(i uint) *Expr {
+	return newExpr(g.ctx, C.Z3_goal_formula(g.ctx.ptr, g.ptr, C.uint(i)))
+}
+
+// NumExprs returns the number of expressions in the goal.
+func (g *Goal) NumExprs() uint {
+	return uint(C.Z3_goal_num_exprs(g.ctx.ptr, g.ptr))
+}
+
+// IsDecidedSat returns true if the goal is decided to be satisfiable.
+func (g *Goal) IsDecidedSat() bool {
+	return bool(C.Z3_goal_is_decided_sat(g.ctx.ptr, g.ptr))
+}
+
+// IsDecidedUnsat returns true if the goal is decided to be unsatisfiable.
+func (g *Goal) IsDecidedUnsat() bool {
+	return bool(C.Z3_goal_is_decided_unsat(g.ctx.ptr, g.ptr))
+}
+
+// Reset removes all formulas from the goal.
+func (g *Goal) Reset() {
+	C.Z3_goal_reset(g.ctx.ptr, g.ptr)
+}
+
+// String returns the string representation of the goal.
+func (g *Goal) String() string {
+	return C.GoString(C.Z3_goal_to_string(g.ctx.ptr, g.ptr))
+}
+
+// ApplyResult represents the result of applying a tactic to a goal.
+type ApplyResult struct {
+	ctx *Context
+	ptr C.Z3_apply_result
+}
+
+// newApplyResult creates a new ApplyResult and manages its reference count.
+func newApplyResult(ctx *Context, ptr C.Z3_apply_result) *ApplyResult {
+	ar := &ApplyResult{ctx: ctx, ptr: ptr}
+	C.Z3_apply_result_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(ar, func(result *ApplyResult) {
+		C.Z3_apply_result_dec_ref(result.ctx.ptr, result.ptr)
+	})
+	return ar
+}
+
+// NumSubgoals returns the number of subgoals in the result.
+func (ar *ApplyResult) NumSubgoals() uint {
+	return uint(C.Z3_apply_result_get_num_subgoals(ar.ctx.ptr, ar.ptr))
+}
+
+// Subgoal returns the i-th subgoal.
+func (ar *ApplyResult) Subgoal(i uint) *Goal {
+	return newGoal(ar.ctx, C.Z3_apply_result_get_subgoal(ar.ctx.ptr, ar.ptr, C.uint(i)))
+}
+
+// String returns the string representation of the apply result.
+func (ar *ApplyResult) String() string {
+	return C.GoString(C.Z3_apply_result_to_string(ar.ctx.ptr, ar.ptr))
+}
+
+// Probe represents a probe for checking properties of goals.
+type Probe struct {
+	ctx *Context
+	ptr C.Z3_probe
+}
+
+// newProbe creates a new Probe and manages its reference count.
+func newProbe(ctx *Context, ptr C.Z3_probe) *Probe {
+	p := &Probe{ctx: ctx, ptr: ptr}
+	C.Z3_probe_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(p, func(probe *Probe) {
+		C.Z3_probe_dec_ref(probe.ctx.ptr, probe.ptr)
+	})
+	return p
+}
+
+// MkProbe creates a probe with the given name.
+func (c *Context) MkProbe(name string) *Probe {
+	cName := C.CString(name)
+	defer C.free(unsafe.Pointer(cName))
+	return newProbe(c, C.Z3_mk_probe(c.ptr, cName))
+}
+
+// Apply evaluates the probe on a goal.
+func (p *Probe) Apply(g *Goal) float64 {
+	return float64(C.Z3_probe_apply(p.ctx.ptr, p.ptr, g.ptr))
+}
+
+// ProbeConst creates a probe that always evaluates to the given value.
+func (c *Context) ProbeConst(val float64) *Probe {
+	return newProbe(c, C.Z3_probe_const(c.ptr, C.double(val)))
+}
+
+// ProbeLt creates a probe that evaluates to true if p1 < p2.
+func (p *Probe) Lt(p2 *Probe) *Probe {
+	return newProbe(p.ctx, C.Z3_probe_lt(p.ctx.ptr, p.ptr, p2.ptr))
+}
+
+// ProbeGt creates a probe that evaluates to true if p1 > p2.
+func (p *Probe) Gt(p2 *Probe) *Probe {
+	return newProbe(p.ctx, C.Z3_probe_gt(p.ctx.ptr, p.ptr, p2.ptr))
+}
+
+// ProbeLe creates a probe that evaluates to true if p1 <= p2.
+func (p *Probe) Le(p2 *Probe) *Probe {
+	return newProbe(p.ctx, C.Z3_probe_le(p.ctx.ptr, p.ptr, p2.ptr))
+}
+
+// ProbeGe creates a probe that evaluates to true if p1 >= p2.
+func (p *Probe) Ge(p2 *Probe) *Probe {
+	return newProbe(p.ctx, C.Z3_probe_ge(p.ctx.ptr, p.ptr, p2.ptr))
+}
+
+// ProbeEq creates a probe that evaluates to true if p1 == p2.
+func (p *Probe) Eq(p2 *Probe) *Probe {
+	return newProbe(p.ctx, C.Z3_probe_eq(p.ctx.ptr, p.ptr, p2.ptr))
+}
+
+// ProbeAnd creates a probe that is the conjunction of p1 and p2.
+func (p *Probe) And(p2 *Probe) *Probe {
+	return newProbe(p.ctx, C.Z3_probe_and(p.ctx.ptr, p.ptr, p2.ptr))
+}
+
+// ProbeOr creates a probe that is the disjunction of p1 and p2.
+func (p *Probe) Or(p2 *Probe) *Probe {
+	return newProbe(p.ctx, C.Z3_probe_or(p.ctx.ptr, p.ptr, p2.ptr))
+}
+
+// ProbeNot creates a probe that is the negation of p.
+func (p *Probe) Not() *Probe {
+	return newProbe(p.ctx, C.Z3_probe_not(p.ctx.ptr, p.ptr))
+}
+
+// Params represents a parameter set.
+type Params struct {
+	ctx *Context
+	ptr C.Z3_params
+}
+
+// newParams creates a new Params and manages its reference count.
+func newParams(ctx *Context, ptr C.Z3_params) *Params {
+	params := &Params{ctx: ctx, ptr: ptr}
+	C.Z3_params_inc_ref(ctx.ptr, ptr)
+	runtime.SetFinalizer(params, func(p *Params) {
+		C.Z3_params_dec_ref(p.ctx.ptr, p.ptr)
+	})
+	return params
+}
+
+// MkParams creates a new parameter set.
+func (c *Context) MkParams() *Params {
+	return newParams(c, C.Z3_mk_params(c.ptr))
+}
+
+// SetBool sets a Boolean parameter.
+func (p *Params) SetBool(key string, value bool) {
+	sym := p.ctx.MkStringSymbol(key)
+	C.Z3_params_set_bool(p.ctx.ptr, p.ptr, sym.ptr, C.bool(value))
+}
+
+// SetUint sets an unsigned integer parameter.
+func (p *Params) SetUint(key string, value uint) {
+	sym := p.ctx.MkStringSymbol(key)
+	C.Z3_params_set_uint(p.ctx.ptr, p.ptr, sym.ptr, C.uint(value))
+}
+
+// SetDouble sets a double parameter.
+func (p *Params) SetDouble(key string, value float64) {
+	sym := p.ctx.MkStringSymbol(key)
+	C.Z3_params_set_double(p.ctx.ptr, p.ptr, sym.ptr, C.double(value))
+}
+
+// SetSymbol sets a symbol parameter.
+func (p *Params) SetSymbol(key string, value *Symbol) {
+	sym := p.ctx.MkStringSymbol(key)
+	C.Z3_params_set_symbol(p.ctx.ptr, p.ptr, sym.ptr, value.ptr)
+}
+
+// String returns the string representation of the parameters.
+func (p *Params) String() string {
+	return C.GoString(C.Z3_params_to_string(p.ctx.ptr, p.ptr))
+}
diff --git a/src/api/go/z3.go b/src/api/go/z3.go
new file mode 100644
index 000000000..810308047
--- /dev/null
+++ b/src/api/go/z3.go
@@ -0,0 +1,763 @@
+// Package z3 provides Go bindings for the Z3 theorem prover.
+//
+// Z3 is a high-performance SMT (Satisfiability Modulo Theories) solver
+// developed at Microsoft Research. These bindings wrap the Z3 C API using
+// CGO and provide idiomatic Go interfaces with automatic memory management.
+//
+// # Basic Usage
+//
+// Create a context and solver:
+//
+//	ctx := z3.NewContext()
+//	solver := ctx.NewSolver()
+//
+// Create variables and constraints:
+//
+//	x := ctx.MkIntConst("x")
+//	y := ctx.MkIntConst("y")
+//	solver.Assert(ctx.MkEq(ctx.MkAdd(x, y), ctx.MkInt(10, ctx.MkIntSort())))
+//	solver.Assert(ctx.MkGt(x, y))
+//
+// Check satisfiability and get model:
+//
+//	if solver.Check() == z3.Satisfiable {
+//	    model := solver.Model()
+//	    xVal, _ := model.Eval(x, true)
+//	    fmt.Println("x =", xVal.String())
+//	}
+//
+// # Memory Management
+//
+// All Z3 objects are automatically managed using Go finalizers. Reference
+// counting is handled transparently - you don't need to manually free objects.
+//
+// # Supported Features
+//
+//   - Boolean logic, integer and real arithmetic
+//   - Bit-vectors and floating-point arithmetic
+//   - Arrays, sequences, and strings
+//   - Regular expressions
+//   - Algebraic datatypes
+//   - Quantifiers and lambda expressions
+//   - Tactics and goal-based solving
+//   - Optimization (MaxSMT)
+//   - Fixedpoint solver (Datalog/CHC)
+//
+// For more examples, see the examples/go directory in the Z3 repository.
+package z3
+
+/*
+#cgo CFLAGS: -I${SRCDIR}/..
+#cgo LDFLAGS: -lz3
+#include "z3.h"
+#include <stdlib.h>
+*/
+import "C"
+import (
+"runtime"
+"unsafe"
+)
+
+// Config represents a Z3 configuration object.
+type Config struct {
+ptr C.Z3_config
+}
+
+// NewConfig creates a new Z3 configuration.
+func NewConfig() *Config {
+cfg := &Config{ptr: C.Z3_mk_config()}
+runtime.SetFinalizer(cfg, func(c *Config) {
+C.Z3_del_config(c.ptr)
+})
+return cfg
+}
+
+// SetParamValue sets a configuration parameter.
+func (c *Config) SetParamValue(paramID, paramValue string) {
+cParamID := C.CString(paramID)
+cParamValue := C.CString(paramValue)
+defer C.free(unsafe.Pointer(cParamID))
+defer C.free(unsafe.Pointer(cParamValue))
+C.Z3_set_param_value(c.ptr, cParamID, cParamValue)
+}
+
+// Context represents a Z3 logical context.
+type Context struct {
+ptr C.Z3_context
+}
+
+// NewContext creates a new Z3 context with default configuration.
+func NewContext() *Context {
+ctx := &Context{ptr: C.Z3_mk_context_rc(C.Z3_mk_config())}
+runtime.SetFinalizer(ctx, func(c *Context) {
+C.Z3_del_context(c.ptr)
+})
+return ctx
+}
+
+// NewContextWithConfig creates a new Z3 context with the given configuration.
+func NewContextWithConfig(cfg *Config) *Context {
+ctx := &Context{ptr: C.Z3_mk_context_rc(cfg.ptr)}
+runtime.SetFinalizer(ctx, func(c *Context) {
+C.Z3_del_context(c.ptr)
+})
+return ctx
+}
+
+// SetParam sets a global or context parameter.
+func (c *Context) SetParam(key, value string) {
+cKey := C.CString(key)
+cValue := C.CString(value)
+defer C.free(unsafe.Pointer(cKey))
+defer C.free(unsafe.Pointer(cValue))
+C.Z3_update_param_value(c.ptr, cKey, cValue)
+}
+
+// Symbol represents a Z3 symbol.
+type Symbol struct {
+ctx *Context
+ptr C.Z3_symbol
+}
+
+// MkIntSymbol creates an integer symbol.
+func (c *Context) MkIntSymbol(i int) *Symbol {
+return &Symbol{
+ctx: c,
+ptr: C.Z3_mk_int_symbol(c.ptr, C.int(i)),
+}
+}
+
+// MkStringSymbol creates a string symbol.
+func (c *Context) MkStringSymbol(s string) *Symbol {
+cStr := C.CString(s)
+defer C.free(unsafe.Pointer(cStr))
+return &Symbol{
+ctx: c,
+ptr: C.Z3_mk_string_symbol(c.ptr, cStr),
+}
+}
+
+// String returns the string representation of the symbol.
+func (s *Symbol) String() string {
+kind := C.Z3_get_symbol_kind(s.ctx.ptr, s.ptr)
+if kind == C.Z3_INT_SYMBOL {
+return string(rune(C.Z3_get_symbol_int(s.ctx.ptr, s.ptr)))
+}
+return C.GoString(C.Z3_get_symbol_string(s.ctx.ptr, s.ptr))
+}
+
+// AST represents a Z3 abstract syntax tree node.
+type AST struct {
+ctx *Context
+ptr C.Z3_ast
+}
+
+// incRef increments the reference count of the AST.
+func (a *AST) incRef() {
+C.Z3_inc_ref(a.ctx.ptr, a.ptr)
+}
+
+// decRef decrements the reference count of the AST.
+func (a *AST) decRef() {
+C.Z3_dec_ref(a.ctx.ptr, a.ptr)
+}
+
+// String returns the string representation of the AST.
+func (a *AST) String() string {
+return C.GoString(C.Z3_ast_to_string(a.ctx.ptr, a.ptr))
+}
+
+// Hash returns the hash code of the AST.
+func (a *AST) Hash() uint32 {
+return uint32(C.Z3_get_ast_hash(a.ctx.ptr, a.ptr))
+}
+
+// Equal checks if two ASTs are equal.
+func (a *AST) Equal(other *AST) bool {
+if a.ctx != other.ctx {
+return false
+}
+return bool(C.Z3_is_eq_ast(a.ctx.ptr, a.ptr, other.ptr))
+}
+
+// Sort represents a Z3 sort (type).
+type Sort struct {
+ctx *Context
+ptr C.Z3_sort
+}
+
+// newSort creates a new Sort and manages its reference count.
+func newSort(ctx *Context, ptr C.Z3_sort) *Sort {
+sort := &Sort{ctx: ctx, ptr: ptr}
+C.Z3_inc_ref(ctx.ptr, C.Z3_sort_to_ast(ctx.ptr, ptr))
+runtime.SetFinalizer(sort, func(s *Sort) {
+C.Z3_dec_ref(s.ctx.ptr, C.Z3_sort_to_ast(s.ctx.ptr, s.ptr))
+})
+return sort
+}
+
+// String returns the string representation of the sort.
+func (s *Sort) String() string {
+return C.GoString(C.Z3_sort_to_string(s.ctx.ptr, s.ptr))
+}
+
+// Equal checks if two sorts are equal.
+func (s *Sort) Equal(other *Sort) bool {
+if s.ctx != other.ctx {
+return false
+}
+return bool(C.Z3_is_eq_sort(s.ctx.ptr, s.ptr, other.ptr))
+}
+
+// MkBoolSort creates the Boolean sort.
+func (c *Context) MkBoolSort() *Sort {
+return newSort(c, C.Z3_mk_bool_sort(c.ptr))
+}
+
+// MkBvSort creates a bit-vector sort of the given size.
+func (c *Context) MkBvSort(sz uint) *Sort {
+return newSort(c, C.Z3_mk_bv_sort(c.ptr, C.uint(sz)))
+}
+
+// Expr represents a Z3 expression.
+type Expr struct {
+ctx *Context
+ptr C.Z3_ast
+}
+
+// newExpr creates a new Expr and manages its reference count.
+func newExpr(ctx *Context, ptr C.Z3_ast) *Expr {
+expr := &Expr{ctx: ctx, ptr: ptr}
+C.Z3_inc_ref(ctx.ptr, ptr)
+runtime.SetFinalizer(expr, func(e *Expr) {
+C.Z3_dec_ref(e.ctx.ptr, e.ptr)
+})
+return expr
+}
+
+// String returns the string representation of the expression.
+func (e *Expr) String() string {
+return C.GoString(C.Z3_ast_to_string(e.ctx.ptr, e.ptr))
+}
+
+// Equal checks if two expressions are equal.
+func (e *Expr) Equal(other *Expr) bool {
+if e.ctx != other.ctx {
+return false
+}
+return bool(C.Z3_is_eq_ast(e.ctx.ptr, e.ptr, other.ptr))
+}
+
+// GetSort returns the sort of the expression.
+func (e *Expr) GetSort() *Sort {
+return newSort(e.ctx, C.Z3_get_sort(e.ctx.ptr, e.ptr))
+}
+
+// MkTrue creates the Boolean constant true.
+func (c *Context) MkTrue() *Expr {
+return newExpr(c, C.Z3_mk_true(c.ptr))
+}
+
+// MkFalse creates the Boolean constant false.
+func (c *Context) MkFalse() *Expr {
+return newExpr(c, C.Z3_mk_false(c.ptr))
+}
+
+// MkBool creates a Boolean constant.
+func (c *Context) MkBool(value bool) *Expr {
+if value {
+return c.MkTrue()
+}
+return c.MkFalse()
+}
+
+// MkNumeral creates a numeral from a string.
+func (c *Context) MkNumeral(numeral string, sort *Sort) *Expr {
+cStr := C.CString(numeral)
+defer C.free(unsafe.Pointer(cStr))
+return newExpr(c, C.Z3_mk_numeral(c.ptr, cStr, sort.ptr))
+}
+
+// MkConst creates a constant (variable) with the given name and sort.
+func (c *Context) MkConst(name *Symbol, sort *Sort) *Expr {
+return newExpr(c, C.Z3_mk_const(c.ptr, name.ptr, sort.ptr))
+}
+
+// MkBoolConst creates a Boolean constant (variable) with the given name.
+func (c *Context) MkBoolConst(name string) *Expr {
+sym := c.MkStringSymbol(name)
+return c.MkConst(sym, c.MkBoolSort())
+}
+
+// Boolean operations
+
+// MkAnd creates a conjunction.
+func (c *Context) MkAnd(exprs ...*Expr) *Expr {
+if len(exprs) == 0 {
+return c.MkTrue()
+}
+if len(exprs) == 1 {
+return exprs[0]
+}
+cExprs := make([]C.Z3_ast, len(exprs))
+for i, e := range exprs {
+cExprs[i] = e.ptr
+}
+return newExpr(c, C.Z3_mk_and(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+// MkOr creates a disjunction.
+func (c *Context) MkOr(exprs ...*Expr) *Expr {
+if len(exprs) == 0 {
+return c.MkFalse()
+}
+if len(exprs) == 1 {
+return exprs[0]
+}
+cExprs := make([]C.Z3_ast, len(exprs))
+for i, e := range exprs {
+cExprs[i] = e.ptr
+}
+return newExpr(c, C.Z3_mk_or(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+// MkNot creates a negation.
+func (c *Context) MkNot(expr *Expr) *Expr {
+return newExpr(c, C.Z3_mk_not(c.ptr, expr.ptr))
+}
+
+// MkImplies creates an implication.
+func (c *Context) MkImplies(lhs, rhs *Expr) *Expr {
+return newExpr(c, C.Z3_mk_implies(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkIff creates a bi-implication (if and only if).
+func (c *Context) MkIff(lhs, rhs *Expr) *Expr {
+return newExpr(c, C.Z3_mk_iff(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkXor creates exclusive or.
+func (c *Context) MkXor(lhs, rhs *Expr) *Expr {
+return newExpr(c, C.Z3_mk_xor(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+if len(exprs) == 1 {
+return exprs[0]
+}
+cExprs := make([]C.Z3_ast, len(exprs))
+for i, e := range exprs {
+cExprs[i] = e.ptr
+}
+return newExpr(c, C.Z3_mk_add(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+if len(exprs) == 1 {
+return newExpr(c, C.Z3_mk_unary_minus(c.ptr, exprs[0].ptr))
+}
+cExprs := make([]C.Z3_ast, len(exprs))
+for i, e := range exprs {
+cExprs[i] = e.ptr
+}
+return newExpr(c, C.Z3_mk_sub(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+if len(exprs) == 1 {
+return exprs[0]
+}
+cExprs := make([]C.Z3_ast, len(exprs))
+for i, e := range exprs {
+cExprs[i] = e.ptr
+}
+return newExpr(c, C.Z3_mk_mul(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+// Comparison operations
+
+// MkEq creates an equality.
+func (c *Context) MkEq(lhs, rhs *Expr) *Expr {
+return newExpr(c, C.Z3_mk_eq(c.ptr, lhs.ptr, rhs.ptr))
+}
+
+// MkDistinct creates a distinct constraint.
+func (c *Context) MkDistinct(exprs ...*Expr) *Expr {
+if len(exprs) <= 1 {
+return c.MkTrue()
+}
+cExprs := make([]C.Z3_ast, len(exprs))
+for i, e := range exprs {
+cExprs[i] = e.ptr
+}
+return newExpr(c, C.Z3_mk_distinct(c.ptr, C.uint(len(exprs)), &cExprs[0]))
+}
+
+// FuncDecl represents a function declaration.
+type FuncDecl struct {
+ctx *Context
+ptr C.Z3_func_decl
+}
+
+// newFuncDecl creates a new FuncDecl and manages its reference count.
+func newFuncDecl(ctx *Context, ptr C.Z3_func_decl) *FuncDecl {
+fd := &FuncDecl{ctx: ctx, ptr: ptr}
+C.Z3_inc_ref(ctx.ptr, C.Z3_func_decl_to_ast(ctx.ptr, ptr))
+runtime.SetFinalizer(fd, func(f *FuncDecl) {
+C.Z3_dec_ref(f.ctx.ptr, C.Z3_func_decl_to_ast(f.ctx.ptr, f.ptr))
+})
+return fd
+}
+
+// String returns the string representation of the function declaration.
+func (f *FuncDecl) String() string {
+return C.GoString(C.Z3_func_decl_to_string(f.ctx.ptr, f.ptr))
+}
+
+// GetName returns the name of the function declaration.
+func (f *FuncDecl) GetName() *Symbol {
+return &Symbol{
+ctx: f.ctx,
+ptr: C.Z3_get_decl_name(f.ctx.ptr, f.ptr),
+}
+}
+
+// GetArity returns the arity (number of parameters) of the function.
+func (f *FuncDecl) GetArity() int {
+return int(C.Z3_get_arity(f.ctx.ptr, f.ptr))
+}
+
+// GetDomain returns the sort of the i-th parameter.
+func (f *FuncDecl) GetDomain(i int) *Sort {
+return newSort(f.ctx, C.Z3_get_domain(f.ctx.ptr, f.ptr, C.uint(i)))
+}
+
+// GetRange returns the sort of the return value.
+func (f *FuncDecl) GetRange() *Sort {
+return newSort(f.ctx, C.Z3_get_range(f.ctx.ptr, f.ptr))
+}
+
+// MkFuncDecl creates a function declaration.
+func (c *Context) MkFuncDecl(name *Symbol, domain []*Sort, range_ *Sort) *FuncDecl {
+cDomain := make([]C.Z3_sort, len(domain))
+for i, s := range domain {
+cDomain[i] = s.ptr
+}
+var domainPtr *C.Z3_sort
+if len(domain) > 0 {
+domainPtr = &cDomain[0]
+}
+return newFuncDecl(c, C.Z3_mk_func_decl(c.ptr, name.ptr, C.uint(len(domain)), domainPtr, range_.ptr))
+}
+
+// MkApp creates a function application.
+func (c *Context) MkApp(decl *FuncDecl, args ...*Expr) *Expr {
+cArgs := make([]C.Z3_ast, len(args))
+for i, a := range args {
+cArgs[i] = a.ptr
+}
+var argsPtr *C.Z3_ast
+if len(args) > 0 {
+argsPtr = &cArgs[0]
+}
+return newExpr(c, C.Z3_mk_app(c.ptr, decl.ptr, C.uint(len(args)), argsPtr))
+}
+
+// Quantifier operations
+
+// MkForall creates a universal quantifier.
+func (c *Context) MkForall(bound []*Expr, body *Expr) *Expr {
+cBound := make([]C.Z3_ast, len(bound))
+for i, b := range bound {
+cBound[i] = b.ptr
+}
+var boundPtr *C.Z3_ast
+if len(bound) > 0 {
+boundPtr = &cBound[0]
+}
+return newExpr(c, C.Z3_mk_forall_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr))
+}
+
+// MkExists creates an existential quantifier.
+func (c *Context) MkExists(bound []*Expr, body *Expr) *Expr {
+cBound := make([]C.Z3_ast, len(bound))
+for i, b := range bound {
+cBound[i] = b.ptr
+}
+var boundPtr *C.Z3_ast
+if len(bound) > 0 {
+boundPtr = &cBound[0]
+}
+return newExpr(c, C.Z3_mk_exists_const(c.ptr, 0, C.uint(len(bound)), boundPtr, 0, nil, body.ptr))
+}
+
+// Simplify simplifies an expression.
+func (e *Expr) Simplify() *Expr {
+return newExpr(e.ctx, C.Z3_simplify(e.ctx.ptr, e.ptr))
+}
+
+// MkTypeVariable creates a type variable sort for use in polymorphic functions and datatypes
+func (c *Context) MkTypeVariable(name *Symbol) *Sort {
+return newSort(c, C.Z3_mk_type_variable(c.ptr, name.ptr))
+}
+
+// Quantifier represents a quantified formula (forall or exists)
+type Quantifier struct {
+ctx *Context
+ptr C.Z3_ast
+}
+
+// newQuantifier creates a new Quantifier with proper memory management
+func newQuantifier(ctx *Context, ptr C.Z3_ast) *Quantifier {
+q := &Quantifier{ctx: ctx, ptr: ptr}
+C.Z3_inc_ref(ctx.ptr, ptr)
+runtime.SetFinalizer(q, func(qf *Quantifier) {
+C.Z3_dec_ref(qf.ctx.ptr, qf.ptr)
+})
+return q
+}
+
+// AsExpr converts a Quantifier to an Expr
+func (q *Quantifier) AsExpr() *Expr {
+return newExpr(q.ctx, q.ptr)
+}
+
+// IsUniversal returns true if this is a universal quantifier (forall)
+func (q *Quantifier) IsUniversal() bool {
+return C.Z3_is_quantifier_forall(q.ctx.ptr, q.ptr) != 0
+}
+
+// IsExistential returns true if this is an existential quantifier (exists)
+func (q *Quantifier) IsExistential() bool {
+return C.Z3_is_quantifier_exists(q.ctx.ptr, q.ptr) != 0
+}
+
+// GetWeight returns the weight of the quantifier
+func (q *Quantifier) GetWeight() int {
+return int(C.Z3_get_quantifier_weight(q.ctx.ptr, q.ptr))
+}
+
+// GetNumPatterns returns the number of patterns
+func (q *Quantifier) GetNumPatterns() int {
+return int(C.Z3_get_quantifier_num_patterns(q.ctx.ptr, q.ptr))
+}
+
+// GetPattern returns the pattern at the given index
+func (q *Quantifier) GetPattern(idx int) *Pattern {
+ptr := C.Z3_get_quantifier_pattern_ast(q.ctx.ptr, q.ptr, C.uint(idx))
+return newPattern(q.ctx, ptr)
+}
+
+// GetNumNoPatterns returns the number of no-patterns
+func (q *Quantifier) GetNumNoPatterns() int {
+return int(C.Z3_get_quantifier_num_no_patterns(q.ctx.ptr, q.ptr))
+}
+
+// GetNoPattern returns the no-pattern at the given index
+func (q *Quantifier) GetNoPattern(idx int) *Pattern {
+ptr := C.Z3_get_quantifier_no_pattern_ast(q.ctx.ptr, q.ptr, C.uint(idx))
+return newPattern(q.ctx, ptr)
+}
+
+// GetNumBound returns the number of bound variables
+func (q *Quantifier) GetNumBound() int {
+return int(C.Z3_get_quantifier_num_bound(q.ctx.ptr, q.ptr))
+}
+
+// GetBoundName returns the name of the bound variable at the given index
+func (q *Quantifier) GetBoundName(idx int) *Symbol {
+ptr := C.Z3_get_quantifier_bound_name(q.ctx.ptr, q.ptr, C.uint(idx))
+return newSymbol(q.ctx, ptr)
+}
+
+// GetBoundSort returns the sort of the bound variable at the given index
+func (q *Quantifier) GetBoundSort(idx int) *Sort {
+ptr := C.Z3_get_quantifier_bound_sort(q.ctx.ptr, q.ptr, C.uint(idx))
+return newSort(q.ctx, ptr)
+}
+
+// GetBody returns the body of the quantifier
+func (q *Quantifier) GetBody() *Expr {
+ptr := C.Z3_get_quantifier_body(q.ctx.ptr, q.ptr)
+return newExpr(q.ctx, ptr)
+}
+
+// String returns the string representation of the quantifier
+func (q *Quantifier) String() string {
+return q.AsExpr().String()
+}
+
+// MkQuantifier creates a quantifier with patterns
+func (c *Context) MkQuantifier(isForall bool, weight int, sorts []*Sort, names []*Symbol, body *Expr, patterns []*Pattern) *Quantifier {
+var forallInt C.int
+if isForall {
+forallInt = 1
+} else {
+forallInt = 0
+}
+
+numBound := len(sorts)
+if numBound != len(names) {
+panic("Number of sorts must match number of names")
+}
+
+var cSorts []C.Z3_sort
+var cNames []C.Z3_symbol
+if numBound > 0 {
+cSorts = make([]C.Z3_sort, numBound)
+cNames = make([]C.Z3_symbol, numBound)
+for i := 0; i < numBound; i++ {
+cSorts[i] = sorts[i].ptr
+cNames[i] = names[i].ptr
+}
+}
+
+var cPatterns []C.Z3_pattern
+var patternsPtr *C.Z3_pattern
+numPatterns := len(patterns)
+if numPatterns > 0 {
+cPatterns = make([]C.Z3_pattern, numPatterns)
+for i := 0; i < numPatterns; i++ {
+cPatterns[i] = patterns[i].ptr
+}
+patternsPtr = &cPatterns[0]
+}
+
+var sortsPtr *C.Z3_sort
+var namesPtr *C.Z3_symbol
+if numBound > 0 {
+sortsPtr = &cSorts[0]
+namesPtr = &cNames[0]
+}
+
+ptr := C.Z3_mk_quantifier(c.ptr, forallInt, C.uint(weight), C.uint(numPatterns), patternsPtr,
+C.uint(numBound), sortsPtr, namesPtr, body.ptr)
+return newQuantifier(c, ptr)
+}
+
+// MkQuantifierConst creates a quantifier using constant bound variables
+func (c *Context) MkQuantifierConst(isForall bool, weight int, bound []*Expr, body *Expr, patterns []*Pattern) *Quantifier {
+var forallInt C.int
+if isForall {
+forallInt = 1
+} else {
+forallInt = 0
+}
+
+numBound := len(bound)
+var cBound []C.Z3_app
+var boundPtr *C.Z3_app
+if numBound > 0 {
+cBound = make([]C.Z3_app, numBound)
+for i := 0; i < numBound; i++ {
+cBound[i] = C.Z3_app(bound[i].ptr)
+}
+boundPtr = &cBound[0]
+}
+
+var cPatterns []C.Z3_pattern
+var patternsPtr *C.Z3_pattern
+numPatterns := len(patterns)
+if numPatterns > 0 {
+cPatterns = make([]C.Z3_pattern, numPatterns)
+for i := 0; i < numPatterns; i++ {
+cPatterns[i] = patterns[i].ptr
+}
+patternsPtr = &cPatterns[0]
+}
+
+ptr := C.Z3_mk_quantifier_const(c.ptr, forallInt, C.uint(weight), C.uint(numBound), boundPtr,
+C.uint(numPatterns), patternsPtr, body.ptr)
+return newQuantifier(c, ptr)
+}
+
+// Lambda represents a lambda expression
+type Lambda struct {
+ctx *Context
+ptr C.Z3_ast
+}
+
+// newLambda creates a new Lambda with proper memory management
+func newLambda(ctx *Context, ptr C.Z3_ast) *Lambda {
+l := &Lambda{ctx: ctx, ptr: ptr}
+C.Z3_inc_ref(ctx.ptr, ptr)
+runtime.SetFinalizer(l, func(lam *Lambda) {
+C.Z3_dec_ref(lam.ctx.ptr, lam.ptr)
+})
+return l
+}
+
+// AsExpr converts a Lambda to an Expr
+func (l *Lambda) AsExpr() *Expr {
+return newExpr(l.ctx, l.ptr)
+}
+
+// GetNumBound returns the number of bound variables
+func (l *Lambda) GetNumBound() int {
+return int(C.Z3_get_quantifier_num_bound(l.ctx.ptr, l.ptr))
+}
+
+// GetBoundName returns the name of the bound variable at the given index
+func (l *Lambda) GetBoundName(idx int) *Symbol {
+ptr := C.Z3_get_quantifier_bound_name(l.ctx.ptr, l.ptr, C.uint(idx))
+return newSymbol(l.ctx, ptr)
+}
+
+// GetBoundSort returns the sort of the bound variable at the given index
+func (l *Lambda) GetBoundSort(idx int) *Sort {
+ptr := C.Z3_get_quantifier_bound_sort(l.ctx.ptr, l.ptr, C.uint(idx))
+return newSort(l.ctx, ptr)
+}
+
+// GetBody returns the body of the lambda expression
+func (l *Lambda) GetBody() *Expr {
+ptr := C.Z3_get_quantifier_body(l.ctx.ptr, l.ptr)
+return newExpr(l.ctx, ptr)
+}
+
+// String returns the string representation of the lambda
+func (l *Lambda) String() string {
+return l.AsExpr().String()
+}
+
+// MkLambda creates a lambda expression with sorts and names
+func (c *Context) MkLambda(sorts []*Sort, names []*Symbol, body *Expr) *Lambda {
+numBound := len(sorts)
+if numBound != len(names) {
+panic("Number of sorts must match number of names")
+}
+
+var cSorts []C.Z3_sort
+var cNames []C.Z3_symbol
+var sortsPtr *C.Z3_sort
+var namesPtr *C.Z3_symbol
+
+if numBound > 0 {
+cSorts = make([]C.Z3_sort, numBound)
+cNames = make([]C.Z3_symbol, numBound)
+for i := 0; i < numBound; i++ {
+cSorts[i] = sorts[i].ptr
+cNames[i] = names[i].ptr
+}
+sortsPtr = &cSorts[0]
+namesPtr = &cNames[0]
+}
+
+ptr := C.Z3_mk_lambda(c.ptr, C.uint(numBound), sortsPtr, namesPtr, body.ptr)
+return newLambda(c, ptr)
+}
+
+// MkLambdaConst creates a lambda expression using constant bound variables
+func (c *Context) MkLambdaConst(bound []*Expr, body *Expr) *Lambda {
+numBound := len(bound)
+var cBound []C.Z3_app
+var boundPtr *C.Z3_app
+
+if numBound > 0 {
+cBound = make([]C.Z3_app, numBound)
+for i := 0; i < numBound; i++ {
+cBound[i] = C.Z3_app(bound[i].ptr)
+}
+boundPtr = &cBound[0]
+}
+
+ptr := C.Z3_mk_lambda_const(c.ptr, C.uint(numBound), boundPtr, body.ptr)
+return newLambda(c, ptr)
+}