diff --git a/collects/redex/private/reduction-semantics.rkt b/collects/redex/private/reduction-semantics.rkt
index bf2d4fcd5e..f2a119b299 100644
--- a/collects/redex/private/reduction-semantics.rkt
+++ b/collects/redex/private/reduction-semantics.rkt
@@ -2253,11 +2253,13 @@
       (print-failed srcinfo)
       (inc-failures)
       (begin
-        (fprintf (current-error-port) "no reachable term ~a ~a" 
-                 (if (procedure? goal) "satisfying" "equal to")
-                 goal)
+        (if (procedure? goal)
+            (fprintf (current-error-port) 
+                     "no term satisfying ~a reachable from ~a" goal start)
+            (fprintf (current-error-port) 
+                     "term ~a not reachable from ~a" goal start))
         (when (search-failure-cutoff? result)
-          (fprintf (current-error-port) " (but some terms were not explored)"))
+          (fprintf (current-error-port) " (within ~a steps)" steps))
         (newline (current-error-port))))))
 
 (define-syntax (test-predicate stx)
diff --git a/collects/redex/tests/tl-test.rkt b/collects/redex/tests/tl-test.rkt
index 767a4fb996..81cdec76e2 100644
--- a/collects/redex/tests/tl-test.rkt
+++ b/collects/redex/tests/tl-test.rkt
@@ -2459,7 +2459,7 @@
     
     (define (equal-to-7 x) (= x 7))
     (test (capture-output (test-->>∃ #:steps 5 1+ 0 equal-to-7))
-          #rx"^FAILED .*\nno reachable term satisfying #<procedure:equal-to-7> \\(but some terms were not explored\\)\n$")
+          #rx"^FAILED .*\nno term satisfying #<procedure:equal-to-7> reachable from 0 \\(within 5 steps\\)\n$")
     
     (test (capture-output (test-->>∃ 1+ 0 7)) "")
     (test (capture-output (test-->>E 1+ 0 7)) "")
@@ -2472,7 +2472,7 @@
        (--> any any)))
     
     (test (capture-output (test-->>∃ identity 0 1))
-          #rx"^FAILED .*\nno reachable term equal to 1\n$")
+          #rx"^FAILED .*\nterm 1 not reachable from 0\n$")
     
     (test (capture-output (test-results)) "2 tests failed (out of 6 total).\n")