From d34514305fa4d3455395471fe9816c48ecabb69c Mon Sep 17 00:00:00 2001 From: Karthikeyan Bhargavan Date: Wed, 18 Dec 2024 11:15:24 +0100 Subject: [PATCH] rlimit bump --- examples/barrett/src/lib.rs | 1 + 1 file changed, 1 insertion(+) diff --git a/examples/barrett/src/lib.rs b/examples/barrett/src/lib.rs index b5bc7d40e..a867459e3 100644 --- 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)]