[CI] regenerate hints + ocaml snapshot

FStarLang · Nov 11, 2018 · c7037ac · c7037ac
1 parent a762dc2
commit c7037ac
Show file tree

Hide file tree

Showing 5 changed files with 36 additions and 42 deletions.
diff --git a/examples/tactics/CanonCommMonoid.fst.hints b/examples/tactics/CanonCommMonoid.fst.hints
@@ -88,7 +88,7 @@
         "subterm_ordering_CanonCommMonoid.Mult"
       ],
       0,
-      "b1301c09336cdf77214d9d466554ad1c"
+      "5f09f7be81586f390526d57aff6178ab"
     ],
     [
       "CanonCommMonoid.mdenote",
@@ -110,7 +110,7 @@
         "subterm_ordering_CanonCommMonoid.Mult"
       ],
       0,
-      "a94ad837e16f57bb76bea1879838ac47"
+      "a946567ce20254d549f215fa87e63c42"
     ],
     [
       "CanonCommMonoid.xsdenote",
@@ -131,7 +131,7 @@
         "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "12aeb777a294ee724fc39c1a3b0c0127"
+      "d8708790e5ae2c77e6051dd0e9780a43"
     ],
     [
       "CanonCommMonoid.flatten",
@@ -148,7 +148,7 @@
         "subterm_ordering_CanonCommMonoid.Mult"
       ],
       0,
-      "00dab1624648c1e2a1c260a8aae04e9f"
+      "e5281961269f64e0423cc9324c013cb2"
     ],
     [
       "CanonCommMonoid.flatten_correct_aux",
@@ -496,7 +496,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "f74bb0728920c572b0e15bb467ab749e"
+      "5eb3afb69298abe570de2d124e12b2d8"
     ],
     [
       "CanonCommMonoid.reification_aux",
@@ -543,7 +543,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "5630798338a409b427e369cb198cb09a"
+      "2a48e1508dc55b5aa1cbb1114636a55e"
     ],
     [
       "CanonCommMonoid.quote_list",
@@ -794,7 +794,7 @@
         "subterm_ordering_CanonCommMonoid.Mult"
       ],
       0,
-      "eef9143d774be13009a7b8f4d2b78ed1"
+      "3076af9206fdecea57304d6bc465f3a2"
     ],
     [
       "CanonCommMonoid.mdenote",
@@ -816,7 +816,7 @@
         "subterm_ordering_CanonCommMonoid.Mult"
       ],
       0,
-      "bb44086d1dec49c81854b57e546ba7a5"
+      "7f5b75a86d297befcd916677b26155ac"
     ],
     [
       "CanonCommMonoid.xsdenote",
@@ -837,7 +837,7 @@
         "projection_inverse_Prims.Cons_tl", "subterm_ordering_Prims.Cons"
       ],
       0,
-      "7d4048b1b7b2d5e9f2709a9dffa8ad89"
+      "8556c37d362e7df209c939f2212da23a"
     ],
     [
       "CanonCommMonoid.flatten",
@@ -854,7 +854,7 @@
         "subterm_ordering_CanonCommMonoid.Mult"
       ],
       0,
-      "39cda2a3f5651250bbeccfefc06c3d7a"
+      "12ecb37854c4d3b4f7695384faaf6859"
     ],
     [
       "CanonCommMonoid.apply_swap_aux_correct",
@@ -920,7 +920,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "fbcbe150df788a4d866bfc9d3acbe720"
+      "cd16ceaee7379e03e6024a656b76ae94"
     ],
     [
       "CanonCommMonoid.reification_aux",
@@ -967,7 +967,7 @@
         "subterm_ordering_Prims.Cons"
       ],
       0,
-      "2914d023828251711bea4db2d377a031"
+      "2ef36ef3647552503c817c5c1b0588a7"
     ],
     [
       "CanonCommMonoid.quote_list",

diff --git a/examples/tactics/CanonCommSwaps.fst.hints b/examples/tactics/CanonCommSwaps.fst.hints
@@ -75,7 +75,7 @@
         "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented"
       ],
       0,
