Using {:verify false} in Dafny

Due to the nature of the underlying SMT used by Dafny for proof checking, Dafny sometimes takes a very long time to verify things. I find it useful to ask Dafny to work on a single lemma at a time. This can be achieved using the {:verify false} annotation. I set every function and method in my proof to {:verify false}, then change only the one I am working on back to {:verify true}. Occasionally I use find and replace to change all the {:verify false} annotations to {:verify true} and then run the whole proof through the Dafny command line.

Leave a Reply