Skip to content

Commit 35bfda5

Browse files
committedOct 19, 2021
Added unroll folder to regressions
Also, we should only use Corral on the regressions in the unroll folder. The reason is that Boogie's unrolling of nested loops is not intuitive. For example, nested loops of 5 iterations each need 25 or so unrolls in Boogie to be fully unrolled.
1 parent 1f17353 commit 35bfda5

File tree

2 files changed

+2
-0
lines changed

2 files changed

+2
-0
lines changed
 

‎.github/workflows/smack-ci.yaml

+1
Original file line numberDiff line numberDiff line change
@@ -24,6 +24,7 @@ jobs:
2424
"--exhaustive --folder=c/strings",
2525
"--exhaustive --folder=c/special",
2626
"--exhaustive --folder=c/targeted-checks",
27+
"--exhaustive --folder=c/unroll",
2728
"--exhaustive --folder=rust/array --languages=rust",
2829
"--exhaustive --folder=rust/basic --languages=rust",
2930
"--exhaustive --folder=rust/box --languages=rust",

‎test/c/unroll/config.yml

+1
Original file line numberDiff line numberDiff line change
@@ -1,2 +1,3 @@
11
skip: false
2+
verifiers: [corral]
23
flags: [--fail-on-loop-exit]

0 commit comments

Comments
 (0)