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_24 (Apple Inc.) Main-Class: Choose

public class Choose {
    public static void main(String[] args) {
	int i = 3;
	while (i >= 3) {
	    if (i > 5)
		i += 3;
	    else if (i > 10)
		i -= 2;
	    else
		i++;
	}
    }
}

(1) JBCNonTerm (EQUIVALENT transformation)

Reached a loop using the following run:
0:

<Choose.main||0: push 3|| - || ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

1:

<Choose.main||1: store INT to #1|| - ||3>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

2:

<Choose.main||2: load INT #1||#1: 3|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

3:

<Choose.main||3: push 3||#1: 3||3>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

4:

<Choose.main||4: LT||#1: 3||3, 3>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

5:

<Choose.main||7: load INT #1||#1: 3|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

6:

<Choose.main||8: push 5||#1: 3||3>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

7:

<Choose.main||9: LE||#1: 3||3, 5>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

8:

<Choose.main||18: load INT #1||#1: 3|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

9:

<Choose.main||19: push 10||#1: 3||3>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

10:

<Choose.main||21: LE||#1: 3||3, 10>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

11:

<Choose.main||30: increment #1 by 1||#1: 3|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

12:

<Choose.main||33: jmp||#1: 4|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

13:

<Choose.main||2: load INT #1||#1: 4|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

14:

<Choose.main||3: push 3||#1: 4||4>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

15:

<Choose.main||4: LT||#1: 4||4, 3>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

16:

<Choose.main||7: load INT #1||#1: 4|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

17:

<Choose.main||8: push 5||#1: 4||4>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

18:

<Choose.main||9: LE||#1: 4||4, 5>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

19:

<Choose.main||18: load INT #1||#1: 4|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

20:

<Choose.main||19: push 10||#1: 4||4>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

21:

<Choose.main||21: LE||#1: 4||4, 10>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

22:

<Choose.main||30: increment #1 by 1||#1: 4|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

23:

<Choose.main||33: jmp||#1: 5|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

24:

<Choose.main||2: load INT #1||#1: 5|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

25:

<Choose.main||3: push 3||#1: 5||5>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

26:

<Choose.main||4: LT||#1: 5||5, 3>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

27:

<Choose.main||7: load INT #1||#1: 5|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

28:

<Choose.main||8: push 5||#1: 5||5>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

29:

<Choose.main||9: LE||#1: 5||5, 5>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

30:

<Choose.main||18: load INT #1||#1: 5|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

31:

<Choose.main||19: push 10||#1: 5||5>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

32:

<Choose.main||21: LE||#1: 5||5, 10>
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

33:

<Choose.main||30: increment #1 by 1||#1: 5|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

34:

<Choose.main||33: jmp||#1: 6|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

35:

<Choose.main||2: load INT #1||#1: 6|| ->
	String.serialVersionUID: -6849794470754667710L
	String.serialPersistentFields: a273932
	String.CASE_INSENSITIVE_ORDER: o136967
	String$CaseInsensitiveComparator.serialVersionUID: 8575799808933029326L
	RuntimeException.serialVersionUID: -7034897190745766939L
	Exception.serialVersionUID: -3387516993124229948L
	Throwable.serialVersionUID: -3042686055658047285L
	o136967!: String$CaseInsensitiveComparator()
	a273932([java.io.ObjectStreamField|]): length 0
	a273934([java.lang.String...]): length [0,+inf)

In the loop head node, references [i12] were interesting.
By SMT, we could prove
((3 <= initial_i12 and 0 <= initial_i1) and (((path1_i12 = path1_i17 and path1_i18 = (path1_i17 + 3) and path1_i18 = res_i12 and path1_i1 = res_i1 and path1_i12 = initial_i12 and path1_i1 = initial_i1) and (path1_i12 >= 3 and path1_i17 > 5)) and ((res_i12 = res_i17 and res_i18 = (res_i17 + 3)) and !(res_i12 >= 3 and res_i17 > 5))))
to be UNSAT. Consequently, the loop will not terminate.

(2) NO