import org.sosy_lab.sv_benchmarks.Verifier;

public class Main {

    public static void reach_error() {
        assert false;
    }

    static void verifierAssert(boolean cond) {
        if (!cond) reach_error();
    }

    // Merges two sorted sub-arrays arr[left..mid] and arr[mid+1..right]
    static void merge(int[] arr, int left, int mid, int right) {
        int n1 = mid - left + 1;
        int n2 = right - mid;

        int[] L = new int[n1];
        int[] R = new int[n2];

        for (int i = 0; i < n1; i++)
            L[i] = arr[left + i];
        for (int j = 0; j < n2; j++)
            R[j] = arr[mid + 1 + j];

        int i = 0, j = 0, k = left;
        while (i < n1 && j < n2) {
            if (L[i] <= R[j]) {
                arr[k++] = L[i++];
            } else {
                arr[k++] = R[j++];
            }
        }
        while (i < n1) arr[k++] = L[i++];
        while (j < n2) arr[k++] = R[j++];
    }

    // Precondition:  arr != null && 0 <= left <= right < arr.length
    // Postcondition: arr[left..right] is sorted in non-decreasing order
    static void mergeSort(int[] arr, int left, int right) {
        // precondition check
        verifierAssert(arr != null);
        verifierAssert(0 <= left);
        verifierAssert(left <= right);
        verifierAssert(right < arr.length);

        if (left < right) {
            int mid = left + (right - left) / 2;
            mergeSort(arr, left, mid);
            mergeSort(arr, mid + 1, right);
            merge(arr, left, mid, right);
        }

        // postcondition check
        for (int i = left; i < right; i++) {
            verifierAssert(arr[i] <= arr[i + 1]);
        }
    }

    public static void main(String[] args) {
        final int N = 4;
        int[] arr = new int[N];
        for (int i = 0; i < N; i++) {
            arr[i] = Verifier.nondetInt();
        }

        mergeSort(arr, 0, N - 1);

        // Top-level postcondition: entire array is sorted
        for (int i = 0; i < N - 1; i++) {
            verifierAssert(arr[i] <= arr[i + 1]);
        }
    }
}