Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

/**
 * 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 PastaB14 {
    public static void main(String[] args) {
        Random.args = args;
        int x = Random.random();
        int y = Random.random();

        while (x == y && x > 0) {
            while (y > 0) {
                x--;
                y--;                
            }
        }
    }
}


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:
PastaB14.main([Ljava/lang/String;)V: Graph of 190 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: PastaB14.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 20 IRules

P rules:
f1713_0_main_Load(EOS, i498, i499, i498) → f1715_0_main_NE(EOS, i498, i499, i498, i499)
f1715_0_main_NE(EOS, i499, i499, i499, i499) → f1719_0_main_NE(EOS, i499, i499, i499, i499)
f1719_0_main_NE(EOS, i499, i499, i499, i499) → f1723_0_main_Load(EOS, i499, i499)
f1723_0_main_Load(EOS, i499, i499) → f1728_0_main_LE(EOS, i499, i499, i499)
f1728_0_main_LE(EOS, i508, i508, i508) → f1732_0_main_LE(EOS, i508, i508, i508)
f1732_0_main_LE(EOS, i508, i508, i508) → f1741_0_main_Load(EOS, i508, i508) | >(i508, 0)
f1741_0_main_Load(EOS, i508, i508) → f1770_0_main_Load(EOS, i508, i508)
f1770_0_main_Load(EOS, i515, i516) → f2347_0_main_Load(EOS, i515, i516)
f2347_0_main_Load(EOS, i705, i707) → f2875_0_main_Load(EOS, i705, i707)
f2875_0_main_Load(EOS, i883, i884) → f2880_0_main_LE(EOS, i883, i884, i884)
f2880_0_main_LE(EOS, i883, matching1, matching2) → f2882_0_main_LE(EOS, i883, 0, 0) | &&(=(matching1, 0), =(matching2, 0))
f2880_0_main_LE(EOS, i883, i893, i893) → f2883_0_main_LE(EOS, i883, i893, i893)
f2882_0_main_LE(EOS, i883, matching1, matching2) → f2893_0_main_Load(EOS, i883, 0) | &&(&&(<=(0, 0), =(matching1, 0)), =(matching2, 0))
f2893_0_main_Load(EOS, i883, matching1) → f1709_0_main_Load(EOS, i883, 0) | =(matching1, 0)
f1709_0_main_Load(EOS, i498, i499) → f1713_0_main_Load(EOS, i498, i499, i498)
f2883_0_main_LE(EOS, i883, i893, i893) → f2894_0_main_Inc(EOS, i883, i893) | >(i893, 0)
f2894_0_main_Inc(EOS, i883, i893) → f3383_0_main_Inc(EOS, +(i883, -1), i893)
f3383_0_main_Inc(EOS, i1061, i893) → f3384_0_main_JMP(EOS, i1061, +(i893, -1)) | >(i893, 0)
f3384_0_main_JMP(EOS, i1061, i1062) → f3391_0_main_Load(EOS, i1061, i1062)
f3391_0_main_Load(EOS, i1061, i1062) → f2875_0_main_Load(EOS, i1061, i1062)

Combined rules. Obtained 1 IRules

P rules:
f2880_0_main_LE(EOS, x0, x1, x1) → f2880_0_main_LE(EOS, -(x0, 1), -(x1, 1), -(x1, 1)) | >(x1, 0)

Filtered ground terms:

f2880_0_main_LE(x1, x2, x3, x4) → f2880_0_main_LE(x2, x3, x4)
Cond_f2880_0_main_LE(x1, x2, x3, x4, x5) → Cond_f2880_0_main_LE(x1, x3, x4, x5)

Filtered duplicate terms:

f2880_0_main_LE(x1, x2, x3) → f2880_0_main_LE(x1, x3)
Cond_f2880_0_main_LE(x1, x2, x3, x4) → Cond_f2880_0_main_LE(x1, x2, x4)

Filtered unneeded terms:

Cond_f2880_0_main_LE(x1, x2, x3) → Cond_f2880_0_main_LE(x1, x3)
f2880_0_main_LE(x1, x2) → f2880_0_main_LE(x2)

Prepared 1 rules for path length conversion:

P rules:
f2880_0_main_LE(x1) → f2880_0_main_LE(-(x1, 1)) | >(x1, 0)

Finished conversion. Obtained 1 rules.

P rules:
f2880_0_main_LE(x0) → f2880_0_main_LE(-(x0, 1)) | >(x0, 0)

(6) Obligation:

Rules:
f2880_0_main_LE(x0) → f2880_0_main_LE(-(x0, 1)) | >(x0, 0)

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f2880_0_main_LE(x2)] = x2

Therefore the following rule(s) have been dropped:

f2880_0_main_LE(x0) → f2880_0_main_LE(-(x0, 1)) | >(x0, 0)

(8) YES