diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml
index 548fca2eb..180dc6d90 100644
--- a/.github/workflows/nightly.yml
+++ b/.github/workflows/nightly.yml
@@ -244,6 +244,62 @@ jobs:
       
       - name: Test
         run: python z3test/scripts/test_benchmarks.py build-dist/z3 z3test/regressions/smt2
+      - name: Clone bench (for issue-oracle smoke test)
+        continue-on-error: true
+        run: |
+          # Sparse clone: bench is ~12 GB total but only scripts/ and
+          # inputs/issues/ (~800 MB) are needed by the oracle. The
+          # smoke-test runs on a sampled subset of iss-* dirs (see
+          # next step), so even this 800 MB pull is upper-bounded
+          # at the clone level rather than runtime.
+          git clone --depth 1 --filter=blob:none --sparse \
+            https://github.com/Z3Prover/bench bench
+          git -C bench sparse-checkout set scripts inputs/issues
+
+      - name: Run issue-oracle smoke test
+        # continue-on-error: true means this step can NEVER red the
+        # nightly build. Its job is to produce a JSON report artifact,
+        # not to gate the build. The bounds below (--max 200, --timeout
+        # 5, --wallclock 20, outer timeout 90) keep the step under ~2
+        # minutes regardless of corpus growth.
+        continue-on-error: true
+        run: |
+          # SMOKE-TEST budget (sampled subset of the corpus):
+          #   --max 200          first 200 of ~2,700 iss-* dirs
+          #                      (sorted, so the same sample every run
+          #                      and easy to diff across nightlies)
+          #   --timeout 5        per-file z3 cap (matches capture-time
+          #                      timeout/4, so any bench that escapes
+          #                      this cap was already on the edge)
+          #   --wallclock 20     hard global cap INSIDE the script
+          #   --quiet            suppress per-issue progress lines
+          #   timeout 90         shell-level belt-and-braces wrapper,
+          #                      leaves 30 s headroom for the script
+          #                      to flush its JSON report before SIGTERM
+          # The script ALWAYS exits 0 on normal operation, so the only
+          # ways this step can non-zero are: missing z3 binary, sparse
+          # clone failure (the previous step's continue-on-error
+          # absorbs that), or the outer `timeout` firing. All three
+          # are absorbed by this step's continue-on-error: true.
+          timeout 90 python bench/scripts/issues_check_oracle.py \
+            --z3 build-dist/z3 \
+            --all bench/inputs/issues \
+            --max 200 \
+            --timeout 5 \
+            --wallclock 20 \
+            --jobs 0 \
+            --quiet \
+            --json-report issue-oracle-report.json
+
+      - name: Upload issue-oracle report
+        if: always()
+        continue-on-error: true
+        uses: actions/upload-artifact@v7.0.1
+        with:
+          name: issue-oracle-report
+          path: issue-oracle-report.json
+          retention-days: 7
+
       
       - name: Upload artifact
         uses: actions/upload-artifact@v7.0.1