diff --git a/src/util/marshal.i.dfy b/src/util/marshal.i.dfy index c7afdd6..99e3906 100644 --- a/src/util/marshal.i.dfy +++ b/src/util/marshal.i.dfy @@ -151,7 +151,7 @@ module Marshal ) } - lemma decode_encode_uint64_seq_id(es: seq) + lemma {:timeLimitMultiplier 2} decode_encode_uint64_seq_id(es: seq) ensures (enc_uint64_len(es); decode_uint64_seq(seq_encode(seq_fmap(encUInt64, es))) == es) {