Skip to content

Commit

Permalink
Fix rlimit
Browse files Browse the repository at this point in the history
  • Loading branch information
gebner committed Jan 10, 2025
1 parent 1b8d140 commit 2ca268c
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion ulib/FStar.ModifiesGen.fst
Original file line number Diff line number Diff line change
Expand Up @@ -1799,7 +1799,7 @@ let union_loc_of_loc_addresses #al c b preserve_liveness r n =
let union_loc_of_loc_regions #al c b preserve_liveness r =
assert (loc_equal #_ #(cls_union c) (union_loc_of_loc c b (loc_regions #_ #(c b) preserve_liveness r)) (loc_regions #_ #(cls_union c) preserve_liveness r))

#push-options "--z3rlimit 25"
#push-options "--z3rlimit 30"
let union_loc_of_loc_includes_intro
(#al: (bool -> HS.rid -> nat -> Tot Type))
(c: ((b: bool) -> Tot (cls (al b))))
Expand Down

0 comments on commit 2ca268c

Please sign in to comment.