FStarLang / FStarLang/FStar

Checked files should be mindful of options

Open
#3,333 0 comments 0 reactions 0 assignees View on GitHub
Dominant language
F*
Stars
3.1k
Forks
266
Avg merge
21h 1m
Merged PRs (30d)
54

Description

```
$ 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
```

Contributor guide

Open the contributing guide

Assessment

This issue has not been assessed yet.

Get new issues in your inbox

A short digest of beginner-friendly GitHub issues.