 Some examples (see below about `…'):
 
 - (setq fstar-subp-prover-args \"--ab\") results in F* being
-called as ‘fstar.exe … --ab’.
+called as ‘fstar.exe … --ab …’.
 
 - (setq fstar-subp-prover-args \\='(\"--ab\" \"--cd\")) results in
-F* being called as ‘fstar.exe … --ab --cd’.
+F* being called as ‘fstar.exe … --ab --cd …’.
 
 - (setq fstar-subp-prover-args (lambda () \\='(\"--ab\" \"--cd\")))
-results in F* being called as ‘fstar.exe … --ab --cd’.
-
-In addition to these setting, `fstar-mode' always includes (as
-indicated above with `…') both \\='--smt <path-to-z3>\\=' and one
-of \\='--ide\\=' and \\='--in\\='.
+results in F* being called as ‘fstar.exe … --ab --cd …’.
+
+In addition to these flags, `fstar-mode' always includes (as
+indicated above by the first `…') both \\='--smt <path-to-z3>\\='
+and one of \\='--ide\\=' and \\='--in\\=', and any flags computed
+from `fstar-subp-prover-additional-args' (as indicated above by
+the second `…').
 
 To debug unexpected behaviors with this variable, try
 evaluating (fstar-subp-get-prover-args).  Note that passing

  (equal args 'fstar-subp-prover-args-for-compiler-hacking))

(defcustom fstar-subp-prover-args nil
  "Used for computing arguments to pass to F* in interactive mode.

If set to a string, that string is considered to be a single
argument to pass to F*.  If set to a list of strings, each element

  "Find path to SMT solver executable."
  (fstar-find-executable fstar-smt-executable "SMT solver" 'fstar-smt-executable))

(defun fstar-subp--parse-prover-args-1 (args var-name)
  "Parse value of ARGS into a list of strings.
Complain about VAR-NAME if the final value isn't a string or a
list of strings."
  (let ((args (fstar--resolve-fn-value args)))
    (when (stringp args)
      (setq args (list args)))
    (unless (and (listp args) (cl-every #'stringp args))
      (user-error "Interpreting `%s' \
led to invalid value [%s]" var-name args))
    args))

(defmacro fstar-subp--parse-prover-args (argsv)
  "Like `fstar-subp--parse-prover-args-1' on ARGSV, but infer VAR-NAME."
  `(fstar-subp--parse-prover-args-1 ,argsv ',argsv))

(defun fstar-subp-get-prover-args ()
  "Compute F*'s arguments.
Function is public to make it easier to debug
`fstar-subp-prover-args' and
`fstar-subp-prover-additional-args'."
  (let ((smt-path (fstar--maybe-cygpath (fstar-subp-find-smt-solver)))
        (ide-flag (if (fstar--has-feature 'json-subp) "--ide" "--in"))
        (usr-args (append
                   (fstar-subp--parse-prover-args fstar-subp-prover-args)
                   (fstar-subp--parse-prover-args fstar-subp-prover-additional-args))))
    `(,(fstar-subp--buffer-file-name) ,ide-flag "--smt" ,smt-path ,@usr-args)))

(defun fstar-subp--prover-includes-for-compiler-hacking ()
