FStarLang / FStar

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

Discrepancy with/without checked files for name resolution #3589

Open mtzguido opened 4 weeks ago

mtzguido commented 4 weeks ago

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.