Checked files should be mindful of options
Opened this issue · 0 comments
mtzguido commented
$ 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