Termination of the given JBC could be proven:

0 JBC
↳1 JBC2FIG (⇐)
↳2 FIGraph
↳3 FIGtoITRSProof (⇐)
↳4 ITRS
↳5 ITRSFilterProcessorProof (⇐)
↳6 ITRS
↳7 ITRStoIDPProof (⇔)
↳8 IDP
↳9 UsableRulesProof (⇔)
↳10 IDP
↳11 ItpfGraphProof (⇔)
↳12 IDP
↳13 IDPNonInfProof (⇐)
↳14 AND
    ↳15 IDP
        ↳16 IDependencyGraphProof (⇔)
        ↳17 TRUE
    ↳18 IDP
        ↳19 IDependencyGraphProof (⇔)
        ↳20 TRUE

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_16 (Sun Microsystems Inc.) Main-Class: PastaC10 
/**
 * Example taken from "A Term Rewriting Approach to the Automated Termination
 * Analysis of Imperative Programs" (http://www.cs.unm.edu/~spf/papers/2009-02.pdf)
 * and converted to Java.
 */

public class PastaC10 {
    public static void main(String[] args) {
        Random.args = args;
        int i = Random.random();
        int j = Random.random();

        while (i - j >= 1) {
			i = i - Random.random();
			int r = Random.random() + 1;
			j = j + r;
        }
    } 
}


public class Random {
  static String[] args;
  static int index = 0;

  public static int random() {
    String string = args[index];
    index++;
    return string.length();
  }
}


(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
Graph of 319 nodes with 1 SCC.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph to ITRS rules

(4) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load2257(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → Load2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201)))
Load2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201))) → Cond_Load2257ARR1(i135 + 1 > 0 && i135 + 1 < i5 && i135 > 0 && i135 < i5 && i136 - i137 >= 1 && i135 + 1 + 1 > 0, java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201)))
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201))) → Load2257(java.lang.Object(ARRAY(i5, a5033data)), i135 + 1 + 1, i136 - i201, i137 + i476 + 1)
The set Q consists of the following terms:
Load2257(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load2257ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(5) ITRSFilterProcessorProof (SOUND transformation)

We filter according the heuristic IdpCand1ShapeHeuristic
We removed arguments according to the following replacements:

Load2257ARR1(x1, x2, x3, x4, x5, x6) → Load2257ARR1(x1, x2, x3, x4)

(6) Obligation:

ITRS problem:

The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean

The TRS R consists of the following rules:
Load2257(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → Load2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137)
Load2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → Cond_Load2257ARR1(i135 + 1 > 0 && i135 + 1 < i5 && i135 > 0 && i135 < i5 && i136 - i137 >= 1 && i135 + 1 + 1 > 0, java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201)))
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201))) → Load2257(java.lang.Object(ARRAY(i5, a5033data)), i135 + 1 + 1, i136 - i201, i137 + i476 + 1)
The set Q consists of the following terms:
Load2257(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load2257ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(7) ITRStoIDPProof (EQUIVALENT transformation)

Added dependency pairs

(8) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


The ITRS R consists of the following rules:
Load2257(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → Load2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137)
Load2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → Cond_Load2257ARR1(i135 + 1 > 0 && i135 + 1 < i5 && i135 > 0 && i135 < i5 && i136 - i137 >= 1 && i135 + 1 + 1 > 0, java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201)))
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201))) → Load2257(java.lang.Object(ARRAY(i5, a5033data)), i135 + 1 + 1, i136 - i201, i137 + i476 + 1)

The integer pair graph contains the following rules and edges:
(0): LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) → LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])
(1): LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(i135[1] + 1 > 0 && i135[1] + 1 < i5[1] && i135[1] > 0 && i135[1] < i5[1] && i136[1] - i137[1] >= 1 && i135[1] + 1 + 1 > 0, java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))
(2): COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2]))) → LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2] + 1 + 1, i136[2] - i201[2], i137[2] + i476[2] + 1)

(0) -> (1), if ((i137[0] →* i137[1])∧(i135[0] →* i135[1])∧(java.lang.Object(ARRAY(i5[0], a5033data[0])) →* java.lang.Object(ARRAY(i5[1], a5033data[1])))∧(i136[0] →* i136[1]))


