diff --git a/examples/HeapSort.java b/examples/HeapSort.java
index 0a5e5ff..6f1970d 100644
--- a/examples/HeapSort.java
+++ b/examples/HeapSort.java
@@ -9,7 +9,7 @@ public class HeapSort {
       ensures \forall int k;i <= k <= len/2;arr[k-1] <= arr[2*k-1];
       ensures \forall int k;i <= k <= (len-1)/2;arr[k-1] <= arr[2*k]; 
   @*/
-  public static void heapify(/*@ non_null @*/ int [] arr, final int i, final int len) {
+  public static void heapify(int /*@ non_null @*/ [] arr, final int i, final int len) {
     int j = i;
     /*@ loop_invariant i <= j <= len;
         loop_invariant \forall int k; j < k <= len/2; arr[k-1] <= arr[2*k-1];
@@ -41,7 +41,7 @@ public static void heapify(/*@ non_null @*/ int [] arr, final int i, final int l
     requires \forall int k; 1 <= k <= len/2; arr[k-1] <= arr[2*k-1];
     requires \forall int k; 1 <= k <= (len-1)/2; arr[k-1] <= arr[2*k]; 
     ensures  \result && \forall int k; 0 < k < len; arr[k] >= arr[0]; //Always true
-  public static pure model boolean isGeq(final  non_null  int [] arr, final int len) {
+  public static pure model boolean isGeq(final int  non_null [] arr, final int len) {
     loop_invariant 0 <= i < len;
     loop_invariant \forall int k;i < k < len;arr[k] >= arr[0];
     decreasing i;
@@ -62,7 +62,7 @@ public static pure model boolean isGeq(final  non_null  int [] arr, final int le
   /*@
     ensures \forall int k,j; 0 <= k < j < arr.length; arr[k] >= arr[j];
   @*/
-  public static void sort(/*@ non_null @*/ int [] arr) {
+  public static void sort(int /*@ non_null @*/ [] arr) {
     // Array of size 1 is already sorted
      if (arr.length < 2) return;
 		
diff --git a/examples/MergeSort.java b/examples/MergeSort.java
index 6d2abb1..5004ee4 100644
--- a/examples/MergeSort.java
+++ b/examples/MergeSort.java
@@ -36,7 +36,7 @@ private static void sortRec(int [] arr, int l, int r) {
       requires \forall int k,j; m <= k < j < r; arr[k] >= arr[j];
       ensures  \forall int k,j; l <= k < j < r; arr[k] >= arr[j] ;
     @*/
-    private static void merge(/*@ non_null @*/ int [] arr, final int l, final int m, final int r) {
+    private static void merge(int /*@ non_null @*/ [] arr, final int l, final int m, final int r) {
         final int [] lCpy = Arrays.copyOfRange(arr, l, m),
                      rCpy = Arrays.copyOfRange(arr,m, r);
             
diff --git a/examples/SelectionSort.java b/examples/SelectionSort.java
index 75b6a0c..9102c6e 100644
--- a/examples/SelectionSort.java
+++ b/examples/SelectionSort.java
@@ -5,7 +5,7 @@ public class SelectionSort {
     /*@
         ensures \forall int k;0 <= k && k < arr.length-1;arr[k] >= arr[k+1];
     @*/
-    public static void sort(/*@ non_null @*/ int [] arr) {
+    public static void sort(int /*@ non_null @*/ [] arr) {
         //@ ghost final int n = arr.length;
         
         //@ loop_invariant 0 <= i <= n; // Bounds check
diff --git a/images/.gitignore b/images/.gitignore
index 085e8ba..c16430d 100644
--- a/images/.gitignore
+++ b/images/.gitignore
@@ -1 +1 @@
-Thumbs.db
+**/Thumbs.db
diff --git a/images/images/.gitignore b/images/images/.gitignore
deleted file mode 100644
index 085e8ba..0000000
--- a/images/images/.gitignore
+++ /dev/null
@@ -1 +0,0 @@
-Thumbs.db