unknown

Initial ITS

Start location: l6
Program variables: ___cil_tmp2_10^0 ___cil_tmp4_8^0 ___retres1_9^0 ___retres3_7^0 d_6^0 i_5^0 result_4^0
   0: l0 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (-___retres1_9^post1+___retres1_9^0 == 0 /\ i_5^0-i_5^post1 == 0 /\ -___cil_tmp4_8^post1+___cil_tmp4_8^0 == 0 /\ -d_6^post1+d_6^0 == 0 /\ ___retres3_7^0-___retres3_7^post1 == 0 /\ -result_4^post1+result_4^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post1 == 0), cost: 1
   4: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post5, ___cil_tmp4_8^0'=___cil_tmp4_8^post5, ___retres1_9^0'=___retres1_9^post5, ___retres3_7^0'=___retres3_7^post5, d_6^0'=d_6^post5, i_5^0'=i_5^post5, result_4^0'=result_4^post5, (___retres1_9^0-___retres1_9^post5 == 0 /\ ___cil_tmp4_8^post5-___retres3_7^post5 == 0 /\ -d_6^0 <= 0 /\ -d_6^post5+d_6^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post5 == 0 /\ i_5^0-i_5^post5 == 0 /\ -___cil_tmp4_8^post5+result_4^post5 == 0 /\ ___retres3_7^post5 == 0), cost: 1
   5: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post6, ___cil_tmp4_8^0'=___cil_tmp4_8^post6, ___retres1_9^0'=___retres1_9^post6, ___retres3_7^0'=___retres3_7^post6, d_6^0'=d_6^post6, i_5^0'=i_5^post6, result_4^0'=result_4^post6, (-result_4^post6+result_4^0 == 0 /\ -d_6^post6+d_6^0 == 0 /\ 1+d_6^0 <= 0 /\ -___cil_tmp2_10^post6+___cil_tmp2_10^0 == 0 /\ i_5^0-i_5^post6 == 0 /\ ___retres3_7^0-___retres3_7^post6 == 0 /\ ___retres1_9^0-___retres1_9^post6 == 0 /\ -___cil_tmp4_8^post6+___cil_tmp4_8^0 == 0), cost: 1
   1: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post2, ___cil_tmp4_8^0'=___cil_tmp4_8^post2, ___retres1_9^0'=___retres1_9^post2, ___retres3_7^0'=___retres3_7^post2, d_6^0'=d_6^post2, i_5^0'=i_5^post2, result_4^0'=result_4^post2, (1+i_5^0 <= 0 /\ result_4^post2-___cil_tmp4_8^post2 == 0 /\ -i_5^post2+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post2 == 0 /\ ___retres3_7^post2 == 0 /\ d_6^0-d_6^post2 == 0 /\ -___retres1_9^post2+___retres1_9^0 == 0 /\ -___retres3_7^post2+___cil_tmp4_8^post2 == 0), cost: 1
   2: l2 -> l4 : ___cil_tmp2_10^0'=___cil_tmp2_10^post3, ___cil_tmp4_8^0'=___cil_tmp4_8^post3, ___retres1_9^0'=___retres1_9^post3, ___retres3_7^0'=___retres3_7^post3, d_6^0'=d_6^post3, i_5^0'=i_5^post3, result_4^0'=result_4^post3, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ i_5^post3-i_5^0-d_6^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1
   6: l3 -> l5 : ___cil_tmp2_10^0'=___cil_tmp2_10^post7, ___cil_tmp4_8^0'=___cil_tmp4_8^post7, ___retres1_9^0'=___retres1_9^post7, ___retres3_7^0'=___retres3_7^post7, d_6^0'=d_6^post7, i_5^0'=i_5^post7, result_4^0'=result_4^post7, (___retres1_9^post7 == 0 /\ -___cil_tmp4_8^post7+___cil_tmp4_8^0 == 0 /\ ___retres3_7^0-___retres3_7^post7 == 0 /\ d_6^0-d_6^post7 == 0 /\ -___cil_tmp2_10^post7+result_4^post7 == 0 /\ -___retres1_9^post7+___cil_tmp2_10^post7 == 0 /\ -i_5^post7+i_5^0 == 0), cost: 1
   3: l4 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (-___retres1_9^post4+___retres1_9^0 == 0 /\ -d_6^post4+d_6^0 == 0 /\ ___retres3_7^0-___retres3_7^post4 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^0 == 0 /\ -i_5^post4+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post4 == 0 /\ -result_4^post4+result_4^0 == 0), cost: 1
   7: l6 -> l0 : ___cil_tmp2_10^0'=___cil_tmp2_10^post8, ___cil_tmp4_8^0'=___cil_tmp4_8^post8, ___retres1_9^0'=___retres1_9^post8, ___retres3_7^0'=___retres3_7^post8, d_6^0'=d_6^post8, i_5^0'=i_5^post8, result_4^0'=result_4^post8, (i_5^0-i_5^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ result_4^0-result_4^post8 == 0), cost: 1

