NO

Initial ITS

Start location: l4
Program variables: pre_v^0 v^0 v_next^0
   0: l0 -> l1 : pre_v^0'=pre_v^post1, v^0'=v^post1, v_next^0'=v_next^post1, (-v_next^post1+v_next^0 == 0 /\ 1+v^0-v_next^0 <= 0 /\ -v^post1+v^0 == 0 /\ pre_v^0-pre_v^post1 == 0), cost: 1
   1: l0 -> l2 : pre_v^0'=pre_v^post2, v^0'=v^post2, v_next^0'=v_next^post2, (-v^post2+v^0 == 0 /\ -v_next^post2+v_next^0 == 0 /\ pre_v^0-pre_v^post2 == 0), cost: 1
   2: l2 -> l0 : pre_v^0'=pre_v^post3, v^0'=v^post3, v_next^0'=v_next^post3, (0 == 0 /\ -v_next^post3+v^1 == 0 /\ pre_v^post3-v^0 == 0 /\ -1+v^post3-v^1 == 0), cost: 1
   3: l3 -> l2 : pre_v^0'=pre_v^post4, v^0'=v^post4, v_next^0'=v_next^post4, (-v^post4+v^0 == 0 /\ -v_next^post4+v_next^0 == 0 /\ -pre_v^post4+pre_v^0 == 0), cost: 1
   4: l4 -> l3 : pre_v^0'=pre_v^post5, v^0'=v^post5, v_next^0'=v_next^post5, (-v^post5+v^0 == 0 /\ -v_next^post5+v_next^0 == 0 /\ pre_v^0-pre_v^post5 == 0), cost: 1

Chained Linear Paths

Start location: l4
Program variables: pre_v^0 v^0 v_next^0
   0: l0 -> l1 : pre_v^0'=pre_v^post1, v^0'=v^post1, v_next^0'=v_next^post1, (-v_next^post1+v_next^0 == 0 /\ 1+v^0-v_next^0 <= 0 /\ -v^post1+v^0 == 0 /\ pre_v^0-pre_v^post1 == 0), cost: 1
   1: l0 -> l2 : pre_v^0'=pre_v^post2, v^0'=v^post2, v_next^0'=v_next^post2, (-v^post2+v^0 == 0 /\ -v_next^post2+v_next^0 == 0 /\ pre_v^0-pre_v^post2 == 0), cost: 1
   2: l2 -> l0 : pre_v^0'=pre_v^post3, v^0'=v^post3, v_next^0'=v_next^post3, (0 == 0 /\ -v_next^post3+v^1 == 0 /\ pre_v^post3-v^0 == 0 /\ -1+v^post3-v^1 == 0), cost: 1
   5: l4 -> l2 : pre_v^0'=pre_v^post4, v^0'=v^post4, v_next^0'=v_next^post4, (-v^post5+v^0 == 0 /\ v_next^post5-v_next^post4 == 0 /\ -v_next^post5+v_next^0 == 0 /\ pre_v^0-pre_v^post5 == 0 /\ v^post5-v^post4 == 0 /\ -pre_v^post4+pre_v^post5 == 0), cost: 1

	Eliminating location l3 by chaining:

	Applied chaining

	First rule:
	l4 -> l3 : pre_v^0'=pre_v^post5, v^0'=v^post5, v_next^0'=v_next^post5, (-v^post5+v^0 == 0 /\ -v_next^post5+v_next^0 == 0 /\ pre_v^0-pre_v^post5 == 0), cost: 1
	Second rule:
	l3 -> l2 : pre_v^0'=pre_v^post4, v^0'=v^post4, v_next^0'=v_next^post4, (-v^post4+v^0 == 0 /\ -v_next^post4+v_next^0 == 0 /\ -pre_v^post4+pre_v^0 == 0), cost: 1
	New rule:
	l4 -> l2 : pre_v^0'=pre_v^post4, v^0'=v^post4, v_next^0'=v_next^post4, (-v^post5+v^0 == 0 /\ v_next^post5-v_next^post4 == 0 /\ -v_next^post5+v_next^0 == 0 /\ pre_v^0-pre_v^post5 == 0 /\ v^post5-v^post4 == 0 /\ -pre_v^post4+pre_v^post5 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 3 4

