system ComparableSort
{

	extension Set for edu.ksu.cis.projects.spex.set.SetModule
	{
		typedef type<'a>;
		
		expdef Set.type<'a> create<'a>('a ...);
		
		expdef Set.type<int> createIntRangeSet<'a>(int, int);
		
		expdef boolean forAll<'a>('a -> boolean, Set.type<'a>);
		
		expdef boolean forAll2Context<'a,'b,'c>('a * 'b * 'c -> boolean, Set.type<'a>, 'b, 'c);
		
		expdef boolean forAll3Context<'a,'b,'c, 'd>('a * 'b * 'c * 'd -> boolean, Set.type<'a>, 'b, 'c, 'd);
		
		expdef boolean forAll4Context<'a,'b,'c, 'd, 'e>('a * 'b * 'c * 'd * 'e -> boolean, Set.type<'a>, 'b, 'c, 'd, 'e);
		
		expdef boolean exists2Context<'a,'b,'c>('a * 'b * 'c -> boolean, Set.type<'a>, 'b, 'c);
		
		expdef boolean exists3Context<'a,'b,'c, 'd>('a * 'b * 'c * 'd -> boolean, Set.type<'a>, 'b, 'c, 'd);

		expdef boolean contains<'a>(Set.type<'a>, 'a);

		actiondef add<'a>(Set.type<'a>, 'a);
		
		actiondef remove<'a>(Set.type<'a>, 'a);
	}
	
	extension State for edu.ksu.cis.projects.spex.state.StateModule
	{
		expdef Set.type<'a> reachSet<'a>('a);
		expdef boolean isFresh<'rec$a>(lazy 'rec$a);
		expdef 'a preVal<'a>(lazy 'a, tid);
		expdef int getCollapsedState<'a>('a);
		expdef tid getCurrentThreadId();
		actiondef addAssignable<'a>(lazy 'a);
		actiondef addAssignableAllFields<'a>(lazy 'a);
		actiondef enterAssignable();
		actiondef exitAssignable();
	}
	
	extension Debug for edu.ksu.cis.projects.spex.debug.DebugModule
	{
		actiondef printString(string);
		actiondef printExpValue<'a>(lazy 'a);
	}

    main thread MAIN()
    {
        loc loc0: live {}
            invoke {|sort.ComparableSort.main(java.lang.String[])|}() return;
    }
    record (|sort.ComparableSort|) extends (|java.lang.Object|) {}
    virtual +|java.lang.Comparable.compareTo(java.lang.Object)|+ { (|java.lang.Integer|) -> {|java.lang.Integer.compareTo(java.lang.Object)|} }
    function {|sort.ComparableSort.mergeSort(java.lang.Object[],java.lang.Object[],java.lang.Object[],java.lang.Object[],java.lang.Object[])|}((|java.lang.Object|)[] [|r0|], (|java.lang.Object|)[] [|r1|], int [|i0|], int [|i1|], int [|i2|])
    {
        int [|i3|];
        int [|i4|];
        int [|i5|];
        int [|i6|];
        int [|i7|];
        int [|i8|];
        int [|i9|];
        int [|$i10|];
        int [|$i11|];
        (|java.lang.Object|) [|$r2|];
        (|java.lang.Object|) [|$r3|];
        (|java.lang.Object|) [|$r4|];
        (|java.lang.Object|) [|$r5|];
        int [|$i12|];
        int [|i13|];
        int [|i14|];
        int [|i15|];
        int [|i16|];
        int [|$i17|];
        int [|$i18|];
        int [|$i19|];
        int [|$i20|];
        (|java.lang.Object|) [|$r6|];
        (|java.lang.Object|) [|$r7|];
        (|java.lang.Object|) [|$r8|];
        (|java.lang.Object|) [|$r9|];
        int [|$i21|];
        (|java.lang.Object|) [|$r10|];
        (|java.lang.Object|) [|$r11|];
        (|java.lang.Object|) [|$r12|];
        int [|$i22|];
        int [|$i23|];
        (|java.lang.Object|) [|$r13|];
        int [|$i24|];
        (|java.lang.Object|) [|$r14|];

        loc loc5: live { [|i0|], [|i3|], [|r0|], [|i2|], [|i1|], [|r1|] }
            do
            {
                [|i3|] := [|i1|] - [|i0|];
            }
            goto loc6;
        loc loc6: live { [|i0|], [|i3|], [|r0|], [|i2|], [|i1|], [|r1|] }
            when [|i3|] >= 7 do
            {
            }
            goto loc25;
            when !([|i3|] >= 7) do
            {
            }
            goto loc7;
        loc loc7: live { [|i0|], [|i1|], [|r1|], [|i4|] }
            do
            {
                [|i4|] := [|i0|];
            }
            goto loc8;
        loc loc8: live { [|i0|], [|i1|], [|r1|], [|i4|] }
            do
            {
            }
            goto loc23;
        loc loc9: live { [|i0|], [|i1|], [|r1|], [|i5|], [|i4|] }
            do
            {
                [|i5|] := [|i4|];
            }
            goto loc10;
        loc loc10: live { [|i0|], [|i1|], [|r1|], [|i5|], [|i4|] }
            do
            {
            }
            goto loc14;
        loc loc11: live { [|i0|], [|i1|], [|r1|], [|i5|], [|i4|], [|$i10|] }
            do
            {
                [|$i10|] := [|i5|] - 1;
            }
            goto loc12;
        loc loc12: live { [|i0|], [|i1|], [|r1|], [|i5|], [|i4|] }
            invoke {|sort.ComparableSort.swap(java.lang.Object[],int,int)|}(((|java.lang.Object|)[]) [|r1|], (int) [|i5|], (int) [|$i10|]) goto loc13;
        loc loc13: live { [|i0|], [|i1|], [|r1|], [|i5|], [|i4|] }
            do
            {
                [|i5|] := [|i5|] + -1;
            }
            goto loc14;
        loc loc14: live { [|i0|], [|i1|], [|r1|], [|i5|], [|i4|] }
            when [|i5|] <= [|i0|] do
            {
            }
            goto loc22;
            when !([|i5|] <= [|i0|]) do
            {
            }
            goto loc15;
        loc loc15: live { [|i0|], [|i1|], [|r1|], [|i5|], [|$i11|], [|i4|] }
            do
            {
                [|$i11|] := [|i5|] - 1;
            }
            goto loc16;
        loc loc16: live { [|i0|], [|i1|], [|$r2|], [|r1|], [|i5|], [|i4|] }
            do
            {
                [|$r2|] := [|r1|][[|$i11|]];
            }
            goto loc17;
        loc loc17: live { [|i0|], [|$r3|], [|i1|], [|r1|], [|i5|], [|i4|] }
            do
            {
                [|$r3|] := ((|java.lang.Object|)) [|$r2|];
            }
            goto loc18;
        loc loc18: live { [|i0|], [|$r4|], [|$r3|], [|i1|], [|r1|], [|i5|], [|i4|] }
            do
            {
                [|$r4|] := [|r1|][[|i5|]];
            }
            goto loc19;
        loc loc19: live { [|i0|], [|$r3|], [|i1|], [|r1|], [|i5|], [|i4|], [|$r5|] }
            do
            {
                [|$r5|] := ((|java.lang.Object|)) [|$r4|];
            }
            goto loc20;
        loc loc20: live { [|$i12|], [|i0|], [|i1|], [|r1|], [|i5|], [|i4|] }
            [|$i12|] := invoke virtual +|java.lang.Comparable.compareTo(java.lang.Object)|+([|$r3|], [|$r5|]) goto loc21;
        loc loc21: live { [|i0|], [|i1|], [|r1|], [|i5|], [|i4|] }
            when [|$i12|] > 0 do
            {
            }
            goto loc11;
            when !([|$i12|] > 0) do
            {
            }
            goto loc22;
        loc loc22: live { [|i0|], [|i1|], [|r1|], [|i4|] }
            do
            {
                [|i4|] := [|i4|] + 1;
            }
            goto loc23;
        loc loc23: live { [|i0|], [|i1|], [|r1|], [|i4|] }
            when [|i4|] < [|i1|] do
            {
            }
            goto loc9;
            when !([|i4|] < [|i1|]) do
            {
            }
            goto loc24;
        loc loc24: live {}
            do
            {
            }
            return;
        loc loc25: live { [|i0|], [|i13|], [|i3|], [|r0|], [|i2|], [|i1|], [|r1|] }
            do
            {
                [|i13|] := [|i0|];
            }
            goto loc26;
        loc loc26: live { [|i0|], [|i13|], [|i3|], [|r0|], [|i14|], [|i2|], [|i1|], [|r1|] }
            do
            {
                [|i14|] := [|i1|];
            }
            goto loc27;
        loc loc27: live { [|i13|], [|i3|], [|r0|], [|i14|], [|i2|], [|i1|], [|r1|], [|i15|] }
            do
            {
                [|i15|] := [|i0|] + [|i2|];
            }
            goto loc28;
        loc loc28: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i2|], [|r1|], [|i15|] }
            do
            {
                [|i16|] := [|i1|] + [|i2|];
            }
            goto loc29;
        loc loc29: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i2|], [|r1|], [|$i17|], [|i15|] }
            do
            {
                [|$i17|] := [|i15|] + [|i16|];
            }
            goto loc30;
        loc loc30: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i2|], [|i6|], [|r1|], [|i15|] }
            do
            {
                [|i6|] := [|$i17|] shr 1;
            }
            goto loc31;
        loc loc31: live { [|$i18|], [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i2|], [|i6|], [|r1|], [|i15|] }
            do
            {
                [|$i18|] := -([|i2|]);
            }
            goto loc32;
        loc loc32: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i2|], [|i6|], [|r1|], [|i15|] }
            invoke {|sort.ComparableSort.mergeSort(java.lang.Object[],java.lang.Object[],java.lang.Object[],java.lang.Object[],java.lang.Object[])|}(((|java.lang.Object|)[]) [|r1|], ((|java.lang.Object|)[]) [|r0|], (int) [|i15|], (int) [|i6|], (int) [|$i18|]) goto loc33;
        loc loc33: live { [|i13|], [|i16|], [|i3|], [|r0|], [|$i19|], [|i14|], [|i6|], [|r1|], [|i15|] }
            do
            {
                [|$i19|] := -([|i2|]);
            }
            goto loc34;
        loc loc34: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i6|], [|r1|], [|i15|] }
            invoke {|sort.ComparableSort.mergeSort(java.lang.Object[],java.lang.Object[],java.lang.Object[],java.lang.Object[],java.lang.Object[])|}(((|java.lang.Object|)[]) [|r1|], ((|java.lang.Object|)[]) [|r0|], (int) [|i6|], (int) [|i16|], (int) [|$i19|]) goto loc35;
        loc loc35: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i6|], [|$i20|], [|r1|], [|i15|] }
            do
            {
                [|$i20|] := [|i6|] - 1;
            }
            goto loc36;
        loc loc36: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i6|], [|r1|], [|$r6|], [|i15|] }
            do
            {
                [|$r6|] := [|r0|][[|$i20|]];
            }
            goto loc37;
        loc loc37: live { [|$r7|], [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i6|], [|r1|], [|i15|] }
            do
            {
                [|$r7|] := ((|java.lang.Object|)) [|$r6|];
            }
            goto loc38;
        loc loc38: live { [|$r7|], [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i6|], [|r1|], [|$r8|], [|i15|] }
            do
            {
                [|$r8|] := [|r0|][[|i6|]];
            }
            goto loc39;
        loc loc39: live { [|$r7|], [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i6|], [|$r9|], [|r1|], [|i15|] }
            do
            {
                [|$r9|] := ((|java.lang.Object|)) [|$r8|];
            }
            goto loc40;
        loc loc40: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i6|], [|r1|], [|$i21|], [|i15|] }
            [|$i21|] := invoke virtual +|java.lang.Comparable.compareTo(java.lang.Object)|+([|$r7|], [|$r9|]) goto loc41;
        loc loc41: live { [|i13|], [|i16|], [|i3|], [|r0|], [|i14|], [|i6|], [|r1|], [|i15|] }
            when [|$i21|] > 0 do
            {
            }
            goto loc44;
            when !([|$i21|] > 0) do
            {
            }
            goto loc42;
        loc loc42: live {}
            invoke {|java.lang.System.arraycopy(java.lang.Object[],int,int,int,int)|}(((|java.lang.Object|)[]) [|r0|], (int) [|i15|], ((|java.lang.Object|)[]) [|r1|], (int) [|i13|], (int) [|i3|]) goto loc43;
        loc loc43: live {}
            do
            {
            }
            return;
        loc loc44: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i7|], [|r1|], [|i15|] }
            do
            {
                [|i7|] := [|i13|];
            }
            goto loc45;
        loc loc45: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|i8|] := [|i15|];
            }
            goto loc46;
        loc loc46: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|i9|] := [|i6|];
            }
            goto loc47;
        loc loc47: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
            }
            goto loc65;
        loc loc48: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            when [|i9|] >= [|i16|] do
            {
            }
            goto loc55;
            when !([|i9|] >= [|i16|]) do
            {
            }
            goto loc49;
        loc loc49: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            when [|i8|] >= [|i6|] do
            {
            }
            goto loc60;
            when !([|i8|] >= [|i6|]) do
            {
            }
            goto loc50;
        loc loc50: live { [|i16|], [|r0|], [|$r10|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|$r10|] := [|r0|][[|i8|]];
            }
            goto loc51;
        loc loc51: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|$r11|], [|i7|], [|r1|] }
            do
            {
                [|$r11|] := ((|java.lang.Object|)) [|$r10|];
            }
            goto loc52;
        loc loc52: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|$r11|], [|i7|], [|r1|], [|$r12|] }
            do
            {
                [|$r12|] := [|r0|][[|i9|]];
            }
            goto loc53;
        loc loc53: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|$i22|], [|i7|], [|r1|] }
            [|$i22|] := invoke virtual +|java.lang.Comparable.compareTo(java.lang.Object)|+([|$r11|], [|$r12|]) goto loc54;
        loc loc54: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            when [|$i22|] > 0 do
            {
            }
            goto loc60;
            when !([|$i22|] > 0) do
            {
            }
            goto loc55;
        loc loc55: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|$i23|], [|r1|] }
            do
            {
                [|$i23|] := [|i8|];
            }
            goto loc56;
        loc loc56: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|$i23|], [|r1|] }
            do
            {
                [|i8|] := [|i8|] + 1;
            }
            goto loc57;
        loc loc57: live { [|i16|], [|r0|], [|i14|], [|$r13|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|$r13|] := [|r0|][[|$i23|]];
            }
            goto loc58;
        loc loc58: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|r1|][[|i7|]] := [|$r13|];
            }
            goto loc59;
        loc loc59: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
            }
            goto loc64;
        loc loc60: live { [|i16|], [|r0|], [|i14|], [|$i24|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|$i24|] := [|i9|];
            }
            goto loc61;
        loc loc61: live { [|i16|], [|r0|], [|i14|], [|$i24|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|i9|] := [|i9|] + 1;
            }
            goto loc62;
        loc loc62: live { [|i16|], [|r0|], [|$r14|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|$r14|] := [|r0|][[|$i24|]];
            }
            goto loc63;
        loc loc63: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|r1|][[|i7|]] := [|$r14|];
            }
            goto loc64;
        loc loc64: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            do
            {
                [|i7|] := [|i7|] + 1;
            }
            goto loc65;
        loc loc65: live { [|i16|], [|r0|], [|i14|], [|i6|], [|i9|], [|i8|], [|i7|], [|r1|] }
            when [|i7|] < [|i14|] do
            {
            }
            goto loc48;
            when !([|i7|] < [|i14|]) do
            {
            }
            goto loc66;
        loc loc66: live {}
            do
            {
            }
            return;
    }
    function {|sort.ComparableSort.<init>()|}((|sort.ComparableSort|) [|r0|])
    {

        loc loc1: live {}
            invoke {|java.lang.Object.<init>()|}([|r0|]) goto loc2;
        loc loc2: live {}
            do
            {
            }
            return;
    }
    function {|sort.ComparableSort.swap(java.lang.Object[],int,int)|}((|java.lang.Object|)[] [|r0|], int [|i0|], int [|i1|])
    {
        (|java.lang.Object|) [|r1|];
        (|java.lang.Object|) [|$r2|];
        
        Set.type<int> spec1;
        (|java.lang.Object|)[] spec2;

        loc locSpec0: live {}
            do invisible
            {
            }
            goto locSpec1;
        loc locSpec1: live {}
            do invisible
            {
            	assert([|r0|] != null);
            	assert([|r0|][[|i0|]] != null);
            	assert([|r0|][[|i1|]] != null);
            }
            goto locSpec3;
        loc locSpec3: live {}
            do
            {
            	State.enterAssignable();
            	State.addAssignable<(|java.lang.Object|)>([|r0|][[|i0|]]);
            	State.addAssignable<(|java.lang.Object|)>([|r0|][[|i1|]]);
            }
            goto loc3;
        loc loc3: live { [|i1|], [|r1|], [|i0|], [|r0|] }
            do
            {
                [|r1|] := [|r0|][[|i0|]];
            }
            goto loc4;
        loc loc4: live { [|i1|], [|$r2|], [|r1|], [|i0|], [|r0|] }
            do
            {
                [|$r2|] := [|r0|][[|i1|]];
            }
            goto loc5;
        loc loc5: live { [|i1|], [|r1|], [|r0|] }
            do
            {
                [|r0|][[|i0|]] := [|$r2|];
            }
            goto loc6;
        loc loc6: live {}
            do invisible
            {
                [|r0|][[|i1|]] := [|r1|];
            }
            goto locSpec4;
        loc locSpec4: live { spec1, spec2 }
            do invisible
            {
            	State.exitAssignable();
            }
            goto locSpec2;
        loc locSpec2: live { spec1, spec2 }
            do
            {
            	spec1 := Set.createIntRangeSet<int>(0, [|r0|].length - 1);
            	spec2 := State.preVal<(|java.lang.Object|)[]>([|r0|], State.getCurrentThreadId());
            	assert(Set.forAll4Context<int, int, int, (|java.lang.Object|)[], (|java.lang.Object|)[]>(specFun5, spec1, [|i0|], [|i1|], [|r0|], spec2));
            	assert(State.preVal<(|java.lang.Object|)>([|r0|][[|i0|]], State.getCurrentThreadId()) == [|r0|][[|i1|]]);
            	assert(State.preVal<(|java.lang.Object|)>([|r0|][[|i1|]], State.getCurrentThreadId()) == [|r0|][[|i0|]]);
            }
            goto loc7;
        loc loc7: live {}
            do
            {
            }
            return;
    }
    
    fun specFun5(int i, int a, int b, (|java.lang.Object|)[] array, (|java.lang.Object|)[] oldArray) returns boolean =
        i != a && i != b ? oldArray[i] == array[i]: true;
    
    function {|sort.ComparableSort.main(java.lang.String[])|}()
    {
        (|java.lang.Integer|)[] [|array|];
        int [|i|];
        (|java.lang.Integer|) [|$r0|];
        int [|$i0|];
        int [|$i1|];

        loc loc1: live { [|array|] }
            do
            {
                [|array|] := new (|java.lang.Integer|)[1000];
            }
            goto loc2;
        loc loc2: live { [|i|], [|array|] }
            do
            {
                [|i|] := 0;
            }
            goto loc3;
        loc loc3: live { [|i|], [|array|] }
            do
            {
            }
            goto loc9;
        loc loc4: live { [|i|], [|array|], [|$r0|] }
            do invisible
            {
                [|$r0|] := new (|java.lang.Integer|);
            }
            goto loc5;
        loc loc5: live { [|i|], [|array|], [|$i0|], [|$r0|] }
            do
            {
                [|$i0|] := 999 - [|i|];
            }
            goto loc6;
        loc loc6: live { [|i|], [|array|], [|$r0|] }
            invoke {|java.lang.Integer.<init>(int)|}([|$r0|], [|$i0|]) goto loc7;
        loc loc7: live { [|i|], [|array|] }
            do
            {
                [|array|][[|i|]] := [|$r0|];
            }
            goto loc8;
        loc loc8: live { [|i|], [|array|] }
            do
            {
                [|i|] := [|i|] + 1;
            }
            goto loc9;
        loc loc9: live { [|i|], [|array|], [|$i1|] }
            do
            {
                [|$i1|] := [|array|].length;
            }
            goto loc10;
        loc loc10: live { [|i|], [|array|] }
            when [|i|] < [|$i1|] do
            {
            }
            goto loc4;
            when !([|i|] < [|$i1|]) do
            {
            }
            goto loc11;
        loc loc11: live {}
            invoke {|sort.ComparableSort.sort(java.lang.Object[])|}(((|java.lang.Object|)[]) [|array|]) goto loc12;
        loc loc12: live {}
            do
            {
            }
            return;
    }
    function {|sort.ComparableSort.sort(java.lang.Object[])|}((|java.lang.Object|)[] [|r0|])
    {
        (|java.lang.Object|)[] [|r1|];
        int [|$i0|];
        int [|$i1|];
        int [|$i2|];
        
        Set.type<int> spec1;
        (|java.lang.Object|)[] spec2;

        loc locSpec0: live {}
            do invisible
            {
            }
            goto locSpec1;
        loc locSpec1: live {}
            do invisible
            {
            	assert([|r0|] != null);
            }
            goto locSpec3;
        loc locSpec3: live {}
            do
            {
            	State.enterAssignable();
            	State.addAssignableAllFields<(|java.lang.Object|)[]>([|r0|]);
            }
            goto loc1;
        loc loc1: live { [|$i0|], [|r0|] }
            do
            {
                [|$i0|] := [|r0|].length;
            }
            goto loc2;
        loc loc2: live { [|r1|], [|r0|] }
            do
            {
                [|r1|] := new (|java.lang.Object|)[[|$i0|]];
                State.addAssignable<(|java.lang.Object|)[]>([|r1|]);
            }
            goto loc3;
        loc loc3: live { [|$i1|], [|r1|], [|r0|] }
            do
            {
                [|$i1|] := [|r0|].length;
            }
            goto loc4;
        loc loc4: live { [|r1|], [|r0|] }
            invoke {|java.lang.System.arraycopy(java.lang.Object[],int,int,int,int)|}(((|java.lang.Object|)[]) [|r0|], (int) 0, ((|java.lang.Object|)[]) [|r1|], (int) 0, (int) [|$i1|]) goto loc5;
        loc loc5: live { [|$i2|], [|r1|], [|r0|] }
            do
            {
                [|$i2|] := [|r0|].length;
            }
            goto loc6;
        loc loc6: live {}
            invoke {|sort.ComparableSort.mergeSort(java.lang.Object[],java.lang.Object[],java.lang.Object[],java.lang.Object[],java.lang.Object[])|}(((|java.lang.Object|)[]) [|r1|], ((|java.lang.Object|)[]) [|r0|], (int) 0, (int) [|$i2|], (int) 0) goto locSpec4b;
        loc locSpec4b: live {}
            do invisible
            {
            }
            goto locSpec4;
        loc locSpec4: live { spec1, spec2 }
            do invisible
            {
            	State.exitAssignable();
            }
            goto locSpec2;
        loc locSpec2: live { spec1, spec2 }
            do
            {
            	spec1 := Set.createIntRangeSet<int>(0, [|r0|].length - 1);
            	spec2 := State.preVal<(|java.lang.Object|)[]>([|r0|], State.getCurrentThreadId());
            	assert([|r0|].length == State.preVal<int>([|r0|].length, State.getCurrentThreadId()));
            	assert(Set.forAll3Context<int, Set.type<int>, (|java.lang.Object|)[], (|java.lang.Object|)[]>(specFun1, spec1, spec1, [|r0|], spec2));
            	assert(Set.forAll2Context<int, (|java.lang.Object|)[], int>(specFun3, spec1, [|r0|], 0));
            }
            goto loc7;
        loc loc7: live {}
            do
            {
            }
            return;
    }
    
    fun specFun1(int i, Set.type<int> set, (|java.lang.Object|)[] array, (|java.lang.Object|)[] oldArray) returns boolean =
       Set.exists3Context<int, int, (|java.lang.Object|)[], (|java.lang.Object|)[]>(specFun2, set, i, array, oldArray);
       
    fun specFun2(int i, int j, (|java.lang.Object|)[] array, (|java.lang.Object|)[] oldArray) returns boolean =
       oldArray[i] == array[j];
       
    fun specFun3(int i, (|java.lang.Object|)[] array, int nothing) returns boolean =
       i < array.length - 1 ? (((|java.lang.Integer|))array[i])./|java.lang.Integer.value|\ <= (((|java.lang.Integer|))array[i + 1])./|java.lang.Integer.value|\ : true;
       
    int /|java.lang.Integer.MIN_VALUE|\;
    int /|java.lang.Integer.MAX_VALUE|\;
    record (|java.lang.Integer|) extends (|java.lang.Object|) { int /|java.lang.Integer.value|\; }
    virtual +|java.lang.Integer.intValue()|+ { (|java.lang.Integer|) -> {|java.lang.Integer.intValue()|} }
    function {|java.lang.Integer.equals(java.lang.Object)|}((|java.lang.Integer|) [|r0|], (|java.lang.Object|) [|r1|]) returns boolean
    {
        boolean ret;
        boolean [|$z0|];
        int [|$i0|];
        (|java.lang.Integer|) [|$r2|];
        int [|$i1|];

        loc loc2: live { [|$z0|], [|r1|], [|r0|] }
            do
            {
                [|$z0|] := [|r1|] instanceof (|java.lang.Integer|);
            }
            goto loc3;
        loc loc3: live { [|r1|], [|r0|] }
            when !([|$z0|]) do
            {
            }
            goto loc10;
            when !(!([|$z0|])) do
            {
            }
            goto loc4;
        loc loc4: live { [|r1|], [|$i0|] }
            do
            {
                [|$i0|] := [|r0|]./|java.lang.Integer.value|\;
            }
            goto loc5;
        loc loc5: live { [|$r2|], [|$i0|] }
            do
            {
                [|$r2|] := ((|java.lang.Integer|)) [|r1|];
            }
            goto loc6;
        loc loc6: live { [|$i0|], [|$i1|] }
            [|$i1|] := invoke virtual +|java.lang.Integer.intValue()|+([|$r2|]) goto loc7;
        loc loc7: live {}
            when [|$i0|] != [|$i1|] do
            {
            }
            goto loc9;
            when !([|$i0|] != [|$i1|]) do
            {
            }
            goto loc8;
        loc loc8: live {}
            do
            {
                ret := true;
            }
            return ret;
        loc loc9: live {}
            do
            {
                ret := false;
            }
            return ret;
        loc loc10: live {}
            do
            {
                ret := false;
            }
            return ret;
    }
    function {|java.lang.Integer.<init>(int)|}((|java.lang.Integer|) [|r0|], int [|i0|])
    {

        loc loc2: live { [|i0|], [|r0|] }
            invoke {|java.lang.Object.<init>()|}([|r0|]) goto loc3;
        loc loc3: live {}
            do
            {
                [|r0|]./|java.lang.Integer.value|\ := [|i0|];
            }
            goto loc4;
        loc loc4: live {}
            do
            {
            }
            return;
    }
    function {|java.lang.Integer.intValue()|}((|java.lang.Integer|) [|r0|]) returns int
    {
        int ret;
        int [|$i0|];

        loc loc1: live { [|$i0|] }
            do
            {
                [|$i0|] := [|r0|]./|java.lang.Integer.value|\;
            }
            goto loc2;
        loc loc2: live {}
            do
            {
                ret := [|$i0|];
            }
            return ret;
    }
    function {|java.lang.Integer.hashCode()|}((|java.lang.Integer|) [|r0|]) returns int
    {
        int ret;
        int [|$i0|];

        loc loc1: live { [|$i0|] }
            do
            {
                [|$i0|] := [|r0|]./|java.lang.Integer.value|\;
            }
            goto loc2;
        loc loc2: live {}
            do
            {
                ret := [|$i0|];
            }
            return ret;
    }
    function {|java.lang.Integer.compareTo(java.lang.Integer)|}((|java.lang.Integer|) [|r0|], (|java.lang.Integer|) [|r1|]) returns int
    {
        int ret;
        int [|i0|];
        int [|i1|];
        int [|$b2|];

        loc loc2: live { [|i0|], [|r1|] }
            do
            {
                [|i0|] := [|r0|]./|java.lang.Integer.value|\;
            }
            goto loc3;
        loc loc3: live { [|i0|], [|i1|] }
            do
            {
                [|i1|] := [|r1|]./|java.lang.Integer.value|\;
            }
            goto loc4;
        loc loc4: live { [|i0|], [|i1|] }
            when [|i0|] >= [|i1|] do
            {
            }
            goto loc7;
            when !([|i0|] >= [|i1|]) do
            {
            }
            goto loc5;
        loc loc5: live { [|$b2|] }
            do
            {
                [|$b2|] := -1;
            }
            goto loc6;
        loc loc6: live { [|$b2|] }
            do
            {
            }
            goto loc11;
        loc loc7: live {}
            when [|i0|] != [|i1|] do
            {
            }
            goto loc10;
            when !([|i0|] != [|i1|]) do
            {
            }
            goto loc8;
        loc loc8: live { [|$b2|] }
            do
            {
                [|$b2|] := 0;
            }
            goto loc9;
        loc loc9: live { [|$b2|] }
            do
            {
            }
            goto loc11;
        loc loc10: live { [|$b2|] }
            do
            {
                [|$b2|] := 1;
            }
            goto loc11;
        loc loc11: live {}
            do
            {
                ret := [|$b2|];
            }
            return ret;
    }
    virtual +|java.lang.Integer.compareTo(java.lang.Integer)|+ { (|java.lang.Integer|) -> {|java.lang.Integer.compareTo(java.lang.Integer)|} }
    function {|java.lang.Integer.compareTo(java.lang.Object)|}((|java.lang.Integer|) [|r0|], (|java.lang.Object|) [|r1|]) returns int
    {
        int ret;
        (|java.lang.Integer|) [|$r2|];
        int [|$i0|];

        loc loc2: live { [|$r2|], [|r0|] }
            do
            {
                [|$r2|] := ((|java.lang.Integer|)) [|r1|];
            }
            goto loc3;
        loc loc3: live { [|$i0|] }
            [|$i0|] := invoke virtual +|java.lang.Integer.compareTo(java.lang.Integer)|+([|r0|], [|$r2|]) goto loc4;
        loc loc4: live {}
            do
            {
                ret := [|$i0|];
            }
            return ret;
    }
    record (|java.lang.Thread|) extends (|java.lang.Object|) { (|java.lang.Object|) /|java.lang.Thread.target|\; }
    function {|java.lang.Thread.<init>()|}((|java.lang.Thread|) [|r0|])
    {

        loc loc1: live {}
            invoke {|java.lang.Object.<init>()|}([|r0|]) goto loc2;
        loc loc2: live {}
            do
            {
            }
            return;
    }
    function {|java.lang.Thread.<init>(java.lang.Object)|}((|java.lang.Thread|) [|r0|], (|java.lang.Object|) [|r1|])
    {

        loc loc2: live { [|r1|], [|r0|] }
            invoke {|java.lang.Object.<init>()|}([|r0|]) goto loc3;
        loc loc3: live {}
            do
            {
                [|r0|]./|java.lang.Thread.target|\ := [|r1|];
            }
            goto loc4;
        loc loc4: live {}
            do
            {
            }
            return;
    }
    function {|java.lang.Thread.start()|}((|java.lang.Thread|) [|r0|])
    {

        loc loc1: live {}
            do
            {
            }
            return;
    }
    function {|java.lang.Thread.run()|}((|java.lang.Thread|) [|r0|])
    {

        loc loc1: live {}
            do
            {
            }
            return;
    }
    record (|java.lang.RuntimeException|) extends (|java.lang.Exception|) {}
    function {|java.lang.RuntimeException.<init>()|}((|java.lang.RuntimeException|) [|r0|])
    {

        loc loc1: live {}
            invoke {|java.lang.Exception.<init>()|}([|r0|]) goto loc2;
        loc loc2: live {}
            do
            {
            }
            return;
    }
    record (|java.lang.Exception|) extends (|java.lang.Object|) {}
    function {|java.lang.Exception.<init>()|}((|java.lang.Exception|) [|r0|])
    {

        loc loc1: live {}
            invoke {|java.lang.Object.<init>()|}([|r0|]) goto loc2;
        loc loc2: live {}
            do
            {
            }
            return;
    }
    top throwable record (|java.lang.Object|) {}
    function {|java.lang.Object.<init>()|}((|java.lang.Object|) [|r0|])
    {

        loc loc1: live {}
            do
            {
            }
            return;
    }
    function {|java.lang.Object.wait()|}((|java.lang.Object|) [|r0|])
    {

        loc loc1: live {}
            do
            {
            }
            return;
    }
    function {|java.lang.Object.notify()|}((|java.lang.Object|) [|r0|])
    {

        loc loc1: live {}
            do
            {
            }
            return;
    }
    function {|java.lang.Object.notifyAll()|}((|java.lang.Object|) [|r0|])
    {

        loc loc1: live {}
            do
            {
            }
            return;
    }
    function {|java.lang.Object.equals(java.lang.Object)|}((|java.lang.Object|) [|r0|], (|java.lang.Object|) [|r1|]) returns boolean
    {
        boolean ret;

        loc loc2: live {}
            when [|r1|] != [|r0|] do
            {
            }
            goto loc4;
            when !([|r1|] != [|r0|]) do
            {
            }
            goto loc3;
        loc loc3: live {}
            do
            {
                ret := true;
            }
            return ret;
        loc loc4: live {}
            do
            {
                ret := false;
            }
            return ret;
    }
    thread (|java.lang.Thread|)((|java.lang.Thread|) [|this|])
    {
        loc loc0: live {}
            when [|this|]./|java.lang.Thread.target|\ == null invoke virtual +|java.lang.Runnable.run()|+([|this|]) return;
            when [|this|]./|java.lang.Thread.target|\ != null invoke virtual +|java.lang.Runnable.run()|+([|this|]./|java.lang.Thread.target|\) return;
    }
    virtual +|java.lang.Runnable.run()|+ { (|java.lang.Thread|) -> {|java.lang.Thread.run()|} }

    record (|java.lang.System|) extends (|java.lang.Object|) {}
	function {|java.lang.System.arraycopy(java.lang.Object[],int,int,int,int)|}
		((|java.lang.Object|)[] [|src|], int [|srcPos|],
		 (|java.lang.Object|)[] [|dest|], int [|destPos|], int [|length|])
	{
		int temp$0;
		
		loc loc0: live { temp$0 }
			when temp$0 < [|length|] do invisible
			{
				[|dest|][[|destPos|] + temp$0]
					:= [|src|][[|srcPos|] + temp$0];
				temp$0 := temp$0 + 1;
			}
			goto loc0;
			when !(temp$0 < [|length|]) do
			{
			}
			return;
	}
    function {|java.lang.System.<init>()|}((|java.lang.System|) [|r0|])
    {

        loc loc1: live {}
            invoke {|java.lang.Object.<init>()|}([|r0|]) goto loc2;
        loc loc2: live {}
            do
            {
            }
            return;
    }
}