unknown

Initial ITS

Start location: l4
Program variables: ___patmp1^0 ___patmp2^0 k_208^0 k_243^0 len_263^0
   0: l0 -> l1 : ___patmp1^0'=___patmp1^post1, ___patmp2^0'=___patmp2^post1, k_208^0'=k_208^post1, k_243^0'=k_243^post1, len_263^0'=len_263^post1, (-1+___patmp1^post1 == 0 /\ 1-k_243^post1 <= 0 /\ k_208^0-k_208^post1 == 0 /\ -k_208^0 <= 0 /\ ___patmp2^post1-k_208^0 == 0 /\ -___patmp1^post1+len_263^post1 == 0 /\ k_243^post1-___patmp2^post1 == 0), cost: 1
   1: l2 -> l3 : ___patmp1^0'=___patmp1^post2, ___patmp2^0'=___patmp2^post2, k_208^0'=k_208^post2, k_243^0'=k_243^post2, len_263^0'=len_263^post2, (___patmp1^0-___patmp1^post2 == 0 /\ -k_208^post2+k_208^0 == 0 /\ len_263^0-len_263^post2 == 0 /\ -___patmp2^post2+___patmp2^0 == 0 /\ k_243^0-k_243^post2 == 0), cost: 1
   2: l4 -> l0 : ___patmp1^0'=___patmp1^post3, ___patmp2^0'=___patmp2^post3, k_208^0'=k_208^post3, k_243^0'=k_243^post3, len_263^0'=len_263^post3, (k_208^0-k_208^post3 == 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ len_263^0-len_263^post3 == 0 /\ -___patmp2^post3+___patmp2^0 == 0), cost: 1

Chained Linear Paths

Start location: l4
Program variables: ___patmp1^0 ___patmp2^0 k_208^0 k_243^0 len_263^0
   1: l2 -> l3 : ___patmp1^0'=___patmp1^post2, ___patmp2^0'=___patmp2^post2, k_208^0'=k_208^post2, k_243^0'=k_243^post2, len_263^0'=len_263^post2, (___patmp1^0-___patmp1^post2 == 0 /\ -k_208^post2+k_208^0 == 0 /\ len_263^0-len_263^post2 == 0 /\ -___patmp2^post2+___patmp2^0 == 0 /\ k_243^0-k_243^post2 == 0), cost: 1
   3: l4 -> l1 : ___patmp1^0'=___patmp1^post1, ___patmp2^0'=___patmp2^post1, k_208^0'=k_208^post1, k_243^0'=k_243^post1, len_263^0'=len_263^post1, (k_208^0-k_208^post3 == 0 /\ ___patmp2^post1-k_208^post3 == 0 /\ -1+___patmp1^post1 == 0 /\ 1-k_243^post1 <= 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ len_263^0-len_263^post3 == 0 /\ -___patmp1^post1+len_263^post1 == 0 /\ k_243^post1-___patmp2^post1 == 0 /\ -k_208^post3 <= 0 /\ -k_208^post1+k_208^post3 == 0 /\ -___patmp2^post3+___patmp2^0 == 0), cost: 1

	Eliminating location l0 by chaining:

	Applied chaining

	First rule:
	l4 -> l0 : ___patmp1^0'=___patmp1^post3, ___patmp2^0'=___patmp2^post3, k_208^0'=k_208^post3, k_243^0'=k_243^post3, len_263^0'=len_263^post3, (k_208^0-k_208^post3 == 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ len_263^0-len_263^post3 == 0 /\ -___patmp2^post3+___patmp2^0 == 0), cost: 1
	Second rule:
	l0 -> l1 : ___patmp1^0'=___patmp1^post1, ___patmp2^0'=___patmp2^post1, k_208^0'=k_208^post1, k_243^0'=k_243^post1, len_263^0'=len_263^post1, (-1+___patmp1^post1 == 0 /\ 1-k_243^post1 <= 0 /\ k_208^0-k_208^post1 == 0 /\ -k_208^0 <= 0 /\ ___patmp2^post1-k_208^0 == 0 /\ -___patmp1^post1+len_263^post1 == 0 /\ k_243^post1-___patmp2^post1 == 0), cost: 1
	New rule:
	l4 -> l1 : ___patmp1^0'=___patmp1^post1, ___patmp2^0'=___patmp2^post1, k_208^0'=k_208^post1, k_243^0'=k_243^post1, len_263^0'=len_263^post1, (k_208^0-k_208^post3 == 0 /\ ___patmp2^post1-k_208^post3 == 0 /\ -1+___patmp1^post1 == 0 /\ 1-k_243^post1 <= 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ len_263^0-len_263^post3 == 0 /\ -___patmp1^post1+len_263^post1 == 0 /\ k_243^post1-___patmp2^post1 == 0 /\ -k_208^post3 <= 0 /\ -k_208^post1+k_208^post3 == 0 /\ -___patmp2^post3+___patmp2^0 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 2

Simplified Transitions

