diff --git a/.github/workflows/build-test.yml b/.github/workflows/build-test.yml
index 06a01c2673..34b83a768d 100644
--- a/.github/workflows/build-test.yml
+++ b/.github/workflows/build-test.yml
@@ -96,7 +96,7 @@ jobs:
         uses: mikepenz/action-junit-report@v2
         with:
           report_paths: '**/target/test-reports/TEST-*.xml'
-      
+
   integration-test-linux:
     needs: build-test
     runs-on: ubuntu-latest
@@ -119,7 +119,7 @@ jobs:
           name: vercors-debian-package
       - run: "sudo dpkg -i *.deb"
       - run: vercors --silicon examples/manual/fibonacci.pvl
-      - run: SPLIT=${{ matrix.testID }}/${{ env.maxTestID }} vercors --test=examples --test-workers=2 --tool carbon --tool silicon --exclude-suite=slow,medium,problem-fail --progress --actions-test-output --enable-test-coverage --coverage-output-file=jacoco_${{ matrix.testID }}_${{ env.maxTestID }}.xml
+      - run: SPLIT=${{ matrix.testID }}/${{ env.maxTestID }} vercors --test=examples --test-workers=2 --tool carbon --tool silicon --tool veymont --exclude-suite=slow,medium,problem-fail --progress --actions-test-output --enable-test-coverage --coverage-output-file=jacoco_${{ matrix.testID }}_${{ env.maxTestID }}.xml
       - name: Archive Java Code Coverage (jacoco_n_m.xml)
         uses: actions/upload-artifact@v2
         with:
@@ -186,6 +186,23 @@ jobs:
       - run: tar --strip-components=1 --directory vercorszip -xf vercors.zip
       - run: vercorszip/bin/vercors --test=examples/basic --test-workers=2 --tool carbon --tool silicon --exclude-suite=slow,medium,problem-fail --progress --actions-test-output
 
+  integration-test-veymont:
+    needs: build-test
+    runs-on: ubuntu-latest
+    steps:
+      # Need to check out the repo for the "examples" directory and the veymont 2stage testing script
+      - uses: actions/checkout@v2
+      - uses: actions/setup-java@v1
+        with:
+          java-version: "11"
+          java-package: jre
+      - name: Download VerCors binary
+        uses: actions/download-artifact@v2
+        with:
+          name: vercors-debian-package
+      - run: "sudo dpkg -i *.deb"
+      - run: ./util/veymontTesting/veymont-2stage-tests.sh
+
   sonar:
     needs:
       - build-test
diff --git a/build.sbt b/build.sbt
index ba0fda340a..086a535c8c 100644
--- a/build.sbt
+++ b/build.sbt
@@ -114,9 +114,6 @@ lazy val vercors: Project = (project in file("."))
       "-deprecation"
     ),
 
