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

Name not found in smtencoding env #2894

Closed
mtzguido opened this issue Apr 27, 2023 · 1 comment
Closed

Name not found in smtencoding env #2894

mtzguido opened this issue Apr 27, 2023 · 1 comment

Comments

@mtzguido
Copy link
Member

This file triggers it

FStar.Reflection.TermEq.fst.txt

@mtzguido
Copy link
Member Author

mtzguido commented May 1, 2023

Minimized:

module Bug

type comparator_for (t:Type) = x:t -> y:t -> int

val term_eq         : comparator_for int
let rec term_eq t1 t2 = 0

let t = term_eq
ASSERTION FAILURE: Name term_eq not found in the smtencoding env
F* may be in an inconsistent state.
Please file a bug report, ideally with a minimized version of the program that triggered the error.

mtzguido added a commit to mtzguido/FStar that referenced this issue May 3, 2023
mtzguido added a commit that referenced this issue May 5, 2023
Otherwise the encoding will crash for let recs with an abbreviated type.

Fixes #2894.
mtzguido added a commit that referenced this issue May 5, 2023
mtzguido added a commit that referenced this issue May 7, 2023
mtzguido added a commit that referenced this issue May 15, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

No branches or pull requests

1 participant