diff --git a/col/src/main/java/vct/col/ast/type/TypeExpression.scala b/col/src/main/java/vct/col/ast/type/TypeExpression.scala
index 7364d2ea2a..e14041b947 100644
--- a/col/src/main/java/vct/col/ast/type/TypeExpression.scala
+++ b/col/src/main/java/vct/col/ast/type/TypeExpression.scala
@@ -38,6 +38,12 @@ case class TypeExpression(val operator:TypeOperator, val types:List[Type]) exten
   override def isNumeric: Boolean =
     if (isLeaky) firstType.isNumeric else false
 
+  override def isIntegerType: Boolean =
+    if (isLeaky) firstType.isIntegerType else false
+
+  override def isInteger: Boolean =
+    if (isLeaky) firstType.isInteger else false
+
   override def supertypeof(context: ProgramUnit, t: Type): Boolean =
     if (isLeaky) firstType.supertypeof(context, t) else false
 
diff --git a/examples/gpgpu/ASSSP.cu b/examples/gpgpu/ASSSP.cu
index 70fc83fc51..ee150de67d 100644
--- a/examples/gpgpu/ASSSP.cu
+++ b/examples/gpgpu/ASSSP.cu
@@ -1,4 +1,10 @@
 //:: case ASSSP
+
+/* Currently this file does not pass because of some renaming errors. Mohsen Safari might have a version in which
+ * data-race freedom is verified, and which was also used in his ASSSP paper. This file might be included in the future,
+ * and can then replace this file.
+ */
+
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/
diff --git a/examples/gpgpu/ASSSPv3.cu b/examples/gpgpu/ASSSPv3.cu
index caa25dd6ee..3d9b443f12 100644
--- a/examples/gpgpu/ASSSPv3.cu
+++ b/examples/gpgpu/ASSSPv3.cu
@@ -1,4 +1,5 @@
 //:: case ASSSPv3
+//:: tool silicon
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/
diff --git a/examples/gpgpu/ASSSPv4.cu b/examples/gpgpu/ASSSPv4.cu
index 8d6b375135..c7b91a7cb7 100644
--- a/examples/gpgpu/ASSSPv4.cu
+++ b/examples/gpgpu/ASSSPv4.cu
@@ -1,4 +1,9 @@
 //:: case ASSSPv4
+
+/* Currently this file does not verify because CUDA features are needed that VerCors doesn't support yet. This file
+ * is included in the example folder to serve as an example of CUDA features we might want in the future.
+ */
+
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/
diff --git a/examples/gpgpu/GPGPU-Example-updates.cu b/examples/gpgpu/GPGPU-Example-updates.cu
index b4e6a4d6fc..93b5286ac5 100644
--- a/examples/gpgpu/GPGPU-Example-updates.cu
+++ b/examples/gpgpu/GPGPU-Example-updates.cu
@@ -1,5 +1,10 @@
 //:: case GPGPUExampleUpdates
 
+/* This is the realistic version of GPGPU-Example.cu, with the difference that this version uses actual CUDA functions,
+ * such as cudaMemcpy. Unfortunately this file cannot be verified yet as VerCors does not yet support these primitives.
+ * Therefore it is not included in the test suite.
+ */
+
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/
diff --git a/examples/gpgpu/GPGPU-Example.cu b/examples/gpgpu/GPGPU-Example.cu
index 374e33c381..5f0cd5336c 100644
--- a/examples/gpgpu/GPGPU-Example.cu
+++ b/examples/gpgpu/GPGPU-Example.cu
@@ -1,4 +1,11 @@
 //:: case GPGPUExample
+//:: tool silicon
+
+/* This is the verifiable version of GPGPU-Example-updates.cu, with the difference being that we use custom functions
+ * for modelling the GPU here (vercorsCudaMalloc, vercorsCudaFreeInt, etc.) instead of actual CUDA functions. This
+ * example is verified to be memory safe and has some functional properties.
+ */
+
 /***********************************************************************************
 Created by Mohsen Safari.
 ************************************************************************************/
@@ -22,7 +29,7 @@ __global__ void CUDAKernel(int* g_array1, int* g_array2, int N)
 {
   int tid = blockIdx.x * N + threadIdx.x;
   //@ assert tid == \gtid;
-  atomicMin(g_array1 + tid, g_array2[tid]) /*@ then { assert false && false; } */;
+  atomicMin(g_array1 + tid, g_array2[tid]);
 }
 
 //@ ensures \pointer(\result, N, write);
diff --git a/examples/gpgpu/cuda.cu b/examples/gpgpu/cuda.cu
index c15bddeef5..9fe8c386b8 100644
--- a/examples/gpgpu/cuda.cu
+++ b/examples/gpgpu/cuda.cu
@@ -1,4 +1,5 @@
 //:: cases BasicCuda
+//:: tool silicon
 //:: verdict Pass
 
 #include <cuda.h>
diff --git a/examples/gpgpu/opencl.c b/examples/gpgpu/opencl.c
index cafadcb1c6..28a09a3ec4 100644
--- a/examples/gpgpu/opencl.c
+++ b/examples/gpgpu/opencl.c
@@ -1,4 +1,5 @@
 //:: cases BasicOpenCL
+//:: tool silicon
 //:: verdict Pass
 
 #include <opencl.h>