Termination of the given JBC could be proven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_20 (Sun Microsystems Inc.) Main-Class: TypeSwitch

public class A {
  public boolean hasSuperType() {
    return false;
  }

  public A getSuperType() {
    return null;
  }
}


public class B extends A {
  public boolean hasSuperType() {
    return true;
  }

  public A getSuperType() {
    return new A();
  }
}


public class C extends B {
  public A getSuperType() {
    return new B();
  }
}


public class TypeSwitch {
  public static void main(String[] args) {
    A x = null;
    switch (args.length) {
      case 0: x = new A();
              break;
      case 1: x = new B();
              break;
      case 2: x = new C();
              break;
    }

    while (x.hasSuperType()) {
      x = x.getSuperType();
    }
  }
}

(1) JBC2FIG (SOUND transformation)

Constructed FIGraph.

(2) Obligation:

FIGraph based on JBC Program:
TypeSwitch.main([Ljava/lang/String;)V: Graph of 142 nodes with 0 SCCs.

(3) FIGtoITRSProof (SOUND transformation)

Transformed FIGraph SCCs to IDPs. Logs:

(4) TRUE