diff --git a/.github/workflows/nightly-validation.yml b/.github/workflows/nightly-validation.yml
new file mode 100644
index 000000000..6a361c5b6
--- /dev/null
+++ b/.github/workflows/nightly-validation.yml
@@ -0,0 +1,540 @@
+name: Nightly Build Validation
+
+on:
+  workflow_run:
+    workflows: ["Nightly Build"]
+    types:
+      - completed
+  workflow_dispatch:
+    inputs:
+      release_tag:
+        description: 'Release tag to validate (default: Nightly)'
+        required: false
+        default: 'Nightly'
+
+permissions:
+  contents: read
+
+jobs:
+  # ============================================================================
+  # VALIDATION JOBS FOR NUGET PACKAGES
+  # ============================================================================
+  
+  validate-nuget-windows-x64:
+    name: "Validate NuGet on Windows x64"
+    runs-on: windows-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Setup .NET
+        uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: '8.x'
+      
+      - name: Download NuGet package from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        shell: pwsh
+        run: |
+          $tag = "${{ github.event.inputs.release_tag }}"
+          if ([string]::IsNullOrEmpty($tag)) {
+            $tag = "Nightly"
+          }
+          gh release download $tag --pattern "*.nupkg" --dir nuget-packages
+      
+      - name: Create test project
+        shell: pwsh
+        run: |
+          mkdir test-nuget
+          cd test-nuget
+          dotnet new console
+          $nupkgFile = Get-ChildItem ../nuget-packages/*.nupkg -Exclude *.symbols.nupkg | Select-Object -First 1
+          dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
+      
+      - name: Create test code
+        shell: pwsh
+        run: |
+          @"
+          using Microsoft.Z3;
+          class Program {
+              static void Main() {
+                  using (Context ctx = new Context()) {
+                      IntExpr x = ctx.MkIntConst("x");
+                      Solver solver = ctx.MkSolver();
+                      solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
+                      if (solver.Check() == Status.SATISFIABLE) {
+                          System.Console.WriteLine("sat");
+                          System.Console.WriteLine(solver.Model);
+                      }
+                  }
+              }
+          }
+          "@ | Out-File -FilePath test-nuget/Program.cs -Encoding utf8
+      
+      - name: Run test
+        shell: pwsh
+        run: |
+          cd test-nuget
+          dotnet run
+
+  validate-nuget-ubuntu-x64:
+    name: "Validate NuGet on Ubuntu x64"
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Setup .NET
+        uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: '8.x'
+      
+      - name: Download NuGet package from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
+      
+      - name: Create test project
+        run: |
+          mkdir test-nuget
+          cd test-nuget
+          dotnet new console
+          dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
+      
+      - name: Create test code
+        run: |
+          cat > test-nuget/Program.cs << 'EOF'
+          using Microsoft.Z3;
+          class Program {
+              static void Main() {
+                  using (Context ctx = new Context()) {
+                      IntExpr x = ctx.MkIntConst("x");
+                      Solver solver = ctx.MkSolver();
+                      solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
+                      if (solver.Check() == Status.SATISFIABLE) {
+                          System.Console.WriteLine("sat");
+                          System.Console.WriteLine(solver.Model);
+                      }
+                  }
+              }
+          }
+          EOF
+      
+      - name: Run test
+        run: |
+          cd test-nuget
+          dotnet run
+
+  validate-nuget-macos-x64:
+    name: "Validate NuGet on macOS x64"
+    runs-on: macos-13
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Setup .NET
+        uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: '8.x'
+      
+      - name: Download NuGet package from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
+      
+      - name: Create test project
+        run: |
+          mkdir test-nuget
+          cd test-nuget
+          dotnet new console
+          dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
+      
+      - name: Create test code
+        run: |
+          cat > test-nuget/Program.cs << 'EOF'
+          using Microsoft.Z3;
+          class Program {
+              static void Main() {
+                  using (Context ctx = new Context()) {
+                      IntExpr x = ctx.MkIntConst("x");
+                      Solver solver = ctx.MkSolver();
+                      solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
+                      if (solver.Check() == Status.SATISFIABLE) {
+                          System.Console.WriteLine("sat");
+                          System.Console.WriteLine(solver.Model);
+                      }
+                  }
+              }
+          }
+          EOF
+      
+      - name: Run test
+        run: |
+          cd test-nuget
+          dotnet run
+
+  validate-nuget-macos-arm64:
+    name: "Validate NuGet on macOS ARM64"
+    runs-on: macos-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Setup .NET
+        uses: actions/setup-dotnet@v4
+        with:
+          dotnet-version: '8.x'
+      
+      - name: Download NuGet package from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*.nupkg" --dir nuget-packages
+      
+      - name: Create test project
+        run: |
+          mkdir test-nuget
+          cd test-nuget
+          dotnet new console
+          dotnet add package Microsoft.Z3 --source ../nuget-packages --prerelease
+      
+      - name: Create test code
+        run: |
+          cat > test-nuget/Program.cs << 'EOF'
+          using Microsoft.Z3;
+          class Program {
+              static void Main() {
+                  using (Context ctx = new Context()) {
+                      IntExpr x = ctx.MkIntConst("x");
+                      Solver solver = ctx.MkSolver();
+                      solver.Assert(ctx.MkGt(x, ctx.MkInt(0)));
+                      if (solver.Check() == Status.SATISFIABLE) {
+                          System.Console.WriteLine("sat");
+                          System.Console.WriteLine(solver.Model);
+                      }
+                  }
+              }
+          }
+          EOF
+      
+      - name: Run test
+        run: |
+          cd test-nuget
+          dotnet run
+
+  # ============================================================================
+  # VALIDATION JOBS FOR EXECUTABLES
+  # ============================================================================
+  
+  validate-exe-windows-x64:
+    name: "Validate executable on Windows x64"
+    runs-on: windows-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Download Windows x64 build from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        shell: pwsh
+        run: |
+          $tag = "${{ github.event.inputs.release_tag }}"
+          if ([string]::IsNullOrEmpty($tag)) {
+            $tag = "Nightly"
+          }
+          gh release download $tag --pattern "*x64-win*.zip" --dir downloads
+      
+      - name: Extract and test
+        shell: pwsh
+        run: |
+          $zipFile = Get-ChildItem downloads/*x64-win*.zip | Select-Object -First 1
+          Expand-Archive -Path $zipFile -DestinationPath z3-test
+          $z3Dir = Get-ChildItem z3-test -Directory | Select-Object -First 1
+          & "$z3Dir/bin/z3.exe" --version
+          
+          # Test basic SMT solving
+          @"
+          (declare-const x Int)
+          (assert (> x 0))
+          (check-sat)
+          (get-model)
+          "@ | & "$z3Dir/bin/z3.exe" -in
+
+  validate-exe-windows-x86:
+    name: "Validate executable on Windows x86"
+    runs-on: windows-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Download Windows x86 build from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        shell: pwsh
+        run: |
+          $tag = "${{ github.event.inputs.release_tag }}"
+          if ([string]::IsNullOrEmpty($tag)) {
+            $tag = "Nightly"
+          }
+          gh release download $tag --pattern "*x86-win*.zip" --dir downloads
+      
+      - name: Extract and test
+        shell: pwsh
+        run: |
+          $zipFile = Get-ChildItem downloads/*x86-win*.zip | Select-Object -First 1
+          Expand-Archive -Path $zipFile -DestinationPath z3-test
+          $z3Dir = Get-ChildItem z3-test -Directory | Select-Object -First 1
+          & "$z3Dir/bin/z3.exe" --version
+          
+          # Test basic SMT solving
+          @"
+          (declare-const x Int)
+          (assert (> x 0))
+          (check-sat)
+          (get-model)
+          "@ | & "$z3Dir/bin/z3.exe" -in
+
+  validate-exe-ubuntu-x64:
+    name: "Validate executable on Ubuntu x64"
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Download Ubuntu x64 build from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*x64-glibc*.zip" --dir downloads
+      
+      - name: Extract and test
+        run: |
+          cd downloads
+          unzip *x64-glibc*.zip
+          cd z3-*
+          ./bin/z3 --version
+          
+          # Test basic SMT solving
+          echo "(declare-const x Int)
+          (assert (> x 0))
+          (check-sat)
+          (get-model)" | ./bin/z3 -in
+
+  validate-exe-macos-x64:
+    name: "Validate executable on macOS x64"
+    runs-on: macos-13
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Download macOS x64 build from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*x64-osx*.zip" --dir downloads
+      
+      - name: Extract and test
+        run: |
+          cd downloads
+          unzip *x64-osx*.zip
+          cd z3-*
+          ./bin/z3 --version
+          
+          # Test basic SMT solving
+          echo "(declare-const x Int)
+          (assert (> x 0))
+          (check-sat)
+          (get-model)" | ./bin/z3 -in
+
+  validate-exe-macos-arm64:
+    name: "Validate executable on macOS ARM64"
+    runs-on: macos-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 30
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Download macOS ARM64 build from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*arm64-osx*.zip" --dir downloads
+      
+      - name: Extract and test
+        run: |
+          cd downloads
+          unzip *arm64-osx*.zip
+          cd z3-*
+          ./bin/z3 --version
+          
+          # Test basic SMT solving
+          echo "(declare-const x Int)
+          (assert (> x 0))
+          (check-sat)
+          (get-model)" | ./bin/z3 -in
+
+  # ============================================================================
+  # REGRESSION TEST VALIDATION
+  # ============================================================================
+  
+  validate-regressions-ubuntu:
+    name: "Validate regression tests on Ubuntu"
+    runs-on: ubuntu-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 60
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Setup Python
+        uses: actions/setup-python@v6
+        with:
+          python-version: '3.x'
+      
+      - name: Download Ubuntu x64 build from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*x64-glibc*.zip" --dir downloads
+      
+      - name: Extract build
+        run: |
+          cd downloads
+          unzip *x64-glibc*.zip
+          cd ..
+      
+      - name: Clone z3test repository
+        run: git clone https://github.com/z3prover/z3test z3test
+      
+      - name: Run regression tests
+        run: |
+          Z3_PATH=$(find downloads -name z3 -type f | head -n 1)
+          chmod +x $Z3_PATH
+          python z3test/scripts/test_benchmarks.py $Z3_PATH z3test/regressions/smt2
+
+  validate-regressions-windows:
+    name: "Validate regression tests on Windows"
+    runs-on: windows-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 60
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Setup Python
+        uses: actions/setup-python@v6
+        with:
+          python-version: '3.x'
+      
+      - name: Download Windows x64 build from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        shell: pwsh
+        run: |
+          $tag = "${{ github.event.inputs.release_tag }}"
+          if ([string]::IsNullOrEmpty($tag)) {
+            $tag = "Nightly"
+          }
+          gh release download $tag --pattern "*x64-win*.zip" --dir downloads
+      
+      - name: Extract build
+        shell: pwsh
+        run: |
+          $zipFile = Get-ChildItem downloads/*x64-win*.zip | Select-Object -First 1
+          Expand-Archive -Path $zipFile -DestinationPath downloads
+      
+      - name: Clone z3test repository
+        run: git clone https://github.com/z3prover/z3test z3test
+      
+      - name: Run regression tests
+        shell: pwsh
+        run: |
+          $z3Path = Get-ChildItem downloads -Filter z3.exe -Recurse | Select-Object -First 1
+          python z3test/scripts/test_benchmarks.py $z3Path.FullName z3test/regressions/smt2
+
+  validate-regressions-macos:
+    name: "Validate regression tests on macOS"
+    runs-on: macos-latest
+    if: ${{ github.event.workflow_run.conclusion == 'success' || github.event_name == 'workflow_dispatch' }}
+    timeout-minutes: 60
+    steps:
+      - name: Checkout code
+        uses: actions/checkout@v6
+      
+      - name: Setup Python
+        uses: actions/setup-python@v6
+        with:
+          python-version: '3.x'
+      
+      - name: Download macOS ARM64 build from release
+        env:
+          GH_TOKEN: ${{ github.token }}
+        run: |
+          TAG="${{ github.event.inputs.release_tag }}"
+          if [ -z "$TAG" ]; then
+            TAG="Nightly"
+          fi
+          gh release download $TAG --pattern "*arm64-osx*.zip" --dir downloads
+      
+      - name: Extract build
+        run: |
+          cd downloads
+          unzip *arm64-osx*.zip
+          cd ..
+      
+      - name: Clone z3test repository
+        run: git clone https://github.com/z3prover/z3test z3test
+      
+      - name: Run regression tests
+        run: |
+          Z3_PATH=$(find downloads -name z3 -type f | head -n 1)
+          chmod +x $Z3_PATH
+          python z3test/scripts/test_benchmarks.py $Z3_PATH z3test/regressions/smt2