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/narrowing/Main

package simple.narrowing;

public class Main {

	/**
	 * @param args
	 */
	public static void main(String[] args) {
		Narrowing.loop(args.length);
	}

}


package simple.narrowing;

public class Narrowing {

	public static void loop(int i) {
		int range = 20;
		boolean up = false;
		while (0 <= i && i <= range) {
			if (i == 0) {
				up = true;
			} 
			if (i == range) {
				up = false;
			}
			if (up) {
				i++;
			}
			if (!up) {
				i--;
			}
			if (i == range-2) {
				range--;
			}
		}
	}
}

(1) JBCNonTerm (EQUIVALENT transformation)

Reached a loop using the following run:
0:

<simple.narrowing.Main.main||0: load ADDR args||args: a266|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a264
	String.CASE_INSENSITIVE_ORDER: o133
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o133!: String$CaseInsensitiveComparator()
	a264([java.io.ObjectStreamField|]): length 0
	a266([java.lang.String...]): length 0

1:

<simple.narrowing.Main.main||1: arraylength|| - ||a266>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a264
	String.CASE_INSENSITIVE_ORDER: o133
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o133!: String$CaseInsensitiveComparator()
	a264([java.io.ObjectStreamField|]): length 0
	a266([java.lang.String...]): length 0

2:

<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop(I)V|| - ||0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a264
	String.CASE_INSENSITIVE_ORDER: o133
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o133!: String$CaseInsensitiveComparator()
	a264([java.io.ObjectStreamField|]): length 0
	a266([java.lang.String...]): length 0

3:

<simple.narrowing.Narrowing.loop||0: push 20||i: 0|| ->
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a264
	String.CASE_INSENSITIVE_ORDER: o133
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o133!: String$CaseInsensitiveComparator()
	a264([java.io.ObjectStreamField|]): length 0
	a266([java.lang.String...]): length 0

4:

<simple.narrowing.Narrowing.loop||2: store INT to range||i: 0||20>
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a264
	String.CASE_INSENSITIVE_ORDER: o133
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o133!: String$CaseInsensitiveComparator()
	a264([java.io.ObjectStreamField|]): length 0
	a266([java.lang.String...]): length 0

5:

<simple.narrowing.Narrowing.loop||3: push 0||i: 0, range: 20|| ->
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a264
	String.CASE_INSENSITIVE_ORDER: o133
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o133!: String$CaseInsensitiveComparator()
	a264([java.io.ObjectStreamField|]): length 0
	a266([java.lang.String...]): length 0

6:

<simple.narrowing.Narrowing.loop||4: store INT to up||i: 0, range: 20||0>
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a264
	String.CASE_INSENSITIVE_ORDER: o133
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o133!: String$CaseInsensitiveComparator()
	a264([java.io.ObjectStreamField|]): length 0
	a266([java.lang.String...]): length 0

7:

<simple.narrowing.Narrowing.loop||5: push 0||i: 0, range: 20, up: 0|| ->
<simple.narrowing.Main.main||2: simple.narrowing.Narrowing.loop|| - ||0>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a264
	String.CASE_INSENSITIVE_ORDER: o133
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o133!: String$CaseInsensitiveComparator()
	a264([java.io.ObjectStreamField|]): length 0
	a266([java.lang.String...]): length 0

In the loop head node, references [i40, iconst_20, iconst_0, i41] were interesting.
By SMT, we could prove
((0 <= initial_i40 and 0 <= initial_i41 and initial_i41 <= 1 and 0 <= initial_i19) and ((((path1_i40 = path1_i64 and 1 = res_i40 and 1 = res_i41 and path1_i19 = res_i19 and path1_i40 = initial_i40 and path1_i41 = initial_i41 and path1_i19 = initial_i19) and (0 <= path1_i40 and path1_i64 <= 20 and path1_i64 = 0 and T and 1 > 0 and 1 > 0)) or ((path4_i40 = path4_i64 and path4_i64 = path4_i67 and path4_i67 = path4_i69 and path4_i71 = (path4_i69 + -1) and path4_i71 = path4_i79 and path4_i79 = res_i40 and 0 = res_i41 and path4_i19 = res_i19 and path4_i40 = initial_i40 and path4_i41 = initial_i41 and path4_i19 = initial_i19) and (0 <= path4_i40 and path4_i64 <= 20 and path4_i67 > 0 and path4_i69 != 20 and path4_i41 = 0 and T and T and path4_i79 != 18)) or ((path2_i40 = path2_i64 and path2_i64 = path2_i67 and path2_i67 = path2_i69 and path2_i70 = (path2_i69 + 1) and path2_i70 = path2_i77 and path2_i77 = res_i40 and 1 = res_i41 and path2_i19 = res_i19 and path2_i40 = initial_i40 and path2_i41 = initial_i41 and path2_i19 = initial_i19) and (0 <= path2_i40 and path2_i64 <= 20 and path2_i67 > 0 and path2_i41 = 1 and 1 > 0 and 1 > 0 and path2_i77 != 18 and path2_i69 > 20))) and ((res_i40 = res_i64 and !(0 <= res_i40 and res_i64 <= 20 and res_i64 = 0 and T and 1 > 0 and 1 > 0)) and ((res_i40 = res_i64 and res_i64 = res_i67 and res_i67 = res_i69 and res_i71 = (res_i69 + -1) and res_i71 = res_i79) and !(0 <= res_i40 and res_i64 <= 20 and res_i67 > 0 and res_i69 != 20 and res_i41 = 0 and T and T and res_i79 != 18)) and ((res_i40 = res_i64 and res_i64 = res_i67 and res_i67 = res_i69 and res_i70 = (res_i69 + 1) and res_i70 = res_i77) and !(0 <= res_i40 and res_i64 <= 20 and res_i67 > 0 and res_i69 != 20 and res_i41 = 1 and 1 > 0 and 1 > 0 and res_i77 != 18)))))
to be UNSAT. Consequently, the loop will not terminate.

(2) NO