Fully implement prettyModelVal

Model:

i!1 -> #x00000000
a.length -> #x00000001
a -> (_ as-array k!3)
i!2 -> #x00000000
retval -> #x00000000
k!3 -> {
  #x00000000
}

With function:

    public static void getMax_spec1(int[] a) {
        pre(a != null && a.length > 0);
        int retval = getMax(a);
        post(exists(a, i -> a[i] == retval) && forall(a, i -> a[i] <= retval));
    }

Should become something like:

a -> [0]
retval -> 0;