Skip to content

Commit 0ddd794

Browse files
committed
feat: added extras
1 parent 3fe7c75 commit 0ddd794

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

specs/sources/math_u128_specs.move

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -205,7 +205,7 @@ public fun lo_u128_spec(n: u128): u128 {
205205
✅ Constructs a u128 from low and high u64 components.
206206
⏮️ The function does not abort.
207207
*/
208-
#[spec(prove, target = from_lo_hi)]
208+
#[spec(prove, target = from_lo_hi, boogie_opt=b"proverOpt:O:smt.QI.LAZY_THRESHOLD=100 proverOpt:O:smt.QI.EAGER_THRESHOLD=100")]
209209
public fun from_lo_hi_spec(lo: u64, hi: u64): u128 {
210210
let result = from_lo_hi(lo, hi);
211211
let expected_result = hi.to_int().mul(1u64.to_int().shl(64u64.to_int())).add(lo.to_int());

0 commit comments

Comments
 (0)