-      "94a86c3c29289473f7b0a9ea5d6325ea"
+      "4248ab6f1ba00c9a23cc09401e22d196"
     ],
     [
       "CanonCommSwaps.apply_swaps",
@@ -99,7 +99,7 @@
         "subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.length"
       ],
       0,
-      "a22a3de8de497c5855c8b84929fe0386"
+      "08cb0724040d2a9fa5b9617cc56c53cc"
     ],
     [
       "CanonCommSwaps.extend_equal_counts",
@@ -187,7 +187,7 @@
         "typing_CanonCommSwaps.swap", "typing_FStar.List.Tot.Base.length"
       ],
       0,
-      "4c0542db4c1aff7da3590f03025466ef"
+      "89166833d28cde76fc0c35911e902898"
     ],
     [
       "CanonCommSwaps.append_swaps",
@@ -252,15 +252,15 @@
         "projection_inverse_Prims.Cons_hd",
         "projection_inverse_Prims.Cons_tl",
         "refinement_interpretation_CanonCommSwaps_Tm_refine_1a90870aa2e2cdbf55c12113e539b1bc",
-        "refinement_interpretation_CanonCommSwaps_Tm_refine_5d4d8348c79b3c48cb71e5bb5f681e45",
+        "refinement_interpretation_CanonCommSwaps_Tm_refine_bf9c57438e052f6804b39e7e4beba630",
         "refinement_interpretation_Prims_Tm_refine_414d0a9f578ab0048252f8c8f552b99f",
         "refinement_interpretation_Prims_Tm_refine_8d65e998a07dd53ec478e27017d9dba5",
         "refinement_interpretation_Prims_Tm_refine_ba523126f67e00e7cd55f0b92f16681d",
         "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented",
         "unit_typing"
       ],
       0,
-      "dc86c95858d20eb41c61414503c110f9"
+      "21af96c77f8b91593ca32f16da17e52b"
     ],
     [
       "CanonCommSwaps.lift_swap_cons",
@@ -346,7 +346,7 @@
         "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented"
       ],
       0,
-      "82a2060fd19a218c0f93259b3aa3c6b3"
+      "8917745f4005e8ebf989b71459cb7ae8"
     ],
     [
       "CanonCommSwaps.swap_to_front",
@@ -392,7 +392,7 @@
         "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented"
       ],
       0,
-      "3f3b099c5f6e831d2b0c54e2736b91f0"
+      "ae20b6752474da3eed4de59758e3fd38"
     ],
     [
       "CanonCommSwaps.swap_to_front",
@@ -438,7 +438,7 @@
         "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented"
       ],
       0,
-      "42f686df4362f087623e68906e4b3479"
+      "c128083636d2a9b3253bbf08927735be"
     ],
     [
       "CanonCommSwaps.equal_counts_implies_swaps",
@@ -477,7 +477,7 @@
         "typing_FStar.List.Tot.Base.length"
       ],
       0,
-      "55a0ecc48bb8b634f9a97ca7a9ffe1ca"
+      "1abd1c63b6f53cba4472675910daf334"
     ],
     [
       "CanonCommSwaps.apply_swap_aux",
@@ -531,7 +531,7 @@
         "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented"
       ],
       0,
-      "f048a545e7887dc24eb08a8aa9b909a1"
+      "42852db46994035eaf1f717ca43a5f58"
     ],
     [
       "CanonCommSwaps.apply_swaps",
@@ -556,7 +556,7 @@
         "subterm_ordering_Prims.Cons", "typing_FStar.List.Tot.Base.length"
       ],
       0,
-      "101e672c038e7e757ee8c11b6e512a23"
+      "c36a5845537cfbf05d48ffa17f46fcf1"
     ],
     [
       "CanonCommSwaps.append_swaps",
@@ -637,7 +637,7 @@
         "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented"
       ],
       0,
-      "ca8cd50ac6acf90369a48934bb6cd197"
+      "e5e755d56e8137ff84168f626a7cab77"
     ],
     [
       "CanonCommSwaps.swap_to_front",
@@ -646,7 +646,7 @@
       1,
       [ "@query" ],
       0,
-      "0c5424c1ef45b4afcb657d7844d5b84d"
+      "70240f89dfca5a56a9da887d64ab07a0"
     ],
     [
       "CanonCommSwaps.swap_to_front",
@@ -692,7 +692,7 @@
         "token_correspondence_FStar.List.Tot.Base.length.fuel_instrumented"
       ],
       0,
-      "e432027e838957a867c12ed2e8da4104"
+      "c636440f6bc8cd5943d011cc843dd5c5"
     ],
     [
       "CanonCommSwaps.equal_counts_implies_swaps",
@@ -731,7 +731,7 @@
         "typing_FStar.List.Tot.Base.length"
       ],
       0,
-      "51b45fbf497100823fe7f4184d0814f4"
+      "9f2c17b43a8f70fa4c3111ad09d0467c"
     ]
   ]
 ]
diff --git a/src/ocaml-output/FStar_Options.ml b/src/ocaml-output/FStar_Options.ml
@@ -3018,14 +3018,14 @@ let (initial_ifuel : unit -> Prims.int) =
 
 let (interactive : unit -> Prims.bool) =
   fun uu____10709  -> (get_in ()) || (get_ide ()) 
-let (keep_query_captions : unit -> Prims.bool) =
-  fun uu____10716  -> get_keep_query_captions () 
-let (lax : unit -> Prims.bool) = fun uu____10723  -> get_lax () 
+let (lax : unit -> Prims.bool) = fun uu____10716  -> get_lax () 
 let (load : unit -> Prims.string Prims.list) =
-  fun uu____10732  -> get_load () 
-let (legacy_interactive : unit -> Prims.bool) = fun uu____10739  -> get_in () 
+  fun uu____10725  -> get_load () 
+let (legacy_interactive : unit -> Prims.bool) = fun uu____10732  -> get_in () 
 let (log_queries : unit -> Prims.bool) =
-  fun uu____10746  -> get_log_queries () 
+  fun uu____10739  -> get_log_queries () 
+let (keep_query_captions : unit -> Prims.bool) =
+  fun uu____10746  -> (log_queries ()) && (get_keep_query_captions ()) 
 let (log_types : unit -> Prims.bool) = fun uu____10753  -> get_log_types () 
 let (max_fuel : unit -> Prims.int) = fun uu____10760  -> get_max_fuel () 
 let (max_ifuel : unit -> Prims.int) = fun uu____10767  -> get_max_ifuel () 

diff --git a/src/ocaml-output/FStar_SMTEncoding_Term.ml b/src/ocaml-output/FStar_SMTEncoding_Term.ml
@@ -1906,7 +1906,7 @@ let rec (declToSmt' : Prims.bool -> Prims.string -> decl -> Prims.string) =
                 FStar_List.map (declToSmt' print_captions z3options) decls
                  in
               FStar_All.pipe_right uu____7661 (FStar_String.concat "\n")  in
-            let uu____7671 = FStar_Options.log_queries ()  in
+            let uu____7671 = FStar_Options.keep_query_captions ()  in
             if uu____7671
             then
               let uu____7675 =
@@ -2001,10 +2001,7 @@ let rec (declToSmt' : Prims.bool -> Prims.string -> decl -> Prims.string) =
 and (declToSmt : Prims.string -> decl -> Prims.string) =
   fun z3options  ->
     fun decl  ->
-      let uu____7897 =
-        (FStar_Options.log_queries ()) &&
-          (FStar_Options.keep_query_captions ())
-         in
+      let uu____7897 = FStar_Options.keep_query_captions ()  in
       declToSmt' uu____7897 z3options decl
 
 and (declToSmt_no_caps : Prims.string -> decl -> Prims.string) =

diff --git a/src/ocaml-output/FStar_SMTEncoding_Z3.ml b/src/ocaml-output/FStar_SMTEncoding_Z3.ml
@@ -1067,10 +1067,7 @@ let (mk_input :
             let ps = FStar_String.concat "\n" ps_lines  in
             let ss = FStar_String.concat "\n" ss_lines  in
             let hs =
-              let uu____5794 =
-                (FStar_Options.log_queries ()) &&
-                  (FStar_Options.keep_query_captions ())
-                 in
+              let uu____5794 = FStar_Options.keep_query_captions ()  in
               if uu____5794
               then
                 let uu____5798 =