From ec057c6ba7b71697fa8cd22356a772ce8291037e Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Mon, 26 Jul 2021 11:53:46 +0200
Subject: [PATCH 01/11] Add veymont testing shell script.

---
 .github/workflows/build-test.yml            | 25 ++++++++-
 util/veymontTesting/veymont-2stage-tests.sh | 59 +++++++++++++++++++++
 2 files changed, 83 insertions(+), 1 deletion(-)
 create mode 100755 util/veymontTesting/veymont-2stage-tests.sh

diff --git a/.github/workflows/build-test.yml b/.github/workflows/build-test.yml
index 06a01c2673..8b27592a66 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
@@ -186,6 +186,29 @@ 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
+    strategy:
+      matrix:
+        testID: [0, 1, 2, 3, 4]
+      fail-fast: false
+    env:
+      maxTestID: 5
+    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/util/veymontTesting/veymont-2stage-tests.sh b/util/veymontTesting/veymont-2stage-tests.sh
new file mode 100755
index 0000000000..f519274160
--- /dev/null
+++ b/util/veymontTesting/veymont-2stage-tests.sh
@@ -0,0 +1,59 @@
+#!/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 then 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"
+
+# Move to the directory of the shell script
+cd "$(dirname "$0")"
+# Move to veymont global tests
+cd ../../examples/veymont-global-programs
+
+# Collect all cases. For now we only collect the first 4 cases of each file, as there are no tests with more than 2 cases anyway
+cases1=$(grep -r cases | cut -d " " -f 3)
+#                |           |      - Print the third element after splitting
+#                |           - Split at space
+#                - search for "cases"
+cases2=$(grep -r cases | cut -d " " -f 4)
+cases3=$(grep -r cases | cut -d " " -f 5)
+cases4=$(grep -r cases | cut -d " " -f 6)
+# The awk invocation drops all empty lines from stdin and prints the leftover lines
+# Also, use printf because echo ignores \n newlines
+allCases=$(printf "$cases1\n$cases2\n$cases3\n$cases4\n" | awk NF | sort -u)
+
+echo "##### Detected cases: #####"
+echo "$allCases"
+
+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"
+    exit 1
+  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"
+    exit 1
+  fi
+done
\ No newline at end of file

From 86d5aa1a3beffb461bfe8fc6916197354d1f3424 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Mon, 26 Jul 2021 11:55:01 +0200
Subject: [PATCH 02/11] Remove matrix from veymont job

---
 .github/workflows/build-test.yml | 6 ------
 1 file changed, 6 deletions(-)

diff --git a/.github/workflows/build-test.yml b/.github/workflows/build-test.yml
index 8b27592a66..346cff3e6c 100644
--- a/.github/workflows/build-test.yml
+++ b/.github/workflows/build-test.yml
@@ -189,12 +189,6 @@ jobs:
   integration-test-veymont:
     needs: build-test
     runs-on: ubuntu-latest
-    strategy:
-      matrix:
-        testID: [0, 1, 2, 3, 4]
-      fail-fast: false
-    env:
-      maxTestID: 5
     steps:
       # Need to check out the repo for the "examples" directory and the veymont 2stage testing script
       - uses: actions/checkout@v2

From bf59ed3e9345537a4b1d69ecbc5f2ccbc7b64972 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Mon, 26 Jul 2021 13:51:19 +0200
Subject: [PATCH 03/11] Further implement test suite and fix veymont tests

---
 .../checkTypesNonMain/RoleFieldType2.pvl      |  2 +-
 examples/veymont-global-programs/Move.pvl     |  2 +-
 .../veymont-global-programs/TicTacToe.pvl     |  2 +-
 util/veymontTesting/veymont-2stage-tests.sh   | 50 +++++++++++--------
 4 files changed, 31 insertions(+), 25 deletions(-)

