Tweak rlimit

This proof failed on the Mac build only, which is bizarre. We should
isolate it and report the failure to Z3 (if we are indeed sending it the
same query, which we should).

Author: mtzguido

ulib/FStar.Math.Fermat.fst

@@ -392,6 +392,7 @@ let binomial_prime p k =
       factorial_mod_prime p (p - k)
     end
 
+#push-options "--z3rlimit 40"
 val freshman_aux (p:int{is_prime p}) (a b:int) (i:pos{i < p}): Lemma
   ((binomial p i * pow a (p - i) * pow b i) % p == 0)
 let freshman_aux p a b i =
@@ -404,6 +405,7 @@ let freshman_aux p a b i =
     == { binomial_prime p i }
     0;
   }
+#pop-options
 
 val freshman (p:int{is_prime p}) (a b:int) : Lemma
   (pow (a + b) p % p = (pow a p + pow b p) % p)