FStarLang/FStar

Checked files should be mindful of options

Opened this issue · 0 comments

$ cat X.fst
module X
let _ = assert False
$ ./bin/fstar.exe --cache_checked_modules --admit_smt_queries true X.fst
Verified module: X
All verification conditions discharged successfully     # OK...
$ ./bin/fstar.exe --cache_checked_modules --admit_smt_queries false X.fst
Verified module: X
All verification conditions discharged successfully     # Misleading, we did NOT verify this file