diff --git a/examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl b/examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl
index 3ecc5bb32f..6a50460976 100644
--- a/examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl
+++ b/examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl
@@ -13,7 +13,7 @@ class Main {
 	}
 	
 	void run() {
-		a.x = 1;
+		a.x = new Other();
 	}
 	
 	void main() {
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..2efe770d94 100644
--- a/examples/veymont-global-programs/TicTacToe.pvl
+++ b/examples/veymont-global-programs/TicTacToe.pvl
@@ -1,5 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
-//:: cases TicTacToeInt TicTacToeMatrix
+//:: cases TicTacToeInt
 //:: tools veymont
 //:: verdict Pass
 
diff --git a/util/veymontTesting/veymont-2stage-tests.sh b/util/veymontTesting/veymont-2stage-tests.sh
index f519274160..c2bb62d8f9 100755
--- a/util/veymontTesting/veymont-2stage-tests.sh
+++ b/util/veymontTesting/veymont-2stage-tests.sh
@@ -1,9 +1,12 @@
 #!/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 then 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.
+# 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
@@ -12,26 +15,23 @@ if [ -z $vercorsPath ]; then
 fi
 echo "VerCors path: $vercorsPath"
 
-# Move to the directory of the shell script
+# Cd to the directory of the shell script
 cd "$(dirname "$0")"
-# Move to veymont global tests
+
 cd ../../examples/veymont-global-programs
 
-# Collect all cases. For now we only collect the first 4 cases of each file, as there are no tests with more than 2 cases anyway
-cases1=$(grep -r cases | cut -d " " -f 3)
-#                |           |      - Print the third element after splitting
-#                |           - Split at space
-#                - search for "cases"
-cases2=$(grep -r cases | cut -d " " -f 4)
-cases3=$(grep -r cases | cut -d " " -f 5)
-cases4=$(grep -r cases | cut -d " " -f 6)
-# The awk invocation drops all empty lines from stdin and prints the leftover lines
-# Also, use printf because echo ignores \n newlines
-allCases=$(printf "$cases1\n$cases2\n$cases3\n$cases4\n" | awk NF | sort -u)
-
-echo "##### Detected cases: #####"
+# 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: #####"
 echo "$allCases"
 
+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 #####"
@@ -45,7 +45,9 @@ do
   echo "$output"
   if [[ $output != *"Pass"* ]]; then
     echo "VeyMont did not succeed in analyzing case $kees, files: $files"
-    exit 1
+    failingReport="$failingReport\n- $kees"
+    totalReturnCode=1
+    continue
   fi
 
   vercorsCmd="$vercorsPath --silicon ${kees}_output.pvl"
@@ -54,6 +56,10 @@ do
   echo "$output"
   if [[ $output != *"Pass"* ]]; then
     echo "VerCors did not succeed in analyzing the VeyMont output for case $kees"
-    exit 1
+    failingReport="$failingReport\n- $kees"
+    totalReturnCode=1
   fi
-done
\ No newline at end of file
+done
+
+printf "$failingReport\n"
+exit $totalReturnCode

From bc91aebb8b3611968b12a92b8009fd040eddf041 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Mon, 26 Jul 2021 14:32:13 +0200
Subject: [PATCH 04/11] Adjust testsuite for veymont.

Strict internal must be disabled when doing veymont tests as veymont was not designed with the feature system in mind. Additionally, no "--tool" flag must be added when running veymont tests, as veymont is not enabled with a "--tool" flag yet.
---
 .github/workflows/build-test.yml                |  2 +-
 src/main/java/vct/test/CommandLineTesting.scala | 10 ++++++++--
 2 files changed, 9 insertions(+), 3 deletions(-)

diff --git a/.github/workflows/build-test.yml b/.github/workflows/build-test.yml
index 346cff3e6c..34b83a768d 100644
--- a/.github/workflows/build-test.yml
+++ b/.github/workflows/build-test.yml
@@ -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:
diff --git a/src/main/java/vct/test/CommandLineTesting.scala b/src/main/java/vct/test/CommandLineTesting.scala
index 3e8a54f15f..508c4c9257 100644
--- a/src/main/java/vct/test/CommandLineTesting.scala
+++ b/src/main/java/vct/test/CommandLineTesting.scala
@@ -186,8 +186,14 @@ object CommandLineTesting {
       for (tool <- filterEnabledBackends(kees.tools.asScala.toSet)) {
         val args = mutable.ArrayBuffer[String]()
         args += "--progress"
-        args += "--" + tool
-        args += "--strict-internal"
+        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)
 

From a3173d12cc6cf8d005d11de08071c9f74471cbce Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Mon, 26 Jul 2021 14:32:42 +0200
Subject: [PATCH 05/11] Add "tool veymont" to veymont-check tests.

---
 examples/veymont-check/checkLTS/ltstest.pvl                    | 1 +
 examples/veymont-check/checkLTS/simpleifelse.pvl               | 1 +
 examples/veymont-check/checkLTS/simplemethodcall.pvl           | 1 +
 examples/veymont-check/checkLTS/simplewhile.pvl                | 1 +
 examples/veymont-check/checkMainClass/MainConstructorArg.pvl   | 2 ++
 examples/veymont-check/checkMainClass/NoMain.pvl               | 1 +
 examples/veymont-check/checkMainClass/NoMainConstructor.pvl    | 1 +
 examples/veymont-check/checkMainClass/NoMainMethod.pvl         | 1 +
 examples/veymont-check/checkMainClass/NoMainMethod2.pvl        | 1 +
 examples/veymont-check/checkMainClass/NoRunArg.pvl             | 1 +
 examples/veymont-check/checkMainClass/NoRunMethod.pvl          | 1 +
 examples/veymont-check/checkMainClass/OtherMainConstructor.pvl | 1 +
 examples/veymont-check/checkMainClass/TwoMainConstructors.pvl  | 1 +
 examples/veymont-check/checkMainClass/WrongRunType.pvl         | 1 +
 .../MainConstructorAssignmentWrongType.pvl                     | 1 +
 .../checkMainConstructor/MainConstructorAssignsNoRole.pvl      | 1 +
 .../checkMainConstructor/MainConstructorBlock.pvl              | 1 +
 .../checkMainConstructor/MainConstructorNonRoleAssignment.pvl  | 1 +
 .../checkMainConstructor/MainConstructorNonRoleAssignment2.pvl | 1 +
 .../checkMainConstructor/MainConstructorNonRoleAssignment3.pvl | 1 +
 .../checkMainConstructor/MainConstructorNonRoleAssignment4.pvl | 1 +
 .../checkMainConstructor/MainConstructorWrongRoleNr.pvl        | 1 +
 .../checkMainSyntaxAndWellFormedness/ConstructorCall.pvl       | 1 +
 .../checkMainSyntaxAndWellFormedness/ConstructorCall2.pvl      | 1 +
 .../veymont-check/checkMainSyntaxAndWellFormedness/ForLoop.pvl | 1 +
 .../checkMainSyntaxAndWellFormedness/GuardedRecursion.pvl      | 1 +
 .../checkMainSyntaxAndWellFormedness/GuardedRecursion2.pvl     | 3 ++-
 .../checkMainSyntaxAndWellFormedness/IfCondition.pvl           | 1 +
 .../checkMainSyntaxAndWellFormedness/MainMethodCall.pvl        | 1 +
 .../checkMainSyntaxAndWellFormedness/NewNonRoleObject.pvl      | 1 +
 .../checkMainSyntaxAndWellFormedness/NewRoleObject.pvl         | 1 +
 .../checkMainSyntaxAndWellFormedness/NonRoleMethodCall.pvl     | 1 +
 .../checkMainSyntaxAndWellFormedness/PureMethodCall.pvl        | 1 +
 .../checkMainSyntaxAndWellFormedness/RoleFieldAssignment.pvl   | 1 +
 .../checkMainSyntaxAndWellFormedness/WaitStatement.pvl         | 1 +
 .../checkMainSyntaxAndWellFormedness/WhileCondition.pvl        | 1 +
 .../checkMainSyntaxAndWellFormedness/WrongAssignment.pvl       | 1 +
 .../checkMainSyntaxAndWellFormedness/WrongAssignment2.pvl      | 1 +
 .../checkMainSyntaxAndWellFormedness/WrongSyntax.pvl           | 1 +
 .../veymont-check/checkTerminationNonMain/AbsenceRecursion.pvl | 1 +
 .../checkTerminationNonMain/AbsenceRecursion2.pvl              | 1 +
 .../checkTerminationNonMain/AbsenceRecursion3.pvl              | 1 +
 .../checkTerminationNonMain/AbsenceRecursion4.pvl              | 1 +
 examples/veymont-check/checkTerminationNonMain/ForLoop.pvl     | 1 +
 .../checkTerminationNonMain/LoopStatementInRole.pvl            | 1 +
 .../veymont-check/checkTerminationNonMain/MainCallFromRole.pvl | 1 +
 .../checkTerminationNonMain/WaitStatementInRole.pvl            | 1 +
 .../veymont-check/checkTypesNonMain/OtherClassFieldType.pvl    | 1 +
 .../veymont-check/checkTypesNonMain/OtherClassFieldType2.pvl   | 1 +
 .../veymont-check/checkTypesNonMain/OtherClassMethodType.pvl   | 1 +
 .../veymont-check/checkTypesNonMain/OtherClassMethodType2.pvl  | 1 +
 examples/veymont-check/checkTypesNonMain/RoleFieldType.pvl     | 1 +
 examples/veymont-check/checkTypesNonMain/RoleFieldType2.pvl    | 1 +
 examples/veymont-check/checkTypesNonMain/RoleFieldType3.pvl    | 1 +
 examples/veymont-check/checkTypesNonMain/RoleFieldType4.pvl    | 1 +
 examples/veymont-check/checkTypesNonMain/RoleMethodType.pvl    | 1 +
 examples/veymont-check/checkTypesNonMain/RoleMethodType2.pvl   | 1 +
 examples/veymont-check/checkTypesNonMain/RoleMethodType3.pvl   | 1 +
 examples/veymont-check/checkTypesNonMain/VoidField.pvl         | 1 +
 59 files changed, 61 insertions(+), 1 deletion(-)

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 6a50460976..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;
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;

From 9d6ce19f164a1ad40ac0ead6fff828f2259222d4 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Mon, 26 Jul 2021 16:16:37 +0200
Subject: [PATCH 06/11] Set default stack size to 128mb for packaged vercors.

---
 build.sbt | 6 ++++++
 1 file changed, 6 insertions(+)

diff --git a/build.sbt b/build.sbt
index ba0fda340a..07c7ddca10 100644
--- a/build.sbt
+++ b/build.sbt
@@ -150,6 +150,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

From f06bc0fd6cbdce9c1c69adc1243c3de2505297aa Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Mon, 26 Jul 2021 16:36:23 +0200
Subject: [PATCH 07/11] Add global programs to problem-fail so they are not
 executed in the regular test suite

---
 examples/veymont-global-programs/IntGrid.pvl                   | 1 +
 examples/veymont-global-programs/Move.pvl                      | 1 +
 examples/veymont-global-programs/TicTacToe.pvl                 | 1 +
 examples/veymont-global-programs/leaderelectring.pvl           | 1 +
 examples/veymont-global-programs/leaderelectstar.pvl           | 1 +
 examples/veymont-global-programs/paperscissorsrock.pvl         | 1 +
 examples/veymont-global-programs/parallel_while.pvl            | 1 +
 examples/veymont-global-programs/parallel_while_simplified.pvl | 1 +
 8 files changed, 8 insertions(+)

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 e42674411b..e39ab8cdf7 100644
--- a/examples/veymont-global-programs/Move.pvl
+++ b/examples/veymont-global-programs/Move.pvl
@@ -1,5 +1,6 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases TicTacToeInt
+//:: suite problem-fail
 
 class Move {
 	int i, j, token;
diff --git a/examples/veymont-global-programs/TicTacToe.pvl b/examples/veymont-global-programs/TicTacToe.pvl
index 2efe770d94..e630367cf0 100644
--- a/examples/veymont-global-programs/TicTacToe.pvl
+++ b/examples/veymont-global-programs/TicTacToe.pvl
@@ -2,6 +2,7 @@
 //:: cases TicTacToeInt
 //:: tools veymont
 //:: verdict Pass
+//:: suite problem-fail
 
 class Main {
 	
diff --git a/examples/veymont-global-programs/leaderelectring.pvl b/examples/veymont-global-programs/leaderelectring.pvl
index 718c2a7989..32cf857b28 100644
--- a/examples/veymont-global-programs/leaderelectring.pvl
+++ b/examples/veymont-global-programs/leaderelectring.pvl
@@ -2,6 +2,7 @@
 //:: cases LeaderElectRing
 //:: tools veymont
 //:: verdict Pass
+//:: suite problem-fail
 
 class Node {
 	
diff --git a/examples/veymont-global-programs/leaderelectstar.pvl b/examples/veymont-global-programs/leaderelectstar.pvl
index 9c86b4174a..7be54df4f0 100644
--- a/examples/veymont-global-programs/leaderelectstar.pvl
+++ b/examples/veymont-global-programs/leaderelectstar.pvl
@@ -2,6 +2,7 @@
 //:: cases LeaderElectStar
 //:: tools veymont
 //:: verdict Pass
+//:: suite problem-fail
 
 class EndPoint {
 	
diff --git a/examples/veymont-global-programs/paperscissorsrock.pvl b/examples/veymont-global-programs/paperscissorsrock.pvl
index d1188ca6c1..42ea7384c7 100644
--- a/examples/veymont-global-programs/paperscissorsrock.pvl
+++ b/examples/veymont-global-programs/paperscissorsrock.pvl
@@ -2,6 +2,7 @@
 //:: cases PaperScissorsRock
 //:: tools veymont
 //:: verdict Pass
+//:: suite problem-fail
 
 class Role {
 	
diff --git a/examples/veymont-global-programs/parallel_while.pvl b/examples/veymont-global-programs/parallel_while.pvl
index 21dd9f72c6..0f57de2a86 100644
--- a/examples/veymont-global-programs/parallel_while.pvl
+++ b/examples/veymont-global-programs/parallel_while.pvl
@@ -2,6 +2,7 @@
 //:: cases ParallelWhile
 //:: tools veymont
 //:: verdict Pass
+//:: suite problem-fail
 
 class Role {
 	
diff --git a/examples/veymont-global-programs/parallel_while_simplified.pvl b/examples/veymont-global-programs/parallel_while_simplified.pvl
index 5960ee7db2..ed1727d3e0 100644
--- a/examples/veymont-global-programs/parallel_while_simplified.pvl
+++ b/examples/veymont-global-programs/parallel_while_simplified.pvl
@@ -2,6 +2,7 @@
 //:: cases ParallelWhileSimplified
 //:: tools veymont
 //:: verdict Pass
+//:: suite problem-fail
 
 class Role {
 	

From 8886a179f3d8b5cdf1b25651f52844bbf8fce8bc Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Tue, 27 Jul 2021 10:20:57 +0200
Subject: [PATCH 08/11] javacOptions is deprecated, done now by the javaOptions
 setting.

---
 build.sbt | 3 ---
 1 file changed, 3 deletions(-)

diff --git a/build.sbt b/build.sbt
index 07c7ddca10..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

From 2792944fcf7574fbe51895b44c2cbe3830ba853a Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Tue, 27 Jul 2021 10:21:31 +0200
Subject: [PATCH 09/11] Remove tool from global check programs to make sure
 they cannot be picked up by the test suite.

---
 examples/veymont-global-programs/Move.pvl                      | 1 -
 examples/veymont-global-programs/TicTacToe.pvl                 | 2 --
 examples/veymont-global-programs/leaderelectring.pvl           | 2 --
 examples/veymont-global-programs/leaderelectstar.pvl           | 2 --
 examples/veymont-global-programs/paperscissorsrock.pvl         | 2 --
 examples/veymont-global-programs/parallel_while.pvl            | 2 --
 examples/veymont-global-programs/parallel_while_simplified.pvl | 2 --
 7 files changed, 13 deletions(-)

diff --git a/examples/veymont-global-programs/Move.pvl b/examples/veymont-global-programs/Move.pvl
index e39ab8cdf7..e42674411b 100644
--- a/examples/veymont-global-programs/Move.pvl
+++ b/examples/veymont-global-programs/Move.pvl
@@ -1,6 +1,5 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases TicTacToeInt
-//:: suite problem-fail
 
 class Move {
 	int i, j, token;
diff --git a/examples/veymont-global-programs/TicTacToe.pvl b/examples/veymont-global-programs/TicTacToe.pvl
index e630367cf0..f4c816de8f 100644
--- a/examples/veymont-global-programs/TicTacToe.pvl
+++ b/examples/veymont-global-programs/TicTacToe.pvl
@@ -1,8 +1,6 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases TicTacToeInt
-//:: tools veymont
 //:: verdict Pass
-//:: suite problem-fail
 
 class Main {
 	
diff --git a/examples/veymont-global-programs/leaderelectring.pvl b/examples/veymont-global-programs/leaderelectring.pvl
index 32cf857b28..1c652fe609 100644
--- a/examples/veymont-global-programs/leaderelectring.pvl
+++ b/examples/veymont-global-programs/leaderelectring.pvl
@@ -1,8 +1,6 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases LeaderElectRing
-//:: tools veymont
 //:: verdict Pass
-//:: suite problem-fail
 
 class Node {
 	
diff --git a/examples/veymont-global-programs/leaderelectstar.pvl b/examples/veymont-global-programs/leaderelectstar.pvl
index 7be54df4f0..5b76756602 100644
--- a/examples/veymont-global-programs/leaderelectstar.pvl
+++ b/examples/veymont-global-programs/leaderelectstar.pvl
@@ -1,8 +1,6 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases LeaderElectStar
-//:: tools veymont
 //:: verdict Pass
-//:: suite problem-fail
 
 class EndPoint {
 	
diff --git a/examples/veymont-global-programs/paperscissorsrock.pvl b/examples/veymont-global-programs/paperscissorsrock.pvl
index 42ea7384c7..6e84f8decf 100644
--- a/examples/veymont-global-programs/paperscissorsrock.pvl
+++ b/examples/veymont-global-programs/paperscissorsrock.pvl
@@ -1,8 +1,6 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases PaperScissorsRock
-//:: tools veymont
 //:: verdict Pass
-//:: suite problem-fail
 
 class Role {
 	
diff --git a/examples/veymont-global-programs/parallel_while.pvl b/examples/veymont-global-programs/parallel_while.pvl
index 0f57de2a86..90baa22279 100644
--- a/examples/veymont-global-programs/parallel_while.pvl
+++ b/examples/veymont-global-programs/parallel_while.pvl
@@ -1,8 +1,6 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases ParallelWhile
-//:: tools veymont
 //:: verdict Pass
-//:: suite problem-fail
 
 class Role {
 	
diff --git a/examples/veymont-global-programs/parallel_while_simplified.pvl b/examples/veymont-global-programs/parallel_while_simplified.pvl
index ed1727d3e0..fd0d17db43 100644
--- a/examples/veymont-global-programs/parallel_while_simplified.pvl
+++ b/examples/veymont-global-programs/parallel_while_simplified.pvl
@@ -1,8 +1,6 @@
 // -*- tab-width:4 ; indent-tabs-mode:nil -*-
 //:: cases ParallelWhileSimplified
-//:: tools veymont
 //:: verdict Pass
-//:: suite problem-fail
 
 class Role {
 	

From 3de5bcc5b3f5b315c05dd0faf1be1f4910e44a76 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Tue, 27 Jul 2021 11:04:44 +0200
Subject: [PATCH 10/11] Refactor inner loop into separate method.

---
 .../java/vct/test/CommandLineTesting.scala    | 66 ++++++++++---------
 1 file changed, 35 insertions(+), 31 deletions(-)

diff --git a/src/main/java/vct/test/CommandLineTesting.scala b/src/main/java/vct/test/CommandLineTesting.scala
index 508c4c9257..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,37 +218,7 @@ object CommandLineTesting {
 
     for ((name, kees) <- getCases) {
       for (tool <- filterEnabledBackends(kees.tools.asScala.toSet)) {
-        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)
-
-        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))
       }
     }
 

From 91e41797aaec21d740dcd981532d3efb773d88e2 Mon Sep 17 00:00:00 2001
From: Bob Rubbens <bobrubbens@gmail.com>
Date: Tue, 27 Jul 2021 17:04:02 +0200
Subject: [PATCH 11/11] Prevent overlapping case names from merging

---
 util/veymontTesting/veymont-2stage-tests.sh | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/util/veymontTesting/veymont-2stage-tests.sh b/util/veymontTesting/veymont-2stage-tests.sh
index c2bb62d8f9..b02011aac5 100755
--- a/util/veymontTesting/veymont-2stage-tests.sh
+++ b/util/veymontTesting/veymont-2stage-tests.sh
@@ -24,7 +24,7 @@ cd ../../examples/veymont-global-programs
 allCases=$(grep -r cases | cut -d " " -f 3 | sort -u)
 
 echo "##### Detected cases for 2-stage tests: #####"
-echo "$allCases"
+printf "$allCases\n"
 
 failingReport="##### Failing 2-stage cases #####"
 # This is the final return code to be returned
@@ -37,7 +37,7 @@ 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" " ")
+  files=$(grep -r "\\<$kees\\>" -l | tr "\n" " ")
 
   veymontCmd="$vercorsPath --veymont ${kees}_output.pvl $files"
   echo "-- Running VeyMont: $veymontCmd"