diff --git a/LabeledCryptoAPI.fsti b/LabeledCryptoAPI.fsti
index 4f62a3f..93d13a2 100644
--- a/LabeledCryptoAPI.fsti
+++ b/LabeledCryptoAPI.fsti
@@ -507,12 +507,12 @@ val mac_lemma: #p:global_usage -> #i:timestamp -> #l:label -> #l':label ->
 
 val verify_mac: #p:global_usage -> #i:timestamp -> #l:label -> #l':label ->
     k:lbytes p i l{is_publishable p i k \/ (exists s. is_mac_key p i k l s)} ->
-    m:msg p i l'{forall s. is_mac_key p i k l s ==> mac_pred p.usage_preds i s k m} -> 
+    m:msg p i l' -> 
     t:msg p i l' -> bool
 
 val verify_mac_lemma: #p:global_usage -> #i:timestamp -> #l:label -> #l':label ->
     k:lbytes p i l{is_publishable p i k \/ (exists s. is_mac_key p i k l s)} ->
-    m:msg p i l'{forall s. is_mac_key p i k l s ==> mac_pred p.usage_preds i s k m} ->
+    m:msg p i l' ->
     t:msg p i l' ->
     Lemma (if verify_mac k m t then 
 	      C.verify_mac k m t /\
diff --git a/Makefile b/Makefile
index 5439244..80e6521 100644
--- a/Makefile
+++ b/Makefile
@@ -26,7 +26,7 @@ FSTAR_FLAGS = --cmi \
   --already_cached "+Prims +FStar +LowStar +C +Spec.Loops +TestLib" \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
-FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS) --z3version 4.13.3
 
 ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
 
diff --git a/Makefile.concrete b/Makefile.concrete
index e53df56..278cced 100644
--- a/Makefile.concrete
+++ b/Makefile.concrete
@@ -28,7 +28,7 @@ FSTAR_FLAGS = --cmi \
   --already_cached "+Prims +FStar +LowStar +C +TestLib" \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
-FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS) --z3version 4.13.3
 
 ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
 
diff --git a/SecurityLemmas.fst b/SecurityLemmas.fst
index d5335cc..4fac853 100644
--- a/SecurityLemmas.fst
+++ b/SecurityLemmas.fst
@@ -43,7 +43,7 @@ val attacker_only_derives_public_values_:
     (requires (valid_trace pr h /\ later_than (trace_len h) i))
     (ensures (forall t. Att.attacker_can_derive i steps t ==> is_publishable pr.global_usage i t))
 
-#push-options "--z3rlimit 50"
+#push-options "--z3rlimit 200"
 let rec attacker_only_derives_public_values_ pr h i steps =
   if steps = 0 then (
         strings_are_publishable_forall pr.global_usage;
diff --git a/comparse/Comparse.Parser.Derived.fst b/comparse/Comparse.Parser.Derived.fst
index e00c1d8..890a431 100644
--- a/comparse/Comparse.Parser.Derived.fst
+++ b/comparse/Comparse.Parser.Derived.fst
@@ -591,6 +591,7 @@ let ps_quic_nat #bytes #bl =
     a_to_b b_to_a
     a_to_b_to_a
     b_to_a_to_b
+#pop-options
 
 let ps_quic_nat_length #bytes #bl n =
   assert_norm(pow2 0 == 1);
diff --git a/comparse/Makefile b/comparse/Makefile
index ec60c23..5f49044 100644
--- a/comparse/Makefile
+++ b/comparse/Makefile
@@ -25,7 +25,7 @@ FSTAR_FLAGS = --cmi \
   --already_cached "+Prims +FStar +LowStar +C +Spec.Loops +TestLib" \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
-FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS) --z3version 4.13.3
 
 ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
 
