 (defun fstar-subp-json--parse-issue (json)
   "Convert JSON issue into fstar-mode issue."
   (let-alist json
-    (make-fstar-issue
-     :level (intern .level)
-     :locs (mapcar #'fstar-subp-json--parse-location .ranges)
-     :message .message)))
+    (pcase-let* ((`(,msg . ,alt-locs) (fstar-subp-json--extract-alt-locs .message)))
+      (make-fstar-issue
+       :level (intern .level)
+       :locs (append (mapcar #'fstar-subp-json--parse-location .ranges) alt-locs)
+       :message msg))))
 
 (defun fstar-subp-parse-issues (response)
   "Parse RESPONSE into a list of issues."

(defconst fstar-subp-legacy--issue-regexp
  (concat "^" fstar-subp-issue-location-regexp "\\s-*:\\s-*"))

(defconst fstar-subp-legacy--also-see-regexp
  (concat "(Also see: " fstar-subp-issue-location-regexp ")"))

(defun fstar-subp-legacy--parse-issue (limit)
  "Construct an issue object from the current match data up to LIMIT."

                   collect (fstar-subp-legacy--parse-issue bound)
                   do (setq bound (match-beginning 0)))))))))

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

(defun fstar-subp-cleanup-issue (issue &optional ov)
  "Fixup ISSUE: include a file name, and adjust line numbers wrt OV."
  (dolist (loc (fstar-issue-locs issue))
    ;; Clean up file names
    (when (member (fstar-location-filename loc) '("unknown" "<input>"))
      (cl-assert buffer-file-name) ;; FIXME "unknown"
      (setf (fstar-location-filename loc) buffer-file-name))
    ;; Adjust line numbers
    (unless (or (fstar--has-feature 'absolute-linums-in-errors) (null ov))
      (let ((linum (1- (line-number-at-pos (overlay-start ov)))))
        (cl-incf (fstar-location-line-from loc) linum)
        (cl-incf (fstar-location-line-to loc) linum))))
  ;; Put local ranges first
  (let ((partitioned (-group-by #'fstar-subp--local-loc-p (fstar-issue-locs issue))))
    (setf (fstar-issue-locs issue)
          (append (cdr (assq t partitioned))
                  (cdr (assq nil partitioned)))))
  issue)

(defun fstar-subp--in-issue-p (pt)