Start location: l4
Program variables: ___patmp1^0 ___patmp2^0 k_208^0 k_243^0 len_263^0
   4: l2 -> l3 : T, cost: 1
   5: l4 -> l1 : ___patmp1^0'=1, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, len_263^0'=1, (1-k_208^0 <= 0 /\ -k_208^0 <= 0), cost: 1

	Propagated Equalities

	Original rule:
	l2 -> l3 : ___patmp1^0'=___patmp1^post2, ___patmp2^0'=___patmp2^post2, k_208^0'=k_208^post2, k_243^0'=k_243^post2, len_263^0'=len_263^post2, (___patmp1^0-___patmp1^post2 == 0 /\ -k_208^post2+k_208^0 == 0 /\ len_263^0-len_263^post2 == 0 /\ -___patmp2^post2+___patmp2^0 == 0 /\ k_243^0-k_243^post2 == 0), cost: 1
	New rule:
	l2 -> l3 : ___patmp1^0'=___patmp1^0, ___patmp2^0'=___patmp2^0, k_208^0'=k_208^0, k_243^0'=k_243^0, len_263^0'=len_263^0, 0 == 0, cost: 1
	
		propagated equality ___patmp1^post2 = ___patmp1^0
		
		propagated equality k_208^post2 = k_208^0
		
		propagated equality len_263^post2 = len_263^0
		
		propagated equality ___patmp2^post2 = ___patmp2^0
		
		propagated equality k_243^post2 = k_243^0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : ___patmp1^0'=___patmp1^0, ___patmp2^0'=___patmp2^0, k_208^0'=k_208^0, k_243^0'=k_243^0, len_263^0'=len_263^0, 0 == 0, cost: 1
	New rule:
	l2 -> l3 : ___patmp1^0'=___patmp1^0, ___patmp2^0'=___patmp2^0, k_208^0'=k_208^0, k_243^0'=k_243^0, len_263^0'=len_263^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : ___patmp1^0'=___patmp1^0, ___patmp2^0'=___patmp2^0, k_208^0'=k_208^0, k_243^0'=k_243^0, len_263^0'=len_263^0, T, cost: 1
	New rule:
	l2 -> l3 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l1 : ___patmp1^0'=___patmp1^post1, ___patmp2^0'=___patmp2^post1, k_208^0'=k_208^post1, k_243^0'=k_243^post1, len_263^0'=len_263^post1, (k_208^0-k_208^post3 == 0 /\ ___patmp2^post1-k_208^post3 == 0 /\ -1+___patmp1^post1 == 0 /\ 1-k_243^post1 <= 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ len_263^0-len_263^post3 == 0 /\ -___patmp1^post1+len_263^post1 == 0 /\ k_243^post1-___patmp2^post1 == 0 /\ -k_208^post3 <= 0 /\ -k_208^post1+k_208^post3 == 0 /\ -___patmp2^post3+___patmp2^0 == 0), cost: 1
	New rule:
	l4 -> l1 : ___patmp1^0'=1, ___patmp2^0'=k_208^post3, k_208^0'=k_208^post3, k_243^0'=k_208^post3, len_263^0'=1, (0 == 0 /\ k_208^0-k_208^post3 == 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ len_263^0-len_263^post3 == 0 /\ 1-k_208^post3 <= 0 /\ -k_208^post3 <= 0 /\ -___patmp2^post3+___patmp2^0 == 0), cost: 1
	
		propagated equality ___patmp2^post1 = k_208^post3
		
		propagated equality ___patmp1^post1 = 1
		
		propagated equality len_263^post1 = 1
		
		propagated equality k_243^post1 = k_208^post3
		
		propagated equality k_208^post1 = k_208^post3
		
	Propagated Equalities

	Original rule:
	l4 -> l1 : ___patmp1^0'=1, ___patmp2^0'=k_208^post3, k_208^0'=k_208^post3, k_243^0'=k_208^post3, len_263^0'=1, (0 == 0 /\ k_208^0-k_208^post3 == 0 /\ -___patmp1^post3+___patmp1^0 == 0 /\ k_243^0-k_243^post3 == 0 /\ len_263^0-len_263^post3 == 0 /\ 1-k_208^post3 <= 0 /\ -k_208^post3 <= 0 /\ -___patmp2^post3+___patmp2^0 == 0), cost: 1
	New rule:
	l4 -> l1 : ___patmp1^0'=1, ___patmp2^0'=k_208^0, k_208^0'=k_208^0, k_243^0'=k_208^0, len_263^0'=1, (0 == 0 /\ 1-k_208^0 <= 0 /\ -k_208^0 <= 0), cost: 1
	
		propagated equality k_208^post3 = k_208^0
		
		propagated equality ___patmp1^post3 = ___patmp1^0
		
		propagated equality k_243^post3 = k_243^0
		
		propagated equality len_263^post3 = len_263^0
		
		propagated equality ___patmp2^post3 = ___patmp2^0
		
	Simplified Guard

	Original rule:
	l4 -> l1 : ___patmp1^0'=1, ___patmp2^0'=k_208^0, k_208^0'=k_208^0, k_243^0'=k_208^0, len_263^0'=1, (0 == 0 /\ 1-k_208^0 <= 0 /\ -k_208^0 <= 0), cost: 1
	New rule:
	l4 -> l1 : ___patmp1^0'=1, ___patmp2^0'=k_208^0, k_208^0'=k_208^0, k_243^0'=k_208^0, len_263^0'=1, (1-k_208^0 <= 0 /\ -k_208^0 <= 0), cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l1 : ___patmp1^0'=1, ___patmp2^0'=k_208^0, k_208^0'=k_208^0, k_243^0'=k_208^0, len_263^0'=1, (1-k_208^0 <= 0 /\ -k_208^0 <= 0), cost: 1
	New rule:
	l4 -> l1 : ___patmp1^0'=1, ___patmp2^0'=k_208^0, k_243^0'=k_208^0, len_263^0'=1, (1-k_208^0 <= 0 /\ -k_208^0 <= 0), cost: 1

Step with 5

	Trace

	5[(1-k_208^0 <= 0 /\ -k_208^0 <= 0)]
	
	Blocked

	[{}, {}]

Backtrack

	Trace

	Blocked

	[{5[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b