Simplified Transitions

Start location: l4
Program variables: pre_v^0 v^0 v_next^0
   6: l0 -> l1 : 1+v^0-v_next^0 <= 0, cost: 1
   7: l0 -> l2 : T, cost: 1
   8: l2 -> l0 : pre_v^0'=v^0, v^0'=1+v^1, v_next^0'=v^1, T, cost: 1
   9: l4 -> l2 : T, cost: 1

	Propagated Equalities

	Original rule:
	l0 -> l1 : pre_v^0'=pre_v^post1, v^0'=v^post1, v_next^0'=v_next^post1, (-v_next^post1+v_next^0 == 0 /\ 1+v^0-v_next^0 <= 0 /\ -v^post1+v^0 == 0 /\ pre_v^0-pre_v^post1 == 0), cost: 1
	New rule:
	l0 -> l1 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, (0 == 0 /\ 1+v^0-v_next^0 <= 0), cost: 1
	
		propagated equality v_next^post1 = v_next^0
		
		propagated equality v^post1 = v^0
		
		propagated equality pre_v^post1 = pre_v^0
		
	Simplified Guard

	Original rule:
	l0 -> l1 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, (0 == 0 /\ 1+v^0-v_next^0 <= 0), cost: 1
	New rule:
	l0 -> l1 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, 1+v^0-v_next^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l1 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, 1+v^0-v_next^0 <= 0, cost: 1
	New rule:
	l0 -> l1 : 1+v^0-v_next^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l0 -> l2 : pre_v^0'=pre_v^post2, v^0'=v^post2, v_next^0'=v_next^post2, (-v^post2+v^0 == 0 /\ -v_next^post2+v_next^0 == 0 /\ pre_v^0-pre_v^post2 == 0), cost: 1
	New rule:
	l0 -> l2 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, 0 == 0, cost: 1
	
		propagated equality v^post2 = v^0
		
		propagated equality v_next^post2 = v_next^0
		
		propagated equality pre_v^post2 = pre_v^0
		
	Simplified Guard

	Original rule:
	l0 -> l2 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, 0 == 0, cost: 1
	New rule:
	l0 -> l2 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l0 -> l2 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, T, cost: 1
	New rule:
	l0 -> l2 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l0 : pre_v^0'=pre_v^post3, v^0'=v^post3, v_next^0'=v_next^post3, (0 == 0 /\ -v_next^post3+v^1 == 0 /\ pre_v^post3-v^0 == 0 /\ -1+v^post3-v^1 == 0), cost: 1
	New rule:
	l2 -> l0 : pre_v^0'=v^0, v^0'=1+v^1, v_next^0'=v^1, 0 == 0, cost: 1
	
		propagated equality v_next^post3 = v^1
		
		propagated equality pre_v^post3 = v^0
		
		propagated equality v^post3 = 1+v^1
		
	Simplified Guard

	Original rule:
	l2 -> l0 : pre_v^0'=v^0, v^0'=1+v^1, v_next^0'=v^1, 0 == 0, cost: 1
	New rule:
	l2 -> l0 : pre_v^0'=v^0, v^0'=1+v^1, v_next^0'=v^1, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l4 -> l2 : pre_v^0'=pre_v^post4, v^0'=v^post4, v_next^0'=v_next^post4, (-v^post5+v^0 == 0 /\ v_next^post5-v_next^post4 == 0 /\ -v_next^post5+v_next^0 == 0 /\ pre_v^0-pre_v^post5 == 0 /\ v^post5-v^post4 == 0 /\ -pre_v^post4+pre_v^post5 == 0), cost: 1
	New rule:
	l4 -> l2 : pre_v^0'=pre_v^post5, v^0'=v^post5, v_next^0'=v_next^post5, (0 == 0 /\ -v^post5+v^0 == 0 /\ -v_next^post5+v_next^0 == 0 /\ pre_v^0-pre_v^post5 == 0), cost: 1
	
		propagated equality v_next^post4 = v_next^post5
		
		propagated equality v^post4 = v^post5
		
		propagated equality pre_v^post4 = pre_v^post5
		
	Propagated Equalities

	Original rule:
	l4 -> l2 : pre_v^0'=pre_v^post5, v^0'=v^post5, v_next^0'=v_next^post5, (0 == 0 /\ -v^post5+v^0 == 0 /\ -v_next^post5+v_next^0 == 0 /\ pre_v^0-pre_v^post5 == 0), cost: 1
	New rule:
	l4 -> l2 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, 0 == 0, cost: 1
	
		propagated equality v^post5 = v^0
		
		propagated equality v_next^post5 = v_next^0
		
		propagated equality pre_v^post5 = pre_v^0
		
	Simplified Guard

	Original rule:
	l4 -> l2 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, 0 == 0, cost: 1
	New rule:
	l4 -> l2 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l4 -> l2 : pre_v^0'=pre_v^0, v^0'=v^0, v_next^0'=v_next^0, T, cost: 1
	New rule:
	l4 -> l2 : T, cost: 1

