Termination of the given JBC could be disproven:

(0) Obligation:

JBC Problem based on JBC Program:
Manifest-Version: 1.0 Created-By: 1.6.0_26 (Sun Microsystems Inc.) Main-Class: simple/middle/Main

package simple.middle;

public class Main {

	/**
	 * @param args
	 */
	public static void main(String[] args) {
		Middle.middle(args[0].length(), args[1].length());
	}

}


package simple.middle;

public class Middle {

	/*
	 * returns the number which is exactly between the first and the second
	 * input number, does not work if one number is even and one is odd or if i <
	 * j
	 */
	public static int middle(int i, int j) {
		while (i != j) {
			i--;
			j++;
		}
		return i;
	}
}

(1) JBCNonTerm (EQUIVALENT transformation)

Reached a loop using the following run:
0:

<simple.middle.Main.main||0: load ADDR args||args: a156|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

1:

<simple.middle.Main.main||1: push 0||args: a156||a156>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

2:

<simple.middle.Main.main||2: Read ADDR from array||args: a156||a156, 0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

3:

<simple.middle.Main.main||3: java.lang.String.length()I||args: a156||o19>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=i18, offset=0, value=a7?)
	i18: #I
a7:: [CHAR]
a12:: [CHAR]

4:

<java.lang.String.length||0: load ADDR this||this: o19|| ->
<simple.middle.Main.main||3: java.lang.String.length||args: a156||o19>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=i18, offset=0, value=a7?)
	i18: #I
a7:: [CHAR]
a12:: [CHAR]

5:

<java.lang.String.length||1: Read from count|| - ||o19>
<simple.middle.Main.main||3: java.lang.String.length||args: a156||o19>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=i18, offset=0, value=a7?)
	i18: #I
a7:: [CHAR]
a12:: [CHAR]

6:

<java.lang.String.length||4: return INT|| - ||0>
<simple.middle.Main.main||3: java.lang.String.length||args: a156||o19>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=i18, offset=0, value=a7?)
	i18: #I
a7:: [CHAR]
a12:: [CHAR]

7:

<simple.middle.Main.main||6: load ADDR args||args: a156||0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

8:

<simple.middle.Main.main||7: push 1|| - ||0, a156>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

9:

<simple.middle.Main.main||8: Read ADDR from array|| - ||0, a156, 1>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

10:

<simple.middle.Main.main||9: java.lang.String.length()I|| - ||0, o32>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=i36, offset=0, value=a12?)
	i36: #I
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

11:

<java.lang.String.length||0: load ADDR this||this: o32|| ->
<simple.middle.Main.main||9: java.lang.String.length|| - ||0, o32>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=i36, offset=0, value=a12?)
	i36: #I
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

12:

<java.lang.String.length||1: Read from count|| - ||o32>
<simple.middle.Main.main||9: java.lang.String.length|| - ||0, o32>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=i36, offset=0, value=a12?)
	i36: #I
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

13:

<java.lang.String.length||4: return INT|| - ||1>
<simple.middle.Main.main||9: java.lang.String.length|| - ||0, o32>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=i36, offset=0, value=a12?)
	i36: #I
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

14:

<simple.middle.Main.main||12: simple.middle.Middle.middle(II)I|| - ||0, 1>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

15:

<simple.middle.Middle.middle||0: load INT i||i: 0, j: 1|| ->
<simple.middle.Main.main||12: simple.middle.Middle.middle|| - ||0, 1>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a154
	String.CASE_INSENSITIVE_ORDER: o121
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o121!: String$CaseInsensitiveComparator()
	a154([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=1, hash=#I, offset=0, value=a12?)
	a156([java.lang.String...]): {o19, o32}
	o19(java.lang.String...): String(count=0, hash=#I, offset=0, value=a7?)
a7:: [CHAR]
a12:: [CHAR]

In the loop head node, references [i79, i80] were interesting.
By SMT, we could prove
((0 <= initial_i19 and 0 <= initial_i37 and 2 <= initial_i27) and (((path1_i87 = (path1_i79 + -1) and path1_i88 = (path1_i80 + 1) and path1_i87 = res_i79 and path1_i88 = res_i80 and path1_i19 = res_i19 and path1_i37 = res_i37 and path1_i27 = res_i27 and path1_i79 = initial_i79 and path1_i80 = initial_i80 and path1_i19 = initial_i19 and path1_i37 = initial_i37 and path1_i27 = initial_i27) and path1_i79 < path1_i80) and ((res_i87 = (res_i79 + -1) and res_i88 = (res_i80 + 1)) and !res_i79 != res_i80)))
to be UNSAT. Consequently, the loop will not terminate.

(2) NO