Skip to content

Commit

Permalink
increase rlimit
Browse files Browse the repository at this point in the history
Increasing FStar.UInt rlimit seems to be necessary to build on MacOS,
unrelated to `no_inline_let`.
Increasing FStar.Seq.Properties necessary with `no_inline_let`, though
I'm not sure why.
Increasing FStar.Sequence.Base necessary with `no_inline_let` on MacOS,
but wasn't necessary on Linux.
  • Loading branch information
amosr committed Dec 15, 2023
1 parent 69dd118 commit d78eaf9
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion ulib/FStar.UInt.fst
Original file line number Diff line number Diff line change
Expand Up @@ -571,7 +571,7 @@ let lemma_lognot_value_zero #n a =
}
#pop-options

#push-options "--z3rlimit 150"
#push-options "--z3rlimit 200"
private
val lemma_mod_variation: #n:pos -> a:uint_t n ->
Lemma (a <> 0 ==> ((-a) % pow2 n) - 1 % pow2 n = (((-a) % pow2 n) - 1) % pow2 n)
Expand Down
2 changes: 1 addition & 1 deletion ulib/experimental/FStar.Sequence.Base.fst
Original file line number Diff line number Diff line change
Expand Up @@ -345,7 +345,7 @@ private let take_contains_equiv_exists_lemma () : Lemma (take_contains_equiv_exi
take_contains_equiv_exists_helper3 ty s n x
)

#push-options "--z3rlimit_factor 10 --fuel 1 --ifuel 1"
#push-options "--z3rlimit_factor 30 --fuel 1 --ifuel 1"
private let rec drop_contains_equiv_exists_helper1 (ty: Type) (s: list ty) (n: nat{n <= length s}) (x: ty)
: Lemma (requires FLT.memP x (drop s n))
(ensures (exists (i: nat).{:pattern index s i} n <= i /\ i < length s /\ index s i == x)) =
Expand Down

0 comments on commit d78eaf9

Please sign in to comment.