rlimit bump

cryspen · Dec 18, 2024 · d345143 · d345143
1 parent 20cee83
commit d345143
Showing 1 changed file with 1 addition and 0 deletions.
diff --git a/examples/barrett/src/lib.rs b/examples/barrett/src/lib.rs
@@ -23,6 +23,7 @@ pub(crate) const FIELD_MODULUS: i32 = 3329;
 /// `|result| ≤ FIELD_MODULUS / 2 · (|value|/BARRETT_R + 1)
 ///
 /// In particular, if `|value| < BARRETT_R`, then `|result| < FIELD_MODULUS`.
+#[hax::fstar::options("--z3rlimit 200")]
 #[hax::requires((i64::from(value) >= -BARRETT_R && i64::from(value) <= BARRETT_R))]
 #[hax::ensures(|result| result > -FIELD_MODULUS && result < FIELD_MODULUS &&
                    result % FIELD_MODULUS == value % FIELD_MODULUS)]