diff --git a/.github/skills/memory-safety/scripts/memory_safety.py b/.github/skills/memory-safety/scripts/memory_safety.py
index fa87f8f8c..10fb8ec82 100644
--- a/.github/skills/memory-safety/scripts/memory_safety.py
+++ b/.github/skills/memory-safety/scripts/memory_safety.py
@@ -18,7 +18,7 @@ import time
 from pathlib import Path
 
 sys.path.insert(0, str(Path(__file__).resolve().parent.parent.parent / "shared"))
-from z3db import Z3DB, setup_logging
+from z3db import Z3DB, require_repo_root, setup_logging
 
 logger = logging.getLogger("z3agent")
 
@@ -52,19 +52,6 @@ def check_dependencies():
         sys.exit(1)
 
 
-def find_repo_root() -> Path:
-    d = Path.cwd()
-    for _ in range(10):
-        if (d / "CMakeLists.txt").exists() and (d / "src").is_dir():
-            return d
-        parent = d.parent
-        if parent == d:
-            break
-        d = parent
-    logger.error("could not locate Z3 repository root")
-    sys.exit(1)
-
-
 def build_is_configured(build_dir: Path, sanitizer: str) -> bool:
     """Check whether the build directory already has a matching cmake config."""
     cache = build_dir / "CMakeCache.txt"
@@ -220,7 +207,7 @@ def main():
 
     setup_logging(args.debug)
     check_dependencies()
-    repo_root = find_repo_root()
+    repo_root = require_repo_root()
 
     sanitizers = ["asan", "ubsan"] if args.sanitizer == "both" else [args.sanitizer]
     all_findings = []
diff --git a/.github/skills/shared/z3db.py b/.github/skills/shared/z3db.py
index f0f7e3ea2..0d49cb7cf 100644
--- a/.github/skills/shared/z3db.py
+++ b/.github/skills/shared/z3db.py
@@ -3,7 +3,7 @@
 z3db: shared library and CLI for Z3 skill scripts.
 
 Library usage:
-    from z3db import Z3DB, find_z3, run_z3
+    from z3db import Z3DB, find_z3, find_repo_root, require_repo_root, run_z3
 
 CLI usage:
     python z3db.py init
@@ -131,7 +131,7 @@ class Z3DB:
         """Write to stderr and to the interaction_log table."""
         getattr(logger, level, logger.info)(message)
         self.conn.execute(
-            "INSERT INTO interaction_log (run_id, level, message) " "VALUES (?, ?, ?)",
+            "INSERT INTO interaction_log (run_id, level, message) VALUES (?, ?, ?)",
             (run_id, level, message),
         )
         self.conn.commit()
@@ -182,7 +182,7 @@ def find_z3(hint: str = None) -> str:
     if hint:
         candidates.append(hint)
 
-    repo_root = _find_repo_root()
+    repo_root = find_repo_root()
     if repo_root:
         for build_dir in ["build", "build/release", "build/debug"]:
             candidates.append(str(repo_root / build_dir / "z3"))
@@ -201,7 +201,8 @@ def find_z3(hint: str = None) -> str:
     sys.exit(1)
 
 
-def _find_repo_root() -> Optional[Path]:
+def find_repo_root() -> Optional[Path]:
+    """Best-effort search for the Z3 repository root from the current directory."""
     d = Path.cwd()
     for _ in range(10):
         if (d / "CMakeLists.txt").exists() and (d / "src").is_dir():
@@ -213,6 +214,15 @@ def _find_repo_root() -> Optional[Path]:
     return None
 
 
