Termination proof of /tmp/tmpvnhbYl/NonPeriodicNonterm2.jar

Termination of the given JBC could be disproven:

0 JBC

↳1 JBCNonTerm (⇔, 505 ms)

↳2 NO

(0) Obligation:

JBC Problem based on JBC Program:

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:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||0: load ADDR args||args: a301|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||1: push 0||args: a301||a301>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||2: Read ADDR from array||args: a301||a301, iconst_0>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||3: java.lang.String.length()I||args: a301||o19>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

<java.lang.String.length||0: load ADDR this||this: o19|| ->
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||3: java.lang.String.length||args: a301||o19>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

<java.lang.String.length||1: Read from count|| - ||o19>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||3: java.lang.String.length||args: a301||o19>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

<java.lang.String.length||4: return INT|| - ||i526>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||3: java.lang.String.length||args: a301||o19>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||6: store INT to x||args: a301||i526>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||7: load ADDR args||args: a301, x: i526|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||8: push 1||x: i526||a301>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

10:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||9: Read ADDR from array||x: i526||a301, iconst_1>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

11:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||10: java.lang.String.length()I||x: i526||o43>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

12:

<java.lang.String.length||0: load ADDR this||this: o43|| ->
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||10: java.lang.String.length||x: i526||o43>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

13:

<java.lang.String.length||1: Read from count|| - ||o43>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||10: java.lang.String.length||x: i526||o43>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

14:

<java.lang.String.length||4: return INT|| - ||i36>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||10: java.lang.String.length||x: i526||o43>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

15:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||13: store INT to y||x: i526||i36>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

16:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a301(lv_0_0)]
<NonPeriodicNonterm2.main||14: load INT x||x: i526, y: i36|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a303
	String.CASE_INSENSITIVE_ORDER: o276
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i36: [0,+inf){0,+inf}
	i526: [0,+inf)(3){0,+inf}
	a303([java.io.ObjectStreamField|]): length iconst_0
	o276!: String$CaseInsensitiveComparator()
	o43(java.lang.String...): String(count=i36, hash=i35, offset=i37, value=a19?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a301([java.lang.String...]): {o19, o43}
	o19(java.lang.String...): String(count=i526, hash=i18, offset=i20, value=a7?)
	i18: #I{-inf,+inf}
	i20: [0,+inf){0,+inf}
a19:: [CHAR]
a7:: [CHAR]
Relations:

Start state of loop:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a111(lv_0_0)]
<NonPeriodicNonterm2.main||14: load INT x||x: i153, y: i36|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a110
	String.CASE_INSENSITIVE_ORDER: o151
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a110([java.io.ObjectStreamField|]): length iconst_0
	o151!: String$CaseInsensitiveComparator()
	i27: [2,+inf){0,+inf}
	a111([java.lang.String...]): length i27
	i153: #I{-inf,+inf}
	i36: [0,+inf){0,+inf}
Relations:

In the loop head node, references [i153, i36] were interesting.
By SMT, we could prove
((0 <= initial_i36 and 2 <= initial_i27) and ((((path1_i162 = (path1_i153 - path1_i36) and path1_i162 = path1_i167 and path1_i168 = (path1_i153 + -1) and path1_i168 = res_i153 and path1_i36 = res_i36 and path1_i27 = res_i27 and path1_i153 = initial_i153 and path1_i36 = initial_i36 and path1_i27 = initial_i27) and (path1_i153 >= path1_i36 and path1_i167 > 0)) or ((path2_i162 = (path2_i153 - path2_i36) and path2_i162 = path2_i166 and path2_i169 = (2 * path2_i153) and path2_i322 = (path2_i169 + 1) and path2_i323 = (path2_i36 + 1) and path2_i322 = res_i153 and path2_i323 = res_i36 and path2_i27 = res_i27 and path2_i153 = initial_i153 and path2_i36 = initial_i36 and path2_i27 = initial_i27) and (path2_i153 >= path2_i36 and path2_i166 <= 0))) and (((res_i162 = (res_i153 - res_i36) and res_i162 = res_i167 and res_i168 = (res_i153 + -1)) and !(res_i153 >= res_i36 and res_i167 > 0)) and ((res_i162 = (res_i153 - res_i36) and res_i162 = res_i166 and res_i169 = (2 * res_i153) and res_i322 = (res_i169 + 1) and res_i323 = (res_i36 + 1)) and !(res_i153 >= res_i36 and res_i166 <= 0)))))
to be UNSAT. Consequently, the loop will not terminate.

(0) Obligation:

(1) JBCNonTerm (EQUIVALENT transformation)

(2) NO