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: NonPeriodicNonterm2

public class NonPeriodicNonterm2 {
  public static void main(String[] args) {
   int x = args[0].length(); 
   int y = args[1].length();
   while(x >= y) {
    int z = x - y;
    if (z > 0) {
     x--;
    } else {
     x = 2*x + 1;
     y++;
    }
   }
  }
}

(1) JBCNonTerm (EQUIVALENT transformation)

Reached a loop using the following run:
0:

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

1:

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

2:

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

3:

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

4:

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

5:

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

6:

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

7:

<NonPeriodicNonterm2.main||6: store INT to x||args: a246||1>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=#I, offset=0, value=a12?)
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

8:

<NonPeriodicNonterm2.main||7: load ADDR args||args: a246, x: 1|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=#I, offset=0, value=a12?)
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

9:

<NonPeriodicNonterm2.main||8: push 1||x: 1||a246>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=#I, offset=0, value=a12?)
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

10:

<NonPeriodicNonterm2.main||9: Read ADDR from array||x: 1||a246, 1>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=#I, offset=0, value=a12?)
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

11:

<NonPeriodicNonterm2.main||10: java.lang.String.length()I||x: 1||o32>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=i36, offset=0, value=a12?)
	i36: #I
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

12:

<java.lang.String.length||0: load ADDR this||this: o32|| ->
<NonPeriodicNonterm2.main||10: java.lang.String.length||x: 1||o32>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=i36, offset=0, value=a12?)
	i36: #I
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

13:

<java.lang.String.length||1: Read from count|| - ||o32>
<NonPeriodicNonterm2.main||10: java.lang.String.length||x: 1||o32>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=i36, offset=0, value=a12?)
	i36: #I
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

14:

<java.lang.String.length||4: return INT|| - ||0>
<NonPeriodicNonterm2.main||10: java.lang.String.length||x: 1||o32>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=i36, offset=0, value=a12?)
	i36: #I
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

15:

<NonPeriodicNonterm2.main||13: store INT to y||x: 1||0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=#I, offset=0, value=a12?)
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

16:

<NonPeriodicNonterm2.main||14: load INT x||x: 1, y: 0|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a244
	String.CASE_INSENSITIVE_ORDER: o183
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o183!: String$CaseInsensitiveComparator()
	a244([java.io.ObjectStreamField|]): length 0
	o32(java.lang.String...): String(count=0, hash=#I, offset=0, value=a12?)
	a246([java.lang.String...]): {o16, o32}
	o16(java.lang.String...): String(count=1, hash=#I, offset=0, value=a7?)
a12:: [CHAR]
a7:: [CHAR]

In the loop head node, references [i105, i37] were interesting.
By SMT, we could prove
((0 <= initial_i37 and 2 <= initial_i27) and ((((path1_i112 = (path1_i105 - path1_i37) and path1_i112 = path1_i117 and path1_i119 = (path1_i105 + -1) and path1_i119 = res_i105 and path1_i37 = res_i37 and path1_i27 = res_i27 and path1_i105 = initial_i105 and path1_i37 = initial_i37 and path1_i27 = initial_i27) and (path1_i105 >= path1_i37 and path1_i117 > 0)) or ((path2_i112 = (path2_i105 - path2_i37) and path2_i112 = path2_i116 and path2_i122 = (2 * path2_i105) and path2_i282 = (path2_i122 + 1) and path2_i284 = (path2_i37 + 1) and path2_i282 = res_i105 and path2_i284 = res_i37 and path2_i27 = res_i27 and path2_i105 = initial_i105 and path2_i37 = initial_i37 and path2_i27 = initial_i27) and (path2_i105 >= path2_i37 and path2_i116 <= 0))) and (((res_i112 = (res_i105 - res_i37) and res_i112 = res_i117 and res_i119 = (res_i105 + -1)) and !(res_i105 >= res_i37 and res_i117 > 0)) and ((res_i112 = (res_i105 - res_i37) and res_i112 = res_i116 and res_i122 = (2 * res_i105) and res_i282 = (res_i122 + 1) and res_i284 = (res_i37 + 1)) and !(res_i105 >= res_i37 and res_i116 <= 0)))))
to be UNSAT. Consequently, the loop will not terminate.

(2) NO