+def require_repo_root() -> Path:
+    """Return the Z3 repository root or exit the process if it is not found."""
+    repo_root = find_repo_root()
+    if repo_root is None:
+        logger.error("could not locate Z3 repository root")
+        sys.exit(1)
+    return repo_root
+
+
 def run_z3(
     formula: str,
     z3_bin: str = None,
diff --git a/.github/skills/static-analysis/scripts/static_analysis.py b/.github/skills/static-analysis/scripts/static_analysis.py
index 65f87e731..f93e43692 100644
--- a/.github/skills/static-analysis/scripts/static_analysis.py
+++ b/.github/skills/static-analysis/scripts/static_analysis.py
@@ -176,9 +176,7 @@ def print_findings(findings: list):
         return
 
     for f in findings:
-        label = f["category"]
-        if f["type"]:
-            label = f["type"]
+        label = f["type"] or f["category"]
         print(f"[{label}] {f['file']}:{f['line']}: {f['description']}")
 
     print()
diff --git a/.github/workflows/fstar-master-build.yml b/.github/workflows/fstar-master-build.yml
index 4b674fc33..8d347be5d 100644
--- a/.github/workflows/fstar-master-build.yml
+++ b/.github/workflows/fstar-master-build.yml
@@ -28,7 +28,7 @@ on:
       fstar_otherflags:
         description: "Extra FStar OTHERFLAGS"
         required: false
-        default: "--split_queries --log_failing_queries --ext higher_order_smt --proof_recovery"
+        default: "--split_queries on_failure --log_failing_queries --ext higher_order_smt --proof_recovery"
       discussion_category:
         description: Discussion category name
         required: false
@@ -86,6 +86,8 @@ jobs:
           /tmp/gh-aw/agent/z3-bin/z3 --version
 
       - name: Build FStar
+        id: build_fstar
+        continue-on-error: true
         run: |
           set -euo pipefail
           rm -rf /tmp/gh-aw/agent/FStar
@@ -105,19 +107,97 @@ jobs:
           test -x /tmp/gh-aw/agent/FStar/out/bin/fstar.exe || { echo "Error: FStar binary not found or not executable at /tmp/gh-aw/agent/FStar/out/bin/fstar.exe"; exit 1; }
           /tmp/gh-aw/agent/FStar/out/bin/fstar.exe --version | tee /tmp/gh-aw/agent/fstar-version.txt
 
+      - name: Collect generated SMT2 files
+        id: collect_smt2
+        if: always()
+        run: |
+          set -euo pipefail
+          rm -rf /tmp/gh-aw/agent/smt2-artifact
+          mkdir -p /tmp/gh-aw/agent/smt2-artifact
+          SMT2_PREVIEW=/tmp/gh-aw/agent/smt2-preview.md
+          SMT2_HEAD_LINES=1000
+          > "$SMT2_PREVIEW"
+
+          if [ -d /tmp/gh-aw/agent/FStar ]; then
+            mapfile -t SMT2_FILES < <(find /tmp/gh-aw/agent/FStar -type f -name '*.smt2' | sort)
+          else
+            SMT2_FILES=()
+          fi
+
+          if [ "${#SMT2_FILES[@]}" -eq 0 ]; then
+            echo "has_files=false" >> "$GITHUB_OUTPUT"
+            exit 0
+          fi
+
+          for file in "${SMT2_FILES[@]}"; do
+            rel="${file#/tmp/gh-aw/agent/FStar/}"
+            target="/tmp/gh-aw/agent/smt2-artifact/${rel}"
+            mkdir -p "$(dirname "$target")"
+            cp "$file" "$target"
+            {
+              printf '#### `%s`\n\n' "$rel"
+              printf '```smt2\n'
+              head -n "$SMT2_HEAD_LINES" "$file"
+              printf '\n```\n\n'
+            } >> "$SMT2_PREVIEW"
+          done
+
+          echo "has_files=true" >> "$GITHUB_OUTPUT"
+
+      - name: Upload generated SMT2 artifact
+        id: upload_smt2
+        if: always() && steps.collect_smt2.outputs.has_files == 'true'
+        uses: actions/upload-artifact@v4
+        with:
+          name: fstar-generated-smt2-${{ github.run_id }}
+          path: /tmp/gh-aw/agent/smt2-artifact
+          if-no-files-found: error
+          retention-days: 7
+
       - name: Create discussion summary
+        if: always()
         uses: actions/github-script@v9
         env:
           RUN_URL: ${{ github.server_url }}/${{ github.repository }}/actions/runs/${{ github.run_id }}
+          FSTAR_BUILD_OUTCOME: ${{ steps.build_fstar.outcome }}
+          SMT2_ARTIFACT_ID: ${{ steps.upload_smt2.outputs.artifact-id }}
         with:
           script: |
             const fs = require('fs');
 
-            const z3VersionText = fs.readFileSync('/tmp/gh-aw/agent/z3-version.txt', 'utf8').trim();
-            const fstarVersionFile = fs.readFileSync('/tmp/gh-aw/agent/fstar-version.txt', 'utf8').trim();
+            const readIfExists = (path) => fs.existsSync(path) ? fs.readFileSync(path, 'utf8').trim() : null;
+            const z3VersionText = readIfExists('/tmp/gh-aw/agent/z3-version.txt') ?? 'unknown';
+            const fstarVersionFile = readIfExists('/tmp/gh-aw/agent/fstar-version.txt') ?? '';
             const fstarVersionText = fstarVersionFile ? fstarVersionFile.split('\n')[0] : 'unknown';
-            const fstarCommitLine = fs.readFileSync('/tmp/gh-aw/agent/fstar-commit.txt', 'utf8').trim();
-            const fstarCommit = fstarCommitLine.replace(/^FStar commit:\s*/, '');
+            const fstarCommitLine = readIfExists('/tmp/gh-aw/agent/fstar-commit.txt') ?? '';
+            const fstarCommit = fstarCommitLine ? fstarCommitLine.replace(/^FStar commit:\s*/, '') : 'unknown';
+            const fstarBuildOutcome = process.env.FSTAR_BUILD_OUTCOME || 'unknown';
+            const fstarBuildSucceeded = fstarBuildOutcome === 'success';
+            const fstarStatus = fstarBuildSucceeded
+              ? '✅ FStar build completed'
+              : `⚠️ FStar build ${fstarBuildOutcome} (pipeline continued)`;
+            const smt2ArtifactId = (process.env.SMT2_ARTIFACT_ID || '').trim();
+            const smt2ArtifactUrl = smt2ArtifactId ? `${process.env.RUN_URL}/artifacts/${smt2ArtifactId}` : '';
+            const smt2PreviewFile = '/tmp/gh-aw/agent/smt2-preview.md';
+            const maxPreviewChars = 55000; // Keep below GitHub's 65536-character discussion body limit, leaving room for non-preview sections.
+            let smt2Preview = readIfExists(smt2PreviewFile) ?? '';
+            const smt2PreviewChars = Array.from(smt2Preview);
+            if (smt2PreviewChars.length > maxPreviewChars) {
+              smt2Preview = `${smt2PreviewChars.slice(0, maxPreviewChars).join('')}\n\n... (truncated due to discussion size limits)`;
+            }
+            const smt2Section = smt2ArtifactId
+              ? [
+                  `### Generated SMT2 files`,
+                  `- Artifact: ${smt2ArtifactUrl}`,
+                  ``,
+                  `First 1000 lines per generated \`.smt2\` file:`,
+                  ``,
+                  smt2Preview || '_No preview content available._'
+                ].join('\n')
+              : [
+                  `### Generated SMT2 files`,
+                  `- No generated \`.smt2\` files were found.`
+                ].join('\n');
             const date = new Date().toISOString().slice(0, 10);
 
             const owner = context.repo.owner;
@@ -146,7 +226,7 @@ jobs:
             const body = [
               `### Build status`,
               `- ✅ Z3 build completed`,
-              `- ✅ FStar build completed`,
+              `- ${fstarStatus}`,
               ``,
               `### Inputs used`,
               `- z3_ref: \`${process.env.Z3_REF}\``,
@@ -161,6 +241,8 @@ jobs:
               `- FStar: \`${fstarVersionText}\``,
               `- FStar commit: \`${fstarCommit}\``,
               ``,
+              smt2Section,
+              ``,
               `### Run`,
               `- Workflow run: ${process.env.RUN_URL}`
             ].join('\n');
diff --git a/.github/workflows/memory-safety-report.lock.yml b/.github/workflows/memory-safety-report.lock.yml
index 647fce0b3..f563a1476 100644
--- a/.github/workflows/memory-safety-report.lock.yml
+++ b/.github/workflows/memory-safety-report.lock.yml
@@ -1,4 +1,4 @@
-# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"3ed9f3a1cb53ff5095a4ff6a8169b75a50977baeddb965694ad30555729d56e4","body_hash":"3fece373efec3e8c9950482fd433a5bb06b3eb702a2e638af34815f937642fbe","compiler_version":"v0.77.5","strict":true,"agent_id":"copilot"}
+# gh-aw-metadata: {"schema_version":"v4","frontmatter_hash":"01e10498ee43530594fb5994a345b01b5718ffabe2872be157994f5489d81dad","body_hash":"f43683a4995003e2678ccce2706b639eb627b48daeafc7f9dded40d4508ef26c","compiler_version":"v0.77.5","strict":true,"agent_id":"copilot"}
 # gh-aw-manifest: {"version":1,"secrets":["COPILOT_GITHUB_TOKEN","GH_AW_GITHUB_MCP_SERVER_TOKEN","GH_AW_GITHUB_TOKEN","GITHUB_TOKEN"],"actions":[{"repo":"actions/cache/restore","sha":"27d5ce7f107fe9357f9df03efb73ab90386fccae","version":"v5.0.5"},{"repo":"actions/cache/save","sha":"27d5ce7f107fe9357f9df03efb73ab90386fccae","version":"v5.0.5"},{"repo":"actions/checkout","sha":"de0fac2e4500dabe0009e67214ff5f5447ce83dd","version":"v6.0.2"},{"repo":"actions/download-artifact","sha":"3e5f45b2cfb9172054b4087a40e8e0b5a5461e7c","version":"v8.0.1"},{"repo":"actions/github-script","sha":"3a2844b7e9c422d3c10d287c895573f7108da1b3","version":"v9.0.0"},{"repo":"actions/github-script","sha":"v9","version":"v9"},{"repo":"actions/setup-node","sha":"48b55a011bda9f5d6aeb4c2d9c7362e8dae4041e","version":"v6.4.0"},{"repo":"actions/upload-artifact","sha":"043fb46d1a93c77aae656e7c1c64a875d1fc6a0a","version":"v7.0.1"},{"repo":"github/gh-aw-actions/setup","sha":"v0.77.5","version":"v0.77.5"}],"resolution_failures":[{"repo":"actions/github-script","ref":"v9","error_type":"dynamic_resolution_failed"}],"containers":[{"image":"ghcr.io/github/gh-aw-firewall/agent:0.25.58"},{"image":"ghcr.io/github/gh-aw-firewall/api-proxy:0.25.58"},{"image":"ghcr.io/github/gh-aw-firewall/squid:0.25.58"},{"image":"ghcr.io/github/gh-aw-mcpg:v0.3.22"},{"image":"ghcr.io/github/github-mcp-server:v1.1.0"},{"image":"node:lts-alpine","digest":"sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f","pinned_image":"node:lts-alpine@sha256:d1b3b4da11eefd5941e7f0b9cf17783fc99d9c6fc34884a665f40a06dbdfc94f"}]}
 #    ___                   _   _      
 #   / _ \                 | | (_)     
@@ -22,7 +22,7 @@
 #
 # For more information: https://github.github.com/gh-aw/introduction/overview/
 #
-# Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and post findings as a GitHub Discussion.
+# Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and file findings as a GitHub issue.
 #
 # Frontmatter env variables:
 #   - GH_TOKEN: (main workflow)
@@ -210,21 +210,21 @@ jobs:
         run: |
           bash "${RUNNER_TEMP}/gh-aw/actions/create_prompt_first.sh"
           {
-          cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF'
+          cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF'
           <system>
-          GH_AW_PROMPT_413c70864e673ac4_EOF
+          GH_AW_PROMPT_0d048d29da1eafa3_EOF
           cat "${RUNNER_TEMP}/gh-aw/prompts/xpia.md"
           cat "${RUNNER_TEMP}/gh-aw/prompts/temp_folder_prompt.md"
           cat "${RUNNER_TEMP}/gh-aw/prompts/markdown.md"
           cat "${RUNNER_TEMP}/gh-aw/prompts/cache_memory_prompt.md"
           cat "${RUNNER_TEMP}/gh-aw/prompts/safe_outputs_prompt.md"
-          cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF'
+          cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF'
           <safe-output-tools>
-          Tools: create_discussion, missing_tool, missing_data, noop
+          Tools: create_issue, missing_tool, missing_data, noop
           </safe-output-tools>
-          GH_AW_PROMPT_413c70864e673ac4_EOF
+          GH_AW_PROMPT_0d048d29da1eafa3_EOF
           cat "${RUNNER_TEMP}/gh-aw/prompts/mcp_cli_tools_prompt.md"
-          cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF'
+          cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF'
           <github-context>
           The following GitHub context information is available for this workflow:
           {{#if github.actor}}
@@ -253,12 +253,12 @@ jobs:
           {{/if}}
           </github-context>
           
-          GH_AW_PROMPT_413c70864e673ac4_EOF
+          GH_AW_PROMPT_0d048d29da1eafa3_EOF
           cat "${RUNNER_TEMP}/gh-aw/prompts/github_mcp_tools_with_safeoutputs_prompt.md"
-          cat << 'GH_AW_PROMPT_413c70864e673ac4_EOF'
+          cat << 'GH_AW_PROMPT_0d048d29da1eafa3_EOF'
           </system>
           {{#runtime-import .github/workflows/memory-safety-report.md}}
-          GH_AW_PROMPT_413c70864e673ac4_EOF
+          GH_AW_PROMPT_0d048d29da1eafa3_EOF
           } > "$GH_AW_PROMPT"
       - name: Interpolate variables and render templates
         uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
@@ -356,7 +356,6 @@ jobs:
     permissions:
       actions: read
       contents: read
-      discussions: read
       issues: read
       pull-requests: read
     concurrency:
@@ -503,40 +502,49 @@ jobs:
           mkdir -p "${RUNNER_TEMP}/gh-aw/safeoutputs"
           mkdir -p /tmp/gh-aw/safeoutputs
           mkdir -p /tmp/gh-aw/mcp-logs/safeoutputs
-          cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_a51ec95cdbf8205c_EOF'
-          {"create_discussion":{"category":"agentic workflows","close_older_discussions":true,"expires":168,"fallback_to_issue":true,"max":1,"title_prefix":"[Memory Safety] "},"create_report_incomplete_issue":{},"max_bot_mentions":1,"mentions":{"enabled":false},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}}
-          GH_AW_SAFE_OUTPUTS_CONFIG_a51ec95cdbf8205c_EOF
+          cat > "${RUNNER_TEMP}/gh-aw/safeoutputs/config.json" << 'GH_AW_SAFE_OUTPUTS_CONFIG_c9563548363f5229_EOF'
+          {"create_issue":{"labels":["bug","memory-safety","automated-analysis"],"max":1,"title_prefix":"[Memory Safety] "},"create_report_incomplete_issue":{},"max_bot_mentions":1,"mentions":{"enabled":false},"missing_data":{},"missing_tool":{},"noop":{"max":1,"report-as-issue":"false"},"report_incomplete":{}}
+          GH_AW_SAFE_OUTPUTS_CONFIG_c9563548363f5229_EOF
       - name: Generate Safe Outputs Tools
         env:
           GH_AW_TOOLS_META_JSON: |
             {
               "description_suffixes": {
-                "create_discussion": " CONSTRAINTS: Maximum 1 discussion(s) can be created. Title will be prefixed with \"[Memory Safety] \". Discussions will be created in category \"agentic workflows\"."
+                "create_issue": " CONSTRAINTS: Maximum 1 issue(s) can be created. Title will be prefixed with \"[Memory Safety] \". Labels [\"bug\" \"memory-safety\" \"automated-analysis\"] will be automatically added."
               },
               "repo_params": {},
               "dynamic_tools": []
             }
           GH_AW_VALIDATION_JSON: |
             {
-              "create_discussion": {
+              "create_issue": {
                 "defaultMax": 1,
                 "fields": {
                   "body": {
                     "required": true,
                     "type": "string",
                     "sanitize": true,
-                    "maxLength": 65000,
-                    "minLength": 64
+                    "maxLength": 65000
                   },
-                  "category": {
-                    "type": "string",
-                    "sanitize": true,
-                    "maxLength": 128
+                  "fields": {
+                    "type": "array"
+                  },
+                  "labels": {
+                    "type": "array",
+                    "itemType": "string",
+                    "itemSanitize": true,
+                    "itemMaxLength": 128
+                  },
+                  "parent": {
+                    "issueOrPRNumber": true
                   },
                   "repo": {
                     "type": "string",
                     "maxLength": 256
                   },
+                  "temporary_id": {
+                    "type": "string"
+                  },
                   "title": {
                     "required": true,
                     "type": "string",
@@ -704,7 +712,7 @@ jobs:
           
           mkdir -p /home/runner/.copilot
           GH_AW_NODE=$(which node 2>/dev/null || command -v node 2>/dev/null || echo node)
-          cat << GH_AW_MCP_CONFIG_d1c0e6d43d005b0a_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs"
+          cat << GH_AW_MCP_CONFIG_5e59fdbe6d1c695e_EOF | "$GH_AW_NODE" "${RUNNER_TEMP}/gh-aw/actions/start_mcp_gateway.cjs"
           {
             "mcpServers": {
               "github": {
@@ -745,7 +753,7 @@ jobs:
               "payloadDir": "${MCP_GATEWAY_PAYLOAD_DIR}"
             }
           }
-          GH_AW_MCP_CONFIG_d1c0e6d43d005b0a_EOF
+          GH_AW_MCP_CONFIG_5e59fdbe6d1c695e_EOF
       - name: Mount MCP servers as CLIs
         id: mount-mcp-clis
         continue-on-error: true
@@ -1015,7 +1023,6 @@ jobs:
     runs-on: ubuntu-slim
     permissions:
       contents: read
-      discussions: write
       issues: write
     concurrency:
       group: "gh-aw-conclusion-memory-safety-report"
@@ -1143,8 +1150,6 @@ jobs:
           GH_AW_AGENTIC_ENGINE_TIMEOUT: ${{ needs.agent.outputs.agentic_engine_timeout }}
           GH_AW_MODEL_NOT_SUPPORTED_ERROR: ${{ needs.agent.outputs.model_not_supported_error }}
           GH_AW_ENGINE_API_HOSTS: "api.enterprise.githubcopilot.com,api.githubcopilot.com,api.business.githubcopilot.com,api.individual.githubcopilot.com"
-          GH_AW_CREATE_DISCUSSION_ERRORS: ${{ needs.safe_outputs.outputs.create_discussion_errors }}
-          GH_AW_CREATE_DISCUSSION_ERROR_COUNT: ${{ needs.safe_outputs.outputs.create_discussion_error_count }}
           GH_AW_LOCKDOWN_CHECK_FAILED: ${{ needs.activation.outputs.lockdown_check_failed }}
           GH_AW_STALE_LOCK_FILE_FAILED: ${{ needs.activation.outputs.stale_lock_file_failed }}
           GH_AW_GROUP_REPORTS: "false"
@@ -1258,7 +1263,7 @@ jobs:
         uses: actions/github-script@3a2844b7e9c422d3c10d287c895573f7108da1b3 # v9.0.0
         env:
           WORKFLOW_NAME: "Memory Safety Analysis Report Generator"
-          WORKFLOW_DESCRIPTION: "Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and post findings as a GitHub Discussion."
+          WORKFLOW_DESCRIPTION: "Analyze ASan/UBSan sanitizer logs from the memory-safety workflow and file findings as a GitHub issue."
           HAS_PATCH: ${{ needs.agent.outputs.has_patch }}
         with:
           script: |
@@ -1421,7 +1426,6 @@ jobs:
     runs-on: ubuntu-slim
     permissions:
       contents: read
-      discussions: write
       issues: write
     timeout-minutes: 15
     env:
@@ -1440,6 +1444,8 @@ jobs:
       code_push_failure_errors: ${{ steps.process_safe_outputs.outputs.code_push_failure_errors }}
       create_discussion_error_count: ${{ steps.process_safe_outputs.outputs.create_discussion_error_count }}
       create_discussion_errors: ${{ steps.process_safe_outputs.outputs.create_discussion_errors }}
+      created_issue_number: ${{ steps.process_safe_outputs.outputs.created_issue_number }}
+      created_issue_url: ${{ steps.process_safe_outputs.outputs.created_issue_url }}
       process_safe_outputs_processed_count: ${{ steps.process_safe_outputs.outputs.processed_count }}
       process_safe_outputs_temporary_id_map: ${{ steps.process_safe_outputs.outputs.temporary_id_map }}
     steps:
@@ -1489,7 +1495,7 @@ jobs:
           GH_AW_ALLOWED_DOMAINS: "api.business.githubcopilot.com,api.enterprise.githubcopilot.com,api.github.com,api.githubcopilot.com,api.individual.githubcopilot.com,api.snapcraft.io,archive.ubuntu.com,azure.archive.ubuntu.com,crl.geotrust.com,crl.globalsign.com,crl.identrust.com,crl.sectigo.com,crl.thawte.com,crl.usertrust.com,crl.verisign.com,crl3.digicert.com,crl4.digicert.com,crls.ssl.com,github.com,host.docker.internal,json-schema.org,json.schemastore.org,keyserver.ubuntu.com,ocsp.digicert.com,ocsp.geotrust.com,ocsp.globalsign.com,ocsp.identrust.com,ocsp.sectigo.com,ocsp.ssl.com,ocsp.thawte.com,ocsp.usertrust.com,ocsp.verisign.com,packagecloud.io,packages.cloud.google.com,packages.microsoft.com,ppa.launchpad.net,raw.githubusercontent.com,registry.npmjs.org,s.symcb.com,s.symcd.com,security.ubuntu.com,telemetry.enterprise.githubcopilot.com,ts-crl.ws.symantec.com,ts-ocsp.ws.symantec.com,www.googleapis.com"
           GITHUB_SERVER_URL: ${{ github.server_url }}
           GITHUB_API_URL: ${{ github.api_url }}
-          GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_discussion\":{\"category\":\"agentic workflows\",\"close_older_discussions\":true,\"expires\":168,\"fallback_to_issue\":true,\"max\":1,\"title_prefix\":\"[Memory Safety] \"},\"create_report_incomplete_issue\":{},\"mentions\":{\"enabled\":false},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}"
+          GH_AW_SAFE_OUTPUTS_HANDLER_CONFIG: "{\"create_issue\":{\"labels\":[\"bug\",\"memory-safety\",\"automated-analysis\"],\"max\":1,\"title_prefix\":\"[Memory Safety] \"},\"create_report_incomplete_issue\":{},\"mentions\":{\"enabled\":false},\"missing_data\":{},\"missing_tool\":{},\"noop\":{\"max\":1,\"report-as-issue\":\"false\"},\"report_incomplete\":{}}"
         with:
           github-token: ${{ secrets.GH_AW_GITHUB_TOKEN || secrets.GITHUB_TOKEN }}
           script: |
diff --git a/.github/workflows/memory-safety-report.md b/.github/workflows/memory-safety-report.md
index 56ffe514f..0e8464471 100644
--- a/.github/workflows/memory-safety-report.md
+++ b/.github/workflows/memory-safety-report.md
@@ -1,7 +1,7 @@
 ---
 description: >
   Analyze ASan/UBSan sanitizer logs from the memory-safety workflow
-  and post findings as a GitHub Discussion.
+  and file findings as a GitHub issue.
 
 on:
   workflow_run:
@@ -16,7 +16,6 @@ timeout-minutes: 30
 permissions:
   actions: read
   contents: read
-  discussions: read
   issues: read
   pull-requests: read
 
@@ -35,11 +34,10 @@ safe-outputs:
   mentions: false
   allowed-github-references: []
   max-bot-mentions: 1
-  create-discussion:
+  create-issue:
     title-prefix: "[Memory Safety] "
-    category: "Agentic Workflows"
-    close-older-discussions: true
-    expires: 7d
+    labels: [bug, memory-safety, automated-analysis]
+    max: 1
   missing-tool:
     create-issue: true
   noop:
@@ -111,9 +109,9 @@ Check cache memory for previous run results:
 - List of previously known issues
 - Identify new findings (regressions) vs. resolved findings (improvements)
 
-### 4. Generate the Discussion Report
+### 4. Generate the Issue Report
 
-Create a GitHub Discussion. Use `###` or lower for section headers, never `##` or `#`. Wrap verbose sections in `<details>` tags to keep the report scannable.
+Create a GitHub issue using `create-issue`. Use `##` or lower for section headers and wrap verbose sections in `<details>` tags to keep the report scannable.
 
 ```markdown
 **Date**: YYYY-MM-DD
@@ -190,7 +188,7 @@ Create a GitHub Discussion. Use `###` or lower for section headers, never `##` o
 </details>
 ```
 
-If zero findings across all tools, create a discussion noting a clean run with the commit and workflow run link.
+If zero findings across all tools, call `noop` and include a clean-run summary (commit and workflow run link) in the no-op message.
 
 ### 5. Update Cache Memory
 
@@ -203,7 +201,7 @@ Store the current run's results in cache memory for future comparison:
 
 - If the triggering workflow failed entirely, report that analysis could not complete and include any partial results.
 - If no artifacts are available, report that and suggest running the workflow manually.
-- If the helper scripts fail, report the error in the discussion body and stop.
+- If the helper scripts fail, report the error in the issue body and stop.
 
 ## Guidelines
 
@@ -217,6 +215,6 @@ Store the current run's results in cache memory for future comparison:
 
 - DO NOT create pull requests or modify source files.
 - DO NOT attempt to fix the findings automatically.
-- DO close older Memory Safety discussions automatically (configured via `close-older-discussions: true`).
+- DO create issues only when there are actionable findings; use `noop` for clean runs.
 - DO always report the commit SHA so findings can be correlated with specific code versions.
 - DO use cache memory to track trends over multiple runs.
\ No newline at end of file
diff --git a/gmon.out b/gmon.out
new file mode 100644
index 000000000..cba10a19b
Binary files /dev/null and b/gmon.out differ
diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 8b862fec2..ff04bfb68 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1919,6 +1919,9 @@ class JavaDLLComponent(Component):
             if IS_WINDOWS: # On Windows, CL creates a .lib file to link against.
                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(LIB_EXT)\n' %
                           os.path.join('api', 'java', 'Native'))
+            elif IS_OSX:
+                out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT) -Wl,-rpath,@loader_path $(SLINK_EXTRA_FLAGS)\n' %
+                          os.path.join('api', 'java', 'Native'))
             else:
                 out.write('\t$(SLINK) $(SLINK_OUT_FLAG)libz3java$(SO_EXT) $(SLINK_FLAGS) %s$(OBJ_EXT) libz3$(SO_EXT) $(SLINK_EXTRA_FLAGS)\n' %
                           os.path.join('api', 'java', 'Native'))
diff --git a/scripts/tests/test_jni_arch_flags.py b/scripts/tests/test_jni_arch_flags.py
index 2796b156d..e60285eec 100644
--- a/scripts/tests/test_jni_arch_flags.py
+++ b/scripts/tests/test_jni_arch_flags.py
@@ -208,6 +208,45 @@ class TestJNIArchitectureFlagsInMakefile(unittest.TestCase):
                 "(the import library)",
             )
 
+    # ------------------------------------------------------------------
+    # Tests for macOS rpath, so libz3java.dylib can find libz3.dylib
+    # ------------------------------------------------------------------
+
+    def test_macos_uses_loader_path_rpath(self):
+        """
+        On macOS, the JNI link command must include -Wl,-rpath,@loader_path
+        so that libz3java.dylib can find libz3.dylib in the same directory
+        at runtime. Without this, Java fails with UnsatisfiedLinkError.
+        """
+        comp = self._make_java_dll_component()
+        text = self._generate_makefile(
+            comp, is_windows=False, is_osx=True, is_arch_arm64=True
+        )
+        link_lines = self._find_jni_link_lines(text)
+        self.assertTrue(link_lines, "Expected at least one JNI link line")
+        for line in link_lines:
+            self.assertIn(
+                '-Wl,-rpath,@loader_path', line,
+                "macOS JNI link command must set rpath to @loader_path "
+                "so libz3java.dylib finds libz3.dylib at runtime",
+            )
+
+    def test_linux_does_not_use_loader_path(self):
+        """
+        On Linux, @loader_path is a macOS concept and must not appear.
+        """
+        comp = self._make_java_dll_component()
+        text = self._generate_makefile(
+            comp, is_windows=False, is_osx=False, is_arch_arm64=False
+        )
+        link_lines = self._find_jni_link_lines(text)
+        self.assertTrue(link_lines, "Expected at least one JNI link line")
+        for line in link_lines:
+            self.assertNotIn(
+                '@loader_path', line,
+                "@loader_path is macOS-specific and must not appear on Linux",
+            )
+
     # ------------------------------------------------------------------
     # Consistency check: SLINK_EXTRA_FLAGS in mk_config for cross-compile
     # ------------------------------------------------------------------
diff --git a/scripts/update_api.py b/scripts/update_api.py
index df80da116..b539165a3 100755
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -631,7 +631,16 @@ def mk_java(java_src, java_dir, package_name):
     java_native.write('      try {\n')
     java_native.write('        System.loadLibrary("z3java");\n')
     java_native.write('      } catch (UnsatisfiedLinkError ex) {\n')
-    java_native.write('        System.loadLibrary("libz3java");\n')
+    java_native.write('        try {\n')
+    java_native.write('          System.loadLibrary("libz3java");\n')
+    java_native.write('        } catch (UnsatisfiedLinkError ex2) {\n')
+    java_native.write('          throw new UnsatisfiedLinkError(\n')
+    java_native.write('            "Failed to load z3java native library. "\n')
+    java_native.write('            + "Tried z3java: " + ex.getMessage() + "; "\n')
+    java_native.write('            + "Tried libz3java: " + ex2.getMessage() + ". "\n')
+    java_native.write('            + "Make sure both the JNI library and libz3 are in java.library.path "\n')
+    java_native.write('            + "or set DYLD_LIBRARY_PATH (macOS) / LD_LIBRARY_PATH (Linux).");\n')
+    java_native.write('        }\n')
     java_native.write('      }\n')
     java_native.write('    }\n')
     java_native.write('  }\n')
diff --git a/src/api/java/CMakeLists.txt b/src/api/java/CMakeLists.txt
index 194b25232..774a293bc 100644
--- a/src/api/java/CMakeLists.txt
+++ b/src/api/java/CMakeLists.txt
@@ -48,17 +48,18 @@ target_include_directories(z3java PRIVATE
   "${PROJECT_BINARY_DIR}/src/api"
   ${JNI_INCLUDE_DIRS}
 )
-# Add header padding for macOS to allow install_name_tool to modify the dylib
+# On macOS, set rpath so libz3java.dylib can find libz3.dylib in the same directory,
+# and add header padding to allow install_name_tool to modify the dylib.
 if (CMAKE_SYSTEM_NAME STREQUAL "Darwin")
+  set_target_properties(z3java PROPERTIES
+    MACOSX_RPATH TRUE
+    INSTALL_RPATH "@loader_path"
+    BUILD_RPATH "@loader_path"
+  )
   target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names")
 endif()
 # FIXME: Should this library have SONAME and VERSION set?
 
-# On macOS, add headerpad for install_name_tool compatibility
-if(CMAKE_SYSTEM_NAME STREQUAL "Darwin")
-  target_link_options(z3java PRIVATE "-Wl,-headerpad_max_install_names")
-endif()
-
 # This prevents CMake from automatically defining ``z3java_EXPORTS``
 set_property(TARGET z3java PROPERTY DEFINE_SYMBOL "")
 
diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt
index 9d529f9b5..ba7eda277 100644
--- a/src/ast/rewriter/CMakeLists.txt
+++ b/src/ast/rewriter/CMakeLists.txt
@@ -39,6 +39,7 @@ z3_add_component(rewriter
     rewriter.cpp
     seq_axioms.cpp
     seq_eq_solver.cpp
+    seq_subset.cpp
     seq_rewriter.cpp
     seq_skolem.cpp
     th_rewriter.cpp
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 4453c94a7..46da49cf2 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -4491,10 +4491,60 @@ br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
     r* ++ r -> r ++ r*
 */
 br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
+    auto accepts_empty_word = [&](expr* r) {
+        auto info = re().get_info(r);
+        return info.interpreted && info.nullable == l_true && info.min_length == 0;
+    };
+    auto starts_with_full_seq = [&](expr* r) {
+        expr* r1 = nullptr, *r2 = nullptr;
+        return re().is_full_seq(r) || (re().is_concat(r, r1, r2) && re().is_full_seq(r1));
+    };
+    auto ends_with_full_seq = [&](expr* r) {
+        expr* r1 = nullptr, *r2 = nullptr;
+        while (re().is_concat(r, r1, r2))
+            r = r2;
+        return re().is_full_seq(r);
+    };
+    auto all_inter_arms_end_with_full_seq = [&](expr* r) {
+        ptr_buffer<expr> todo;
+        todo.push_back(r);
+        while (!todo.empty()) {
+            expr* r1 = nullptr, *r2 = nullptr;
+            expr* t = todo.back();
+            todo.pop_back();
+            if (re().is_intersection(t, r1, r2)) {
+                todo.push_back(r1);
+                todo.push_back(r2);
+            }
+            else if (!ends_with_full_seq(t)) {
+                return false;
+            }
+        }
+        return true;
+    };
     if (re().is_full_seq(a) && re().is_full_seq(b)) {
         result = a;
         return BR_DONE;
     }
+    if (re().is_full_seq(a) && accepts_empty_word(b)) {
+        result = a;
+        return BR_DONE;
+    }
+    if (re().is_full_seq(b) && accepts_empty_word(a)) {
+        result = b;
+        return BR_DONE;
+    }
+    expr* u1 = nullptr, *u2 = nullptr;
+    if (re().is_full_seq(a) && re().is_union(b, u1, u2) &&
+        (starts_with_full_seq(u1) || starts_with_full_seq(u2))) {
+        result = mk_regex_union_normalize(mk_regex_concat(a, u1), mk_regex_concat(a, u2));
+        return BR_REWRITE2;
+    }
+    if (re().is_intersection(a, u1, u2) && re().is_full_seq(b) &&
+        all_inter_arms_end_with_full_seq(a)) {
+        result = a;
+        return BR_DONE;
+    }
     if (re().is_empty(a)) {
         result = a;
         return BR_DONE;
@@ -4525,7 +4575,8 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
         result = re().mk_to_re(str().mk_concat(a_str, b_str));
         return BR_REWRITE2;
     }
-    expr* a1 = nullptr, *b1 = nullptr;
+    expr* a1 = nullptr;
+    expr* b1 = nullptr;
     if (re().is_to_re(a, a1) && re().is_to_re(b, b1)) {
         result = re().mk_to_re(str().mk_concat(a1, b1));
         return BR_DONE;
@@ -4534,6 +4585,11 @@ br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
         result = a;
         return BR_DONE;
     }
+    expr* b2 = nullptr, *b3 = nullptr;
+    if (re().is_star(a, a1) && re().is_concat(b, b1, b2) && re().is_star(b1, b3) && a1 == b3) {
+        result = b;
+        return BR_DONE;
+    }
     if (re().is_star(a, a1) && a1 == b) {
         result = re().mk_concat(b, a);
         return BR_DONE;
@@ -4587,51 +4643,7 @@ bool seq_rewriter::are_complements(expr* r1, expr* r2) const {
  * basic subset checker.
  */
 bool seq_rewriter::is_subset(expr* r1, expr* r2) const {
-    // return false;
-    expr* ra1 = nullptr, *ra2 = nullptr, *ra3 = nullptr;
-    expr* rb1 = nullptr, *rb2 = nullptr, *rb3 = nullptr;
-    unsigned la, ua, lb, ub;
-    if (re().is_complement(r1, ra1) && 
-        re().is_complement(r2, rb1)) {
-        return is_subset(rb1, ra1);
-    }
-    auto is_concat = [&](expr* r, expr*& a, expr*& b, expr*& c) {
-        return re().is_concat(r, a, b) && re().is_concat(b, b, c);
-    };
-    while (true) {
-        if (r1 == r2)
-            return true;
-        if (re().is_full_seq(r2))
-            return true;
-        if (re().is_dot_plus(r2) && re().get_info(r1).nullable == l_false)
-            return true;
-        if (is_concat(r1, ra1, ra2, ra3) &&
-            is_concat(r2, rb1, rb2, rb3) && ra1 == rb1 && ra2 == rb2) {
-            r1 = ra3;
-            r2 = rb3;
-            continue;
-        }
-        if (re().is_concat(r1, ra1, ra2) && 
-            re().is_concat(r2, rb1, rb2) && re().is_full_seq(rb1)) {
-            r1 = ra2;
-            continue;
-        }
-        // r1=ra3{la,ua}ra2, r2=rb3{lb,ub}rb2, ra3=rb3, lb<=la, ua<=ub
-        if (re().is_concat(r1, ra1, ra2) && re().is_loop(ra1, ra3, la, ua) &&
-            re().is_concat(r2, rb1, rb2) && re().is_loop(rb1, rb3, lb, ub) &&
-            ra3 == rb3 && lb <= la && ua <= ub) {
-            r1 = ra2;
-            r2 = rb2;
-            continue;
-        }
-        // ra1=ra3{la,ua}, r2=rb3{lb,ub}, ra3=rb3, lb<=la, ua<=ub
-        if (re().is_loop(r1, ra3, la, ua) &&
-            re().is_loop(r2, rb3, lb, ub) &&
-            ra3 == rb3 && lb <= la && ua <= ub) {
-            return true;
-        }
-        return false;
-    }
+    return m_subset.is_subset(r1, r2);
 }
 
 br_status seq_rewriter::mk_re_union0(expr* a, expr* b, expr_ref& result) {
@@ -6163,4 +6175,3 @@ bool seq_rewriter::get_bounds(expr* e, unsigned& low, unsigned& high) {
     }
     return low <= high;
 }
-
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 583720911..4ebd770a7 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -23,6 +23,7 @@ Notes:
 #include "ast/arith_decl_plugin.h"
 #include "ast/rewriter/rewriter_types.h"
 #include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/seq_subset.h"
 #include "util/params.h"
 #include "util/lbool.h"
 #include "util/sign.h"
@@ -128,6 +129,7 @@ class seq_rewriter {
     };
 
     seq_util       m_util;
+    seq_subset     m_subset;
     arith_util     m_autil;
     bool_rewriter  m_br;
     // re2automaton   m_re2aut;
@@ -340,7 +342,7 @@ class seq_rewriter {
 
 public:
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m), m_autil(m), m_br(m, p), // m_re2aut(m), 
+        m_util(m), m_subset(m_util.re), m_autil(m), m_br(m, p), // m_re2aut(m), 
         m_op_cache(m), m_es(m), 
         m_lhs(m), m_rhs(m), m_coalesce_chars(true) {
     }
@@ -424,4 +426,3 @@ public:
     */
     lbool some_string_in_re(expr* r, zstring& s);
 };
-
diff --git a/src/ast/rewriter/seq_subset.cpp b/src/ast/rewriter/seq_subset.cpp
new file mode 100644
index 000000000..2fc4d1f71
--- /dev/null
+++ b/src/ast/rewriter/seq_subset.cpp
@@ -0,0 +1,146 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    seq_subset.cpp
+
+Abstract:
+
+    Heuristic regular-expression subset checks used by seq_rewriter.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-6-8
+
+--*/
+
+#include "ast/rewriter/seq_subset.h"
+
+bool seq_subset::is_subset_rec(expr* a, expr* b, unsigned depth) const {
+    while (true) {
+        
+        if (a == b)
+            return true;
+        if (m_re.is_empty(a))
+            return true;
+        if (m_re.is_full_seq(b))
+            return true;
+        if (m_re.is_epsilon(a) && m_re.get_info(b).nullable == l_true)
+            return true;
+
+        if (depth >= m_max_depth)
+            return false;        
+
+        expr* a1 = nullptr, * a2 = nullptr, * b1 = nullptr, * b2 = nullptr;
+        unsigned la, ua, lb, ub;
+
+        // a ⊆ .+ iff a is non-nullable
+        if (m_re.is_dot_plus(b) && m_re.get_info(a).nullable == l_false)
+            return true;
+
+        // a ⊆ a*
+        if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth))
+            return true;
+
+        // e ⊆ a*
+        if (m_re.is_epsilon(a) && m_re.is_star(b, b1))
+            return true;
+
+        // R ⊆ R*
+        if (m_re.is_star(b, b1) && is_subset_rec(a, b1, depth + 1))
+            return true;
+
+        // R1* ⊆ R2* if R1 ⊆ R2
+        if (m_re.is_star(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1))
+            return true;
+
+        // R1+ ⊆ R2+ if R1 ⊆ R2
+        if (m_re.is_plus(a, a1) && m_re.is_plus(b, b1) && is_subset_rec(a1, b1, depth))
+            return true;
+
+        // R ⊆ R+
+        if (m_re.is_plus(b, b1) && is_subset_rec(a, b1, depth))
+            return true;
+
+        // R+ ⊆ R*
+        if (m_re.is_plus(a, a1) && m_re.is_star(b, b1) && is_subset_rec(a1, b1, depth + 1))
+            return true;
+
+        // range containment
+        if (m_re.is_range(a, la, ua) && m_re.is_range(b, lb, ub) && lb <= la && ua <= ub)
+            return true;
+
+        // to_re(s) ⊆ range
+        if (m_re.is_to_re(a, a1) && m_re.is_range(b, lb, ub) && is_app(a1)) {
+            func_decl* f = to_app(a1)->get_decl();
+            if (f->get_decl_kind() == OP_STRING_CONST && f->get_num_parameters() == 1) {
+                zstring const& s = f->get_parameter(0).get_zstring();
+                if (s.length() == 1 && lb <= s[0] && s[0] <= ub)
+                    return true;
+            }
+        }
+
+        // a ⊆ b1 ∪ b2 if a ⊆ b1 or a ⊆ b2
+        if (m_re.is_union(b, b1, b2) && (is_subset_rec(a, b1, depth + 1) || is_subset_rec(a, b2, depth + 1)))
+            return true;
+
+        // a1 ∪ a2 ⊆ b if a1 ⊆ b and a2 ⊆ b
+        if (m_re.is_union(a, a1, a2) && is_subset_rec(a1, b, depth + 1) && is_subset_rec(a2, b, depth + 1))
+            return true;
+
+        // a1 ∩ a2 ⊆ b if a1 ⊆ b or a2 ⊆ b
+        if (m_re.is_intersection(a, a1, a2) && (is_subset_rec(a1, b, depth + 1) || is_subset_rec(a2, b, depth + 1)))
+            return true;
+
+        // a ⊆ b1 ∩ b2 if a ⊆ b1 and a ⊆ b2
+        if (m_re.is_intersection(b, b1, b2) && is_subset_rec(a, b1, depth + 1) && is_subset_rec(a, b2, depth + 1))
+            return true;
+
+        // R{la,ua} ⊆  R'{lb,ub} if  R ⊆ R', lb<=la, ua<=ub
+        if (m_re.is_loop(a, a1, la, ua) &&
+            m_re.is_loop(b, b1, lb, ub) &&
+            lb <= la && ua <= ub && is_subset_rec(a1, b1, depth + 1)) {
+            return true;
+        }
+
+        // a1 \ a2 ⊆ b if a1 ⊆ b
+        if (m_re.is_diff(a, a1, a2) && is_subset_rec(a1, b, depth + 1))
+            return true;
+
+        // R ⊆ Σ*·R' if R ⊆ R'
+        if (m_re.is_concat(b, b1, b2) && m_re.is_full_seq(b1) && is_subset_rec(a, b2, depth))
+            return true;
+
+        // R ⊆ R'·Σ* if R ⊆ R'
+        if (m_re.is_concat(b, b1, b2) && m_re.is_full_seq(b2) && is_subset_rec(a, b1, depth))
+            return true;
+
+        // star absorption: R·R* ⊆ R*, R*·R ⊆ R*
+        bool const is_concat_star = m_re.is_concat(a, a1, a2) && m_re.is_star(b, b1);
+        if (is_concat_star &&
+            is_subset_rec(a1, b1, depth + 1) && is_subset_rec(a2, b, depth + 1))
+            return true;
+        if (is_concat_star &&
+            is_subset_rec(a2, b1, depth + 1) && is_subset_rec(a1, b, depth + 1))
+            return true;
+
+        // concat monotonicity:
+        // tail-recursive on second arguments (without increasing depth bound).
+        if (m_re.is_concat(a, a1, a2) && m_re.is_concat(b, b1, b2) && is_subset_rec(a1, b1, depth + 1)) {
+            a = a2;
+            b = b2;
+            continue;
+        }
+
+        // complement: ~a ⊆ ~b if b ⊆ a
+        if (m_re.is_complement(a, a1) && m_re.is_complement(b, b1))
+            return is_subset_rec(b1, a1, depth + 1);
+
+        return false;
+    }
+}
+
+bool seq_subset::is_subset(expr* a, expr* b) const {
+    return is_subset_rec(a, b, 0);
+}
diff --git a/src/ast/rewriter/seq_subset.h b/src/ast/rewriter/seq_subset.h
new file mode 100644
index 000000000..7329c898e
--- /dev/null
+++ b/src/ast/rewriter/seq_subset.h
@@ -0,0 +1,30 @@
+/*++
+Copyright (c) 2026 Microsoft Corporation
+
+Module Name:
+
+    seq_subset.h
+
+Abstract:
+
+    Heuristic regular-expression subset checks used by seq_rewriter.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2026-6-8
+
+--*/
+#pragma once
+
+#include "ast/seq_decl_plugin.h"
+
+class seq_subset {
+    seq_util::rex& m_re;
+    static constexpr unsigned m_max_depth = 3;
+
+    bool is_subset_rec(expr* a, expr* b, unsigned depth) const;
+
+public:
+    explicit seq_subset(seq_util::rex& re) : m_re(re) {}
+    bool is_subset(expr* a, expr* b) const;
+};
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 634ced5c9..8986e7ec1 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -1653,9 +1653,9 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
     if (e->get_family_id() == u.get_family_id()) {
         switch (e->get_decl()->get_decl_kind()) {
         case OP_RE_EMPTY_SET:
-            return info(true, l_false, UINT_MAX);
+            return info(true, l_false, UINT_MAX, false);
         case OP_RE_FULL_SEQ_SET:
-            return info(true, l_true, 0);
+            return info(true, l_true, 0, true);
         case OP_RE_STAR:
             i1 = get_info_rec(e->get_arg(0));
             return i1.star();
@@ -1667,7 +1667,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
         case OP_RE_OF_PRED:
             //TBD: check if the character predicate contains uninterpreted symbols or is nonground or is unsat
             //TBD: check if the range is unsat
-            return info(true, l_false, 1);
+            return info(true, l_false, 1, false);
         case OP_RE_CONCAT:
             i1 = get_info_rec(e->get_arg(0));
             i2 = get_info_rec(e->get_arg(1));
@@ -1684,7 +1684,7 @@ seq_util::rex::info seq_util::rex::mk_info_rec(app* e) const {
             min_length = u.str.min_length(e->get_arg(0));
             is_value = m.is_value(e->get_arg(0));
             nullable = (is_value && min_length == 0 ? l_true : (min_length > 0 ? l_false : l_undef));
-            return info(is_value, nullable, min_length);
+            return info(is_value, nullable, min_length, true);
         case OP_RE_REVERSE:
             return get_info_rec(e->get_arg(0));
         case OP_RE_PLUS:
@@ -1720,7 +1720,8 @@ std::ostream& seq_util::rex::info::display(std::ostream& out) const {
     if (is_known()) {
         out << "info("
             << "nullable=" << (nullable == l_true ? "T" : (nullable == l_false ? "F" : "U")) << ", "
-            << "min_length=" << min_length << ")";
+            << "min_length=" << min_length << ", "
+            << "classical=" << (classical ? "T" : "F") << ")";
     }
     else if (is_valid())
         out << "UNKNOWN";
@@ -1740,13 +1741,13 @@ std::string seq_util::rex::info::str() const {
 
 seq_util::rex::info seq_util::rex::info::star() const {
     //if is_known() is false then all mentioned properties will remain false
-    return seq_util::rex::info(interpreted, l_true, 0);
+    return seq_util::rex::info(interpreted, l_true, 0, classical);
 }
 
 seq_util::rex::info seq_util::rex::info::plus() const {
     if (is_known()) {
         //plus never occurs in a normalized regex
-        return info(interpreted, nullable, min_length);
+        return info(interpreted, nullable, min_length, classical);
     }
     else
         return *this;
@@ -1755,14 +1756,14 @@ seq_util::rex::info seq_util::rex::info::plus() const {
 seq_util::rex::info seq_util::rex::info::opt() const {
     // if is_known() is false then all mentioned properties will remain false
     // optional construct never occurs in a normalized regex
-    return seq_util::rex::info(interpreted, l_true, 0);
+    return seq_util::rex::info(interpreted, l_true, 0, classical);
 }
 
 seq_util::rex::info seq_util::rex::info::complement() const {
     if (is_known()) {
         lbool compl_nullable = (nullable == l_true ? l_false : (nullable == l_false ? l_true : l_undef));
         unsigned compl_min_length = (compl_nullable == l_false ? 1 : 0);
-        return info(interpreted, compl_nullable, compl_min_length);
+        return info(interpreted, compl_nullable, compl_min_length, false);
     }
     else
         return *this;
@@ -1776,7 +1777,8 @@ seq_util::rex::info seq_util::rex::info::concat(seq_util::rex::info const& rhs,
                 m = UINT_MAX;
             return info(interpreted && rhs.interpreted,
                 ((nullable == l_false || rhs.nullable == l_false) ? l_false : ((nullable == l_true && rhs.nullable == l_true) ? l_true : l_undef)),
-                m);
+                m,
+                classical && rhs.classical);
         }
         else
             return rhs;
@@ -1790,7 +1792,8 @@ seq_util::rex::info seq_util::rex::info::disj(seq_util::rex::info const& rhs) co
         //works correctly if one of the arguments is unknown
         return info(interpreted && rhs.interpreted,
             ((nullable == l_true || rhs.nullable == l_true) ? l_true : ((nullable == l_false && rhs.nullable == l_false) ? l_false : l_undef)),
-            std::min(min_length, rhs.min_length));
+            std::min(min_length, rhs.min_length),
+            classical && rhs.classical);
     }
     else
         return rhs;
@@ -1801,7 +1804,8 @@ seq_util::rex::info seq_util::rex::info::conj(seq_util::rex::info const& rhs) co
         if (rhs.is_known()) {
             return info(interpreted && rhs.interpreted,
                 ((nullable == l_true && rhs.nullable == l_true) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)),
-                std::max(min_length, rhs.min_length));
+                std::max(min_length, rhs.min_length),
+                false);
         }
         else
             return rhs;
@@ -1815,7 +1819,8 @@ seq_util::rex::info seq_util::rex::info::diff(seq_util::rex::info const& rhs) co
         if (rhs.is_known()) {
             return info(interpreted & rhs.interpreted,
                 ((nullable == l_true && rhs.nullable == l_false) ? l_true : ((nullable == l_false || rhs.nullable == l_false) ? l_false : l_undef)),
-                std::max(min_length, rhs.min_length));
+                std::max(min_length, rhs.min_length),
+                false);
         }
         else
             return rhs;
@@ -1832,7 +1837,8 @@ seq_util::rex::info seq_util::rex::info::orelse(seq_util::rex::info const& i) co
             // TBD: whether ite is interpreted or not depends on whether the condition is interpreted and both branches are interpreted
             return info(false,
                 ((nullable == l_true && i.nullable == l_true) ? l_true : ((nullable == l_false && i.nullable == l_false) ? l_false : l_undef)),
-                std::min(min_length, i.min_length));
+                std::min(min_length, i.min_length),
+                classical && i.classical);
         }
         else
             return i;
@@ -1848,7 +1854,7 @@ seq_util::rex::info seq_util::rex::info::loop(unsigned lower, unsigned upper) co
         if (m > 0 && (m < min_length || m < lower))
             m = UINT_MAX;
         lbool loop_nullable = (nullable == l_true || lower == 0 ? l_true : nullable);
-        return info(interpreted, loop_nullable, m);
+        return info(interpreted, loop_nullable, m, classical);
     }
     else
         return *this;
@@ -1863,6 +1869,7 @@ seq_util::rex::info& seq_util::rex::info::operator=(info const& other) {
     interpreted = other.interpreted;
     nullable = other.nullable;
     min_length = other.min_length;
+    classical = other.classical;
     return *this;
 }
 
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 78ad6d544..756ec38e4 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -443,6 +443,8 @@ public:
             lbool nullable { l_undef };
             /* Lower bound  on the length of all accepted words. */
             unsigned min_length { 0 };
+            /* Classical regular expression: does not use complement, intersection, diff, or the empty language (fail). */
+            bool classical { true };
 
             /*
               Default constructor of invalid info.
@@ -459,11 +461,13 @@ public:
             */
             info(bool is_interpreted,
                 lbool is_nullable,
-                unsigned min_l) :
+                unsigned min_l,
+                bool is_classical) :
                 known(l_true), 
                 interpreted(is_interpreted),
                 nullable(is_nullable),
-                min_length(min_l) {}
+                min_length(min_l),
+                classical(is_classical) {}
 
             /*
               Appends a string representation of the info into the stream.
diff --git a/src/ast/sls/sls_seq_plugin.cpp b/src/ast/sls/sls_seq_plugin.cpp
index f516b2948..8584741f3 100644
--- a/src/ast/sls/sls_seq_plugin.cpp
+++ b/src/ast/sls/sls_seq_plugin.cpp
@@ -912,7 +912,7 @@ namespace sls {
                         m_string_updates.reset();
                         u[i][j] = d[i - 1][j];
                     }
-                    if (d[i][j - 1] < u[i][j] && b.can_add(i - 1)) {
+                    if (d[i][j - 1] < u[i][j] && b.can_add(j - 1)) {
                         m_string_updates.reset();
                         u[i][j] = d[i][j - 1];
                     }
diff --git a/src/math/lp/dioph_eq.cpp b/src/math/lp/dioph_eq.cpp
index 5058bfaf3..0b3c5166a 100644
--- a/src/math/lp/dioph_eq.cpp
+++ b/src/math/lp/dioph_eq.cpp
@@ -709,8 +709,8 @@ namespace lp {
             while (column.size() > 1) {
                 auto& c = column.back();
                 SASSERT(c.var() != last_row_index);
-                m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j);
                 m_changed_rows.insert(c.var());
+                m_l_matrix.pivot_row_to_row_given_cell(last_row_index, c, j);
             }
         }
 
diff --git a/src/math/lp/lp_core_solver_base_def.h b/src/math/lp/lp_core_solver_base_def.h
index c4c41c26e..21bd48a22 100644
--- a/src/math/lp/lp_core_solver_base_def.h
+++ b/src/math/lp/lp_core_solver_base_def.h
@@ -277,13 +277,11 @@ pivot_column_tableau(unsigned j, unsigned piv_row_index) {
         m_A.m_rows[c.var()][c.offset()].offset() = pivot_col_cell_index;
     }
     while (column.size() > 1) {
-        auto & c = column.back();
+        auto& c = column.back();
         SASSERT(c.var() != piv_row_index);
-        if(! m_A.pivot_row_to_row_given_cell(piv_row_index, c, j)) {
-            return false;
-        }
-        if (m_touched_rows!= nullptr)
+        if (m_touched_rows != nullptr)
             m_touched_rows->insert(c.var());
+        m_A.pivot_row_to_row_given_cell(piv_row_index, c, j);
     }
 
     if (m_settings.simplex_strategy() == simplex_strategy_enum::tableau_costs)
diff --git a/src/math/lp/static_matrix.cpp b/src/math/lp/static_matrix.cpp
index 26ce218de..4abf0d88a 100644
--- a/src/math/lp/static_matrix.cpp
+++ b/src/math/lp/static_matrix.cpp
@@ -51,8 +51,8 @@ namespace lp {
     template void static_matrix<mpq, numeric_pair<mpq> >::set(unsigned int, unsigned int, mpq const&);
 
 
-    template bool static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
-    template bool static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
+    template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell(unsigned int, column_cell& , unsigned int);
+    template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell(unsigned int, column_cell&, unsigned int);
     template void static_matrix<mpq, numeric_pair<mpq> >::pivot_row_to_row_given_cell_with_sign(unsigned int, column_cell&, unsigned int, int);
     template void static_matrix<mpq, mpq>::pivot_row_to_row_given_cell_with_sign(unsigned int, row_cell<empty_struct>&, unsigned int, int);
     template void static_matrix<mpq, numeric_pair<mpq> >::add_rows(mpq const&, unsigned int, unsigned int);
diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h
index 415d3f1a2..08db2245d 100644
--- a/src/math/lp/static_matrix.h
+++ b/src/math/lp/static_matrix.h
@@ -293,7 +293,7 @@ public:
 
 
 // pivot row i to row ii
-    bool pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j);
+    void pivot_row_to_row_given_cell(unsigned i, column_cell& c, unsigned j);
     void pivot_row_to_row_given_cell_with_sign(unsigned piv_row_index, column_cell& c, unsigned j, int j_sign);
     void transpose_rows(unsigned i, unsigned ii) {
         auto t = m_rows[i];
diff --git a/src/math/lp/static_matrix_def.h b/src/math/lp/static_matrix_def.h
index b28d67740..af07c4482 100644
--- a/src/math/lp/static_matrix_def.h
+++ b/src/math/lp/static_matrix_def.h
@@ -48,7 +48,7 @@ namespace lp {
     }
 
 
-    template <typename T, typename X> bool static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i, 
+    template <typename T, typename X> void static_matrix<T, X>::pivot_row_to_row_given_cell(unsigned i, 
                                                                                             column_cell & c, unsigned pivot_col) {
         unsigned ii = c.var();
         SASSERT(i < row_count() && ii < column_count() && i != ii);
@@ -82,7 +82,7 @@ namespace lp {
             if (is_zero(rowii[k].coeff()))
                 remove_element(rowii, rowii[k]);
         }
-        return !rowii.empty();
+        SASSERT(!rowii.empty());
     }
 
     
diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp
index d47a09d14..58499c028 100644
--- a/src/muz/spacer/spacer_qe_project.cpp
+++ b/src/muz/spacer/spacer_qe_project.cpp
@@ -1148,6 +1148,7 @@ class arith_project_util {
                         expr_ref_vector const &lits) {
         app_ref_vector new_vars(m);
         expr_ref_vector result(lits);
+        model::scoped_model_completion _smc(mdl, true);
         for (unsigned i = 0; i < vars.size(); ++i) {
             app *v = vars.get(i);
             m_var = alloc(contains_app, m, v);
@@ -1183,6 +1184,12 @@ class arith_project_util {
                     expr_map &map) {
         app_ref_vector new_vars(m);
 
+        // Variables to be projected may not be assigned in the model
+        // (e.g. grounded auxiliary variables that are don't-cares). Enable
+        // model completion so their evaluation yields concrete numerals,
+        // matching the behavior of the native MBP arith projector.
+        model::scoped_model_completion _smc(mdl, true);
+
         // factor out mod terms by introducing new variables
         TRACE(qe, tout << "before factoring out mod terms:" << "\n";
               tout << mk_pp(fml, m) << "\n"; tout << "mdl:\n";
diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 107456455..492595f60 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -494,6 +494,31 @@ namespace smt {
         else if (is_app(n) && to_app(n)->get_family_id() == get_family_id()) {
             // These are the conversion functions fp.to_* */
             SASSERT(!m_fpa_util.is_float(n) && !m_fpa_util.is_rm(n));
+
+            // The conversion equality and side conditions for fp.to_* terms are
+            // emitted in internalize_term(), which runs exactly once. Those are
+            // asserted as theory axioms at the current decision level and are
+            // undone on DPLL backtracking, while internalize_term() is not run
+            // again for the already-internalized term (e.g. when the term lives
+            // at the user push base level and its clause is not reinitialized).
+            // The side conditions include the axioms linking FP uninterpreted
+            // functions to their bit-vector counterparts; losing them leaves the
+            // BV counterpart unconstrained and causes an incremental-mode
+            // soundness bug. relevant_eh re-fires on relevancy re-propagation
+            // after a backtrack, so re-emit them here to keep them in force.
+            switch ((fpa_op_kind)to_app(n)->get_decl_kind()) {
+            case OP_FPA_TO_FP:
+            case OP_FPA_TO_UBV:
+            case OP_FPA_TO_SBV:
+            case OP_FPA_TO_REAL:
+            case OP_FPA_TO_IEEE_BV: {
+                expr_ref conv = convert(n);
+                assert_cnstr(m.mk_eq(n, conv));
+                assert_cnstr(mk_side_conditions());
+                break;
+            }
+            default: /* ignore */;
+            }
         }
         else {
             /* Theory variables can be merged when (= bv-term (bvwrap fp-term)),
diff --git a/src/test/sls_seq_plugin.cpp b/src/test/sls_seq_plugin.cpp
index b7a23a596..4c8c5340c 100644
--- a/src/test/sls_seq_plugin.cpp
+++ b/src/test/sls_seq_plugin.cpp
@@ -351,4 +351,28 @@ void tst_sls_seq_plugin() {
     app_ref eq(m.mk_eq(l, r), m);
     verbose_stream() << eq << "\n";
     ts.repair_down_str_eq_edit_distance_incremental(eq);
+
+    test_seq::string_instance lhs, rhs;
+    lhs.s = zstring("a");
+    lhs.is_value.push_back(false);
+    lhs.prev_is_var.push_back(false);
+    lhs.next_is_var.push_back(false);
+    rhs.s = zstring("ab");
+    rhs.is_value.push_back(true);
+    rhs.prev_is_var.push_back(false);
+    rhs.next_is_var.push_back(false);
+    rhs.is_value.push_back(false);
+    rhs.prev_is_var.push_back(false);
+    rhs.next_is_var.push_back(false);
+
+    ENSURE(ts.edit_distance_with_updates(lhs, rhs) == 0);
+    ENSURE(ts.m_string_updates.size() == 2);
+    ENSURE(ts.m_string_updates[0].side == test_seq::side_t::right);
+    ENSURE(ts.m_string_updates[0].op == test_seq::op_t::add);
+    ENSURE(ts.m_string_updates[0].i == 0);
+    ENSURE(ts.m_string_updates[0].j == 1);
+    ENSURE(ts.m_string_updates[1].side == test_seq::side_t::right);
+    ENSURE(ts.m_string_updates[1].op == test_seq::op_t::del);
+    ENSURE(ts.m_string_updates[1].i == 1);
+    ENSURE(ts.m_string_updates[1].j == 0);
 }
\ No newline at end of file