   "Convert JSON info an fstar-mode location."
   (let-alist json
     (make-fstar-location
-     :filename .fname
+     :filename (fstar-subp--fixup-fname .fname)
      :line-from (elt .beg 0)
      :line-to (elt .end 0)
      :col-from (elt .beg 1)

      (progn (fstar-assert buffer-file-name) buffer-file-name)
    fname))

(defun fstar-subp--fixup-location (loc)
  "Replace <input> with the name of the current buffer in LOC."
  (cl-typecase loc
    (fstar-location (cl-callf fstar-subp--fixup-fname (fstar-location-filename loc))))
  loc)

(defun fstar-subp-cleanup-issue (issue &optional ov)
  "Fixup ISSUE: clean up file name and adjust line numbers wrt OV."
  (dolist (loc (fstar-issue-locs issue))
    ;; Clean up file name
    (fstar-subp--fixup-location loc)
    ;; Adjust line numbers
    (unless (or (fstar--has-feature 'absolute-linums-in-errors) (null ov))
      (let ((linum (1- (line-number-at-pos (overlay-start ov)))))

  (when (fstar--lispify-null defined-at)
    (let-alist defined-at
      (make-fstar-location
       :filename (fstar-subp--fixup-fname .fname)
       :line-from (elt .beg 0)
       :col-from (elt .beg 1)
       :line-to (elt .end 0)
