   (fstar--comment-beginning pos)
   (forward-comment 1))
 
-(defun fstar--search-predicated-1 (search-fn test-fn move-fn re)
+(defun fstar--search-predicated-1 (search-fn test-fn move-fn re bound)
   "Helper for `fstar--search-predicated'.
-SEARCH-FN, TEST-FN, MOVE-FN, RE: see `fstar--search-predicated'."
+SEARCH-FN, TEST-FN, MOVE-FN, RE, BOUND: see `fstar--search-predicated'."
   (catch 'found
-    (while (funcall search-fn re nil t)
+    (while (funcall search-fn re bound t)
       (when (funcall test-fn)
         (throw 'found (point)))
-      (unless (funcall move-fn)
-        (throw 'found nil)))
+      (when (= (match-beginning 0) (match-end 0))
+        (unless (funcall move-fn)
+          (throw 'found nil))))
     (throw 'found nil)))
 
-(defun fstar--search-predicated (search-fn test-fn move-fn re)
-  "Use SEARCH-FN to find matches of RE satisfying TEST-FN.
-MOVE-FN is used to move the point when TEST-FN returns nil.
-Return non-nil if RE can be found.  This function does not move
-the point."
+(defun fstar--search-predicated (search-fn test-fn move-fn re bound)
+  "Use SEARCH-FN to find matches of RE before BOUND satisfying TEST-FN.
+MOVE-FN is used to move the point when TEST-FN returns nil and
+the match is empty.  Return non-nil if RE can be found.  This
+function does not move the point."
   (save-excursion
     (comment-normalize-vars)
-    (and (fstar--search-predicated-1 search-fn test-fn move-fn re)
+    (and (fstar--search-predicated-1 search-fn test-fn move-fn re bound)
          ;; Ensure that the match is maximal when searching backwards for
          ;; e.g. \n+ in a buffer containing \n•\n
          (goto-char (match-beginning 0))

          (unless (eq (point) (point-at-bol))
            (goto-char (point-at-eol)))
          ;; Jump to previous block separator
          (fstar--search-predicated-backward
           #'fstar-subp--block-start-p fstar-subp-block-sep))
    (goto-char (match-beginning 1))))


          ;; Ensure progress
          (when (bobp) (forward-char))
          ;; Jump to next block separator
          (fstar--re-search-predicated-forward
           #'fstar-subp--block-start-p fstar-subp-block-sep))
    (goto-char (match-beginning 1))))