diff --git a/comparse/Makefile.concrete b/comparse/Makefile.concrete
index 41c3c5b..7ba15c4 100644
--- a/comparse/Makefile.concrete
+++ b/comparse/Makefile.concrete
@@ -28,7 +28,7 @@ FSTAR_FLAGS = --cmi \
   --already_cached "+Prims +FStar +LowStar +C +TestLib" \
   $(addprefix --include ,$(FSTAR_INCLUDE_DIRS))
 
-FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS)
+FSTAR = $(FSTAR_HOME)/bin/fstar.exe $(FSTAR_FLAGS) $(OTHERFLAGS) --z3version 4.13.3
 
 ENABLE_HINTS = --use_hints --use_hint_hashes --record_hints # --query_stats
 
diff --git a/concrete/hacl-star-snapshot/ml/FStar_Kremlin_Endianness.ml b/concrete/hacl-star-snapshot/ml/FStar_Kremlin_Endianness.ml
old mode 100644
new mode 100755
index b4cc226..cadb4a4
--- a/concrete/hacl-star-snapshot/ml/FStar_Kremlin_Endianness.ml
+++ b/concrete/hacl-star-snapshot/ml/FStar_Kremlin_Endianness.ml
@@ -33,7 +33,7 @@ let rec (n_to_le :
          let byte = FStar_UInt8.uint_to_t (n mod (Prims.of_int (256))) in
          let n' = n / (Prims.of_int (256)) in
          let b' = n_to_le len1 n' in
-         let b = FStar_Seq_Properties.cons byte b' in b)
+         let b = FStar_Seq_Base.cons byte b' in b)
 let rec (n_to_be :
   FStar_UInt32.t -> Prims.nat -> FStar_UInt8.t FStar_Seq_Base.seq) =
   fun len ->
@@ -86,7 +86,7 @@ let rec (seq_uint32_of_le :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (4)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint32_of_le hd)
+             FStar_Seq_Base.cons (uint32_of_le hd)
                (seq_uint32_of_le (l - Prims.int_one) tl))
 let rec (le_of_seq_uint32 :
   FStar_UInt32.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -108,7 +108,7 @@ let rec (seq_uint32_of_be :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (4)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint32_of_be hd)
+             FStar_Seq_Base.cons (uint32_of_be hd)
                (seq_uint32_of_be (l - Prims.int_one) tl))
 let rec (be_of_seq_uint32 :
   FStar_UInt32.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -130,7 +130,7 @@ let rec (seq_uint64_of_le :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (8)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint64_of_le hd)
+             FStar_Seq_Base.cons (uint64_of_le hd)
                (seq_uint64_of_le (l - Prims.int_one) tl))
 let rec (le_of_seq_uint64 :
   FStar_UInt64.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
@@ -152,7 +152,7 @@ let rec (seq_uint64_of_be :
         (let uu___1 = FStar_Seq_Properties.split b (Prims.of_int (8)) in
          match uu___1 with
          | (hd, tl) ->
-             FStar_Seq_Properties.cons (uint64_of_be hd)
+             FStar_Seq_Base.cons (uint64_of_be hd)
                (seq_uint64_of_be (l - Prims.int_one) tl))
 let rec (be_of_seq_uint64 :
   FStar_UInt64.t FStar_Seq_Base.seq -> FStar_UInt8.t FStar_Seq_Base.seq) =
diff --git a/concrete/hacl-star-snapshot/ml/Lib_Meta.ml b/concrete/hacl-star-snapshot/ml/Lib_Meta.ml
old mode 100644
new mode 100755
index 901410e..491e1a4
--- a/concrete/hacl-star-snapshot/ml/Lib_Meta.ml
+++ b/concrete/hacl-star-snapshot/ml/Lib_Meta.ml
@@ -67,5 +67,5 @@ let rec (as_uint8s :
 let (from_hex :
   Prims.string -> (FStar_UInt8.t, unit) FStar_Seq_Properties.lseq) =
   fun s ->
-    FStar_Seq_Properties.seq_of_list
-      (as_uint8s [] (FStar_String.list_of_string s))
\ No newline at end of file
+    FStar_Seq_Base.seq_of_list
+      (as_uint8s [] (FStar_String.list_of_string s))
diff --git a/concrete/hacl-star-snapshot/ml/Lib_Sequence.ml b/concrete/hacl-star-snapshot/ml/Lib_Sequence.ml
old mode 100644
new mode 100755
index 40c90fb..0d6ba97
--- a/concrete/hacl-star-snapshot/ml/Lib_Sequence.ml
+++ b/concrete/hacl-star-snapshot/ml/Lib_Sequence.ml
@@ -20,9 +20,9 @@ let op_At_Bar :
       Prims.nat -> ('a, unit) lseq -> ('a, unit) lseq -> ('a, unit) lseq
   = fun len0 -> fun len1 -> fun s0 -> fun s1 -> concat len0 len1 s0 s1
 let to_list : 'a . 'a seq -> 'a Prims.list =
-  fun s -> FStar_Seq_Properties.seq_to_list s
+  fun s -> FStar_Seq_Base.seq_to_list s
 let of_list : 'a . 'a Prims.list -> ('a, unit) lseq =
-  fun l -> FStar_Seq_Properties.seq_of_list l
+  fun l -> FStar_Seq_Base.seq_of_list l
 
 type ('a, 'len, 's1, 's2) equal = unit
 
diff --git a/concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG.ml b/concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG.ml
old mode 100644
new mode 100755
index 10a2f7e..109d0b3
--- a/concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (is_supported_alg : Spec_Hash_Definitions.hash_alg -> Prims.bool) =
   fun uu___ ->
@@ -227,4 +231,4 @@ let (generate' :
                                   (k1, v2,
                                     ((__proj__State__item__reseed_counter a
                                         st)
-                                       + Prims.int_one)))))))
\ No newline at end of file
+                                       + Prims.int_one)))))))
diff --git a/concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG_Test.ml b/concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG_Test.ml
old mode 100644
new mode 100755
index 826a315..f9b90b4
--- a/concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG_Test.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_HMAC_DRBG_Test.ml
@@ -8,10 +8,10 @@ let (print_and_compare :
       fun test_result ->
         FStar_IO.print_string "\n\nResult:   ";
         FStar_List.iter (fun a -> FStar_IO.print_uint8_hex_pad a)
-          (FStar_Seq_Properties.seq_to_list test_result);
+          (FStar_Seq_Base.seq_to_list test_result);
         FStar_IO.print_string "\nExpected: ";
         FStar_List.iter (fun a -> FStar_IO.print_uint8_hex_pad a)
-          (FStar_Seq_Properties.seq_to_list test_expected);
+          (FStar_Seq_Base.seq_to_list test_expected);
         (let res =
            Obj.magic
              (Lib_ByteSequence.seq_eq_mask Lib_IntTypes.U8 len len
diff --git a/concrete/hacl-star-snapshot/ml/Spec_Hash_Test.ml b/concrete/hacl-star-snapshot/ml/Spec_Hash_Test.ml
old mode 100644
new mode 100755
index b4138d9..1352802
--- a/concrete/hacl-star-snapshot/ml/Spec_Hash_Test.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_Hash_Test.ml
@@ -6167,11 +6167,11 @@ let (test_one : vec -> Prims.bool) =
     match uu___ with
     | Vec (a, plain, tag) ->
         let expected =
-          FStar_Seq_Properties.seq_of_list
+          FStar_Seq_Base.seq_of_list
             (FStar_List_Tot_Base.map (fun x -> x) tag) in
         let computed =
           Spec_Agile_Hash.hash a
-            (FStar_Seq_Properties.seq_of_list
+            (FStar_Seq_Base.seq_of_list
                (FStar_List_Tot_Base.map (fun x -> x) plain)) in
         print_and_compare "\nExpected: " "\nComputed: "
           (Spec_Hash_Definitions.hash_length a) expected computed
diff --git a/concrete/hacl-star-snapshot/ml/Spec_Loops.ml b/concrete/hacl-star-snapshot/ml/Spec_Loops.ml
old mode 100644
new mode 100755
index d430cdc..a1b1afc
--- a/concrete/hacl-star-snapshot/ml/Spec_Loops.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_Loops.ml
@@ -7,7 +7,7 @@ let rec seq_map :
       then FStar_Seq_Base.empty ()
       else
         (let s' =
-           FStar_Seq_Properties.cons (f (FStar_Seq_Properties.head s))
+           FStar_Seq_Base.cons (f (FStar_Seq_Properties.head s))
              (seq_map f (FStar_Seq_Properties.tail s)) in
          s')
 let rec seq_map2 :
@@ -22,7 +22,7 @@ let rec seq_map2 :
         then FStar_Seq_Base.empty ()
         else
           (let s'' =
-             FStar_Seq_Properties.cons
+             FStar_Seq_Base.cons
                (f (FStar_Seq_Properties.head s)
                   (FStar_Seq_Properties.head s'))
                (seq_map2 f (FStar_Seq_Properties.tail s)
diff --git a/concrete/hacl-star-snapshot/ml/Spec_MD5.ml b/concrete/hacl-star-snapshot/ml/Spec_MD5.ml
old mode 100644
new mode 100755
index a794fc1..a4b8f8d
--- a/concrete/hacl-star-snapshot/ml/Spec_MD5.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_MD5.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (init_as_list : FStar_UInt32.t Prims.list) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x67452301");
@@ -546,4 +550,4 @@ let (update : unit Spec_Hash_Definitions.update_t) = update_aux
 let (pad : unit Spec_Hash_Definitions.pad_t) =
   Spec_Hash_PadFinish.pad Spec_Hash_Definitions.MD5
 let (finish : unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.MD5
\ No newline at end of file
+  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.MD5
diff --git a/concrete/hacl-star-snapshot/ml/Spec_SHA1.ml b/concrete/hacl-star-snapshot/ml/Spec_SHA1.ml
old mode 100644
new mode 100755
index 8df1d79..c0c9ad5
--- a/concrete/hacl-star-snapshot/ml/Spec_SHA1.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_SHA1.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (init_as_list : FStar_UInt32.t Prims.list) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x67452301");
@@ -353,4 +357,4 @@ let (update : unit Spec_Hash_Definitions.update_t) = update_aux
 let (pad : unit Spec_Hash_Definitions.pad_t) =
   Spec_Hash_PadFinish.pad Spec_Hash_Definitions.SHA1
 let (finish : unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.SHA1
\ No newline at end of file
+  Spec_Hash_PadFinish.finish Spec_Hash_Definitions.SHA1
diff --git a/concrete/hacl-star-snapshot/ml/Spec_SHA2.ml b/concrete/hacl-star-snapshot/ml/Spec_SHA2.ml
old mode 100644
new mode 100755
index 460cec4..777b891
--- a/concrete/hacl-star-snapshot/ml/Spec_SHA2.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_SHA2.ml
@@ -1,3 +1,8 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
+
 open Prims
 let (size_k_w : Spec_Hash_Definitions.sha2_alg -> Prims.nat) =
   fun uu___ ->
@@ -4871,4 +4876,4 @@ let (pad :
   Spec_Hash_PadFinish.pad
 let (finish :
   Spec_Hash_Definitions.sha2_alg -> unit Spec_Hash_Definitions.finish_t) =
-  Spec_Hash_PadFinish.finish
\ No newline at end of file
+  Spec_Hash_PadFinish.finish
diff --git a/concrete/hacl-star-snapshot/ml/Spec_SHA2_Constants.ml b/concrete/hacl-star-snapshot/ml/Spec_SHA2_Constants.ml
old mode 100644
new mode 100755
index 64f50c9..b9f40ab
--- a/concrete/hacl-star-snapshot/ml/Spec_SHA2_Constants.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_SHA2_Constants.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (k224_256_l : (FStar_UInt32.t, unit) FStar_List_Tot_Properties.llist) =
   [FStar_UInt32.uint_to_t (Prims.parse_int "0x428a2f98");
@@ -368,4 +372,4 @@ let (h512 : FStar_UInt64.t FStar_Seq_Base.seq) =
     FStar_UInt64.uint_to_t (Prims.parse_int "0x510e527fade682d1");
     FStar_UInt64.uint_to_t (Prims.parse_int "0x9b05688c2b3e6c1f");
     FStar_UInt64.uint_to_t (Prims.parse_int "0x1f83d9abfb41bd6b");
-    FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]
\ No newline at end of file
+    FStar_UInt64.uint_to_t (Prims.parse_int "0x5be0cd19137e2179")]
diff --git a/concrete/hacl-star-snapshot/ml/Spec_SHA2_Lemmas.ml b/concrete/hacl-star-snapshot/ml/Spec_SHA2_Lemmas.ml
old mode 100644
new mode 100755
index a492d9c..2275137
--- a/concrete/hacl-star-snapshot/ml/Spec_SHA2_Lemmas.ml
+++ b/concrete/hacl-star-snapshot/ml/Spec_SHA2_Lemmas.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let rec (ws_aux :
   Spec_Hash_Definitions.sha2_alg ->
diff --git a/concrete/hacl-star-snapshot/ml/Vale_AES_GCTR_s.ml b/concrete/hacl-star-snapshot/ml/Vale_AES_GCTR_s.ml
old mode 100644
new mode 100755
index 39c0846..0f32db4
--- a/concrete/hacl-star-snapshot/ml/Vale_AES_GCTR_s.ml
+++ b/concrete/hacl-star-snapshot/ml/Vale_AES_GCTR_s.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 type 'p is_gctr_plain_LE = unit
 type gctr_plain_LE = Vale_Def_Words_s.nat8 FStar_Seq_Base.seq
diff --git a/concrete/hacl-star-snapshot/ml/Vale_AES_OptPublic.ml b/concrete/hacl-star-snapshot/ml/Vale_AES_OptPublic.ml
old mode 100644
new mode 100755
index 728175c..3e8ab60
--- a/concrete/hacl-star-snapshot/ml/Vale_AES_OptPublic.ml
+++ b/concrete/hacl-star-snapshot/ml/Vale_AES_OptPublic.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 let (shift_gf128_key_1 : Vale_Math_Poly2_s.poly -> Vale_Math_Poly2_s.poly) =
   fun h ->
diff --git a/concrete/hacl-star-snapshot/ml/Vale_Def_Words_Seq_s.ml b/concrete/hacl-star-snapshot/ml/Vale_Def_Words_Seq_s.ml
old mode 100644
new mode 100755
index e7def6c..5081af6
--- a/concrete/hacl-star-snapshot/ml/Vale_Def_Words_Seq_s.ml
+++ b/concrete/hacl-star-snapshot/ml/Vale_Def_Words_Seq_s.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 type ('n, 'a) seqn = 'a FStar_Seq_Base.seq
 type 'a seq2 = (unit, 'a) seqn
@@ -219,4 +223,4 @@ let (seq_nat8_to_seq_uint8 :
 let (seq_uint8_to_seq_nat8 :
   FStar_UInt8.t FStar_Seq_Base.seq ->
     Vale_Def_Words_s.nat8 FStar_Seq_Base.seq)
-  = fun x -> Vale_Lib_Seqs_s.seq_map FStar_UInt8.v x
\ No newline at end of file
+  = fun x -> Vale_Lib_Seqs_s.seq_map FStar_UInt8.v x
diff --git a/concrete/hacl-star-snapshot/ml/Vale_Lib_Seqs.ml b/concrete/hacl-star-snapshot/ml/Vale_Lib_Seqs.ml
old mode 100644
new mode 100755
index a30d6cb..3f20cd3
--- a/concrete/hacl-star-snapshot/ml/Vale_Lib_Seqs.ml
+++ b/concrete/hacl-star-snapshot/ml/Vale_Lib_Seqs.ml
@@ -1,3 +1,7 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
 open Prims
 
 
diff --git a/concrete/hacl-star-snapshot/ml/Vale_SHA_SHA_helpers.ml b/concrete/hacl-star-snapshot/ml/Vale_SHA_SHA_helpers.ml
old mode 100644
new mode 100755
index ff0e67c..b2f6d45
--- a/concrete/hacl-star-snapshot/ml/Vale_SHA_SHA_helpers.ml
+++ b/concrete/hacl-star-snapshot/ml/Vale_SHA_SHA_helpers.ml
@@ -1,3 +1,8 @@
+module FStar_Seq_Properties = struct
+  include FStar_Seq_Base
+  include FStar_Seq_Properties
+end
+
 open Prims
 let op_String_Access :
   'uuuuu . unit -> 'uuuuu FStar_Seq_Base.seq -> Prims.nat -> 'uuuuu =
diff --git a/iso-dh/ISODH.Sessions.fst b/iso-dh/ISODH.Sessions.fst
index 1d2939e..66ff42f 100644
--- a/iso-dh/ISODH.Sessions.fst
+++ b/iso-dh/ISODH.Sessions.fst
@@ -16,9 +16,11 @@ let parse_session_st (serialized_session:bytes) : result session_st =
   | Some s -> Success s
   | None -> Error "could not parse session"
 
+#push-options "--z3rlimit 25"
 let serialize_valid_session_st i p si vi st =
   serialize_wf_lemma session_st (ComparseGlue.is_msg isodh_global_usage (readers [V p si vi]) i) st;
   (serialize session_st st <: bytes)
+#pop-options
 
 let parse_valid_serialize_session_st_lemma i p si vi ss =
   parse_serialize_inv_lemma #bytes session_st ss
diff --git a/iso-kem/ISOKem.Sessions.fst b/iso-kem/ISOKem.Sessions.fst
index 2f1d9a9..cb3b0dc 100644
--- a/iso-kem/ISOKem.Sessions.fst
+++ b/iso-kem/ISOKem.Sessions.fst
@@ -66,7 +66,7 @@ let serialize_valid_session_st i p si vi st =
 #push-options "--z3rlimit 100"
 let parse_valid_serialize_session_st_lemma i p si vi ss =
    match ss with
-   |InitiatorSentMsg1 b x -> ()
+   |InitiatorSentMsg1 b x -> A.can_flow_transitive i (A.get_label isokem_key_usages x) (readers [P p]) (readers [V p si vi])
    |ResponderSentMsg2 a gx gy k -> assert (includes_ids [P p] [V p si vi]);
      A.can_flow_transitive i (A.get_label isokem_key_usages k) (readers [P p]) (readers [V p si vi])
    |InitiatorSentMsg3 b gx gy k -> ()
diff --git a/nsl_pk/NSL.Protocol.fst b/nsl_pk/NSL.Protocol.fst
index 5283e88..6f531dc 100644
--- a/nsl_pk/NSL.Protocol.fst
+++ b/nsl_pk/NSL.Protocol.fst
@@ -102,7 +102,7 @@ let n_b_pred i a b n_a n_b :prop =
 	  (did_event_occur_before i b (respond a b n_a n_b)) /\
 	    was_rand_generated_before i n_b (readers [P a;P b]) (nonce_usage "NSL.nonce"))
 
-#push-options "--z3rlimit 25"
+#push-options "--z3rlimit 50"
 let initiator_receive_msg_2_helper (i:nat) (a:principal) (b:principal) (c_msg2:msg i public)
 				   (ska:priv_key i a) (n_a:ns_nonce i a b) :
     LCrypto (msg i (readers [P a])) (pki nsl) (requires (fun _ -> True)) (ensures (fun t0 (n_b) t1 -> n_b_pred i a b n_a n_b))
diff --git a/start_dev_env.sh b/start_dev_env.sh
index 589178f..5a843c6 100755
--- a/start_dev_env.sh
+++ b/start_dev_env.sh
@@ -21,7 +21,8 @@ fi
 # Initialize variables for docker call
 #docker_image="foa3ucuvi85/fstar-ocaml-emacs:3.5-b8b1265a"
 # docker_image="foa3ucuvi85/fstar-ocaml-emacs:3.7-master-71facac0"
-docker_image="foa3ucuvi85/fstar-ocaml-emacs:3.7-master-46b9698a"
+#docker_image="foa3ucuvi85/fstar-ocaml-emacs:3.7-master-46b9698a"
+docker_image="foa3ucuvi85/fstar-ocaml-emacs:latest"
 dy_home_host="${DIR}"
 dy_home_container="/home/build/dolev-yao-star"
 
diff --git a/symbolic/LabeledCryptoAPI.fst b/symbolic/LabeledCryptoAPI.fst
index 38fa9d2..2926e86 100644
--- a/symbolic/LabeledCryptoAPI.fst
+++ b/symbolic/LabeledCryptoAPI.fst
@@ -197,6 +197,7 @@ let pk #p #i #l sk = C.pk sk
 let pk_lemma #p #i #l sk = ()
 let sk_label_lemma pr i t l = ()
 
+#push-options "--ifuel 2 --z3rlimit 50"
 let pke_enc #pr #i #l k n msg =
   let c = C.pke_enc k n msg in
   assert (is_valid pr i k);
@@ -209,7 +210,7 @@ let pke_enc #pr #i #l k n msg =
   assert (is_valid pr i c);
   assert (get_label pr.key_usages c == public);
   c
-
+#pop-options
 
 let pke_enc_lemma #pr #i k n msg = ()
 
@@ -224,7 +225,7 @@ let pke_dec_lemma #i #l k c = ()
 let aead_enc #pr #i #l k iv m ad = C.aead_enc k iv m ad
 let aead_enc_lemma #pr #i #l k iv m ad = ()
 
-#push-options "--z3rlimit 25"
+#push-options "--z3rlimit 100"
 let aead_dec #pr #i #l k iv c ad =
   match C.aead_dec k iv c ad with
   | Success p -> can_flow_transitive i (get_label pr.key_usages p) public l; Success p
@@ -250,7 +251,9 @@ let verify_mac_lemma #pr #i #l #l' k m t = ()
 let hash #pr #i #l m = C.hash m
 let hash_lemma #pr #i #l m = ()
 
+#push-options "--z3rlimit 50"
 let extract #pr #i #l #l' k salt = C.extract k salt
+#pop-options
 let extract_lemma #pr #i #l #l' k salt = ()
 
 let expand #pr #i #l #l' k info = C.expand k info 
@@ -261,7 +264,7 @@ let dh_pk_lemma #pr #i #l sk = ()
 let dh_key_label_lemma pr i b = ()
 let dh_private_key_cannot_be_split b = concat_split_lemma b
  
-#push-options "--z3rlimit 25"
+#push-options "--z3rlimit 50"
 let dh #pr #i #l sk pk =
     dh_key_label_lemma pr i pk;
     let k = C.dh sk pk in
@@ -304,6 +307,7 @@ let expand_value_publishable_if_secrets_are_publishable_forall c = ()
 let extract_value_publishable_if_secrets_are_publishable_forall c = ()
 let hash_value_publishable_if_message_is_publishable_forall c = ()
 let dh_public_key_is_publishable_if_private_key_is_publishable_forall c = ()
+#pop-options
 #push-options "--z3rlimit 15"
 let dh_is_publishable_if_keys_are_publishable_forall c = ()
 let dh_is_publishable_if_private_and_public_keys_are_publishable_forall c = ()