Try adding a timeLimitMultiplier

mit-pdos · Oct 16, 2024 · e919ddd · e919ddd
1 parent 7bc9563
commit e919ddd
Showing 1 changed file with 1 addition and 1 deletion.
diff --git 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<uint64>)
+  lemma {:timeLimitMultiplier 2} decode_encode_uint64_seq_id(es: seq<uint64>)
     ensures (enc_uint64_len(es);
              decode_uint64_seq(seq_encode(seq_fmap(encUInt64, es))) == es)
   {