(1) -> (2), if ((java.lang.Object(java.lang.String(i476[1])) →* java.lang.Object(java.lang.String(i476[2])))∧(i135[1] + 1 > 0 && i135[1] + 1 < i5[1] && i135[1] > 0 && i135[1] < i5[1] && i136[1] - i137[1] >= 1 && i135[1] + 1 + 1 > 0 →* TRUE)∧(i137[1] →* i137[2])∧(java.lang.Object(ARRAY(i5[1], a5033data[1])) →* java.lang.Object(ARRAY(i5[2], a5033data[2])))∧(java.lang.Object(java.lang.String(i201[1])) →* java.lang.Object(java.lang.String(i201[2])))∧(i135[1] →* i135[2])∧(i136[1] →* i136[2]))


(2) -> (0), if ((i135[2] + 1 + 1 →* i135[0])∧(java.lang.Object(ARRAY(i5[2], a5033data[2])) →* java.lang.Object(ARRAY(i5[0], a5033data[0])))∧(i137[2] + i476[2] + 1 →* i137[0])∧(i136[2] - i201[2] →* i136[0]))



The set Q consists of the following terms:
Load2257(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load2257ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(9) UsableRulesProof (EQUIVALENT transformation)

As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.

(10) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) → LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])
(1): LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(i135[1] + 1 > 0 && i135[1] + 1 < i5[1] && i135[1] > 0 && i135[1] < i5[1] && i136[1] - i137[1] >= 1 && i135[1] + 1 + 1 > 0, java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))
(2): COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2]))) → LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2] + 1 + 1, i136[2] - i201[2], i137[2] + i476[2] + 1)

(0) -> (1), if ((i137[0] →* i137[1])∧(i135[0] →* i135[1])∧(java.lang.Object(ARRAY(i5[0], a5033data[0])) →* java.lang.Object(ARRAY(i5[1], a5033data[1])))∧(i136[0] →* i136[1]))


(1) -> (2), if ((java.lang.Object(java.lang.String(i476[1])) →* java.lang.Object(java.lang.String(i476[2])))∧(i135[1] + 1 > 0 && i135[1] + 1 < i5[1] && i135[1] > 0 && i135[1] < i5[1] && i136[1] - i137[1] >= 1 && i135[1] + 1 + 1 > 0 →* TRUE)∧(i137[1] →* i137[2])∧(java.lang.Object(ARRAY(i5[1], a5033data[1])) →* java.lang.Object(ARRAY(i5[2], a5033data[2])))∧(java.lang.Object(java.lang.String(i201[1])) →* java.lang.Object(java.lang.String(i201[2])))∧(i135[1] →* i135[2])∧(i136[1] →* i136[2]))


(2) -> (0), if ((i135[2] + 1 + 1 →* i135[0])∧(java.lang.Object(ARRAY(i5[2], a5033data[2])) →* java.lang.Object(ARRAY(i5[0], a5033data[0])))∧(i137[2] + i476[2] + 1 →* i137[0])∧(i136[2] - i201[2] →* i136[0]))



The set Q consists of the following terms:
Load2257(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load2257ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(11) ItpfGraphProof (EQUIVALENT transformation)

Applied rule ItpfICap [ICap]

(12) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) → LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])
(1): LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(i135[1] + 1 > 0 && i135[1] + 1 < i5[1] && i135[1] > 0 && i135[1] < i5[1] && i136[1] - i137[1] >= 1 && i135[1] + 1 + 1 > 0, java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))
(2): COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2]))) → LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2] + 1 + 1, i136[2] - i201[2], i137[2] + i476[2] + 1)

(0) -> (1), if ((i137[0] →* i137[1])∧(i135[0] →* i135[1])∧((i5[0] →* i5[1])∧(a5033data[0] →* a5033data[1]))∧(i136[0] →* i136[1]))


