diff --git a/examples/layeredeffects/GTWP.fst b/examples/layeredeffects/GTWP.fst index 2af0907f4e0..e897f538ccb 100644 --- a/examples/layeredeffects/GTWP.fst +++ b/examples/layeredeffects/GTWP.fst @@ -56,16 +56,23 @@ let bind (a b : Type) (i:idx) (wc:wp a) (wf:a -> wp b) (c : m a i wc) (f : (x:a | D -> coerce (d_bind #_ #_ #wc #wf (coerce c) f) // GM: would be nice to skip the annotations. -let subcomp (a:Type) (i:idx) (wp1 : wp a) - (wp2 : wp a) - (f : m a i wp1) +let subcomp (a:Type u#aa) (i:idx) + (wp1 : wp a) + (wp2 : wp a) + (f : m a i wp1) : Pure (m a i wp2) (requires (forall p. wp2 p ==> wp1 p)) (ensures (fun _ -> True)) = match i with | T -> f | G -> f - | D -> coerce f + | D -> + (* This case needs some handholding. *) + let f : raise_t (unit -> DIV a wp1) = f in + let f : unit -> DIV a wp1 = downgrade_val f in + let f : unit -> DIV a wp2 = f in + assert_norm (m a i wp2 == raise_t (unit -> DIV a wp2)); + coerce (raise_val f) unfold let ite_wp #a (w1 w2 : wp a) (b:bool) : wp a = diff --git a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml index 9a6a72e43a2..dcc8fefc882 100644 --- a/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml +++ b/ocaml/fstar-lib/generated/FStar_CheckedFiles.ml @@ -1,5 +1,5 @@ open Prims -let (cache_version_number : Prims.int) = (Prims.of_int (58)) +let (cache_version_number : Prims.int) = (Prims.of_int (59)) type tc_result = { checked_module: FStar_Syntax_Syntax.modul ; diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml index ca6d13324e6..d9cca8b02af 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_EncodeTerm.ml @@ -1405,9 +1405,7 @@ and (encode_term : let f = FStar_SMTEncoding_Util.mkFreeV fsym in let app = mk_Apply f vars in let tcenv_bs = - let uu___6 = - FStar_TypeChecker_Env.push_binders - env.FStar_SMTEncoding_Env.tcenv binders1 in + let uu___6 = env'.FStar_SMTEncoding_Env.tcenv in { FStar_TypeChecker_Env.solver = (uu___6.FStar_TypeChecker_Env.solver); @@ -1787,53 +1785,115 @@ and (encode_term : FStar_Compiler_Util.digest_of_string tkey_hash1)) in let tsym = Prims.op_Hat "Non_total_Tm_arrow_" tkey_hash in - let tdecl = - FStar_SMTEncoding_Term.DeclFun - (tsym, [], FStar_SMTEncoding_Term.Term_sort, - FStar_Pervasives_Native.None) in - let t2 = FStar_SMTEncoding_Util.mkApp (tsym, []) in - let t_kinding = - let a_name = - Prims.op_Hat "non_total_function_typing_" tsym in - let uu___5 = - let uu___6 = - FStar_SMTEncoding_Term.mk_HasType t2 - FStar_SMTEncoding_Term.mk_Term_type in - (uu___6, - (FStar_Pervasives_Native.Some - "Typing for non-total arrows"), a_name) in - FStar_SMTEncoding_Util.mkAssume uu___5 in - let fsym = - FStar_SMTEncoding_Term.mk_fv - ("f", FStar_SMTEncoding_Term.Term_sort) in - let f = FStar_SMTEncoding_Util.mkFreeV fsym in - let f_has_t = FStar_SMTEncoding_Term.mk_HasType f t2 in - let t_interp = - let a_name = Prims.op_Hat "pre_typing_" tsym in - let uu___5 = + let env0 = env in + let uu___5 = + let fvs = + let uu___6 = FStar_Syntax_Free.names t0 in + FStar_Compiler_Effect.op_Bar_Greater uu___6 + FStar_Compiler_Util.set_elements in + let getfreeV t2 = + match t2.FStar_SMTEncoding_Term.tm with + | FStar_SMTEncoding_Term.FreeV fv -> fv + | uu___6 -> + failwith + "Impossible: getfreeV: gen_term_var should always returns a FreeV" in + let uu___6 = + FStar_Compiler_List.fold_left + (fun uu___7 -> + fun bv -> + match uu___7 with + | (env1, decls, vars, tms, guards) -> + let uu___8 = + FStar_TypeChecker_Env.lookup_bv + env1.FStar_SMTEncoding_Env.tcenv bv in + (match uu___8 with + | (sort, uu___9) -> + let uu___10 = + FStar_SMTEncoding_Env.gen_term_var + env1 bv in + (match uu___10 with + | (sym, smt_tm, env2) -> + let fv = getfreeV smt_tm in + let uu___11 = + let uu___12 = norm env2 sort in + encode_term_pred + FStar_Pervasives_Native.None + uu___12 env2 smt_tm in + (match uu___11 with + | (guard, decls') -> + (env2, + (FStar_Compiler_List.op_At + decls' decls), (fv :: + vars), (smt_tm :: tms), + (guard :: guards)))))) + (env, [], [], [], []) fvs in + (fvs, uu___6) in + match uu___5 with + | (fstar_fvs, + (env1, fv_decls, fv_vars, fv_tms, fv_guards)) -> + let fv_decls1 = FStar_Compiler_List.rev fv_decls in + let fv_vars1 = FStar_Compiler_List.rev fv_vars in + let fv_tms1 = FStar_Compiler_List.rev fv_tms in + let fv_guards1 = FStar_Compiler_List.rev fv_guards in + let arg_sorts = + FStar_Compiler_List.map + (fun uu___6 -> FStar_SMTEncoding_Term.Term_sort) + fv_tms1 in + let tdecl = + FStar_SMTEncoding_Term.DeclFun + (tsym, arg_sorts, + FStar_SMTEncoding_Term.Term_sort, + FStar_Pervasives_Native.None) in + let tapp = + FStar_SMTEncoding_Util.mkApp (tsym, fv_tms1) in + let t_kinding = + let a_name = + Prims.op_Hat "non_total_function_typing_" tsym in + let axiom = + let uu___6 = + let uu___7 = + let uu___8 = + let uu___9 = + FStar_SMTEncoding_Term.mk_HasType tapp + FStar_SMTEncoding_Term.mk_Term_type in + [uu___9] in + [uu___8] in + let uu___8 = + let uu___9 = + let uu___10 = + FStar_SMTEncoding_Util.mk_and_l + fv_guards1 in + let uu___11 = + FStar_SMTEncoding_Term.mk_HasType tapp + FStar_SMTEncoding_Term.mk_Term_type in + (uu___10, uu___11) in + FStar_SMTEncoding_Util.mkImp uu___9 in + (uu___7, fv_vars1, uu___8) in + FStar_SMTEncoding_Term.mkForall + t0.FStar_Syntax_Syntax.pos uu___6 in + let svars = + FStar_SMTEncoding_Term.free_variables axiom in + let axiom1 = + FStar_SMTEncoding_Term.mkForall + t0.FStar_Syntax_Syntax.pos ([], svars, axiom) in + FStar_SMTEncoding_Util.mkAssume + (axiom1, + (FStar_Pervasives_Native.Some + "Typing for non-total arrows"), a_name) in + let tapp_concrete = + let uu___6 = + let uu___7 = + FStar_Compiler_List.map + (FStar_SMTEncoding_Env.lookup_term_var env0) + fstar_fvs in + (tsym, uu___7) in + FStar_SMTEncoding_Util.mkApp uu___6 in let uu___6 = let uu___7 = - let uu___8 = - let uu___9 = - let uu___10 = - let uu___11 = - FStar_SMTEncoding_Term.mk_PreType f in - FStar_SMTEncoding_Term.mk_tester "Tm_arrow" - uu___11 in - (f_has_t, uu___10) in - FStar_SMTEncoding_Util.mkImp uu___9 in - ([[f_has_t]], [fsym], uu___8) in - let uu___8 = - mkForall_fuel module_name - t0.FStar_Syntax_Syntax.pos in - uu___8 uu___7 in - (uu___6, (FStar_Pervasives_Native.Some a_name), - a_name) in - FStar_SMTEncoding_Util.mkAssume uu___5 in - let uu___5 = - FStar_SMTEncoding_Term.mk_decls tsym tkey_hash - [tdecl; t_kinding; t_interp] [] in - (t2, uu___5))) + FStar_SMTEncoding_Term.mk_decls tsym tkey_hash + [tdecl; t_kinding] [] in + FStar_Compiler_List.op_At fv_decls1 uu___7 in + (tapp_concrete, uu___6))) | FStar_Syntax_Syntax.Tm_refine uu___2 -> let uu___3 = let steps = @@ -2833,24 +2893,40 @@ and (encode_term : (match uu___2 with | (bs1, body1, opening) -> let fallback uu___3 = - let f = - FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.fresh - env.FStar_SMTEncoding_Env.current_module_name "Tm_abs" in - let decl = - FStar_SMTEncoding_Term.DeclFun - (f, [], FStar_SMTEncoding_Term.Term_sort, - (FStar_Pervasives_Native.Some - "Imprecise function encoding")) in let uu___4 = + let fvs = + let uu___5 = FStar_Syntax_Free.names t0 in + FStar_Compiler_Effect.op_Bar_Greater uu___5 + FStar_Compiler_Util.set_elements in + let tms = + FStar_Compiler_List.map + (FStar_SMTEncoding_Env.lookup_term_var env) fvs in let uu___5 = - FStar_SMTEncoding_Term.mk_fv - (f, FStar_SMTEncoding_Term.Term_sort) in - FStar_Compiler_Effect.op_Less_Bar - FStar_SMTEncoding_Util.mkFreeV uu___5 in - let uu___5 = - FStar_Compiler_Effect.op_Bar_Greater [decl] - FStar_SMTEncoding_Term.mk_decls_trivial in - (uu___4, uu___5) in + FStar_Compiler_List.map + (fun uu___6 -> FStar_SMTEncoding_Term.Term_sort) fvs in + (uu___5, tms) in + match uu___4 with + | (arg_sorts, arg_terms) -> + let f = + FStar_SMTEncoding_Env.varops.FStar_SMTEncoding_Env.fresh + env.FStar_SMTEncoding_Env.current_module_name + "Tm_abs" in + let decl = + FStar_SMTEncoding_Term.DeclFun + (f, arg_sorts, FStar_SMTEncoding_Term.Term_sort, + (FStar_Pervasives_Native.Some + "Imprecise function encoding")) in + let fv = + let uu___5 = + FStar_SMTEncoding_Term.mk_fv + (f, FStar_SMTEncoding_Term.Term_sort) in + FStar_Compiler_Effect.op_Less_Bar + FStar_SMTEncoding_Util.mkFreeV uu___5 in + let fapp = FStar_SMTEncoding_Util.mkApp (f, arg_terms) in + let uu___5 = + FStar_Compiler_Effect.op_Bar_Greater [decl] + FStar_SMTEncoding_Term.mk_decls_trivial in + (fapp, uu___5) in let is_impure rc = let uu___3 = FStar_TypeChecker_Util.is_pure_or_ghost_effect diff --git a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Env.ml b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Env.ml index 9a2631b38ac..d9859b62934 100644 --- a/ocaml/fstar-lib/generated/FStar_SMTEncoding_Env.ml +++ b/ocaml/fstar-lib/generated/FStar_SMTEncoding_Env.ml @@ -669,19 +669,15 @@ let (lookup_term_var : fun a -> let uu___ = lookup_bvar_binding env a in match uu___ with - | FStar_Pervasives_Native.None -> - let uu___1 = lookup_bvar_binding env a in - (match uu___1 with - | FStar_Pervasives_Native.None -> - let uu___2 = - let uu___3 = FStar_Syntax_Print.bv_to_string a in - let uu___4 = print_env env in - FStar_Compiler_Util.format2 - "Bound term variable not found %s in environment: %s" - uu___3 uu___4 in - failwith uu___2 - | FStar_Pervasives_Native.Some (b, t) -> t) | FStar_Pervasives_Native.Some (b, t) -> t + | FStar_Pervasives_Native.None -> + let uu___1 = + let uu___2 = FStar_Syntax_Print.bv_to_string a in + let uu___3 = print_env env in + FStar_Compiler_Util.format2 + "Bound term variable not found %s in environment: %s" uu___2 + uu___3 in + failwith uu___1 let (mk_fvb : FStar_Ident.lident -> Prims.string -> diff --git a/src/fstar/FStar.CheckedFiles.fst b/src/fstar/FStar.CheckedFiles.fst index c650f317828..030193aad40 100644 --- a/src/fstar/FStar.CheckedFiles.fst +++ b/src/fstar/FStar.CheckedFiles.fst @@ -40,7 +40,7 @@ module Dep = FStar.Parser.Dep * detect when loading the cache that the version number is same * It needs to be kept in sync with prims.fst *) -let cache_version_number = 58 +let cache_version_number = 59 (* * Abbreviation for what we store in the checked files (stages as described below) diff --git a/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst b/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst index a5ddc5b959f..e2d1f8e63fa 100644 --- a/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst +++ b/src/smtencoding/FStar.SMTEncoding.EncodeTerm.fst @@ -677,7 +677,7 @@ and encode_term (t:typ) (env:env_t) : (term (* encoding of t, expects t let fsym = mk_fv (varops.fresh module_name "f", Term_sort) in let f = mkFreeV fsym in let app = mk_Apply f vars in - let tcenv_bs = { Env.push_binders env.tcenv binders with lax=true } in + let tcenv_bs = { env'.tcenv with lax=true } in let pre_opt, res_t = TcUtil.pure_or_ghost_pre_and_post tcenv_bs res in let res_pred, decls' = encode_term_pred None res_t env' app in let guards, guard_decls = match pre_opt with @@ -789,29 +789,70 @@ and encode_term (t:typ) (env:env_t) : (term (* encoding of t, expects t ([], vars, mk_and_l (guards_l@[ct]@effect_args)) in let tkey_hash = "Non_total_Tm_arrow" ^ (hash_of_term tkey) ^ "@Effect=" ^ (c |> U.comp_effect_name |> string_of_lid) in - BU.digest_of_string tkey_hash in + BU.digest_of_string tkey_hash + in let tsym = "Non_total_Tm_arrow_" ^ tkey_hash in - let tdecl = Term.DeclFun(tsym, [], Term_sort, None) in - let t = mkApp(tsym, []) in + (* We need to compute all free variables of this arrow + expression and parametrize the encoding wrt to them. See + issue #3028 *) + let env0 = env in + let fstar_fvs, (env, fv_decls, fv_vars, fv_tms, fv_guards) = + let fvs = Free.names t0 |> BU.set_elements in + + let getfreeV (t:term) : fv = + match t.tm with + | FreeV fv -> fv + | _ -> failwith "Impossible: getfreeV: gen_term_var should always returns a FreeV" + in + + fvs, + List.fold_left (fun (env, decls, vars, tms, guards) bv -> + (* Get the sort from the environment, do not trust .sort field *) + let (sort, _) = Env.lookup_bv env.tcenv bv in + (* Generate a fresh SMT variable for this bv *) + let sym, smt_tm, env = gen_term_var env bv in + let fv = getfreeV smt_tm in + (* Generate typing predicate for it at the sort type *) + let guard, decls' = encode_term_pred None (norm env sort) env smt_tm in + (env, decls'@decls, fv::vars, smt_tm::tms, guard::guards) + ) (env, [], [], [], []) fvs + in + (* Putting in "correct" order... but does it matter? *) + let fv_decls = List.rev fv_decls in + let fv_vars = List.rev fv_vars in + let fv_tms = List.rev fv_tms in + let fv_guards = List.rev fv_guards in + + let arg_sorts = List.map (fun _ -> Term_sort) fv_tms in + let tdecl = Term.DeclFun(tsym, arg_sorts, Term_sort, None) in + let tapp = mkApp(tsym, fv_tms) in let t_kinding = let a_name = "non_total_function_typing_" ^tsym in - Util.mkAssume(mk_HasType t mk_Term_type, - Some "Typing for non-total arrows", - a_name) in - let fsym = mk_fv ("f", Term_sort) in - let f = mkFreeV fsym in - let f_has_t = mk_HasType f t in - let t_interp = - let a_name = "pre_typing_" ^tsym in - Util.mkAssume(mkForall_fuel module_name t0.pos ([[f_has_t]], - [fsym], - mkImp(f_has_t, - mk_tester "Tm_arrow" (mk_PreType f))), - Some a_name, - a_name) in + let axiom = + (* We generate: + forall v1 .. vn, (v1 hasType t1 /\ ... vn hasType tn) ==> tapp hasType Type *) + (* NB: we use the conlusion (HasType tapp Type) as the pattern. Though Z3 + will probably pick the same one if left empty. *) + mkForall t0.pos ([[mk_HasType tapp mk_Term_type]], fv_vars, + mkImp (mk_and_l fv_guards, mk_HasType tapp mk_Term_type)) + in + (* We furthermore must close over any variable that is + still free in the axiom. This can happen since the types + of the fvs we are closing over above may not be closed + in the current env. *) + let svars = Term.free_variables axiom in + let axiom = mkForall t0.pos ([], svars, axiom) in + Util.mkAssume (axiom, Some "Typing for non-total arrows", a_name) + in - t, mk_decls tsym tkey_hash [tdecl; t_kinding; t_interp] [] + (* The axiom above is generated over a universal quantification of + the free variables, but the actual encoding of this instance of the + arrow is applied to (the encoding of) the actual free variables at + this point. *) + + let tapp_concrete = mkApp(tsym, List.map (lookup_term_var env0) fstar_fvs) in + tapp_concrete, fv_decls @ mk_decls tsym tkey_hash [tdecl ; t_kinding ] [] | Tm_refine _ -> let x, f = @@ -1122,9 +1163,20 @@ and encode_term (t:typ) (env:env_t) : (term (* encoding of t, expects t | Tm_abs {bs; body; rc_opt=lopt} -> let bs, body, opening = SS.open_term' bs body in let fallback () = + let arg_sorts, arg_terms = + (* We need to compute all free variables of this lambda + expression and parametrize the encoding wrt to them. See + issue #3028 *) + let fvs = Free.names t0 |> BU.set_elements in + let tms = List.map (lookup_term_var env) fvs in + (List.map (fun _ -> Term_sort) fvs <: list sort), + tms + in let f = varops.fresh env.current_module_name "Tm_abs" in - let decl = Term.DeclFun(f, [], Term_sort, Some "Imprecise function encoding") in - mkFreeV <| mk_fv (f, Term_sort), [decl] |> mk_decls_trivial + let decl = Term.DeclFun(f, arg_sorts, Term_sort, Some "Imprecise function encoding") in + let fv : term = mkFreeV <| mk_fv (f, Term_sort) in + let fapp = mkApp (f, arg_terms) in + fapp, [decl] |> mk_decls_trivial in let is_impure (rc:S.residual_comp) = diff --git a/src/smtencoding/FStar.SMTEncoding.Env.fst b/src/smtencoding/FStar.SMTEncoding.Env.fst index 6b722b7c3e5..0fce15c3477 100644 --- a/src/smtencoding/FStar.SMTEncoding.Env.fst +++ b/src/smtencoding/FStar.SMTEncoding.Env.fst @@ -206,6 +206,9 @@ let fresh_fvar mname x s = let xsym = varops.fresh mname x in xsym, mkFreeV <| m let gen_term_var (env:env_t) (x:bv) = let ysym = "@x"^(string_of_int env.depth) in let y = mkFreeV <| mk_fv (ysym, Term_sort) in + (* Note: the encoding of impure function arrows (among other places + probably) relies on the fact that this is exactly a FreeV. See getfreeV in + FStar.SMTEncoding.EncodeTerm.fst *) ysym, y, {env with bvar_bindings=add_bvar_binding (x, y) env.bvar_bindings ; tcenv = Env.push_bv env.tcenv x ; depth = env.depth + 1 } @@ -228,13 +231,11 @@ let push_term_var (env:env_t) (x:bv) (t:term) = let lookup_term_var env a = match lookup_bvar_binding env a with - | None -> - (match lookup_bvar_binding env a with - | None -> failwith (BU.format2 "Bound term variable not found %s in environment: %s" - (Print.bv_to_string a) - (print_env env)) - | Some (b,t) -> t) | Some (b,t) -> t + | None -> + failwith (BU.format2 "Bound term variable not found %s in environment: %s" + (Print.bv_to_string a) + (print_env env)) (* Qualified term names *) let mk_fvb lid fname arity ftok fuel_partial_app thunked = diff --git a/src/smtencoding/FStar.SMTEncoding.Term.fsti b/src/smtencoding/FStar.SMTEncoding.Term.fsti index 3f27cfd690e..0cd08cebcc7 100644 --- a/src/smtencoding/FStar.SMTEncoding.Term.fsti +++ b/src/smtencoding/FStar.SMTEncoding.Term.fsti @@ -88,7 +88,7 @@ type term' = | LblPos of term * string and pat = term and term = {tm:term'; freevars:Syntax.memo fvs; rng:Range.range} -and fv = string * sort * bool +and fv = string * sort * bool (* bool iff variable must be forced/unthunked *) and fvs = list fv type caption = option string diff --git a/tests/bug-reports/Bug3028.fst b/tests/bug-reports/Bug3028.fst new file mode 100644 index 00000000000..78282e98712 --- /dev/null +++ b/tests/bug-reports/Bug3028.fst @@ -0,0 +1,45 @@ +module Bug3028 + +let mk t = unit -> Dv t +let mk2 t = mk t + +let _ = assert (mk int == mk2 int) + +[@@expect_failure] +let _ = assert (mk int == mk bool) + +[@@expect_failure] +let _ = assert (mk int == mk2 bool) + +let mka (x:int) : unit -> Dv int = fun () -> x + +[@@expect_failure] +let test () = + assert (mka 1 == mka 2) + +assume val st : int -> Type + +(* This example can trigger the scoping bug shown in the comment in PR +#3028. The problem is that when we are encoding the arrow `st ii -> Dv +unit`, `ii` is bound to `reveal i`, so when we generate the typing axiom +for this impure arrow, we must not attempt to state the typing in terms of +the encoding ii. + +The current patch now just looks at the free variables of the arrows, in +this case `ii` at type `int`, and states that `Non_total_Tm_arrow_... +@x0` has type Type whenever `@x0` has type `int`, without considering +(correctly) the fact that `ii` is `reveal i`. + +The encoding of the arrow expression itself is then +`Non_total_Tm_arrow_... (reveal i)`, as this particular _instance_ is +indeed applied to `reveal i`. + +The only tricky missing bit in the explanation above is that the types +of the free variables can themselves have free variables. We just +quantify universally over those, without requiring any typing hypothesis. +*) +let t2 : Type = + i:Ghost.erased int -> Tot (let ii = Ghost.reveal i in st ii -> Dv unit) + +(* Force a query *) +let _ = assert (forall x. x+1 > x) diff --git a/tests/bug-reports/Makefile b/tests/bug-reports/Makefile index 334111eb487..39e6d80502f 100644 --- a/tests/bug-reports/Makefile +++ b/tests/bug-reports/Makefile @@ -53,7 +53,7 @@ SHOULD_VERIFY_CLOSED=Bug022.fst Bug024.fst Bug025.fst Bug026.fst Bug026b.fst Bug Bug2684a.fst Bug2684b.fst Bug2684c.fst Bug2684d.fst Bug2659b.fst\ Bug2756.fst MutualRecPositivity.fst Bug2806a.fst Bug2806b.fst Bug2806c.fst Bug2806d.fst Bug2809.fst\ Bug2849a.fst Bug2849b.fst Bug2045.fst Bug2876.fst Bug2882.fst Bug2895.fst Bug2894.fst \ - Bug2415.fst + Bug2415.fst Bug3028.fst SHOULD_VERIFY_INTERFACE_CLOSED=Bug771.fsti Bug771b.fsti SHOULD_VERIFY_AND_WARN_CLOSED=Bug016.fst diff --git a/ulib/prims.fst b/ulib/prims.fst index 46e2a9a1903..ad859033fd3 100644 --- a/ulib/prims.fst +++ b/ulib/prims.fst @@ -708,4 +708,4 @@ val string_of_int: int -> Tot string (** THIS IS MEANT TO BE KEPT IN SYNC WITH FStar.CheckedFiles.fs Incrementing this forces all .checked files to be invalidated *) irreducible -let __cache_version_number__ = 58 +let __cache_version_number__ = 59