(0) Obligation:

JBC Problem based on JBC Program:
public class NO_01 {
public static void main(String args[]) {
int c = 24*60*60/100;
if (c <= 10)
for (int i = 0; i < 100; i++);
else {
if (c <= 50) for (int i = 0; i < 101; i++);
if (c <= 100) for (int i = 0; i < 102; i++);
else for (int i = 0; i < 103; i += 0);
}
}
}

(1) JBCNonTerm (EQUIVALENT transformation)

Constructed a run with a repetition. States 13 and 18 are repetitions.
0:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||0: push 864|| - || ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
1:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||3: store INT to #1|| - ||iconst_864>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
2:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||4: load INT #1||#1: iconst_864|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
3:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||5: push 10||#1: iconst_864||iconst_864>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
4:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||7: GT||#1: iconst_864||iconst_864, iconst_10>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
5:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||27: load INT #1||#1: iconst_864|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
6:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||28: push 50||#1: iconst_864||iconst_864>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
7:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||30: GT||#1: iconst_864||iconst_864, iconst_50>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
8:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||47: load INT #1||#1: iconst_864|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
9:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||48: push 100|| - ||iconst_864>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
10:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||50: GT|| - ||iconst_864, iconst_100>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
11:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||70: push 0|| - || ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
12:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||71: store INT to #2|| - ||iconst_0>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
13:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||72: load INT #2||#2: iconst_0|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
14:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||73: push 103||#2: iconst_0||iconst_0>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
15:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||75: GE||#2: iconst_0||iconst_0, iconst_103>
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
16:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||78: increment #2 by 0||#2: iconst_0|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
17:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||81: jmp||#2: iconst_0|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 
18:
java.lang.String = serialPersistentFields, CASE_INSENSITIVE_ORDER
[a2(lv_0_0)]
<NO_01.main||72: load INT #2||#2: iconst_0|| ->
	String.serialVersionUID: iconstLong_-6849794470754667710
	String.serialPersistentFields: a3
	String.CASE_INSENSITIVE_ORDER: o2
	String$CaseInsensitiveComparator.serialVersionUID: iconstLong_8575799808933029326
	RuntimeException.serialVersionUID: iconstLong_-7034897190745766939
	Exception.serialVersionUID: iconstLong_-3387516993124229948
	Throwable.serialVersionUID: iconstLong_-3042686055658047285
	a2([java.lang.String...]): length iconst_0
	a3([java.io.ObjectStreamField|]): length iconst_0
	o2!: String$CaseInsensitiveComparator()
Relations: 

(2) NO