            (issues (mapcar #'fstar-subp-cleanup-issue raw-issues)))
       (fstar-log 'info "Highlighting Flycheck issues: %S" issues)
       (funcall callback 'finished
-               (mapcar #'fstar-subp--make-flycheck-issue issues)))))
+               (delq nil (mapcar #'fstar-subp--make-flycheck-issue issues))))))
 
 (defun fstar-subp--start-syntax-check (_checker callback)
   "Start a light syntax check; pass results to CALLBACK."


(defun fstar-subp-jump-to-issue (issue)
  "Jump to ISSUE in current buffer."
  (let ((loc (fstar-issue-loc issue)))
    (goto-char (fstar--row-col-offset (fstar-location-line-from loc)
                                 (fstar-location-col-from loc)))))

(defun fstar-subp--local-issue-p (issue)
  "Check if ISSUE came from the current buffer."
  (string= (expand-file-name buffer-file-name)
           (expand-file-name (fstar-location-filename (fstar-issue-loc issue)))))

(defun fstar-subp-parse-and-highlight-issues (status response overlay)
  "Parse issues in RESPONSE (caused by processing OVERLAY) and display them.

  "Highlight ISSUE in current buffer.
PARENT is the overlay whose processing caused this issue to be
reported."
  (-when-let* ((loc (car (fstar-issue-locs issue)))
               (from (fstar--row-col-offset (fstar-location-line-from loc)
                                       (fstar-location-col-from loc)))
               (to (fstar--row-col-offset (fstar-location-line-to loc)
                                     (fstar-location-col-to loc)))
               (overlay (make-overlay from (max to (1+ from)) (current-buffer) t nil)))
    (overlay-put overlay 'fstar-subp-issue t)
    (overlay-put overlay 'fstar-subp-issue-parent-overlay parent)
    (overlay-put overlay 'face (fstar-subp-issue-face issue))
