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

Verification not supported for match with when clause #64

Open
catalin-hritcu opened this Issue Nov 29, 2014 · 2 comments

Comments

Projects
None yet
3 participants
@catalin-hritcu
Member

catalin-hritcu commented Nov 29, 2014

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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+encode_args@771-1.Invoke (System.Tuple`2 tupledArg) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_args (Microsoft.FSharp.Collections.FSharpList`1 l, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_exp (Microsoft.FStar.Absyn.syntax`2 e, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+enc@827-2.Invoke (System.Tuple`2 x) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+eq_op@849.Invoke (Microsoft.FSharp.Collections.FSharpList`1 _arg8) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.encode_formula_with_labels (Microsoft.FStar.Absyn.syntax`2 phi, Microsoft.FStar.ToSMT.env_t env) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode.solve (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.syntax`2 q) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.ToSMT.Encode+solver@1566-5.Invoke (Microsoft.FStar.Tc.env tcenv, Microsoft.FStar.Absyn.syntax`2 q) [0x00000] in <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.Tc.Util.try_discharge_guard (Microsoft.FStar.Tc.env env, Microsoft.FStar.Tc.guard_t g) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Util.discharge_guard (Microsoft.FStar.Tc.env env, Microsoft.FStar.Tc.guard_t g) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_value (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_exp (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.syntax`2 e) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_decl (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.sigelt se, Boolean deserialized) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc+tc_decls@1426-1.Invoke (Microsoft.FStar.Absyn.sigelt se) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_decls (Microsoft.FStar.Tc.env env, Microsoft.FSharp.Collections.FSharpList`1 ses, Boolean deserialized) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc.tc_modul (Microsoft.FStar.Tc.env env, Microsoft.FStar.Absyn.modul modul) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.Tc.Tc+check_modules@1471-1.Invoke (Microsoft.FStar.Absyn.modul m) [0x00000] in <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>: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 <filename unknown>:0 
  at Microsoft.FStar.FStar.go$cont@55 (Microsoft.FSharp.Collections.FSharpList`1 filenames, Microsoft.FSharp.Core.Unit unitVar) [0x00000] in <filename unknown>:0 
  at Microsoft.FStar.FStar.go[Unit] (Microsoft.FSharp.Core.Unit _arg1) [0x00000] in <filename unknown>:0 
  at <StartupCode$fstar>.$Microsoft.FStar.FStar.main@ () [0x00000] in <filename unknown>:0 

catalin-hritcu added a commit that referenced this issue Nov 29, 2014

@nikswamy

This comment has been minimized.

Contributor

nikswamy commented Jan 9, 2015

Rather than fixing this issue now, I have disabled when clauses for the moment, when --verify is set. Will resurrect them after the POPL tutorial.

nikswamy added a commit that referenced this issue Jan 9, 2015

@catalin-hritcu catalin-hritcu changed the title from Match with when explodes in SMT encoding to Verification not supported for match with when clause Aug 23, 2015

@catalin-hritcu

This comment has been minimized.

Member

catalin-hritcu commented May 23, 2017

This feature is still missing, but the error message is much better:

When clauses are not yet supported in --verify mode; they will be some day

mtzguido added a commit that referenced this issue Jul 17, 2017

tactics: change guard check
Allow for the SMT to help discharging it, since some examples Nick ran
into require it. However, I'd like to revisit this throughout the
engine: when do we consider it acceptable to call the SMT during tactics
execution? I'd like to say never, but not sure how feasible that is.

Example file was:

```
module Test
open FStar.BV
open FStar.Tactics
open FStar.Tactics.BV
module U = FStar.UInt

val lemma_test: x:U.uint_t 64 ->
  Lemma (U.logand #64 x 0 == 0)
let lemma_test x =
 assert_by_tactic (bv_tac ()) (U.logand #64 x 0 == (0 <: uint_t' 64))
```

over commit a50b225

It seems the SMT is needed for deciding equality of two types,
`uint_t 64` and `uint_t' 64`, which have the same definition but the
typechecker can discharge this by itself. They are refinements,
but have the same definition. So maybe the typechecker discharges the
bi-implication instead of noticing the equality.

For now, bite the bullet and call z3.
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment