Merge branch 'main' into gebner_phase1_matcher

Author: mtzguido

share/pulse/examples/dice/cbor/CBOR.Spec.Map.fst

@@ -335,7 +335,7 @@ let rec list_sorted_append_chunk_elim
     end
   | _ :: l1' -> list_sorted_append_chunk_elim order l1' l2 l3
 
-#push-options "--query_stats --fuel 2 --ifuel 1 --z3rlimit_factor 4 --split_queries no"
+#push-options "--fuel 2 --ifuel 1 --z3rlimit_factor 4 --split_queries no"
 #restart-solver
 let rec map_sort_merge_correct
   (#t1 #t2: Type)
@@ -465,7 +465,7 @@ let list_memP_map_forall
 = Classical.forall_intro (fun y -> List.Tot.memP_map_elim f y l);
   Classical.forall_intro (fun x -> List.Tot.memP_map_intro f x l)
 
-#push-options "--z3rlimit_factor 6 --split_queries no --query_stats"
+#push-options "--z3rlimit_factor 6 --split_queries no"
 
 #restart-solver
 let rec map_sort_correct

share/pulse/examples/dice/dpe/DPE.Messages.Parse.fst

@@ -226,7 +226,7 @@ let parse_dpe_cmd_post
       )
 
 
-#push-options "--z3rlimit_factor 2 --fuel 2 --ifuel 1 --query_stats"
+#push-options "--z3rlimit_factor 2 --fuel 2 --ifuel 1"
 #restart-solver
 fn parse_dpe_cmd (#s:erased (Seq.seq U8.t))
                  (#p:perm)

src/checker/Pulse.Checker.Abs.fst

@@ -435,7 +435,7 @@ let close_ascription (c:comp_ascription) (nv:nvar) : comp_ascription =
   subst_ascription c [RT.ND (snd nv) 0]
 
 module R = FStar.Reflection.V2
-#push-options "--z3rlimit_factor 20 --fuel 0 --ifuel 1 --split_queries no --query_stats"
+#push-options "--z3rlimit_factor 20 --fuel 0 --ifuel 1 --split_queries no"
 #restart-solver
 let rec check_abs_core
   (g:env)

src/checker/Pulse.Checker.Base.fst

@@ -613,7 +613,6 @@ let return_in_ctxt (g:env) (y:var) (y_ppname:ppname) (u:universe) (ty:term) (ctx
 
 #push-options "--z3rlimit_factor 4 --ifuel 1 --split_queries always"
 #restart-solver
-#show-options
 let match_comp_res_with_post_hint (#g:env) (#t:st_term) (#c:comp_st)
   (d:st_typing g t c)
   (post_hint:post_hint_opt g)

src/checker/Pulse.Checker.Bind.fst

@@ -31,7 +31,7 @@ module Metatheory = Pulse.Typing.Metatheory
 module Abs = Pulse.Checker.Abs
 module RU = Pulse.Reflection.Util
 
-#push-options "--z3rlimit_factor 8 --split_queries no --query_stats --fuel 0 --ifuel 1"
+#push-options "--z3rlimit_factor 8 --split_queries no --fuel 0 --ifuel 1"
 let check_bind_fn
   (g:env)
   (ctxt:slprop)

src/checker/Pulse.Checker.Match.fst

@@ -139,7 +139,7 @@ let lemma_map_opt_dec_index (top:'z) (f : (x:'a{x << top}) -> option 'b) (xs : l
           (ensures forall i. f (xs `L.index` i) == Some (ys `L.index` i))
   = Classical.forall_intro (Classical.move_requires (__lemma_map_opt_dec_index top f xs ys))
 
-#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 2 --query_stats"
+#push-options "--fuel 2 --ifuel 2 --z3rlimit_factor 2"
 #restart-solver
 let rec elab_readback_pat_x (rp : R.pattern) (p : pattern)
   : Lemma (requires readback_pat rp == Some p)
@@ -538,7 +538,7 @@ let check_branches
   let brs = List.Tot.map dfst checked_brs in
   let d : brs_typing g sc_u sc_ty sc brs c0 = check_branches_aux2 g sc_u sc_ty sc c0 checked_brs in
   (| brs, c0, d |)
-#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 4 --query_stats"
+#push-options "--fuel 0 --ifuel 1 --z3rlimit_factor 4"
 let check
         (g:env)
         (pre:term)

src/checker/Pulse.Checker.Return.fst

@@ -69,7 +69,7 @@ let compute_tot_or_ghost_term_type_and_u (g:env) (e:term) (c:option ctag)
   let (| c, e, d |) = check_effect d c in
   R c e u ty ud d
 
-#push-options "--z3rlimit_factor 16 --fuel 0 --ifuel 1 --query_stats --split_queries no --log_queries"
+#push-options "--z3rlimit_factor 16 --fuel 0 --ifuel 1 --split_queries no"
 #restart-solver
 let check_core
   (g:env)

src/checker/Pulse.Checker.While.fst

@@ -38,7 +38,7 @@ let while_body_comp_typing (#g:env) (u:universe) (x:ppname) (ty:term) (inv_body:
   : Dv (comp_typing_u g (comp_while_body x inv_body))
   = Metatheory.admit_comp_typing g (comp_while_body x inv_body)
 
-#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 8 --query_stats"
+#push-options "--fuel 0 --ifuel 0 --z3rlimit_factor 8"
 #restart-solver
 let check
   (g:env)

src/checker/Pulse.Checker.WithInv.fst

@@ -236,7 +236,7 @@ let withinv_post (#g:env) (#p:term) (#i:term) (#post:term)
   let (| post, _, post_typing |) = normalize_slprop_welltyped g post post_typing in
   __withinv_post #g #p #i #post p_typing i_typing post_typing
 
-#push-options "--fuel 0 --ifuel 0 --query_stats" 
+#push-options "--fuel 0 --ifuel 0" 
 #restart-solver
 let mk_post_hint g returns_inv i p (ph:post_hint_opt g) rng
 : T.Tac (q:post_hint_for_env g { PostHint? ph ==> q == PostHint?.v ph })

src/checker/Pulse.Checker.WithLocal.fst

@@ -46,7 +46,7 @@ let with_local_pre_typing (#g:env) (#pre:term) (pre_typing:tot_typing g pre tm_s
                tm_slprop
   = admit()
 
-#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 0 --query_stats"
+#push-options "--z3rlimit_factor 10 --fuel 0 --ifuel 0"
 
 let head_range (t:st_term {Tm_WithLocal? t.term}) : range =
   let Tm_WithLocal { initializer } = t.term in