rlimit for higherarray

FStarLang · Mar 14, 2023 · f6205dd · f6205dd
1 parent 862fe6e
commit f6205dd
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/ulib/experimental/Steel.ST.HigherArray.fst b/ulib/experimental/Steel.ST.HigherArray.fst
@@ -645,6 +645,7 @@ let memcpy0
                            (pts_to a1 _ e0);
     return ()
 
+#push-options "--z3rlimit 50"
 let blit0 (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t))
            (src:array t)
            (idx_src: US.t)
@@ -677,6 +678,7 @@ let blit0 (#t:_) (#p0:perm) (#s0 #s1:Ghost.erased (Seq.seq t))
   vpattern_rewrite #_ #_ #(merge _ _) (fun a -> pts_to a _ _) src;
   vpattern_rewrite (pts_to src _) (Ghost.reveal s0);
   noop ()
+#pop-options
 
 #pop-options