(1) -> (2), if (((i476[1] →* i476[2]))∧(i135[1] + 1 > 0 && i135[1] + 1 < i5[1] && i135[1] > 0 && i135[1] < i5[1] && i136[1] - i137[1] >= 1 && i135[1] + 1 + 1 > 0 →* TRUE)∧(i137[1] →* i137[2])∧((i5[1] →* i5[2])∧(a5033data[1] →* a5033data[2]))∧((i201[1] →* i201[2]))∧(i135[1] →* i135[2])∧(i136[1] →* i136[2]))


(2) -> (0), if ((i135[2] + 1 + 1 →* i135[0])∧((i5[2] →* i5[0])∧(a5033data[2] →* a5033data[0]))∧(i137[2] + i476[2] + 1 →* i137[0])∧(i136[2] - i201[2] →* i136[0]))



The set Q consists of the following terms:
Load2257(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load2257ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(13) IDPNonInfProof (SOUND transformation)

The constraints were generated the following way:
The DP Problem is simplified using the Induction Calculus [NONINF] with the following steps:
Note that final constraints are written in bold face.


For Pair LOAD2257(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → LOAD2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) the following chains were created:
  • We consider the chain LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) → LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]), LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1]))) which results in the following constraint:

    (1)    (i137[0]=i137[1]∧i135[0]=i135[1]∧i5[0]=i5[1]∧a5033data[0]=a5033data[1]∧i136[0]=i136[1] ⇒ LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])≥NonInfC∧LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])≥LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])∧(UIncreasing(LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])), ≥))



    We simplified constraint (1) using rule (IV) which results in the following new constraint:

    (2)    (LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])≥NonInfC∧LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])≥LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])∧(UIncreasing(LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])), ≥))



    We simplified constraint (2) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (3)    ((UIncreasing(LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])), ≥)∧[1 + (-1)bso_33] ≥ 0)



    We simplified constraint (3) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (4)    ((UIncreasing(LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])), ≥)∧[1 + (-1)bso_33] ≥ 0)



    We simplified constraint (4) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (5)    ((UIncreasing(LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])), ≥)∧[1 + (-1)bso_33] ≥ 0)



    We simplified constraint (5) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (6)    ((UIncreasing(LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_33] ≥ 0)







For Pair LOAD2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135, 1), 0), <(+(i135, 1), i5)), >(i135, 0)), <(i135, i5)), >=(-(i136, i137), 1)), >(+(+(i135, 1), 1), 0)), java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201))) the following chains were created:
  • We consider the chain LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) → LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]), LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1]))), COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2]))) → LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1))) which results in the following constraint:

    (7)    (i137[0]=i137[1]∧i135[0]=i135[1]∧i5[0]=i5[1]∧a5033data[0]=a5033data[1]∧i136[0]=i136[1]∧i476[1]=i476[2]∧&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0))=TRUE∧i137[1]=i137[2]∧i5[1]=i5[2]∧a5033data[1]=a5033data[2]∧i201[1]=i201[2]∧i135[1]=i135[2]∧i136[1]=i136[2] ⇒ LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1])≥NonInfC∧LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1])≥COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))∧(UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥))



    We simplified constraint (7) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (8)    (>(+(+(i135[1], 1), 1), 0)=TRUE∧>=(-(i136[1], i137[1]), 1)=TRUE∧<(i135[1], i5[1])=TRUE∧>(i135[1], 0)=TRUE∧>(+(i135[1], 1), 0)=TRUE∧<(+(i135[1], 1), i5[1])=TRUE ⇒ LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[0])), i135[1], i136[1], i137[1])≥NonInfC∧LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[0])), i135[1], i136[1], i137[1])≥COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[0])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))∧(UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥))



    We simplified constraint (8) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (9)    (i135[1] + [1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-1] + [-1]i135[1] ≥ 0∧i135[1] + [-1] ≥ 0∧i135[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧[(3)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i135[1] + [bni_34]i5[1] ≥ 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (9) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (10)    (i135[1] + [1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-1] + [-1]i135[1] ≥ 0∧i135[1] + [-1] ≥ 0∧i135[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧[(3)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i135[1] + [bni_34]i5[1] ≥ 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (10) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (11)    (i135[1] + [1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-1] + [-1]i135[1] ≥ 0∧i135[1] + [-1] ≥ 0∧i135[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧[(3)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i135[1] + [bni_34]i5[1] ≥ 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (11) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (12)    (i135[1] + [1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-1] + [-1]i135[1] ≥ 0∧i135[1] + [-1] ≥ 0∧i135[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(3)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i135[1] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (12) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (13)    ([2] + i135[1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] + [-3] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i135[1] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (13) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (14)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] + [-3] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(2)bni_34 + (-1)Bound*bni_34] + [(-1)bni_34]i135[1] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (14) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (15)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧[-1] + i5[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(4)bni_34 + (-1)Bound*bni_34] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (15) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (16)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(5)bni_34 + (-1)Bound*bni_34] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)



    We simplified constraint (16) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (17)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0∧i137[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(5)bni_34 + (-1)Bound*bni_34] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)


    (18)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0∧i137[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(5)bni_34 + (-1)Bound*bni_34] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)







For Pair COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201))) → LOAD2257(java.lang.Object(ARRAY(i5, a5033data)), +(+(i135, 1), 1), -(i136, i201), +(i137, +(i476, 1))) the following chains were created:
  • We consider the chain LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1]))), COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2]))) → LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1))), LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) → LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) which results in the following constraint:

    (19)    (i476[1]=i476[2]∧&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0))=TRUE∧i137[1]=i137[2]∧i5[1]=i5[2]∧a5033data[1]=a5033data[2]∧i201[1]=i201[2]∧i135[1]=i135[2]∧i136[1]=i136[2]∧+(+(i135[2], 1), 1)=i135[0]∧i5[2]=i5[0]∧a5033data[2]=a5033data[0]∧+(i137[2], +(i476[2], 1))=i137[0]∧-(i136[2], i201[2])=i136[0] ⇒ COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2])))≥NonInfC∧COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2])))≥LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))∧(UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥))



    We simplified constraint (19) using rules (III), (IV), (IDP_BOOLEAN) which results in the following new constraint:

    (20)    (>(+(+(i135[1], 1), 1), 0)=TRUE∧>=(-(i136[1], i137[1]), 1)=TRUE∧<(i135[1], i5[1])=TRUE∧>(i135[1], 0)=TRUE∧>(+(i135[1], 1), 0)=TRUE∧<(+(i135[1], 1), i5[1])=TRUE ⇒ COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))≥NonInfC∧COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))≥LOAD2257(java.lang.Object(ARRAY(i5[1], a5033data[1])), +(+(i135[1], 1), 1), -(i136[1], i201[1]), +(i137[1], +(i476[1], 1)))∧(UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥))



    We simplified constraint (20) using rule (POLY_CONSTRAINTS) which results in the following new constraint:

    (21)    (i135[1] + [1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-1] + [-1]i135[1] ≥ 0∧i135[1] + [-1] ≥ 0∧i135[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧[(2)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]i135[1] + [bni_36]i5[1] ≥ 0∧[(-1)bso_37] ≥ 0)



    We simplified constraint (21) using rule (IDP_POLY_SIMPLIFY) which results in the following new constraint:

    (22)    (i135[1] + [1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-1] + [-1]i135[1] ≥ 0∧i135[1] + [-1] ≥ 0∧i135[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧[(2)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]i135[1] + [bni_36]i5[1] ≥ 0∧[(-1)bso_37] ≥ 0)



    We simplified constraint (22) using rule (POLY_REMOVE_MIN_MAX) which results in the following new constraint:

    (23)    (i135[1] + [1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-1] + [-1]i135[1] ≥ 0∧i135[1] + [-1] ≥ 0∧i135[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧[(2)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]i135[1] + [bni_36]i5[1] ≥ 0∧[(-1)bso_37] ≥ 0)



    We simplified constraint (23) using rule (IDP_UNRESTRICTED_VARS) which results in the following new constraint:

    (24)    (i135[1] + [1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-1] + [-1]i135[1] ≥ 0∧i135[1] + [-1] ≥ 0∧i135[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(2)bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]i135[1] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)



    We simplified constraint (24) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (25)    ([2] + i135[1] ≥ 0∧i136[1] + [-1] + [-1]i137[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] + [-3] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]i135[1] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)



    We simplified constraint (25) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (26)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧i5[1] + [-2] + [-1]i135[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] + [-3] + [-1]i135[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[bni_36 + (-1)Bound*bni_36] + [(-1)bni_36]i135[1] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)



    We simplified constraint (26) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (27)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧[-1] + i5[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(3)bni_36 + (-1)Bound*bni_36] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)



    We simplified constraint (27) using rule (IDP_SMT_SPLIT) which results in the following new constraint:

    (28)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)



    We simplified constraint (28) using rule (IDP_SMT_SPLIT) which results in the following new constraints:

    (29)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0∧i137[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)


    (30)    ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0∧i137[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)







