Working with files with huge verification times

• Use hints (see Hints (or how to replay verification in milliseconds instead of minutes)). Hints are compatible with interactive-mode.

• Use C-c C-l instead of C-c C-RET to advance to the current point in --lax mode.

• Use #set-options "--lax" and #reset-options for the part of the file that verifies already. That is:

• Pass --admit_except <id> with a query id (eg, '(FStar.Fin.pigeonhole, 1)') to re-run a single SMT query and admit the rest.

module TLS

#set-options "--lax"
// a bunch of definitions that verify already
#reset-options

let f = ...
  // the function that you're currently trying to get to verify

• Use another module

module TLS.Wip

open TLS

let f = ...
  // work here on the function that you're trying to verify so that you can focus on this function only