Skip to content

Commit fb78137

Browse files
committed
updated shl params
1 parent 3d87443 commit fb78137

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

specs/sources/i32_specs.move

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -263,7 +263,7 @@ public fun abs_u32_spec(v: I32): u32 {
263263
✅ Computes `v << shift`.
264264
⏮️ The function aborts unless `shift < 32`.
265265
*/
266-
#[spec(prove, target = shl, boogie_opt=b"proverOpt:O:smt.QI.EAGER_THRESHOLD=100 vcsMaxKeepGoingSplits:4 vcsSplitOnEveryAssert vcsFinalAssertTimeout:300")]
266+
#[spec(prove, target = shl, boogie_opt=b"proverOpt:O:smt.QI.EAGER_THRESHOLD=100")]
267267
public fun shl_spec(v: I32, shift: u8): I32 {
268268
asserts(shift < 32);
269269
let result = shl(v, shift);

specs/sources/i64_specs.move

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -262,7 +262,7 @@ public fun abs_u64_spec(v: I64): u64 {
262262
✅ Computes `v << shift`.
263263
⏮️ The function aborts unless `shift < 64`.
264264
*/
265-
#[spec(prove, target = shl, boogie_opt=b"vcsMaxKeepGoingSplits:4 vcsSplitOnEveryAssert vcsFinalAssertTimeout:600")]
265+
#[spec(prove, target = shl, boogie_opt=b"proverOpt:O:smt.QI.EAGER_THRESHOLD=100 vcsMaxKeepGoingSplits:4 vcsSplitOnEveryAssert vcsFinalAssertTimeout:600")]
266266
public fun shl_spec(v: I64, shift: u8): I64 {
267267
asserts(shift < 64);
268268
let result = shl(v, shift);

0 commit comments

Comments
 (0)