Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

public class GCD3 {
  public static int mod(int a, int b) {
    if(b == 0) {
      return b;
    }
    if(b < 0) {
      a = -a;
    }
    if(a > 0) {
      while(a>=b) {
        a -= b;
      }
      return a;
    } else {
      while(a < 0) {
        a -= b;
      }
      return a;
    }
  }

  public static int gcd(int a, int b) {
    int tmp;
    while(b > 0 && a > 0) {
      tmp = b;
      b = mod(a, b);
      a = tmp;
    }
    return a;
  }

  public static void main(String[] args) {
    Random.args = args;
    int x = Random.random();
    int y = Random.random();
    gcd(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:
GCD3.main([Ljava/lang/String;)V: Graph of 215 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: GCD3.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 37 IRules

P rules:
f846_0_gcd_LE(EOS, i68, i101, i101) → f850_0_gcd_LE(EOS, i68, i101, i101)
f850_0_gcd_LE(EOS, i68, i101, i101) → f854_0_gcd_Load(EOS, i68, i101) | >(i101, 0)
f854_0_gcd_Load(EOS, i68, i101) → f859_0_gcd_LE(EOS, i68, i101, i68)
f859_0_gcd_LE(EOS, i103, i101, i103) → f866_0_gcd_LE(EOS, i103, i101, i103)
f866_0_gcd_LE(EOS, i103, i101, i103) → f873_0_gcd_Load(EOS, i103, i101) | >(i103, 0)
f873_0_gcd_Load(EOS, i103, i101) → f881_0_gcd_Store(EOS, i103, i101, i101)
f881_0_gcd_Store(EOS, i103, i101, i101) → f887_0_gcd_Load(EOS, i103, i101, i101)
f887_0_gcd_Load(EOS, i103, i101, i101) → f895_0_gcd_Load(EOS, i101, i101, i103)
f895_0_gcd_Load(EOS, i101, i101, i103) → f899_0_gcd_InvokeMethod(EOS, i101, i103, i101)
f899_0_gcd_InvokeMethod(EOS, i101, i103, i101) → f901_0_mod_Load(EOS, i101, i103, i101, i103, i101)
f901_0_mod_Load(EOS, i101, i103, i101, i103, i101) → f904_0_mod_NE(EOS, i101, i103, i101, i103, i101, i101)
f904_0_mod_NE(EOS, i101, i103, i101, i103, i101, i101) → f906_0_mod_Load(EOS, i101, i103, i101, i103, i101) | >(i101, 0)
f906_0_mod_Load(EOS, i101, i103, i101, i103, i101) → f908_0_mod_GE(EOS, i101, i103, i101, i103, i101, i101)
f908_0_mod_GE(EOS, i101, i103, i101, i103, i101, i101) → f910_0_mod_Load(EOS, i101, i103, i101, i103, i101) | >=(i101, 0)
f910_0_mod_Load(EOS, i101, i103, i101, i103, i101) → f913_0_mod_LE(EOS, i101, i103, i101, i103, i101, i103)
f913_0_mod_LE(EOS, i101, i103, i101, i103, i101, i103) → f915_0_mod_Load(EOS, i101, i103, i101, i103, i101) | >(i103, 0)
f915_0_mod_Load(EOS, i101, i103, i101, i103, i101) → f967_0_mod_Load(EOS, i101, i103, i101, i103, i101)
f967_0_mod_Load(EOS, i101, i103, i101, i110, i101) → f971_0_mod_Load(EOS, i101, i103, i101, i110, i101, i110)
f971_0_mod_Load(EOS, i101, i103, i101, i110, i101, i110) → f974_0_mod_LT(EOS, i101, i103, i101, i110, i101, i110, i101)
f974_0_mod_LT(EOS, i101, i103, i101, i110, i101, i110, i101) → f976_0_mod_LT(EOS, i101, i103, i101, i110, i101, i110, i101)
f974_0_mod_LT(EOS, i101, i103, i101, i110, i101, i110, i101) → f977_0_mod_LT(EOS, i101, i103, i101, i110, i101, i110, i101)
f976_0_mod_LT(EOS, i101, i103, i101, i110, i101, i110, i101) → f979_0_mod_Load(EOS, i101, i103, i101, i110, i101) | <(i110, i101)
f979_0_mod_Load(EOS, i101, i103, i101, i110, i101) → f984_0_mod_Return(EOS, i101, i103, i101, i110, i101, i110)
f984_0_mod_Return(EOS, i101, i103, i101, i110, i101, i110) → f988_0_gcd_Store(EOS, i101, i110)
f988_0_gcd_Store(EOS, i101, i110) → f993_0_gcd_Load(EOS, i110, i101)
f993_0_gcd_Load(EOS, i110, i101) → f997_0_gcd_Store(EOS, i110, i101)
f997_0_gcd_Store(EOS, i110, i101) → f1002_0_gcd_JMP(EOS, i101, i110)
f1002_0_gcd_JMP(EOS, i101, i110) → f1020_0_gcd_Load(EOS, i101, i110)
f1020_0_gcd_Load(EOS, i101, i110) → f626_0_gcd_Load(EOS, i101, i110)
f626_0_gcd_Load(EOS, i68, i69) → f846_0_gcd_LE(EOS, i68, i69, i69)
f977_0_mod_LT(EOS, i101, i103, i101, i110, i101, i110, i101) → f982_0_mod_Load(EOS, i101, i103, i101, i110, i101) | >=(i110, i101)
f982_0_mod_Load(EOS, i101, i103, i101, i110, i101) → f986_0_mod_Load(EOS, i101, i103, i101, i101, i110)
f986_0_mod_Load(EOS, i101, i103, i101, i101, i110) → f991_0_mod_IntArithmetic(EOS, i101, i103, i101, i101, i110, i101)
f991_0_mod_IntArithmetic(EOS, i101, i103, i101, i101, i110, i101) → f995_0_mod_Store(EOS, i101, i103, i101, i101, -(i110, i101)) | >(i101, 0)
f995_0_mod_Store(EOS, i101, i103, i101, i101, i112) → f999_0_mod_JMP(EOS, i101, i103, i101, i112, i101)
f999_0_mod_JMP(EOS, i101, i103, i101, i112, i101) → f1011_0_mod_Load(EOS, i101, i103, i101, i112, i101)
f1011_0_mod_Load(EOS, i101, i103, i101, i112, i101) → f967_0_mod_Load(EOS, i101, i103, i101, i112, i101)

Combined rules. Obtained 2 IRules

P rules:
f974_0_mod_LT(EOS, x0, x1, x0, x2, x0, x2, x0) → f974_0_mod_LT(EOS, x2, x0, x2, x0, x2, x0, x2) | &&(&&(>(x2, 0), <(x2, x0)), >(x0, 0))
f974_0_mod_LT(EOS, x0, x1, x0, x2, x0, x2, x0) → f974_0_mod_LT(EOS, x0, x1, x0, -(x2, x0), x0, -(x2, x0), x0) | &&(>(x0, 0), >=(x2, x0))

Filtered ground terms:

f974_0_mod_LT(x1, x2, x3, x4, x5, x6, x7, x8) → f974_0_mod_LT(x2, x3, x4, x5, x6, x7, x8)
Cond_f974_0_mod_LT(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f974_0_mod_LT(x1, x3, x4, x5, x6, x7, x8, x9)
Cond_f974_0_mod_LT1(x1, x2, x3, x4, x5, x6, x7, x8, x9) → Cond_f974_0_mod_LT1(x1, x3, x4, x5, x6, x7, x8, x9)

Filtered duplicate terms:

f974_0_mod_LT(x1, x2, x3, x4, x5, x6, x7) → f974_0_mod_LT(x2, x6, x7)
Cond_f974_0_mod_LT(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f974_0_mod_LT(x1, x3, x7, x8)
Cond_f974_0_mod_LT1(x1, x2, x3, x4, x5, x6, x7, x8) → Cond_f974_0_mod_LT1(x1, x3, x7, x8)

Filtered unneeded terms:

Cond_f974_0_mod_LT(x1, x2, x3, x4) → Cond_f974_0_mod_LT(x1, x3, x4)
Cond_f974_0_mod_LT1(x1, x2, x3, x4) → Cond_f974_0_mod_LT1(x1, x3, x4)
f974_0_mod_LT(x1, x2, x3) → f974_0_mod_LT(x2, x3)

Prepared 2 rules for path length conversion:

P rules:
f974_0_mod_LT(x2, x0) → f974_0_mod_LT(x0, x2) | &&(&&(>(x2, 0), <(x2, x0)), >(x0, 0))
f974_0_mod_LT(x2, x0) → f974_0_mod_LT(-(x2, x0), x0) | &&(>(x0, 0), >=(x2, x0))

Finished conversion. Obtained 2 rules.

P rules:
f974_0_mod_LT(x0, x1) → f974_0_mod_LT(x1, x0) | &&(&&(>(x1, x0), >(x0, 0)), >(x1, 0))
f974_0_mod_LT(x2, x3) → f974_0_mod_LT(-(x2, x3), x3) | &&(<=(x3, x2), >(x3, 0))

(6) Obligation:

Rules:
f974_0_mod_LT(x0, x1) → f974_0_mod_LT(x1, x0) | &&(&&(>(x1, x0), >(x0, 0)), >(x1, 0))
f974_0_mod_LT(x2, x3) → f974_0_mod_LT(-(x2, x3), x3) | &&(<=(x3, x2), >(x3, 0))

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f974_0_mod_LT(x5, x7)] = x5 + 2·x7

Therefore the following rule(s) have been dropped:

f974_0_mod_LT(x0, x1) → f974_0_mod_LT(x1, x0) | &&(&&(>(x1, x0), >(x0, 0)), >(x1, 0))
f974_0_mod_LT(x2, x3) → f974_0_mod_LT(-(x2, x3), x3) | &&(<=(x3, x2), >(x3, 0))

(8) YES