Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:

package ClassAnalysisRec;

public class ClassAnalysisRec {
	A field;

	public static void main(String[] args) {
		Random.args = args;
		ClassAnalysisRec t = new ClassAnalysisRec();
		t.field = new A();
		t.field = new B();
		t.eval();
	}

	public void eval() {
		int x = Random.random() % 100;
		this.field.test(x);
	}
}

class A {
	public boolean test(int x) {
		return this.test(x-1);
	}
}

class B extends A {
	public boolean test(int x) {
		if (x <= 0) return true;
		return test(x - 1);
	}
}


package ClassAnalysisRec;

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

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

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

Termination Graph based on JBC Program:
ClassAnalysisRec.ClassAnalysisRec.main([Ljava/lang/String;)V: Graph of 71 nodes with 0 SCCs.

ClassAnalysisRec.ClassAnalysisRec.eval()V: Graph of 82 nodes with 0 SCCs.

ClassAnalysisRec.B.test(I)Z: Graph of 20 nodes with 0 SCCs.

(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: ClassAnalysisRec.B.test(I)Z
SCC calls the following helper methods: ClassAnalysisRec.B.test(I)Z
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 11 IRules

P rules:
f247_0_test_GT(EOS, i24, i24, i24) → f252_0_test_GT(EOS, i24, i24, i24)
f252_0_test_GT(EOS, i24, i24, i24) → f256_0_test_Load(EOS, i24, i24) | >(i24, 0)
f256_0_test_Load(EOS, i24, i24) → f264_0_test_Load(EOS, i24, i24)
f264_0_test_Load(EOS, i24, i24) → f272_0_test_ConstantStackPush(EOS, i24, i24)
f272_0_test_ConstantStackPush(EOS, i24, i24) → f327_0_test_IntArithmetic(EOS, i24, i24, 1)
f327_0_test_IntArithmetic(EOS, i24, i24, matching1) → f334_0_test_InvokeMethod(EOS, i24, -(i24, 1)) | &&(>(i24, 0), =(matching1, 1))
f334_0_test_InvokeMethod(EOS, i24, i34) → f340_0_test_Load(EOS, i34, i34)
f334_0_test_InvokeMethod(EOS, i24, i34) → f340_1_test_Load(EOS, i24, i34, i34)
f340_0_test_Load(EOS, i34, i34) → f346_0_test_Load(EOS, i34, i34)
f346_0_test_Load(EOS, i34, i34) → f241_0_test_Load(EOS, i34, i34)
f241_0_test_Load(EOS, i21, i21) → f247_0_test_GT(EOS, i21, i21, i21)

Combined rules. Obtained 2 IRules

P rules:
f247_0_test_GT(EOS, x0, x0, x0) → f340_1_test_Load(EOS, x0, -(x0, 1), -(x0, 1)) | >(x0, 0)
f247_0_test_GT(EOS, x0, x0, x0) → f247_0_test_GT(EOS, -(x0, 1), -(x0, 1), -(x0, 1)) | >(x0, 0)

Filtered ground terms:

f247_0_test_GT(x1, x2, x3, x4) → f247_0_test_GT(x2, x3, x4)
Cond_f247_0_test_GT(x1, x2, x3, x4, x5) → Cond_f247_0_test_GT(x1, x3, x4, x5)
f340_1_test_Load(x1, x2, x3, x4) → f340_1_test_Load(x2, x3, x4)
Cond_f247_0_test_GT1(x1, x2, x3, x4, x5) → Cond_f247_0_test_GT1(x1, x3, x4, x5)

Filtered duplicate terms:

f247_0_test_GT(x1, x2, x3) → f247_0_test_GT(x3)
Cond_f247_0_test_GT(x1, x2, x3, x4) → Cond_f247_0_test_GT(x1, x4)
f340_1_test_Load(x1, x2, x3) → f340_1_test_Load(x3)
Cond_f247_0_test_GT1(x1, x2, x3, x4) → Cond_f247_0_test_GT1(x1, x4)

Filtered unneeded terms:

Cond_f247_0_test_GT(x1, x2) → Cond_f247_0_test_GT(x1)

Prepared 2 rules for path length conversion:

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

Finished conversion. Obtained 1 rules.

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

(6) Obligation:

Rules:
f247_0_test_GT(x1) → f247_0_test_GT(-(x1, 1)) | >(x1, 0)

(7) PolynomialOrderProcessor (EQUIVALENT transformation)

Found the following polynomial interpretation:

[f247_0_test_GT(x2)] = x2

Therefore the following rule(s) have been dropped:

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

(8) YES