Reenable chopper (#379)

* Reenable chopper * Update .github/workflows/gobra.yml * Update .github/workflows/gobra.yml * Update .github/workflows/gobra.yml
viperproject · Feb 2, 2025 · 3b903bf · 3b903bf
1 parent 76a8578
commit 3b903bf
Showing 1 changed file with 1 addition and 6 deletions.
diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml
@@ -415,12 +415,7 @@ jobs:
           includePaths: ${{ env.includePaths }}
           assumeInjectivityOnInhale: ${{ env.assumeInjectivityOnInhale }}
           checkConsistency: ${{ env.checkConsistency }}
-          # Due to a bug introduced in https://github.com/viperproject/gobra/pull/776,
-          # we must currently disable the chopper, otherwise we well-founded orders
-          # for termination checking are not available at the chopped Viper parts.
-          # We should reenable it whenever possible, as it reduces verification time in
-          # ~8 min (20%).
-          # chop: 10
+          chop: 10
           parallelizeBranches: '1'
           conditionalizePermissions: '1'
           moreJoins: 'impure'