-    javacOptions += "-J-Xss128M",
-    Universal / javacOptions ++= Seq("-J-Xss128M"),
-
     buildInfoKeys := Seq[BuildInfoKey](name, version, scalaVersion, sbtVersion,
       BuildInfoKey.action("currentBranch") {
         Git.currentBranch
@@ -150,6 +147,12 @@ lazy val vercors: Project = (project in file("."))
     Compile / discoveredMainClasses := Seq(),
     Compile / mainClass := Some("vct.main.Main"),
 
+    // Add options to run scripts produced by sbt-native-packager. See: https://www.scala-sbt.org/sbt-native-packager/archetypes/java_app/customize.html#via-build-sbt
+    Universal / javaOptions ++= Seq (
+      // Needed because vercors needs a pretty big stack for some files with deep expressions.
+      "-J-Xss128m"
+    ),
+
     // Make publish-local also create a test artifact, i.e., put a jar-file into the local Ivy
     // repository that contains all classes and resources relevant for testing.
     // Other projects, e.g., Carbon or Silicon, can then depend on the Sil test artifact, which
diff --git a/examples/veymont-check/checkLTS/ltstest.pvl b/examples/veymont-check/checkLTS/ltstest.pvl
index 76c0fba852..1ed2270ac1 100644
--- a/examples/veymont-check/checkLTS/ltstest.pvl
+++ b/examples/veymont-check/checkLTS/ltstest.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 
 class Role {
 	
diff --git a/examples/veymont-check/checkLTS/simpleifelse.pvl b/examples/veymont-check/checkLTS/simpleifelse.pvl
index 5ce42a8c77..b81db2eec6 100644
--- a/examples/veymont-check/checkLTS/simpleifelse.pvl
+++ b/examples/veymont-check/checkLTS/simpleifelse.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 
 class Role {
 	
diff --git a/examples/veymont-check/checkLTS/simplemethodcall.pvl b/examples/veymont-check/checkLTS/simplemethodcall.pvl
index 4bbd274ab9..4464c6dea1 100644
--- a/examples/veymont-check/checkLTS/simplemethodcall.pvl
+++ b/examples/veymont-check/checkLTS/simplemethodcall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 
 class Role {
 	
diff --git a/examples/veymont-check/checkLTS/simplewhile.pvl b/examples/veymont-check/checkLTS/simplewhile.pvl
index 0aeb48844d..280928a5b6 100644
--- a/examples/veymont-check/checkLTS/simplewhile.pvl
+++ b/examples/veymont-check/checkLTS/simplewhile.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 
 class Role {
 	
diff --git a/examples/veymont-check/checkMainClass/MainConstructorArg.pvl b/examples/veymont-check/checkMainClass/MainConstructorArg.pvl
index 6ae6920221..04bd18b138 100644
--- a/examples/veymont-check/checkMainClass/MainConstructorArg.pvl
+++ b/examples/veymont-check/checkMainClass/MainConstructorArg.pvl
@@ -2,6 +2,8 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
+
 class Main {
 
 
diff --git a/examples/veymont-check/checkMainClass/NoMain.pvl b/examples/veymont-check/checkMainClass/NoMain.pvl
index 2d7acc43de..64ec6122ce 100644
--- a/examples/veymont-check/checkMainClass/NoMain.pvl
+++ b/examples/veymont-check/checkMainClass/NoMain.pvl
@@ -1,6 +1,7 @@
 //:: cases NoMain
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
+//:: tool veymont
 //:: verdict Error
 class SomeClass {
 
diff --git a/examples/veymont-check/checkMainClass/NoMainConstructor.pvl b/examples/veymont-check/checkMainClass/NoMainConstructor.pvl
index b87612b1bd..dc88b65ba9 100644
--- a/examples/veymont-check/checkMainClass/NoMainConstructor.pvl
+++ b/examples/veymont-check/checkMainClass/NoMainConstructor.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 
diff --git a/examples/veymont-check/checkMainClass/NoMainMethod.pvl b/examples/veymont-check/checkMainClass/NoMainMethod.pvl
index bc79de71a4..428a79395f 100644
--- a/examples/veymont-check/checkMainClass/NoMainMethod.pvl
+++ b/examples/veymont-check/checkMainClass/NoMainMethod.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkMainClass/NoMainMethod2.pvl b/examples/veymont-check/checkMainClass/NoMainMethod2.pvl
index 3502be0eb5..be8745f09f 100644
--- a/examples/veymont-check/checkMainClass/NoMainMethod2.pvl
+++ b/examples/veymont-check/checkMainClass/NoMainMethod2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkMainClass/NoRunArg.pvl b/examples/veymont-check/checkMainClass/NoRunArg.pvl
index b086c57f8c..3976569560 100644
--- a/examples/veymont-check/checkMainClass/NoRunArg.pvl
+++ b/examples/veymont-check/checkMainClass/NoRunArg.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkMainClass/NoRunMethod.pvl b/examples/veymont-check/checkMainClass/NoRunMethod.pvl
index 2139aa822e..7dd59e6b95 100644
--- a/examples/veymont-check/checkMainClass/NoRunMethod.pvl
+++ b/examples/veymont-check/checkMainClass/NoRunMethod.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkMainClass/OtherMainConstructor.pvl b/examples/veymont-check/checkMainClass/OtherMainConstructor.pvl
index 774a471d16..c3b21a9335 100644
--- a/examples/veymont-check/checkMainClass/OtherMainConstructor.pvl
+++ b/examples/veymont-check/checkMainClass/OtherMainConstructor.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 
diff --git a/examples/veymont-check/checkMainClass/TwoMainConstructors.pvl b/examples/veymont-check/checkMainClass/TwoMainConstructors.pvl
index f7c67dc2e1..457566d3be 100644
--- a/examples/veymont-check/checkMainClass/TwoMainConstructors.pvl
+++ b/examples/veymont-check/checkMainClass/TwoMainConstructors.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Main() {
diff --git a/examples/veymont-check/checkMainClass/WrongRunType.pvl b/examples/veymont-check/checkMainClass/WrongRunType.pvl
index 5a59fdd5e7..b5a8623c8a 100644
--- a/examples/veymont-check/checkMainClass/WrongRunType.pvl
+++ b/examples/veymont-check/checkMainClass/WrongRunType.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorAssignmentWrongType.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorAssignmentWrongType.pvl
index c0affb8628..d800f542e5 100644
--- a/examples/veymont-check/checkMainConstructor/MainConstructorAssignmentWrongType.pvl
+++ b/examples/veymont-check/checkMainConstructor/MainConstructorAssignmentWrongType.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	int i;
diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorAssignsNoRole.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorAssignsNoRole.pvl
index 3ec563fecb..e9628b9a71 100644
--- a/examples/veymont-check/checkMainConstructor/MainConstructorAssignsNoRole.pvl
+++ b/examples/veymont-check/checkMainConstructor/MainConstructorAssignsNoRole.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Main() {
diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorBlock.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorBlock.pvl
index 7c493d2a21..b7b62a38e1 100644
--- a/examples/veymont-check/checkMainConstructor/MainConstructorBlock.pvl
+++ b/examples/veymont-check/checkMainConstructor/MainConstructorBlock.pvl
@@ -1,6 +1,7 @@
 //:: cases MainConstructorBlock
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
+//:: tool veymont
 //:: verdict Error
 class Main {
 
diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment.pvl
index dee1f90fad..60011a0894 100644
--- a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment.pvl
+++ b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	int i;
diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment2.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment2.pvl
index ea54bf493c..9667224f8a 100644
--- a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment2.pvl
+++ b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 
diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment3.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment3.pvl
index e0da6872a3..44ecf963e4 100644
--- a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment3.pvl
+++ b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment3.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	int i;
diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment4.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment4.pvl
index 6e493bee52..3e32202741 100644
--- a/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment4.pvl
+++ b/examples/veymont-check/checkMainConstructor/MainConstructorNonRoleAssignment4.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkMainConstructor/MainConstructorWrongRoleNr.pvl b/examples/veymont-check/checkMainConstructor/MainConstructorWrongRoleNr.pvl
index 9ade7c7f20..0fab322634 100644
--- a/examples/veymont-check/checkMainConstructor/MainConstructorWrongRoleNr.pvl
+++ b/examples/veymont-check/checkMainConstructor/MainConstructorWrongRoleNr.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl
index 5920bc0372..eea37ff8c9 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl
index e260ec0fed..c2e7787c51 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl
index b379be7e50..e6c3cb7ac8 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl
index 4cb0bb369a..f19a36493d 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl
index d6525cb37e..484eaf6b0a 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl
@@ -1,7 +1,8 @@
 //:: cases GuardedRecursion2
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
-//:: verdict Pass
+//:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/IfCondition.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/IfCondition.pvl
index 730c5f2a94..8702956cec 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/IfCondition.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/IfCondition.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl
index a64e1bfc61..07128054e7 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/MainMethodCall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl
index 0744b2bdcd..8c6211f892 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl
index 6c628f1b7d..18c4c38b47 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NewRoleObject.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl
index 0cf3ca9e83..cd6bc93146 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl
index 20d06fb343..1b2cb0e2c8 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/PureMethodCall.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl
index 20934ff96f..c970861143 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 	Role a;
 	
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WaitStatement.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WaitStatement.pvl
index b69d491020..23418f4b10 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WaitStatement.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WaitStatement.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WhileCondition.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WhileCondition.pvl
index 287e886bfa..48dc71f6b4 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WhileCondition.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WhileCondition.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment.pvl
index 22e9bd2001..0bc066621f 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl
index 299a3d5977..58140d165d 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongSyntax.pvl b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongSyntax.pvl
index c4c52eea8c..c6fccc835a 100644
--- a/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongSyntax.pvl
+++ b/examples/veymont-check/checkMainSyntaxAndWellFormedness/WrongSyntax.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl
index f5c02405de..7282b5f1dc 100644
--- a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl
+++ b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion2.pvl b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion2.pvl
index cf6b806657..f110ee4848 100644
--- a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion2.pvl
+++ b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion3.pvl b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion3.pvl
index 3c83b3f6f8..0e96c3cbaa 100644
--- a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion3.pvl
+++ b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion3.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion4.pvl b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion4.pvl
index 17fff4531f..c3442cb081 100644
--- a/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion4.pvl
+++ b/examples/veymont-check/checkTerminationNonMain/AbsenceRecursion4.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTerminationNonMain/ForLoop.pvl b/examples/veymont-check/checkTerminationNonMain/ForLoop.pvl
index 58c2af018c..99585f95f1 100644
--- a/examples/veymont-check/checkTerminationNonMain/ForLoop.pvl
+++ b/examples/veymont-check/checkTerminationNonMain/ForLoop.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkTerminationNonMain/LoopStatementInRole.pvl b/examples/veymont-check/checkTerminationNonMain/LoopStatementInRole.pvl
index 892dc80bd4..c4c4a57c79 100644
--- a/examples/veymont-check/checkTerminationNonMain/LoopStatementInRole.pvl
+++ b/examples/veymont-check/checkTerminationNonMain/LoopStatementInRole.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkTerminationNonMain/MainCallFromRole.pvl b/examples/veymont-check/checkTerminationNonMain/MainCallFromRole.pvl
index d8818b38b8..f60cc7cc6a 100644
--- a/examples/veymont-check/checkTerminationNonMain/MainCallFromRole.pvl
+++ b/examples/veymont-check/checkTerminationNonMain/MainCallFromRole.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a;
diff --git a/examples/veymont-check/checkTerminationNonMain/WaitStatementInRole.pvl b/examples/veymont-check/checkTerminationNonMain/WaitStatementInRole.pvl
index 5aa81ce7a1..ad161d90d2 100644
--- a/examples/veymont-check/checkTerminationNonMain/WaitStatementInRole.pvl
+++ b/examples/veymont-check/checkTerminationNonMain/WaitStatementInRole.pvl
@@ -1,6 +1,7 @@
 //:: cases WaitStatementInRole
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
+//:: tool veymont
 //:: verdict Pass
 class Main {
 
diff --git a/examples/veymont-check/checkTypesNonMain/OtherClassFieldType.pvl b/examples/veymont-check/checkTypesNonMain/OtherClassFieldType.pvl
index af2b171736..f57115144c 100644
--- a/examples/veymont-check/checkTypesNonMain/OtherClassFieldType.pvl
+++ b/examples/veymont-check/checkTypesNonMain/OtherClassFieldType.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/OtherClassFieldType2.pvl b/examples/veymont-check/checkTypesNonMain/OtherClassFieldType2.pvl
index 3152baabfe..4b10d4df42 100644
--- a/examples/veymont-check/checkTypesNonMain/OtherClassFieldType2.pvl
+++ b/examples/veymont-check/checkTypesNonMain/OtherClassFieldType2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/OtherClassMethodType.pvl b/examples/veymont-check/checkTypesNonMain/OtherClassMethodType.pvl
index 8667c97fdb..4934f3d20d 100644
--- a/examples/veymont-check/checkTypesNonMain/OtherClassMethodType.pvl
+++ b/examples/veymont-check/checkTypesNonMain/OtherClassMethodType.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/OtherClassMethodType2.pvl b/examples/veymont-check/checkTypesNonMain/OtherClassMethodType2.pvl
index 004367ff25..d9fd87900f 100644
--- a/examples/veymont-check/checkTypesNonMain/OtherClassMethodType2.pvl
+++ b/examples/veymont-check/checkTypesNonMain/OtherClassMethodType2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/RoleFieldType.pvl b/examples/veymont-check/checkTypesNonMain/RoleFieldType.pvl
index 6eccc3c22b..3fd5682f4a 100644
--- a/examples/veymont-check/checkTypesNonMain/RoleFieldType.pvl
+++ b/examples/veymont-check/checkTypesNonMain/RoleFieldType.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl b/examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl
index 3ecc5bb32f..82c4461787 100644
--- a/examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl
+++ b/examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
@@ -13,7 +14,7 @@ class Main {
 	}
 	
 	void run() {
-		a.x = 1;
+		a.x = new Other();
 	}
 	
 	void main() {
diff --git a/examples/veymont-check/checkTypesNonMain/RoleFieldType3.pvl b/examples/veymont-check/checkTypesNonMain/RoleFieldType3.pvl
index 817b0e58a9..836eb2992e 100644
--- a/examples/veymont-check/checkTypesNonMain/RoleFieldType3.pvl
+++ b/examples/veymont-check/checkTypesNonMain/RoleFieldType3.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/RoleFieldType4.pvl b/examples/veymont-check/checkTypesNonMain/RoleFieldType4.pvl
index b3aa369a12..e865a28673 100644
--- a/examples/veymont-check/checkTypesNonMain/RoleFieldType4.pvl
+++ b/examples/veymont-check/checkTypesNonMain/RoleFieldType4.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/RoleMethodType.pvl b/examples/veymont-check/checkTypesNonMain/RoleMethodType.pvl
index 7fa15fc315..0e633d05ea 100644
--- a/examples/veymont-check/checkTypesNonMain/RoleMethodType.pvl
+++ b/examples/veymont-check/checkTypesNonMain/RoleMethodType.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Pass
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/RoleMethodType2.pvl b/examples/veymont-check/checkTypesNonMain/RoleMethodType2.pvl
index 9c557579f2..9fa59fb215 100644
--- a/examples/veymont-check/checkTypesNonMain/RoleMethodType2.pvl
+++ b/examples/veymont-check/checkTypesNonMain/RoleMethodType2.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/RoleMethodType3.pvl b/examples/veymont-check/checkTypesNonMain/RoleMethodType3.pvl
index d192379418..2bc42e11f6 100644
--- a/examples/veymont-check/checkTypesNonMain/RoleMethodType3.pvl
+++ b/examples/veymont-check/checkTypesNonMain/RoleMethodType3.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-check/checkTypesNonMain/VoidField.pvl b/examples/veymont-check/checkTypesNonMain/VoidField.pvl
index 08c71c7c6a..e37fddc610 100644
--- a/examples/veymont-check/checkTypesNonMain/VoidField.pvl
+++ b/examples/veymont-check/checkTypesNonMain/VoidField.pvl
@@ -2,6 +2,7 @@
 //:: suite veymont veymont-check
 //:: option --veymont tmp.pvl
 //:: verdict Error
+//:: tool veymont
 class Main {
 
 	Role a,b,c;
diff --git a/examples/veymont-global-programs/IntGrid.pvl b/examples/veymont-global-programs/IntGrid.pvl
index 4cff7a7d38..3c042cd35b 100644
--- a/examples/veymont-global-programs/IntGrid.pvl
+++ b/examples/veymont-global-programs/IntGrid.pvl
@@ -1,5 +1,6 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases TicTacToeInt
+//:: suite problem-fail
 
 class Player {
 
diff --git a/examples/veymont-global-programs/Move.pvl b/examples/veymont-global-programs/Move.pvl
index 380c9901a6..e42674411b 100644
--- a/examples/veymont-global-programs/Move.pvl
+++ b/examples/veymont-global-programs/Move.pvl
@@ -1,5 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
-//:: cases TicTacToeInt TicTacToeMatrix
+//:: cases TicTacToeInt
 
 class Move {
 	int i, j, token;
diff --git a/examples/veymont-global-programs/TicTacToe.pvl b/examples/veymont-global-programs/TicTacToe.pvl
index 136f105a5f..f4c816de8f 100644
--- a/examples/veymont-global-programs/TicTacToe.pvl
+++ b/examples/veymont-global-programs/TicTacToe.pvl
@@ -1,6 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
-//:: cases TicTacToeInt TicTacToeMatrix
-//:: tools veymont
+//:: cases TicTacToeInt
 //:: verdict Pass
 
 class Main {
diff --git a/examples/veymont-global-programs/leaderelectring.pvl b/examples/veymont-global-programs/leaderelectring.pvl
index 718c2a7989..1c652fe609 100644
--- a/examples/veymont-global-programs/leaderelectring.pvl
+++ b/examples/veymont-global-programs/leaderelectring.pvl
@@ -1,6 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases LeaderElectRing
-//:: tools veymont
 //:: verdict Pass
 
 class Node {
diff --git a/examples/veymont-global-programs/leaderelectstar.pvl b/examples/veymont-global-programs/leaderelectstar.pvl
index 9c86b4174a..5b76756602 100644
--- a/examples/veymont-global-programs/leaderelectstar.pvl
+++ b/examples/veymont-global-programs/leaderelectstar.pvl
@@ -1,6 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases LeaderElectStar
-//:: tools veymont
 //:: verdict Pass
 
 class EndPoint {
diff --git a/examples/veymont-global-programs/paperscissorsrock.pvl b/examples/veymont-global-programs/paperscissorsrock.pvl
index d1188ca6c1..6e84f8decf 100644
--- a/examples/veymont-global-programs/paperscissorsrock.pvl
+++ b/examples/veymont-global-programs/paperscissorsrock.pvl
@@ -1,6 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases PaperScissorsRock
-//:: tools veymont
 //:: verdict Pass
 
 class Role {
diff --git a/examples/veymont-global-programs/parallel_while.pvl b/examples/veymont-global-programs/parallel_while.pvl
index 21dd9f72c6..90baa22279 100644
--- a/examples/veymont-global-programs/parallel_while.pvl
+++ b/examples/veymont-global-programs/parallel_while.pvl
@@ -1,6 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases ParallelWhile
-//:: tools veymont
 //:: verdict Pass
 
 class Role {
diff --git a/examples/veymont-global-programs/parallel_while_simplified.pvl b/examples/veymont-global-programs/parallel_while_simplified.pvl
index 5960ee7db2..fd0d17db43 100644
--- a/examples/veymont-global-programs/parallel_while_simplified.pvl
+++ b/examples/veymont-global-programs/parallel_while_simplified.pvl
@@ -1,6 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases ParallelWhileSimplified
-//:: tools veymont
 //:: verdict Pass
 
 class Role {
diff --git a/src/main/java/vct/test/CommandLineTesting.scala b/src/main/java/vct/test/CommandLineTesting.scala
index 3e8a54f15f..fc0480c1c1 100644
--- a/src/main/java/vct/test/CommandLineTesting.scala
+++ b/src/main/java/vct/test/CommandLineTesting.scala
@@ -175,6 +175,40 @@ object CommandLineTesting {
   def filterEnabledBackends(tools: Set[String]): Set[String] =
     tools.filter(!backendFilterOption.used() || backendFilter.contains(_))
 
+  def createTask(name: String, kees: Case, tool: String) = {
+    val args = mutable.ArrayBuffer[String]()
+    args += "--progress"
+    if (tool != "veymont") {
+      // Temporary workaround to disable the tool flag when running a veymont test.
+      // This should be removed when we add a proper tool mode for veymont
+      args += "--" + tool
+      // VeyMont was not built with the feature system in mind, so we have to disable it when veymont is executed
+      // in the test suite.
+      args += "--strict-internal"
+    }
+    args ++= kees.options.asScala
+    args ++= kees.files.asScala.map(_.toAbsolutePath.toString)
+
+    val conditions = mutable.ArrayBuffer[TaskCondition]()
+    if (kees.verdict != null) {
+      conditions += ExpectVerdict(kees.verdict)
+    } else {
+      conditions += ExpectVerdict(Verdict.Pass)
+    }
+    if (kees.pass_non_fail) {
+      conditions += PassNonFail(kees.fail_methods.asScala.toSeq)
+    }
+    conditions ++= kees.pass_methods.asScala.map(name => PassMethod(name))
+    conditions ++= kees.fail_methods.asScala.map(name => FailMethod(name))
+
+    // Tests are instrumented at runtime by the jacoco java vm agent
+    val jacocoArg = if (enableCoverage.get()) { jacocoJavaAgentArgs(tool, name) } else { Seq() }
+
+    val vercorsProcess = Configuration.getThisVerCors(jacocoArg.asJava).withArgs(args.toSeq: _*)
+
+    Task(vercorsProcess, conditions.toSeq)
+  }
+
   def getTasks: Map[String, Task] = {
     val result = mutable.HashMap[String, Task]()
 
@@ -184,31 +218,7 @@ object CommandLineTesting {
 
     for ((name, kees) <- getCases) {
       for (tool <- filterEnabledBackends(kees.tools.asScala.toSet)) {
-        val args = mutable.ArrayBuffer[String]()
-        args += "--progress"
-        args += "--" + tool
-        args += "--strict-internal"
-        args ++= kees.options.asScala
-        args ++= kees.files.asScala.map(_.toAbsolutePath.toString)
-
-        var conditions = mutable.ArrayBuffer[TaskCondition]()
-        if (kees.verdict != null) {
-          conditions += ExpectVerdict(kees.verdict)
-        } else {
-          conditions += ExpectVerdict(Verdict.Pass)
-        }
-        if (kees.pass_non_fail) {
-          conditions += PassNonFail(kees.fail_methods.asScala.toSeq)
-        }
-        conditions ++= kees.pass_methods.asScala.map(name => PassMethod(name))
-        conditions ++= kees.fail_methods.asScala.map(name => FailMethod(name))
-
-        // Tests are instrumented at runtime by the jacoco java vm agent
-        val jacocoArg = if (enableCoverage.get()) { jacocoJavaAgentArgs(tool, name) } else { Seq() }
-
-        val vercorsProcess = Configuration.getThisVerCors(jacocoArg.asJava).withArgs(args.toSeq: _*)
-
-        result += (s"$name-$tool" -> Task(vercorsProcess, conditions.toSeq))
+        result += (s"$name-$tool" -> createTask(name, kees, tool))
       }
     }
 
diff --git a/util/veymontTesting/veymont-2stage-tests.sh b/util/veymontTesting/veymont-2stage-tests.sh
new file mode 100755
index 0000000000..b02011aac5
--- /dev/null
+++ b/util/veymontTesting/veymont-2stage-tests.sh
@@ -0,0 +1,65 @@
+#!/usr/bin/env bash
+
+# This is a temporary veymont testing script.
+#
+# It finds all cases in examples/veymont-global-programs, runs them through veymont, and runs the output
+# through vercors.
+#
+# It ignores all other features of the vercors testing framework (e.g. suites, options). If this script gets any more
+# features it should, at least, be re-implemented in scala, but ideally it would be integrated in the test suite.
+
+vercorsPath=$(which vct-dev || which vct || which vercors)
+if [ -z $vercorsPath ]; then
+  echo "Could not detect vct-dev, vct, or vercors executable path"
+  exit 1
+fi
+echo "VerCors path: $vercorsPath"
+
+# Cd to the directory of the shell script
+cd "$(dirname "$0")"
+
+cd ../../examples/veymont-global-programs
+
+# Collect all cases. The cut part of the invocation selects the third element after splitting on spaces.
+allCases=$(grep -r cases | cut -d " " -f 3 | sort -u)
+
+echo "##### Detected cases for 2-stage tests: #####"
+printf "$allCases\n"
+
+failingReport="##### Failing 2-stage cases #####"
+# This is the final return code to be returned
+# In unix-style, 0 is success, anything else is failure
+# So if at some point it is set to something non-zero, it means something went wrong
+totalReturnCode=0
+
+for kees in $allCases
+do
+  echo "##### Case: $kees #####"
+  # Find all files that have the case $kees
+  # Replacing newlines with spaces to make sure all the filenames are on one line
+  files=$(grep -r "\\<$kees\\>" -l | tr "\n" " ")
+
+  veymontCmd="$vercorsPath --veymont ${kees}_output.pvl $files"
+  echo "-- Running VeyMont: $veymontCmd"
+  output=$(eval $veymontCmd)
+  echo "$output"
+  if [[ $output != *"Pass"* ]]; then
+    echo "VeyMont did not succeed in analyzing case $kees, files: $files"
+    failingReport="$failingReport\n- $kees"
+    totalReturnCode=1
+    continue
+  fi
+
+  vercorsCmd="$vercorsPath --silicon ${kees}_output.pvl"
+  echo "-- Running VerCors: $vercorsCmd"
+  output=$(eval $vercorsCmd)
+  echo "$output"
+  if [[ $output != *"Pass"* ]]; then
+    echo "VerCors did not succeed in analyzing the VeyMont output for case $kees"
+    failingReport="$failingReport\n- $kees"
+    totalReturnCode=1
+  fi
+done
+
+printf "$failingReport\n"
+exit $totalReturnCode