Skip to content

Commit 46ab6b6

Browse files
committed
lo_spec patch
1 parent 0ddd794 commit 46ab6b6

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
@@ -166,7 +166,7 @@ public fun hi_spec(n: u128): u64 {
166166
✅ Extracts the low 64 bits of a u128 value.
167167
⏮️ The function does not abort.
168168
*/
169-
#[spec(prove, target = lo)]
169+
#[spec(prove, target = lo, boogie_opt=b"proverOpt:O:smt.QI.LAZY_THRESHOLD=100 proverOpt:O:smt.QI.EAGER_THRESHOLD=100")]
170170
public fun lo_spec(n: u128): u64 {
171171
let n_int = n.to_int();
172172
let result = lo(n);

0 commit comments

Comments
 (0)