From 78b47ac1636ccd6490877544e2df7e144f570f81 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jo=C3=A3o=20Pereira?= <joaopereira.19@gmail.com>
Date: Sat, 28 Sep 2024 19:49:35 +0200
Subject: [PATCH] Reenable chopper

---
 .github/workflows/gobra.yml | 7 +------
 1 file changed, 1 insertion(+), 6 deletions(-)

diff --git a/.github/workflows/gobra.yml b/.github/workflows/gobra.yml
index 567ba92e5..dd3d14629 100644
--- 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'