To summarize, we get the following constraints P≥ for the following pairs.
  • LOAD2257(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → LOAD2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137)
    • ((UIncreasing(LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])), ≥)∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧0 = 0∧[1 + (-1)bso_33] ≥ 0)

  • LOAD2257ARR1(java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137) → COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135, 1), 0), <(+(i135, 1), i5)), >(i135, 0)), <(i135, i5)), >=(-(i136, i137), 1)), >(+(+(i135, 1), 1), 0)), java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201)))
    • ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0∧i137[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(5)bni_34 + (-1)Bound*bni_34] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)
    • ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0∧i137[1] ≥ 0 ⇒ (UIncreasing(COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))), ≥)∧0 = 0∧[(5)bni_34 + (-1)Bound*bni_34] + [bni_34]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_35] ≥ 0)

  • COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5, a5033data)), i135, i136, i137, java.lang.Object(java.lang.String(i476)), java.lang.Object(java.lang.String(i201))) → LOAD2257(java.lang.Object(ARRAY(i5, a5033data)), +(+(i135, 1), 1), -(i136, i201), +(i137, +(i476, 1)))
    • ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0∧i137[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)
    • ([2] + i135[1] ≥ 0∧i136[1] ≥ 0∧[1] + i5[1] ≥ 0∧i135[1] ≥ 0∧[1] + i135[1] ≥ 0∧i5[1] ≥ 0∧i137[1] ≥ 0 ⇒ (UIncreasing(LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))), ≥)∧0 = 0∧0 = 0∧0 = 0∧[(4)bni_36 + (-1)Bound*bni_36] + [bni_36]i5[1] ≥ 0∧0 = 0∧0 = 0∧0 = 0∧[(-1)bso_37] ≥ 0)




