Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class CountUpRound{
  public static int round (int x) {

    if (x % 2 == 0) return x;
    else return x+1;
  }


  public static void main(String[] args) {
    Random.args = args;
    int x = Random.random();
    int y = Random.random();



    while (x > y) {

      y = round(y+1);

    }


  }

}


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

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

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
CountUpRound.main([Ljava/lang/String;)V: Graph of 193 nodes with 1 SCC.

(3) TerminationGraphToSCCProof (SOUND transformation)

Splitted TerminationGraph to 1 SCCs.

(4) Obligation:

SCC of termination graph based on JBC Program.
SCC contains nodes from the following methods: CountUpRound.main([Ljava/lang/String;)V
SCC calls the following helper methods:
Performed SCC analyses:

• Used field analysis yielded the following read fields:
  
• Marker field analysis yielded the following relations that could be markers:
  

(5) SCCToIntTRSProof (SOUND transformation)

Transformed FIGraph SCCs to intTRSs. Log:

Generated rules. Obtained 27 IRules

P rules:
f378_0_main_Load(EOS, i18, i47, i18) → f389_0_main_LE(EOS, i18, i47, i18, i47)
f389_0_main_LE(EOS, i18, i47, i18, i47) → f414_0_main_LE(EOS, i18, i47, i18, i47)
f414_0_main_LE(EOS, i18, i47, i18, i47) → f426_0_main_Load(EOS, i18, i47) | >(i18, i47)
f426_0_main_Load(EOS, i18, i47) → f435_0_main_ConstantStackPush(EOS, i18, i47)
f435_0_main_ConstantStackPush(EOS, i18, i47) → f447_0_main_IntArithmetic(EOS, i18, i47, 1)
f447_0_main_IntArithmetic(EOS, i18, i47, matching1) → f459_0_main_InvokeMethod(EOS, i18, +(i47, 1)) | &&(>=(i47, 0), =(matching1, 1))
f459_0_main_InvokeMethod(EOS, i18, i60) → f470_0_round_Load(EOS, i18, i60, i60)
f470_0_round_Load(EOS, i18, i60, i60) → f493_0_round_ConstantStackPush(EOS, i18, i60, i60, i60)
f493_0_round_ConstantStackPush(EOS, i18, i60, i60, i60) → f504_0_round_IntArithmetic(EOS, i18, i60, i60, i60, 2)
f504_0_round_IntArithmetic(EOS, i18, i60, i60, i60, matching1) → f516_0_round_NE(EOS, i18, i60, i60, %(i60, 2)) | =(matching1, 2)
f516_0_round_NE(EOS, i18, i60, i60, matching1) → f526_0_round_NE(EOS, i18, i60, i60, 1) | =(matching1, 1)
f516_0_round_NE(EOS, i18, i60, i60, matching1) → f527_0_round_NE(EOS, i18, i60, i60, 0) | =(matching1, 0)
f526_0_round_NE(EOS, i18, i60, i60, matching1) → f535_0_round_Load(EOS, i18, i60, i60) | &&(>(1, 0), =(matching1, 1))
f535_0_round_Load(EOS, i18, i60, i60) → f546_0_round_ConstantStackPush(EOS, i18, i60, i60)
f546_0_round_ConstantStackPush(EOS, i18, i60, i60) → f554_0_round_IntArithmetic(EOS, i18, i60, i60, 1)
f554_0_round_IntArithmetic(EOS, i18, i60, i60, matching1) → f563_0_round_Return(EOS, i18, i60, +(i60, 1)) | &&(>(i60, 0), =(matching1, 1))
f563_0_round_Return(EOS, i18, i60, i69) → f574_0_main_Store(EOS, i18, i69)
f574_0_main_Store(EOS, i18, i69) → f611_0_main_JMP(EOS, i18, i69)
f611_0_main_JMP(EOS, i18, i69) → f1094_0_main_Load(EOS, i18, i69)
f1094_0_main_Load(EOS, i18, i69) → f367_0_main_Load(EOS, i18, i69)
f367_0_main_Load(EOS, i18, i47) → f378_0_main_Load(EOS, i18, i47, i18)
f527_0_round_NE(EOS, i18, i60, i60, matching1) → f538_0_round_Load(EOS, i18, i60, i60) | =(matching1, 0)
f538_0_round_Load(EOS, i18, i60, i60) → f548_0_round_Return(EOS, i18, i60, i60, i60)
f548_0_round_Return(EOS, i18, i60, i60, i60) → f556_0_main_Store(EOS, i18, i60)
f556_0_main_Store(EOS, i18, i60) → f566_0_main_JMP(EOS, i18, i60)
f566_0_main_JMP(EOS, i18, i60) → f606_0_main_Load(EOS, i18, i60)
f606_0_main_Load(EOS, i18, i60) → f367_0_main_Load(EOS, i18, i60)

Combined rules. Obtained 2 IRules

P rules:
f378_0_main_Load(EOS, x0, x1, x0) → f378_0_main_Load(EOS, x0, +(x1, 2), x0) | &&(&&(>(+(x1, 1), 0), =(%(+(x1, 1), 2), 1)), <(x1, x0))
f378_0_main_Load(EOS, x0, x1, x0) → f378_0_main_Load(EOS, x0, +(x1, 1), x0) | &&(&&(>(+(x1, 1), 0), =(%(+(x1, 1), 2), 0)), <(x1, x0))

Filtered ground terms:

f378_0_main_Load(x1, x2, x3, x4) → f378_0_main_Load(x2, x3, x4)
Cond_f378_0_main_Load(x1, x2, x3, x4, x5) → Cond_f378_0_main_Load(x1, x3, x4, x5)
Cond_f378_0_main_Load1(x1, x2, x3, x4, x5) → Cond_f378_0_main_Load1(x1, x3, x4, x5)

Filtered duplicate terms:

f378_0_main_Load(x1, x2, x3) → f378_0_main_Load(x2, x3)
Cond_f378_0_main_Load(x1, x2, x3, x4) → Cond_f378_0_main_Load(x1, x3, x4)
Cond_f378_0_main_Load1(x1, x2, x3, x4) → Cond_f378_0_main_Load1(x1, x3, x4)

Prepared 2 rules for path length conversion:

P rules:
f378_0_main_Load(x1, x0) → f378_0_main_Load(+(x1, 2), x0) | &&(&&(>(+(x1, 1), 0), =(%(+(x1, 1), 2), 1)), <(x1, x0))
f378_0_main_Load(x1, x0) → f378_0_main_Load(+(x1, 1), x0) | &&(&&(>(+(x1, 1), 0), =(%(+(x1, 1), 2), 0)), <(x1, x0))

Finished conversion. Obtained 4 rules.

P rules:
f378_0_main_Load(x0, x1) → f378_0_main_Load'(x0, x1) | &&(&&(>(x1, x0), =(-(+(x0, 1), *(2, div)), 1)), >(x0, -1))
f378_0_main_Load'(x0, x1) → f378_0_main_Load(+(x0, 2), x1) | &&(&&(&&(&&(>(x1, x0), >(x0, -1)), >=(-(+(x0, 1), *(2, div)), 0)), <(-(+(x0, 1), *(2, div)), 2)), =(-(+(x0, 1), *(2, div)), 1))
f378_0_main_Load(x2, x3) → f378_0_main_Load'(x2, x3) | &&(&&(>(x3, x2), =(-(+(x2, 1), *(2, div)), 0)), >(x2, -1))
f378_0_main_Load'(x2, x3) → f378_0_main_Load(+(x2, 1), x3) | &&(&&(&&(&&(>(x3, x2), >(x2, -1)), >=(-(+(x2, 1), *(2, div)), 0)), <(-(+(x2, 1), *(2, div)), 2)), =(-(+(x2, 1), *(2, div)), 0))

(6) Obligation:

Rules:
f378_0_main_Load(x0, x1) → f378_0_main_Load'(x0, x1) | &&(&&(>(x1, x0), =(-(+(x0, 1), *(2, div)), 1)), >(x0, -1))
f378_0_main_Load'(x0, x1) → f378_0_main_Load(+(x0, 2), x1) | &&(&&(&&(&&(>(x1, x0), >(x0, -1)), >=(-(+(x0, 1), *(2, div)), 0)), <(-(+(x0, 1), *(2, div)), 2)), =(-(+(x0, 1), *(2, div)), 1))
f378_0_main_Load(x2, x3) → f378_0_main_Load'(x2, x3) | &&(&&(>(x3, x2), =(-(+(x2, 1), *(2, div)), 0)), >(x2, -1))
f378_0_main_Load'(x2, x3) → f378_0_main_Load(+(x2, 1), x3) | &&(&&(&&(&&(>(x3, x2), >(x2, -1)), >=(-(+(x2, 1), *(2, div)), 0)), <(-(+(x2, 1), *(2, div)), 2)), =(-(+(x2, 1), *(2, div)), 0))

(7) TerminationGraphProcessor (SOUND transformation)

Constructed the termination graph and obtained one non-trivial SCC.

(8) Obligation:

Rules:
f378_0_main_Load(x0, x1) → f378_0_main_Load'(x0, x1) | &&(&&(>(x1, x0), =(-(+(x0, 1), *(2, x2)), 1)), >(x0, -1))
f378_0_main_Load'(x3, x4) → f378_0_main_Load(+(x3, 2), x4) | &&(&&(&&(&&(>(x4, x3), >(x3, -1)), >=(-(+(x3, 1), *(2, x5)), 0)), <(-(+(x3, 1), *(2, x5)), 2)), =(-(+(x3, 1), *(2, x5)), 1))

(9) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f378_0_main_Load(x7, x9)] = 1 - x7 + x9
[f378_0_main_Load'(x12, x14)] = -x12 + x14

Therefore the following rule(s) have been dropped:

f378_0_main_Load(x0, x1) → f378_0_main_Load'(x0, x1) | &&(&&(>(x1, x0), =(-(+(x0, 1), *(2, x2)), 1)), >(x0, -1))
f378_0_main_Load'(x3, x4) → f378_0_main_Load(+(x3, 2), x4) | &&(&&(&&(&&(>(x4, x3), >(x3, -1)), >=(-(+(x3, 1), *(2, x5)), 0)), <(-(+(x3, 1), *(2, x5)), 2)), =(-(+(x3, 1), *(2, x5)), 1))

(10) YES