diff --git a/.github/workflows/nightly.yml b/.github/workflows/nightly.yml
index 180dc6d90..12f063db2 100644
--- a/.github/workflows/nightly.yml
+++ b/.github/workflows/nightly.yml
@@ -244,63 +244,7 @@ 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
         with: