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

        if (x > 0) {
            while (x != 0) {
                if (x % 2 == 0) {
                    x = x/2;
                } else {
                    x--;
                }
            }
        }
    }
}


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:
PastaB8.main([Ljava/lang/String;)V: Graph of 124 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: PastaB8.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 19 IRules

P rules:
f330_0_main_EQ(EOS, i52, i52) → f335_0_main_EQ(EOS, i52, i52)
f335_0_main_EQ(EOS, i52, i52) → f341_0_main_Load(EOS, i52) | >(i52, 0)
f341_0_main_Load(EOS, i52) → f352_0_main_ConstantStackPush(EOS, i52, i52)
f352_0_main_ConstantStackPush(EOS, i52, i52) → f358_0_main_IntArithmetic(EOS, i52, i52, 2)
f358_0_main_IntArithmetic(EOS, i52, i52, matching1) → f363_0_main_NE(EOS, i52, %(i52, 2)) | =(matching1, 2)
f363_0_main_NE(EOS, i52, matching1) → f367_0_main_NE(EOS, i52, 1) | =(matching1, 1)
f363_0_main_NE(EOS, i52, matching1) → f368_0_main_NE(EOS, i52, 0) | =(matching1, 0)
f367_0_main_NE(EOS, i52, matching1) → f371_0_main_Inc(EOS, i52) | &&(>(1, 0), =(matching1, 1))
f371_0_main_Inc(EOS, i52) → f375_0_main_JMP(EOS, +(i52, -1)) | >(i52, 0)
f375_0_main_JMP(EOS, i58) → f396_0_main_Load(EOS, i58)
f396_0_main_Load(EOS, i58) → f318_0_main_Load(EOS, i58)
f318_0_main_Load(EOS, i40) → f330_0_main_EQ(EOS, i40, i40)
f368_0_main_NE(EOS, i52, matching1) → f372_0_main_Load(EOS, i52) | =(matching1, 0)
f372_0_main_Load(EOS, i52) → f377_0_main_ConstantStackPush(EOS, i52)
f377_0_main_ConstantStackPush(EOS, i52) → f399_0_main_IntArithmetic(EOS, i52, 2)
f399_0_main_IntArithmetic(EOS, i52, matching1) → f740_0_main_Store(EOS, /(i52, 2)) | &&(>=(i52, 1), =(matching1, 2))
f740_0_main_Store(EOS, i137) → f742_0_main_JMP(EOS, i137)
f742_0_main_JMP(EOS, i137) → f749_0_main_Load(EOS, i137)
f749_0_main_Load(EOS, i137) → f318_0_main_Load(EOS, i137)

Combined rules. Obtained 2 IRules

P rules:
f330_0_main_EQ(EOS, x0, x0) → f330_0_main_EQ(EOS, -(x0, 1), -(x0, 1)) | &&(>(x0, 0), =(%(x0, 2), 1))
f330_0_main_EQ(EOS, x0, x0) → f330_0_main_EQ(EOS, /(x0, 2), /(x0, 2)) | &&(=(%(x0, 2), 0), >(+(x0, 1), 1))

Filtered ground terms:

f330_0_main_EQ(x1, x2, x3) → f330_0_main_EQ(x2, x3)
Cond_f330_0_main_EQ(x1, x2, x3, x4) → Cond_f330_0_main_EQ(x1, x3, x4)
Cond_f330_0_main_EQ1(x1, x2, x3, x4) → Cond_f330_0_main_EQ1(x1, x3, x4)

Filtered duplicate terms:

f330_0_main_EQ(x1, x2) → f330_0_main_EQ(x2)
Cond_f330_0_main_EQ(x1, x2, x3) → Cond_f330_0_main_EQ(x1, x3)
Cond_f330_0_main_EQ1(x1, x2, x3) → Cond_f330_0_main_EQ1(x1, x3)

Prepared 2 rules for path length conversion:

P rules:
f330_0_main_EQ(x0) → f330_0_main_EQ(-(x0, 1)) | &&(>(x0, 0), =(%(x0, 2), 1))
f330_0_main_EQ(x0) → f330_0_main_EQ(/(x0, 2)) | &&(=(%(x0, 2), 0), >(+(x0, 1), 1))

Finished conversion. Obtained 4 rules.

P rules:
f330_0_main_EQ(x0) → f330_0_main_EQ'(x0) | &&(=(-(x0, *(2, div)), 1), >(x0, 0))
f330_0_main_EQ'(x0) → f330_0_main_EQ(-(x0, 1)) | &&(&&(&&(>(x0, 0), >=(-(x0, *(2, div)), 0)), <(-(x0, *(2, div)), 2)), =(-(x0, *(2, div)), 1))
f330_0_main_EQ(x1) → f330_0_main_EQ'(x1) | &&(=(-(x1, *(2, div)), 0), >(x1, 0))
f330_0_main_EQ'(x1) → f330_0_main_EQ(arith) | &&(&&(&&(&&(&&(>(x1, 0), >=(-(x1, *(2, div)), 0)), =(-(x1, *(2, div)), 0)), <(-(x1, *(2, div)), 2)), <(-(x1, *(2, arith)), 2)), >=(-(x1, *(2, arith)), 0))

(6) Obligation:

Rules:
f330_0_main_EQ(x0) → f330_0_main_EQ'(x0) | &&(=(-(x0, *(2, div)), 1), >(x0, 0))
f330_0_main_EQ'(x0) → f330_0_main_EQ(-(x0, 1)) | &&(&&(&&(>(x0, 0), >=(-(x0, *(2, div)), 0)), <(-(x0, *(2, div)), 2)), =(-(x0, *(2, div)), 1))
f330_0_main_EQ(x1) → f330_0_main_EQ'(x1) | &&(=(-(x1, *(2, div)), 0), >(x1, 0))
f330_0_main_EQ'(x1) → f330_0_main_EQ(arith) | &&(&&(&&(&&(&&(>(x1, 0), >=(-(x1, *(2, div)), 0)), =(-(x1, *(2, div)), 0)), <(-(x1, *(2, div)), 2)), <(-(x1, *(2, arith)), 2)), >=(-(x1, *(2, arith)), 0))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f330_0_main_EQ(x10)] = 1 + 2·x10
[f330_0_main_EQ'(x13)] = 2·x13

Therefore the following rule(s) have been dropped:

f330_0_main_EQ(x0) → f330_0_main_EQ'(x0) | &&(=(-(x0, *(2, x1)), 1), >(x0, 0))
f330_0_main_EQ'(x2) → f330_0_main_EQ(-(x2, 1)) | &&(&&(&&(>(x2, 0), >=(-(x2, *(2, x3)), 0)), <(-(x2, *(2, x3)), 2)), =(-(x2, *(2, x3)), 1))
f330_0_main_EQ(x4) → f330_0_main_EQ'(x4) | &&(=(-(x4, *(2, x5)), 0), >(x4, 0))
f330_0_main_EQ'(x6) → f330_0_main_EQ(x7) | &&(&&(&&(&&(&&(>(x6, 0), >=(-(x6, *(2, x8)), 0)), =(-(x6, *(2, x8)), 0)), <(-(x6, *(2, x8)), 2)), <(-(x6, *(2, x7)), 2)), >=(-(x6, *(2, x7)), 0))

(8) YES