Fix issue in receive_confidential_proof postcondition

Author: fabian-hk

src/lib/communication/DY.Lib.Communication.Core.Lemmas.fst

@@ -207,7 +207,7 @@ val receive_confidential_proof:
     | (Some payload, tr_out) ->
       trace_invariant tr_out /\
       event_triggered tr_out receiver (CommConfReceiveMsg receiver payload <: communication_core_event a) /\
-      is_well_formed a (is_knowable_by (principal_label receiver) tr) payload
+      is_well_formed a (is_knowable_by (principal_label receiver) tr_out) payload
   ))
   [SMTPat (trace_invariant tr);
    SMTPat (receive_confidential #a comm_keys_ids receiver msg_id tr);

src/lib/communication/DY.Lib.Communication.RequestResponse.Lemmas.fst

@@ -523,7 +523,7 @@ val comm_client_send_request_injective:
 let comm_client_send_request_injective #invs #a #config #crpreds tr client client' server request request' key = ()
 #pop-options
 
-#push-options "--z3rlimit 75"
+#push-options "--z3rlimit 100"
 val request_response_property:
   {|protocol_invariants|} ->
   #a:Type -> {|comm_layer_reqres_config a|} ->