Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Discrepancy with/without checked files for name resolution #3589

Open
mtzguido opened this issue Oct 22, 2024 · 0 comments
Open

Discrepancy with/without checked files for name resolution #3589

mtzguido opened this issue Oct 22, 2024 · 0 comments

Comments

@mtzguido
Copy link
Member

Setup: A.fst:

module A

let a = "A.a"
let b = "A.b"

B.fst:

module B
let a = "B.a"
let b = "B.b"
include A {a}

C.fst:

module C
include B
let _ = assert (a == "A.a")
let _ = assert (b == "B.b")

C checks fine witout checked files for A/B, fails with them (it solves a to B.a instead).

$ ../../../bin/fstar.exe A.fst --cache_checked_modules 
Verified module: A
All verification conditions discharged successfully
$ ../../../bin/fstar.exe B.fst --cache_checked_modules 
Verified module: B
All verification conditions discharged successfully
$ ../../../bin/fstar.exe C.fst 
* Error 19 at C.fst(3,8-3,14):
  - Assertion failed
  - The SMT solver could not prove the query. Use --query_stats for more
    details.
  - See also C.fst(3,15-3,27)

1 error was reported (see above)
$ ../../../bin/fstar.exe C.fst --cache_off 
Verified module: C
All verification conditions discharged successfully

Noticed while reworking the bug-reports Makefile, related to #3559.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant