FStarLang / FStar

A Proof-oriented Programming Language
https://www.fstar-lang.org
Apache License 2.0
2.65k stars 232 forks source link

Checked files should be mindful of options #3333

Open mtzguido opened 1 week ago

mtzguido commented 1 week ago
$ 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