The constraints for P> respective Pbound are constructed from P≥ where we just replace every occurence of "t ≥ s" in P≥ by "t > s" respective "t ≥ c". Here c stands for the fresh constant used for Pbound.
Using the following integer polynomial ordering the resulting constraints can be solved
Polynomial interpretation over integers[POLO]:

POL(TRUE) = 0   
POL(FALSE) = [2]   
POL(LOAD2257(x1, x2, x3, x4)) = [1] + [-1]x2 + [-1]x1   
POL(java.lang.Object(x1)) = [-1] + [-1]x1   
POL(ARRAY(x1, x2)) = [2] + x1   
POL(LOAD2257ARR1(x1, x2, x3, x4)) = [-1]x2 + [-1]x1   
POL(COND_LOAD2257ARR1(x1, x2, x3, x4, x5, x6, x7)) = [-1] + [-1]x3 + [-1]x2 + [-1]x1   
POL(&&(x1, x2)) = [-1]   
POL(>(x1, x2)) = [-1]   
POL(+(x1, x2)) = x1 + x2   
POL(1) = [1]   
POL(0) = 0   
POL(<(x1, x2)) = [-1]   
POL(>=(x1, x2)) = [-1]   
POL(-(x1, x2)) = x1 + [-1]x2   
POL(java.lang.String(x1)) = [-1] + [-1]x1   

The following pairs are in P>:

LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) → LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])

The following pairs are in Pbound:

LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))
COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2]))) → LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))

The following pairs are in P≥:

LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(&&(&&(&&(&&(&&(>(+(i135[1], 1), 0), <(+(i135[1], 1), i5[1])), >(i135[1], 0)), <(i135[1], i5[1])), >=(-(i136[1], i137[1]), 1)), >(+(+(i135[1], 1), 1), 0)), java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))
COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2]))) → LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), +(+(i135[2], 1), 1), -(i136[2], i201[2]), +(i137[2], +(i476[2], 1)))

At least the following rules have been oriented under context sensitive arithmetic replacement:

TRUE1 → &&(TRUE, TRUE)1
FALSE1 → &&(TRUE, FALSE)1
FALSE1 → &&(FALSE, TRUE)1
FALSE1 → &&(FALSE, FALSE)1

(14) Complex Obligation (AND)

(15) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:

Boolean, Integer


R is empty.

The integer pair graph contains the following rules and edges:
(1): LOAD2257ARR1(java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1]) → COND_LOAD2257ARR1(i135[1] + 1 > 0 && i135[1] + 1 < i5[1] && i135[1] > 0 && i135[1] < i5[1] && i136[1] - i137[1] >= 1 && i135[1] + 1 + 1 > 0, java.lang.Object(ARRAY(i5[1], a5033data[1])), i135[1], i136[1], i137[1], java.lang.Object(java.lang.String(i476[1])), java.lang.Object(java.lang.String(i201[1])))
(2): COND_LOAD2257ARR1(TRUE, java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2], i136[2], i137[2], java.lang.Object(java.lang.String(i476[2])), java.lang.Object(java.lang.String(i201[2]))) → LOAD2257(java.lang.Object(ARRAY(i5[2], a5033data[2])), i135[2] + 1 + 1, i136[2] - i201[2], i137[2] + i476[2] + 1)

(1) -> (2), if (((i476[1] →* i476[2]))∧(i135[1] + 1 > 0 && i135[1] + 1 < i5[1] && i135[1] > 0 && i135[1] < i5[1] && i136[1] - i137[1] >= 1 && i135[1] + 1 + 1 > 0 →* TRUE)∧(i137[1] →* i137[2])∧((i5[1] →* i5[2])∧(a5033data[1] →* a5033data[2]))∧((i201[1] →* i201[2]))∧(i135[1] →* i135[2])∧(i136[1] →* i136[2]))



The set Q consists of the following terms:
Load2257(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load2257ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(16) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 2 less nodes.

(17) TRUE

(18) Obligation:

IDP problem:
The following function symbols are pre-defined:
!=~Neq: (Integer, Integer) -> Boolean
*~Mul: (Integer, Integer) -> Integer
>=~Ge: (Integer, Integer) -> Boolean
-1~UnaryMinus: (Integer) -> Integer
|~Bwor: (Integer, Integer) -> Integer
/~Div: (Integer, Integer) -> Integer
=~Eq: (Integer, Integer) -> Boolean
~Bwxor: (Integer, Integer) -> Integer
||~Lor: (Boolean, Boolean) -> Boolean
!~Lnot: (Boolean) -> Boolean
<~Lt: (Integer, Integer) -> Boolean
-~Sub: (Integer, Integer) -> Integer
<=~Le: (Integer, Integer) -> Boolean
>~Gt: (Integer, Integer) -> Boolean
~~Bwnot: (Integer) -> Integer
%~Mod: (Integer, Integer) -> Integer
&~Bwand: (Integer, Integer) -> Integer
+~Add: (Integer, Integer) -> Integer
&&~Land: (Boolean, Boolean) -> Boolean


The following domains are used:
none


R is empty.

The integer pair graph contains the following rules and edges:
(0): LOAD2257(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0]) → LOAD2257ARR1(java.lang.Object(ARRAY(i5[0], a5033data[0])), i135[0], i136[0], i137[0])


The set Q consists of the following terms:
Load2257(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Load2257ARR1(java.lang.Object(ARRAY(x0, x1)), x2, x3, x4)
Cond_Load2257ARR1(TRUE, java.lang.Object(ARRAY(x0, x1)), x2, x3, x4, java.lang.Object(java.lang.String(x5)), java.lang.Object(java.lang.String(x6)))

(19) IDependencyGraphProof (EQUIVALENT transformation)

The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.

(20) TRUE