Chained Linear Paths

Start location: l6
Program variables: ___cil_tmp2_10^0 ___cil_tmp4_8^0 ___retres1_9^0 ___retres3_7^0 d_6^0 i_5^0 result_4^0
   4: l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post5, ___cil_tmp4_8^0'=___cil_tmp4_8^post5, ___retres1_9^0'=___retres1_9^post5, ___retres3_7^0'=___retres3_7^post5, d_6^0'=d_6^post5, i_5^0'=i_5^post5, result_4^0'=result_4^post5, (___retres1_9^0-___retres1_9^post5 == 0 /\ ___cil_tmp4_8^post5-___retres3_7^post5 == 0 /\ -d_6^0 <= 0 /\ -d_6^post5+d_6^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post5 == 0 /\ i_5^0-i_5^post5 == 0 /\ -___cil_tmp4_8^post5+result_4^post5 == 0 /\ ___retres3_7^post5 == 0), cost: 1
   5: l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post6, ___cil_tmp4_8^0'=___cil_tmp4_8^post6, ___retres1_9^0'=___retres1_9^post6, ___retres3_7^0'=___retres3_7^post6, d_6^0'=d_6^post6, i_5^0'=i_5^post6, result_4^0'=result_4^post6, (-result_4^post6+result_4^0 == 0 /\ -d_6^post6+d_6^0 == 0 /\ 1+d_6^0 <= 0 /\ -___cil_tmp2_10^post6+___cil_tmp2_10^0 == 0 /\ i_5^0-i_5^post6 == 0 /\ ___retres3_7^0-___retres3_7^post6 == 0 /\ ___retres1_9^0-___retres1_9^post6 == 0 /\ -___cil_tmp4_8^post6+___cil_tmp4_8^0 == 0), cost: 1
   1: l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post2, ___cil_tmp4_8^0'=___cil_tmp4_8^post2, ___retres1_9^0'=___retres1_9^post2, ___retres3_7^0'=___retres3_7^post2, d_6^0'=d_6^post2, i_5^0'=i_5^post2, result_4^0'=result_4^post2, (1+i_5^0 <= 0 /\ result_4^post2-___cil_tmp4_8^post2 == 0 /\ -i_5^post2+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post2 == 0 /\ ___retres3_7^post2 == 0 /\ d_6^0-d_6^post2 == 0 /\ -___retres1_9^post2+___retres1_9^0 == 0 /\ -___retres3_7^post2+___cil_tmp4_8^post2 == 0), cost: 1
   9: l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ ___retres3_7^post3-___retres3_7^post4 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ i_5^post3-i_5^0-d_6^0 == 0 /\ ___cil_tmp2_10^post3-___cil_tmp2_10^post4 == 0 /\ i_5^post3-i_5^post4 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^post3 == 0 /\ ___retres1_9^post3-___retres1_9^post4 == 0 /\ -d_6^post4+d_6^post3 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ result_4^post3-result_4^post4 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1
   6: l3 -> l5 : ___cil_tmp2_10^0'=___cil_tmp2_10^post7, ___cil_tmp4_8^0'=___cil_tmp4_8^post7, ___retres1_9^0'=___retres1_9^post7, ___retres3_7^0'=___retres3_7^post7, d_6^0'=d_6^post7, i_5^0'=i_5^post7, result_4^0'=result_4^post7, (___retres1_9^post7 == 0 /\ -___cil_tmp4_8^post7+___cil_tmp4_8^0 == 0 /\ ___retres3_7^0-___retres3_7^post7 == 0 /\ d_6^0-d_6^post7 == 0 /\ -___cil_tmp2_10^post7+result_4^post7 == 0 /\ -___retres1_9^post7+___cil_tmp2_10^post7 == 0 /\ -i_5^post7+i_5^0 == 0), cost: 1
   8: l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (i_5^0-i_5^post8 == 0 /\ -___retres1_9^post1+___retres1_9^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ -___cil_tmp2_10^post1+___cil_tmp2_10^post8 == 0 /\ i_5^post8-i_5^post1 == 0 /\ -result_4^post1+result_4^post8 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ d_6^post8-d_6^post1 == 0 /\ result_4^0-result_4^post8 == 0 /\ ___cil_tmp4_8^post8-___cil_tmp4_8^post1 == 0 /\ -___retres3_7^post1+___retres3_7^post8 == 0), cost: 1

	Eliminating location l0 by chaining:

	Applied chaining

	First rule:
	l6 -> l0 : ___cil_tmp2_10^0'=___cil_tmp2_10^post8, ___cil_tmp4_8^0'=___cil_tmp4_8^post8, ___retres1_9^0'=___retres1_9^post8, ___retres3_7^0'=___retres3_7^post8, d_6^0'=d_6^post8, i_5^0'=i_5^post8, result_4^0'=result_4^post8, (i_5^0-i_5^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ result_4^0-result_4^post8 == 0), cost: 1
	Second rule:
	l0 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (-___retres1_9^post1+___retres1_9^0 == 0 /\ i_5^0-i_5^post1 == 0 /\ -___cil_tmp4_8^post1+___cil_tmp4_8^0 == 0 /\ -d_6^post1+d_6^0 == 0 /\ ___retres3_7^0-___retres3_7^post1 == 0 /\ -result_4^post1+result_4^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post1 == 0), cost: 1
	New rule:
	l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (i_5^0-i_5^post8 == 0 /\ -___retres1_9^post1+___retres1_9^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ -___cil_tmp2_10^post1+___cil_tmp2_10^post8 == 0 /\ i_5^post8-i_5^post1 == 0 /\ -result_4^post1+result_4^post8 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ d_6^post8-d_6^post1 == 0 /\ result_4^0-result_4^post8 == 0 /\ ___cil_tmp4_8^post8-___cil_tmp4_8^post1 == 0 /\ -___retres3_7^post1+___retres3_7^post8 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 0 7
	
	Eliminating location l4 by chaining:

	Applied chaining

	First rule:
	l2 -> l4 : ___cil_tmp2_10^0'=___cil_tmp2_10^post3, ___cil_tmp4_8^0'=___cil_tmp4_8^post3, ___retres1_9^0'=___retres1_9^post3, ___retres3_7^0'=___retres3_7^post3, d_6^0'=d_6^post3, i_5^0'=i_5^post3, result_4^0'=result_4^post3, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ i_5^post3-i_5^0-d_6^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1
	Second rule:
	l4 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (-___retres1_9^post4+___retres1_9^0 == 0 /\ -d_6^post4+d_6^0 == 0 /\ ___retres3_7^0-___retres3_7^post4 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^0 == 0 /\ -i_5^post4+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post4 == 0 /\ -result_4^post4+result_4^0 == 0), cost: 1
	New rule:
	l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ ___retres3_7^post3-___retres3_7^post4 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ i_5^post3-i_5^0-d_6^0 == 0 /\ ___cil_tmp2_10^post3-___cil_tmp2_10^post4 == 0 /\ i_5^post3-i_5^post4 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^post3 == 0 /\ ___retres1_9^post3-___retres1_9^post4 == 0 /\ -d_6^post4+d_6^post3 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ result_4^post3-result_4^post4 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1
	
	Applied deletion

	Removed the following rules: 2 3

Simplified Transitions

Start location: l6
Program variables: ___cil_tmp2_10^0 ___cil_tmp4_8^0 ___retres1_9^0 ___retres3_7^0 d_6^0 i_5^0 result_4^0
  11: l1 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, -d_6^0 <= 0, cost: 1
  12: l1 -> l2 : 1+d_6^0 <= 0, cost: 1
  10: l2 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1
  15: l2 -> l2 : i_5^0'=i_5^0+d_6^0, -i_5^0 <= 0, cost: 1
  13: l3 -> l5 : ___cil_tmp2_10^0'=0, ___retres1_9^0'=0, result_4^0'=0, T, cost: 1
  14: l6 -> l1 : T, cost: 1

	Propagated Equalities

	Original rule:
	l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post2, ___cil_tmp4_8^0'=___cil_tmp4_8^post2, ___retres1_9^0'=___retres1_9^post2, ___retres3_7^0'=___retres3_7^post2, d_6^0'=d_6^post2, i_5^0'=i_5^post2, result_4^0'=result_4^post2, (1+i_5^0 <= 0 /\ result_4^post2-___cil_tmp4_8^post2 == 0 /\ -i_5^post2+i_5^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post2 == 0 /\ ___retres3_7^post2 == 0 /\ d_6^0-d_6^post2 == 0 /\ -___retres1_9^post2+___retres1_9^0 == 0 /\ -___retres3_7^post2+___cil_tmp4_8^post2 == 0), cost: 1
	New rule:
	l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, (0 == 0 /\ 1+i_5^0 <= 0), cost: 1
	
		propagated equality ___cil_tmp4_8^post2 = result_4^post2
		
		propagated equality i_5^post2 = i_5^0
		
		propagated equality ___cil_tmp2_10^post2 = ___cil_tmp2_10^0
		
		propagated equality ___retres3_7^post2 = 0
		
		propagated equality d_6^post2 = d_6^0
		
		propagated equality ___retres1_9^post2 = ___retres1_9^0
		
		propagated equality result_4^post2 = 0
		
	Simplified Guard

	Original rule:
	l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, (0 == 0 /\ 1+i_5^0 <= 0), cost: 1
	New rule:
	l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1
	New rule:
	l2 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^post5, ___cil_tmp4_8^0'=___cil_tmp4_8^post5, ___retres1_9^0'=___retres1_9^post5, ___retres3_7^0'=___retres3_7^post5, d_6^0'=d_6^post5, i_5^0'=i_5^post5, result_4^0'=result_4^post5, (___retres1_9^0-___retres1_9^post5 == 0 /\ ___cil_tmp4_8^post5-___retres3_7^post5 == 0 /\ -d_6^0 <= 0 /\ -d_6^post5+d_6^0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post5 == 0 /\ i_5^0-i_5^post5 == 0 /\ -___cil_tmp4_8^post5+result_4^post5 == 0 /\ ___retres3_7^post5 == 0), cost: 1
	New rule:
	l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, (0 == 0 /\ -d_6^0 <= 0), cost: 1
	
		propagated equality ___retres1_9^post5 = ___retres1_9^0
		
		propagated equality ___cil_tmp4_8^post5 = ___retres3_7^post5
		
		propagated equality d_6^post5 = d_6^0
		
		propagated equality ___cil_tmp2_10^post5 = ___cil_tmp2_10^0
		
		propagated equality i_5^post5 = i_5^0
		
		propagated equality ___retres3_7^post5 = result_4^post5
		
		propagated equality result_4^post5 = 0
		
	Simplified Guard

	Original rule:
	l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, (0 == 0 /\ -d_6^0 <= 0), cost: 1
	New rule:
	l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, -d_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l3 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, -d_6^0 <= 0, cost: 1
	New rule:
	l1 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, -d_6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post6, ___cil_tmp4_8^0'=___cil_tmp4_8^post6, ___retres1_9^0'=___retres1_9^post6, ___retres3_7^0'=___retres3_7^post6, d_6^0'=d_6^post6, i_5^0'=i_5^post6, result_4^0'=result_4^post6, (-result_4^post6+result_4^0 == 0 /\ -d_6^post6+d_6^0 == 0 /\ 1+d_6^0 <= 0 /\ -___cil_tmp2_10^post6+___cil_tmp2_10^0 == 0 /\ i_5^0-i_5^post6 == 0 /\ ___retres3_7^0-___retres3_7^post6 == 0 /\ ___retres1_9^0-___retres1_9^post6 == 0 /\ -___cil_tmp4_8^post6+___cil_tmp4_8^0 == 0), cost: 1
	New rule:
	l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, (0 == 0 /\ 1+d_6^0 <= 0), cost: 1
	
		propagated equality result_4^post6 = result_4^0
		
		propagated equality d_6^post6 = d_6^0
		
		propagated equality ___cil_tmp2_10^post6 = ___cil_tmp2_10^0
		
		propagated equality i_5^post6 = i_5^0
		
		propagated equality ___retres3_7^post6 = ___retres3_7^0
		
		propagated equality ___retres1_9^post6 = ___retres1_9^0
		
		propagated equality ___cil_tmp4_8^post6 = ___cil_tmp4_8^0
		
	Simplified Guard

	Original rule:
	l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, (0 == 0 /\ 1+d_6^0 <= 0), cost: 1
	New rule:
	l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, 1+d_6^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l1 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, 1+d_6^0 <= 0, cost: 1
	New rule:
	l1 -> l2 : 1+d_6^0 <= 0, cost: 1
	
	Propagated Equalities

	Original rule:
	l3 -> l5 : ___cil_tmp2_10^0'=___cil_tmp2_10^post7, ___cil_tmp4_8^0'=___cil_tmp4_8^post7, ___retres1_9^0'=___retres1_9^post7, ___retres3_7^0'=___retres3_7^post7, d_6^0'=d_6^post7, i_5^0'=i_5^post7, result_4^0'=result_4^post7, (___retres1_9^post7 == 0 /\ -___cil_tmp4_8^post7+___cil_tmp4_8^0 == 0 /\ ___retres3_7^0-___retres3_7^post7 == 0 /\ d_6^0-d_6^post7 == 0 /\ -___cil_tmp2_10^post7+result_4^post7 == 0 /\ -___retres1_9^post7+___cil_tmp2_10^post7 == 0 /\ -i_5^post7+i_5^0 == 0), cost: 1
	New rule:
	l3 -> l5 : ___cil_tmp2_10^0'=0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, 0 == 0, cost: 1
	
		propagated equality ___retres1_9^post7 = 0
		
		propagated equality ___cil_tmp4_8^post7 = ___cil_tmp4_8^0
		
		propagated equality ___retres3_7^post7 = ___retres3_7^0
		
		propagated equality d_6^post7 = d_6^0
		
		propagated equality ___cil_tmp2_10^post7 = result_4^post7
		
		propagated equality result_4^post7 = 0
		
		propagated equality i_5^post7 = i_5^0
		
	Simplified Guard

	Original rule:
	l3 -> l5 : ___cil_tmp2_10^0'=0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, 0 == 0, cost: 1
	New rule:
	l3 -> l5 : ___cil_tmp2_10^0'=0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l3 -> l5 : ___cil_tmp2_10^0'=0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=0, T, cost: 1
	New rule:
	l3 -> l5 : ___cil_tmp2_10^0'=0, ___retres1_9^0'=0, result_4^0'=0, T, cost: 1
	
	Propagated Equalities

	Original rule:
	l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post1, ___cil_tmp4_8^0'=___cil_tmp4_8^post1, ___retres1_9^0'=___retres1_9^post1, ___retres3_7^0'=___retres3_7^post1, d_6^0'=d_6^post1, i_5^0'=i_5^post1, result_4^0'=result_4^post1, (i_5^0-i_5^post8 == 0 /\ -___retres1_9^post1+___retres1_9^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ -___cil_tmp2_10^post1+___cil_tmp2_10^post8 == 0 /\ i_5^post8-i_5^post1 == 0 /\ -result_4^post1+result_4^post8 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ d_6^post8-d_6^post1 == 0 /\ result_4^0-result_4^post8 == 0 /\ ___cil_tmp4_8^post8-___cil_tmp4_8^post1 == 0 /\ -___retres3_7^post1+___retres3_7^post8 == 0), cost: 1
	New rule:
	l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post8, ___cil_tmp4_8^0'=___cil_tmp4_8^post8, ___retres1_9^0'=___retres1_9^post8, ___retres3_7^0'=___retres3_7^post8, d_6^0'=d_6^post8, i_5^0'=i_5^post8, result_4^0'=result_4^post8, (0 == 0 /\ i_5^0-i_5^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ result_4^0-result_4^post8 == 0), cost: 1
	
		propagated equality ___retres1_9^post1 = ___retres1_9^post8
		
		propagated equality ___cil_tmp2_10^post1 = ___cil_tmp2_10^post8
		
		propagated equality i_5^post1 = i_5^post8
		
		propagated equality result_4^post1 = result_4^post8
		
		propagated equality d_6^post1 = d_6^post8
		
		propagated equality ___cil_tmp4_8^post1 = ___cil_tmp4_8^post8
		
		propagated equality ___retres3_7^post1 = ___retres3_7^post8
		
	Propagated Equalities

	Original rule:
	l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^post8, ___cil_tmp4_8^0'=___cil_tmp4_8^post8, ___retres1_9^0'=___retres1_9^post8, ___retres3_7^0'=___retres3_7^post8, d_6^0'=d_6^post8, i_5^0'=i_5^post8, result_4^0'=result_4^post8, (0 == 0 /\ i_5^0-i_5^post8 == 0 /\ -d_6^post8+d_6^0 == 0 /\ -___cil_tmp4_8^post8+___cil_tmp4_8^0 == 0 /\ -___retres1_9^post8+___retres1_9^0 == 0 /\ ___retres3_7^0-___retres3_7^post8 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post8 == 0 /\ result_4^0-result_4^post8 == 0), cost: 1
	New rule:
	l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, 0 == 0, cost: 1
	
		propagated equality i_5^post8 = i_5^0
		
		propagated equality d_6^post8 = d_6^0
		
		propagated equality ___cil_tmp4_8^post8 = ___cil_tmp4_8^0
		
		propagated equality ___retres1_9^post8 = ___retres1_9^0
		
		propagated equality ___retres3_7^post8 = ___retres3_7^0
		
		propagated equality ___cil_tmp2_10^post8 = ___cil_tmp2_10^0
		
		propagated equality result_4^post8 = result_4^0
		
	Simplified Guard

	Original rule:
	l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, 0 == 0, cost: 1
	New rule:
	l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, T, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l6 -> l1 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0, result_4^0'=result_4^0, T, cost: 1
	New rule:
	l6 -> l1 : T, cost: 1
	
	Propagated Equalities

	Original rule:
	l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post4, ___cil_tmp4_8^0'=___cil_tmp4_8^post4, ___retres1_9^0'=___retres1_9^post4, ___retres3_7^0'=___retres3_7^post4, d_6^0'=d_6^post4, i_5^0'=i_5^post4, result_4^0'=result_4^post4, (___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ ___retres3_7^post3-___retres3_7^post4 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ i_5^post3-i_5^0-d_6^0 == 0 /\ ___cil_tmp2_10^post3-___cil_tmp2_10^post4 == 0 /\ i_5^post3-i_5^post4 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -___cil_tmp4_8^post4+___cil_tmp4_8^post3 == 0 /\ ___retres1_9^post3-___retres1_9^post4 == 0 /\ -d_6^post4+d_6^post3 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ result_4^post3-result_4^post4 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1
	New rule:
	l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post3, ___cil_tmp4_8^0'=___cil_tmp4_8^post3, ___retres1_9^0'=___retres1_9^post3, ___retres3_7^0'=___retres3_7^post3, d_6^0'=d_6^post3, i_5^0'=i_5^post3, result_4^0'=result_4^post3, (0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ i_5^post3-i_5^0-d_6^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1
	
		propagated equality ___retres3_7^post4 = ___retres3_7^post3
		
		propagated equality ___cil_tmp2_10^post4 = ___cil_tmp2_10^post3
		
		propagated equality i_5^post4 = i_5^post3
		
		propagated equality ___cil_tmp4_8^post4 = ___cil_tmp4_8^post3
		
		propagated equality ___retres1_9^post4 = ___retres1_9^post3
		
		propagated equality d_6^post4 = d_6^post3
		
		propagated equality result_4^post4 = result_4^post3
		
	Propagated Equalities

	Original rule:
	l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^post3, ___cil_tmp4_8^0'=___cil_tmp4_8^post3, ___retres1_9^0'=___retres1_9^post3, ___retres3_7^0'=___retres3_7^post3, d_6^0'=d_6^post3, i_5^0'=i_5^post3, result_4^0'=result_4^post3, (0 == 0 /\ ___cil_tmp2_10^0-___cil_tmp2_10^post3 == 0 /\ ___cil_tmp4_8^0-___cil_tmp4_8^post3 == 0 /\ -___retres1_9^post3+___retres1_9^0 == 0 /\ i_5^post3-i_5^0-d_6^0 == 0 /\ -result_4^post3+result_4^0 == 0 /\ -i_5^0 <= 0 /\ d_6^0-d_6^post3 == 0 /\ ___retres3_7^0-___retres3_7^post3 == 0), cost: 1
	New rule:
	l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0+d_6^0, result_4^0'=result_4^0, (0 == 0 /\ -i_5^0 <= 0), cost: 1
	
		propagated equality ___cil_tmp2_10^post3 = ___cil_tmp2_10^0
		
		propagated equality ___cil_tmp4_8^post3 = ___cil_tmp4_8^0
		
		propagated equality ___retres1_9^post3 = ___retres1_9^0
		
		propagated equality i_5^post3 = i_5^0+d_6^0
		
		propagated equality result_4^post3 = result_4^0
		
		propagated equality d_6^post3 = d_6^0
		
		propagated equality ___retres3_7^post3 = ___retres3_7^0
		
	Simplified Guard

	Original rule:
	l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0+d_6^0, result_4^0'=result_4^0, (0 == 0 /\ -i_5^0 <= 0), cost: 1
	New rule:
	l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0+d_6^0, result_4^0'=result_4^0, -i_5^0 <= 0, cost: 1
	
	Removed Trivial Updates

	Original rule:
	l2 -> l2 : ___cil_tmp2_10^0'=___cil_tmp2_10^0, ___cil_tmp4_8^0'=___cil_tmp4_8^0, ___retres1_9^0'=___retres1_9^0, ___retres3_7^0'=___retres3_7^0, d_6^0'=d_6^0, i_5^0'=i_5^0+d_6^0, result_4^0'=result_4^0, -i_5^0 <= 0, cost: 1
	New rule:
	l2 -> l2 : i_5^0'=i_5^0+d_6^0, -i_5^0 <= 0, cost: 1

Step with 14

	Trace

	14[T]
	
	Blocked

	[{}, {}]

Step with 11

	Trace

	14[T], 11[(-d_6^0 <= 0)]
	
	Blocked

	[{}, {}, {}]

Step with 13

	Trace

	14[T], 11[(-d_6^0 <= 0)], 13[T]
	
	Blocked

	[{}, {}, {}, {}]

Backtrack

	Trace

	14[T], 11[(-d_6^0 <= 0)]
	
	Blocked

	[{}, {}, {13[T]}]

Backtrack

	Trace

	14[T]
	
	Blocked

	[{}, {11[T]}]

Step with 12

	Trace

	14[T], 12[(1+d_6^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {}]

Step with 10

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 10[(1+i_5^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {}, {}]

Step with 13

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 10[(1+i_5^0 <= 0)], 13[T]
	
	Blocked

	[{}, {11[T]}, {}, {}, {}]

Backtrack

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 10[(1+i_5^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {}, {13[T]}]

Backtrack

	Trace

	14[T], 12[(1+d_6^0 <= 0)]
	
	Blocked

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

Step with 15

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 15[(-i_5^0 <= 0)]
	
	Blocked

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

Accelerate

Start location: l6
Program variables: ___cil_tmp2_10^0 ___cil_tmp4_8^0 ___retres1_9^0 ___retres3_7^0 d_6^0 i_5^0 result_4^0
  11: l1 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, -d_6^0 <= 0, cost: 1
  12: l1 -> l2 : 1+d_6^0 <= 0, cost: 1
  10: l2 -> l3 : ___cil_tmp4_8^0'=0, ___retres3_7^0'=0, result_4^0'=0, 1+i_5^0 <= 0, cost: 1
  15: l2 -> l2 : i_5^0'=i_5^0+d_6^0, -i_5^0 <= 0, cost: 1
  16: l2 -> LoAT_sink : (i_5^0 >= 0 /\ -d_6^0 <= 0), cost: NONTERM
  17: l2 -> l2 : i_5^0'=i_5^0+n*d_6^0, (i_5^0 >= 0 /\ -1+n >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0), cost: 1
  13: l3 -> l5 : ___cil_tmp2_10^0'=0, ___retres1_9^0'=0, result_4^0'=0, T, cost: 1
  14: l6 -> l1 : T, cost: 1

	Certificate of Non-Termination

	Original rule:
	l2 -> l2 : i_5^0'=i_5^0+d_6^0, (-i_5^0 <= 0), cost: 1
	New rule:
	l2 -> LoAT_sink : (i_5^0 >= 0 /\ -d_6^0 <= 0), cost: NONTERM

		i_5^0 >= 0 [0]: eventual decrease yields (i_5^0 >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0)
		
		i_5^0 >= 0 [1]: eventual increase yields (i_5^0 >= 0 /\ -d_6^0 <= 0)
		
		Replacement map: {i_5^0 >= 0 -> (i_5^0 >= 0 /\ -d_6^0 <= 0)}

	Loop Acceleration

	Original rule:
	l2 -> l2 : i_5^0'=i_5^0+d_6^0, (-i_5^0 <= 0), cost: 1
	New rule:
	l2 -> l2 : i_5^0'=i_5^0+n*d_6^0, (i_5^0 >= 0 /\ -1+n >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0), cost: 1

		i_5^0 >= 0 [0]: eventual decrease yields (i_5^0 >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0)
		
		i_5^0 >= 0 [1]: eventual increase yields (i_5^0 >= 0 /\ -d_6^0 <= 0)
		
		Replacement map: {i_5^0 >= 0 -> (i_5^0 >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0)}

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 17[(i_5^0 >= 0 /\ -1+n >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0)]
	
	Blocked

	[{}, {11[T]}, {10[T]}, {15[T], 17[T]}]

Step with 10

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 17[(i_5^0 >= 0 /\ -1+n >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0)], 10[(1+i_5^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {10[T]}, {15[T], 16[T], 17[T]}, {}]

Step with 13

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 17[(i_5^0 >= 0 /\ -1+n >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0)], 10[(1+i_5^0 <= 0)], 13[T]
	
	Blocked

	[{}, {11[T]}, {10[T]}, {15[T], 16[T], 17[T]}, {}, {}]

Backtrack

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 17[(i_5^0 >= 0 /\ -1+n >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0)], 10[(1+i_5^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {10[T]}, {15[T], 16[T], 17[T]}, {13[T]}]

Backtrack

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 17[(i_5^0 >= 0 /\ -1+n >= 0 /\ i_5^0+(-1+n)*d_6^0 >= 0)]
	
	Blocked

	[{}, {11[T]}, {10[T]}, {10[T], 15[T], 16[T], 17[T]}]

Backtrack

	Trace

	14[T], 12[(1+d_6^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {10[T], 17[T]}]

Step with 15

	Trace

	14[T], 12[(1+d_6^0 <= 0)], 15[(-i_5^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {10[T], 17[T]}, {}]

Covered

	Trace

	14[T], 12[(1+d_6^0 <= 0)]
	
	Blocked

	[{}, {11[T]}, {10[T], 15[T], 17[T]}]

Backtrack

	Trace

	14[T]
	
	Blocked

	[{}, {11[T], 12[T]}]

Backtrack

	Trace

	Blocked

	[{14[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b