FStarLang / FStarLang/FStar

Verification not supported for match with when clause

Open
#64 2 comments 0 reactions 0 assignees View on GitHub
component/typechecker kind/enhancement
Dominant language
F*
Stars
3.1k
Forks
266
Avg merge
21h 1m
Merged PRs (30d)
54

Description

The following simple program:

```
let f = function
| 0 -> 0
| n when (n>1) -> 1
```

produces the following error trace:

```
../../bin/fstar.exe --fstar_home ../.. bug64.fst --trace_error
Bound term variable not found: n
at Microsoft.FStar.ToSMT.Encode.lookup_term_var[syntax`2,syntax`2] (Microsoft.FStar.ToSMT.env_t env, Microsoft.FStar.Absyn.withinfo_t`2 a) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+encode_args@771-1.Invoke (System.Tuple`2 tupledArg) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`3[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Util+either`2[Microsoft.FStar.ToSMT.Term+term,Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean],System.Tuple`3[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Util+either`2[Microsoft.FStar.ToSMT.Term+term,Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]]].Invoke (System.Tuple`3 , System.Tuple`2 ) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.loop@144-20[Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`3 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Fold[Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`3 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_args (Microsoft.FSharp.Collections.FSharpList`1 l, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+enc@827-2.Invoke (System.Tuple`2 x) [0x00000] in :0
at Microsoft.FSharp.Core.FSharpFunc`2[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]].InvokeFast[Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 func, System.Tuple`2 arg1, System.Tuple`2 arg2) [0x00000] in :0
at Microsoft.FStar.Util+fold@385-1[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean],Microsoft.FStar.ToSMT.Term+term].Invoke (System.Tuple`2 x) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`2[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term]],System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean],System.Tuple`2[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],Microsoft.FStar.ToSMT.Term+term]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term]]].Invoke (System.Tuple`2 , System.Tuple`2 ) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.loop@144-20[Tuple`2,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Fold[Tuple`2,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in :0
at Microsoft.FStar.Util.fold_map[Tuple`2,Tuple`2,term] (Microsoft.FSharp.Core.FSharpFunc`2 f, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 s) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.enc@826 (Microsoft.FStar.ToSMT.env_t env, Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+eq_op@849.Invoke (Microsoft.FSharp.Collections.FSharpList`1 _arg8) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FSharp.Primitives.Basics.List.map2ToFreshConsTail[Tuple`3,Boolean,Tuple`2] (Microsoft.FSharp.Collections.FSharpList`1 cons, Microsoft.FSharp.Core.FSharpFunc`3 f, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in :0
at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FSharp.Primitives.Basics.List.map2ToFreshConsTail[Tuple`3,Boolean,Tuple`2] (Microsoft.FSharp.Collections.FSharpList`1 cons, Microsoft.FSharp.Core.FSharpFunc`3 f, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in :0
at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_q_body@908 (Microsoft.FStar.ToSMT.env_t env, Microsoft.FSharp.Collections.FSharpList`1 bs, Microsoft.FSharp.Collections.FSharpList`1 ps, Microsoft.FStar.Absyn.syntax`2 body) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FSharp.Primitives.Basics.List.map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 xs1, Microsoft.FSharp.Collections.FSharpList`1 xs2) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Map2[Boolean,Tuple`2,Tuple`3] (Microsoft.FSharp.Core.FSharpFunc`2 mapping, Microsoft.FSharp.Collections.FSharpList`1 list1, Microsoft.FSharp.Collections.FSharpList`1 list2) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+enc_prop_c@833-1.Invoke (Microsoft.FSharp.Core.FSharpFunc`2 f, Microsoft.FSharp.Collections.FSharpList`1 l) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Invoke@3000[Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[Microsoft.FStar.Util+either`2[Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]],Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+exp',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]]],System.Boolean]],System.Tuple`3[Microsoft.FStar.ToSMT.Term+term,Microsoft.FSharp.Collections.FSharpList`1[System.Tuple`2[System.Tuple`2[System.String,Microsoft.FStar.ToSMT.Term+sort],System.String]],Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+decl]],Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.ToSMT.Term+term],Microsoft.FStar.ToSMT.Term+term]].Invoke (Microsoft.FSharp.Collections.FSharpList`1 u) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode.solve (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.syntax`2 q) [0x00000] in :0
at Microsoft.FStar.ToSMT.Encode+solver@1566-5.Invoke (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.syntax`2 q) [0x00000] in :0
at Microsoft.FSharp.Core.FSharpFunc`2[Microsoft.FStar.Tc.Env+env,Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+typ',Microsoft.FStar.Absyn.Syntax+syntax`2[Microsoft.FStar.Absyn.Syntax+knd',Microsoft.FSharp.Core.Unit]]].InvokeFast[Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 func, Microsoft.FStar.Tc.env arg1, Microsoft.FStar.Absyn.syntax`2 arg2) [0x00000] in :0
at Microsoft.FStar.Tc.Util.try_discharge_guard (Microsoft.FStar.Tc.env env, Microsoft.FStar.Tc.guard_t g) [0x00000] in :0
at Microsoft.FStar.Tc.Util.discharge_guard (Microsoft.FStar.Tc.env env, Microsoft.FStar.Tc.guard_t g) [0x00000] in :0
at Microsoft.FStar.Tc.Tc.tc_value (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in :0
at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in :0
at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in :0
at Microsoft.FStar.Tc.Tc.tc_decl (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.sigelt se, Boolean deserialized) [0x00000] in :0
at Microsoft.FStar.Tc.Tc+tc_decls@1426-1.Invoke (Microsoft.FStar.Absyn.sigelt se) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+sigelt,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+sigelt],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.sigelt ) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.loop@144-20[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Fold[sigelt,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in :0
at Microsoft.FStar.Tc.Tc.tc_decls (Microsoft.FStar.Tc.env env, Microsoft.FSharp.Collections.FSharpList`1 ses, Boolean deserialized) [0x00000] in :0
at Microsoft.FStar.Tc.Tc.tc_modul (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.modul modul) [0x00000] in :0
at Microsoft.FStar.Tc.Tc+check_modules@1471-1.Invoke (Microsoft.FStar.Absyn.modul m) [0x00000] in :0
at Microsoft.FSharp.Core.OptimizedClosures+Adapt@3006[System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env],Microsoft.FStar.Absyn.Syntax+modul,System.Tuple`2[Microsoft.FSharp.Collections.FSharpList`1[Microsoft.FStar.Absyn.Syntax+modul],Microsoft.FStar.Tc.Env+env]].Invoke (System.Tuple`2 , Microsoft.FStar.Absyn.modul ) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.loop@144-20[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`3 f, System.Tuple`2 s, Microsoft.FSharp.Collections.FSharpList`1 xs) [0x00000] in :0
at Microsoft.FSharp.Collections.ListModule.Fold[modul,Tuple`2] (Microsoft.FSharp.Core.FSharpFunc`2 folder, System.Tuple`2 state, Microsoft.FSharp.Collections.FSharpList`1 list) [0x00000] in :0
at Microsoft.FStar.Tc.Tc.check_modules (Microsoft.FStar.Tc.solver_t s, Microsoft.FStar.Tc.solver_t ds, Microsoft.FSharp.Collections.FSharpList`1 mods) [0x00000] in :0
at Microsoft.FStar.FStar.go$cont@55 (Microsoft.FSharp.Collections.FSharpList`1 filenames, Microsoft.FSharp.Core.Unit unitVar) [0x00000] in :0
at Microsoft.FStar.FStar.go[Unit] (Microsoft.FSharp.Core.Unit _arg1) [0x00000] in :0
at .$Microsoft.FStar.FStar.main@ () [0x00000] in :0
```

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.