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_16 (Sun Microsystems Inc.) Main-Class: BTree

/**
 * A program that creates a binary tree of arbitrary height and then
 * computes that height with a recursive descent on the tree.
 *
 * All calls terminate.
 *
 * Julia + BinTerm prove that all calls terminate
 *
 * @author <A HREF="mailto:[e-mail]">Fausto Spoto</A>
 */

public class BTree {
    private BTree left, right;

    public BTree(int height) {
	if (height > 1) {
	    this.left = new BTree(height - 1);
	    this.right = new BTree(height - 1);
	}
    }

    public int height() {
	if (left == null && right == null) return 1;
	else if (left == null) return 1 + right.height();
	else return 1 + left.height();
    }

    public static void main(String[] args) {
	BTree bt = new BTree(5);
  bt.height();
    }
}

(1) JBCToGraph (SOUND transformation)

Constructed TerminationGraph.

(2) Obligation:

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

(3) TerminationGraphToSCCProof (SOUND transformation)

Proven termination by absence of SCCs

(4) TRUE