Termination proof of /tmp/tmpMyqFLJ/Velroyen08-gauss.jar

Termination of the given JBC could be disproven:

0 JBC

↳1 JBCNonTerm (⇔, 358 ms)

↳2 NO

(0) Obligation:

JBC Problem based on JBC Program:

package simple.gauss;

public class Gauss {

	// does not terminate for negative numbers 
	
	public static int sum(int n) {
		int sum = 0;
		while (n != 0) {
			sum += n;
			n--;
		}
		return sum;
	}

}


package simple.gauss;

public class Main {

	/**
	 * @param args
	 */
	public static void main(String[] args) {
        int value = args[1].length();
        if (args[0].length() % 2 == 0) {
            value = -value;
        }
		Gauss.sum(value);
	}

}

(1) JBCNonTerm (EQUIVALENT transformation)

Reached a loop using the following run:
0:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||0: load ADDR args||args: a181|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||1: push 1||args: a181||a181>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||2: Read ADDR from array||args: a181||a181, iconst_1>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||3: java.lang.String.length()I||args: a181||o16>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

<java.lang.String.length||0: load ADDR this||this: o16|| ->
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||3: java.lang.String.length||args: a181||o16>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

<java.lang.String.length||1: Read from count|| - ||o16>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||3: java.lang.String.length||args: a181||o16>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

<java.lang.String.length||4: return INT|| - ||i315>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||3: java.lang.String.length||args: a181||o16>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||6: store INT to value||args: a181||i315>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||7: load ADDR args||args: a181, value: i315|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||8: push 0||value: i315||a181>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

10:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||9: Read ADDR from array||value: i315||a181, iconst_0>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

11:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||10: java.lang.String.length()I||value: i315||o36>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

12:

<java.lang.String.length||0: load ADDR this||this: o36|| ->
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||10: java.lang.String.length||value: i315||o36>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

13:

<java.lang.String.length||1: Read from count|| - ||o36>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||10: java.lang.String.length||value: i315||o36>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

14:

<java.lang.String.length||4: return INT|| - ||iconst_1>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||10: java.lang.String.length||value: i315||o36>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

15:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||13: push 2||value: i315||iconst_1>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

16:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||14: REM||value: i315||iconst_1, iconst_2>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

17:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||15: NE 0||value: i315||iconst_1>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

18:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||21: load INT value||value: i315|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

19:

java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||22: simple.gauss.Gauss.sum(I)I|| - ||i315>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

20:

<simple.gauss.Gauss.sum||0: push 0||n: i315|| ->
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||22: simple.gauss.Gauss.sum|| - ||i315>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

21:

<simple.gauss.Gauss.sum||1: store INT to sum||n: i315||iconst_0>
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||22: simple.gauss.Gauss.sum|| - ||i315>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

22:

<simple.gauss.Gauss.sum||2: load INT n||n: i315, sum: iconst_0|| ->
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a181(lv_0_0)]
<simple.gauss.Main.main||22: simple.gauss.Gauss.sum|| - ||i315>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a183
	String.CASE_INSENSITIVE_ORDER: o171
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	i315: [0,+inf)(1){0,+inf}
	a183([java.io.ObjectStreamField|]): length iconst_0
	o171!: String$CaseInsensitiveComparator()
	o36(java.lang.String...): String(count=iconst_1, hash=i35, offset=i37, value=a16?)
	i35: #I{-inf,+inf}
	i37: [0,+inf){0,+inf}
	a181([java.lang.String...]): {o36, o16}
	o16(java.lang.String...): String(count=i315, hash=i20, offset=i22, value=a7?)
	i20: #I{-inf,+inf}
	i22: [0,+inf){0,+inf}
a16:: [CHAR]
a7:: [CHAR]
Relations:

Start state of loop:

<simple.gauss.Gauss.sum||2: load INT n||n: i96, sum: i97|| ->
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a81(lv_0_0)]
<simple.gauss.Main.main||22: simple.gauss.Gauss.sum|| - ||i98>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a80
	String.CASE_INSENSITIVE_ORDER: o105
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a80([java.io.ObjectStreamField|]): length iconst_0
	o105!: String$CaseInsensitiveComparator()
	i96: #I{-inf,+inf}
	i97: #I{-inf,+inf}
	i7: [2,+inf){0,+inf}
	a81([java.lang.String...]): length i7
	i98: #I{-inf,+inf}
Relations:

In the loop head node, references [i96] were interesting.
By SMT, we could prove
(2 <= initial_i7 and (((path1_i96 = path1_i113 and path1_i116 = (path1_i97 + path1_i113) and path1_i118 = (path1_i113 + -1) and path1_i118 = res_i96 and path1_i116 = res_i97 and path1_i98 = res_i98 and path1_i7 = res_i7 and path1_i96 = initial_i96 and path1_i97 = initial_i97 and path1_i98 = initial_i98 and path1_i7 = initial_i7) and path1_i113 < 0) and ((res_i96 = res_i113 and res_i116 = (res_i97 + res_i113) and res_i118 = (res_i113 + -1)) and !res_i113 != 0)))
to be UNSAT. Consequently, the loop will not terminate.

(0) Obligation:

(1) JBCNonTerm (EQUIVALENT transformation)

(2) NO