Skip to content

Commit f0da3de

Browse files
skip i64/i128 shl specs.
1 parent 4669a4c commit f0da3de

File tree

2 files changed

+16
-2
lines changed

2 files changed

+16
-2
lines changed

specs/sources/i128_specs.move

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -244,7 +244,14 @@ public fun abs_u128_spec(v: I128): u128 {
244244
✅ Computes `v << shift`.
245245
⏮️ The function aborts unless `shift < 128`.
246246
*/
247-
#[spec(prove, target = shl, boogie_opt=b"vcsSplitOnEveryAssert vcsMaxKeepGoingSplits:4 proverOpt:O:smt.QI.EAGER_THRESHOLD=100 vcsFinalAssertTimeout:600")]
247+
#[
248+
spec(
249+
prove,
250+
target = shl,
251+
boogie_opt = b"vcsSplitOnEveryAssert vcsMaxKeepGoingSplits:4 proverOpt:O:smt.QI.EAGER_THRESHOLD=100 vcsFinalAssertTimeout:600",
252+
skip = b"skip ci run.",
253+
),
254+
]
248255
public fun shl_spec(v: I128, shift: u8): I128 {
249256
asserts(shift < 128);
250257
let result = shl(v, shift);

specs/sources/i64_specs.move

Lines changed: 8 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -206,7 +206,14 @@ public fun abs_u64_spec(v: I64): u64 {
206206
✅ Computes `v << shift`.
207207
⏮️ The function aborts unless `shift < 64`.
208208
*/
209-
#[spec(prove, target = shl, boogie_opt=b"vcsSplitOnEveryAssert vcsMaxKeepGoingSplits:4 proverOpt:O:smt.QI.EAGER_THRESHOLD=100 vcsFinalAssertTimeout:600")]
209+
#[
210+
spec(
211+
prove,
212+
target = shl,
213+
boogie_opt = b"vcsSplitOnEveryAssert vcsMaxKeepGoingSplits:4 proverOpt:O:smt.QI.EAGER_THRESHOLD=100 vcsFinalAssertTimeout:600",
214+
skip = b"skip ci run.",
215+
),
216+
]
210217
public fun shl_spec(v: I64, shift: u8): I64 {
211218
asserts(shift < 64);
212219
let result = shl(v, shift);

0 commit comments

Comments
 (0)