Step with 9

	Trace

	9[T]
	
	Blocked

	[{}, {}]

Step with 8

	Trace

	9[T], 8[T]
	
	Blocked

	[{}, {}, {}]

Step with 7

	Trace

	9[T], 8[T], 7[T]
	
	Blocked

	[{}, {}, {6[T]}, {}]

Nonterm

Start location: l4
Program variables: pre_v^0 v^0 v_next^0
   6: l0 -> l1 : 1+v^0-v_next^0 <= 0, cost: 1
   7: l0 -> l2 : T, cost: 1
   8: l2 -> l0 : pre_v^0'=v^0, v^0'=1+v^1, v_next^0'=v^1, T, cost: 1
  10: l2 -> LoAT_sink : -1+n >= 0, cost: NONTERM
  11: l2 -> l2 : pre_v^0'=1+v^11, v^0'=1+v^111, v_next^0'=v^111, T, cost: 1
   9: l4 -> l2 : T, cost: 1

	unrolling

	Original rule:
	l2 -> l2 : pre_v^0'=v^0, v^0'=1+v^11, v_next^0'=v^11, T, cost: 1
	New rule:
	l2 -> l2 : pre_v^0'=1+v^11, v^0'=1+v^111, v_next^0'=v^111, T, cost: 1
	
	Certificate of Non-Termination

	Original rule:
	l2 -> l2 : pre_v^0'=1+v^11, v^0'=1+v^111, v_next^0'=v^111, T, cost: 1
	New rule:
	l2 -> LoAT_sink : -1+n >= 0, cost: NONTERM

		Replacement map: {}

	Loop Acceleration

	Original rule:
	l2 -> l2 : pre_v^0'=1+v^11, v^0'=1+v^111, v_next^0'=v^111, T, cost: 1
	New rule:
	l2 -> l2 : pre_v^0'=1+v^11, v^0'=1+v^111, v_next^0'=v^111, -1+n >= 0, cost: 1

		Replacement map: {}

	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	l2 -> l2 : pre_v^0'=1+v^11, v^0'=1+v^111, v_next^0'=v^111, -1+n >= 0, cost: 1
	New rule:
	l2 -> l2 : pre_v^0'=1+v^11, v^0'=1+v^111, v_next^0'=v^111, T, cost: 1

Step with 10

	Trace

	9[T], 10[-1+n >= 0]
	
	Blocked

	[{}, {}, {10[T]}]

Refute

	Counterexample

	[ pre_v^0=0 v^0=0 v_next^0=0 ] 9 [ pre_v^0=0 v^0=0 v_next^0=0 ] 10
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b