unknown

Initial ITS

Start location: [1]
Program variables: oldx x
   0: [1] -> [2] : x'=nondet, T, cost: 1
   1: [2] -> [3] : (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
   5: [2] -> [6] : (-oldx+2*x > 0 \/ -1+x <= 0), cost: 1
   2: [3] -> [4] : oldx'=x, T, cost: 1
   3: [4] -> [5] : x'=nondet1, T, cost: 1
   4: [5] -> [2] : T, cost: 1

Chained Linear Paths

Start location: [1]
Program variables: oldx x
   0: [1] -> [2] : x'=nondet, T, cost: 1
   5: [2] -> [6] : (-oldx+2*x > 0 \/ -1+x <= 0), cost: 1
   8: [2] -> [2] : oldx'=x, x'=nondet1, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1

	Eliminating location [3] by chaining:

	Applied chaining

	First rule:
	[2] -> [3] : (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
	Second rule:
	[3] -> [4] : oldx'=x, T, cost: 1
	New rule:
	[2] -> [4] : oldx'=x, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 1 2
	
	Eliminating location [4] by chaining:

	Applied chaining

	First rule:
	[2] -> [4] : oldx'=x, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
	Second rule:
	[4] -> [5] : x'=nondet1, T, cost: 1
	New rule:
	[2] -> [5] : oldx'=x, x'=nondet1, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 3 6
	
	Eliminating location [5] by chaining:

	Applied chaining

	First rule:
	[2] -> [5] : oldx'=x, x'=nondet1, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
	Second rule:
	[5] -> [2] : T, cost: 1
	New rule:
	[2] -> [2] : oldx'=x, x'=nondet1, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
	
	Applied deletion

	Removed the following rules: 4 7

Unrolled Loops

Start location: [1]
Program variables: oldx x
   0: [1] -> [2] : x'=nondet, T, cost: 1
   5: [2] -> [6] : (-oldx+2*x > 0 \/ -1+x <= 0), cost: 1
   8: [2] -> [2] : oldx'=x, x'=nondet1, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
   9: [2] -> [2] : oldx'=nondet1, x'=nondet11, (-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0), cost: 1

	Unrolling

	Original rule:
	[2] -> [2] : oldx'=x, x'=nondet1, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
	New rule:
	[2] -> [2] : oldx'=nondet1, x'=nondet11, (-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0), cost: 1

Step with 0

	Trace

	0[T]
	
	Blocked

	[{}, {}]

Step with 5

	Trace

	0[T], 5[(-oldx+2*x > 0)]
	
	Blocked

	[{}, {}, {}]

Backtrack

	Trace

	0[T]
	
	Blocked

	[{}, {5[-oldx+2*x > 0]}]

Step with 5

	Trace

	0[T], 5[(-1+x <= 0)]
	
	Blocked

	[{}, {5[-oldx+2*x > 0]}, {}]

Backtrack

	Trace

	0[T]
	
	Blocked

	[{}, {5[(-oldx+2*x > 0 /\ -1+x <= 0)]}]

Step with 8

	Trace

	0[T], 8[(-oldx+2*x <= 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {}]

Accelerate

Start location: [1]
Program variables: oldx x
   0: [1] -> [2] : x'=nondet, T, cost: 1
   5: [2] -> [6] : (-oldx+2*x > 0 \/ -1+x <= 0), cost: 1
   8: [2] -> [2] : oldx'=x, x'=nondet1, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
   9: [2] -> [2] : oldx'=nondet1, x'=nondet11, (-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0), cost: 1
  10: [2] -> [2] : oldx'=nondet1, x'=nondet13, (-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0), cost: 1

	unrolling

	Original rule:
	[2] -> [2] : oldx'=x, x'=nondet1, (-oldx+2*x <= 0 /\ -1+x > 0), cost: 1
	New rule:
	[2] -> [2] : oldx'=nondet1, x'=nondet13, (-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0), cost: 1
	rule cannot be iterated more than once

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {8[T], 10[T]}]

Step with 5

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-oldx+2*x > 0)]
	
	Blocked

	[{}, {5[T]}, {8[T], 10[T]}, {}]

Backtrack

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[-oldx+2*x > 0], 8[T], 10[T]}]

Step with 5

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-1+x <= 0)]
	
	Blocked

	[{}, {5[T]}, {5[-oldx+2*x > 0], 8[T], 10[T]}, {}]

Backtrack

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[(-oldx+2*x > 0 /\ -1+x <= 0)], 8[T], 10[T]}]

Step with 9

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 9

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {}, {}]

Covered

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {9[T]}]

Step with 10

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {9[T]}, {10[T]}]

Acceleration Failed

marked recursive suffix as redundant

Acceleration Failed

marked recursive suffix as redundant

Step with 5

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-oldx+2*x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {9[T]}, {10[T]}, {}]

Backtrack

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {9[T]}, {5[-oldx+2*x > 0], 10[T]}]

Backtrack

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {9[T], 10[T]}]

Step with 5

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-oldx+2*x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {9[T], 10[T]}, {}]

Backtrack

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {5[-oldx+2*x > 0], 9[T], 10[T]}]

Step with 5

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-1+x <= 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {5[-oldx+2*x > 0], 9[T], 10[T]}, {}]

Backtrack

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {5[(-oldx+2*x > 0 /\ -1+x <= 0)], 9[T], 10[T]}]

Step with 8

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 8[(-oldx+2*x <= 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {5[T], 9[T], 10[T]}, {}]

Covered

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 10[T]}, {5[T], 8[T], 9[T], 10[T]}]

Backtrack

	Trace

	0[T], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T]}, {5[T], 8[T], 9[T], 10[T]}]

Backtrack

	Trace

	0[T]
	
	Blocked

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

Step with 8

	Trace

	0[T], 8[(-oldx+2*x <= 0 /\ -1+x > 0)]
	
	Blocked

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

Covered

	Trace

	0[T]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}]

Step with 9

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {}]

Step with 9

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {}, {}]

Covered

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}]

Step with 10

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {10[T]}]

Step with 5

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-oldx+2*x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {10[T]}, {}]

Backtrack

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[-oldx+2*x > 0], 10[T]}]

Step with 5

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-1+x <= 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[-oldx+2*x > 0], 10[T]}, {}]

Backtrack

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[(-oldx+2*x > 0 /\ -1+x <= 0)], 10[T]}]

Step with 8

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 8[(-oldx+2*x <= 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[T], 10[T]}, {}]

Covered

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[T], 8[T], 10[T]}]

Step with 9

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[T], 8[T], 10[T]}, {}]

Acceleration Failed

marked recursive suffix as redundant

Step with 5

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-oldx+2*x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[T], 8[T], 10[T]}, {9[T], 10[T]}, {}]

Backtrack

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[T], 8[T], 10[T]}, {5[-oldx+2*x > 0], 9[T], 10[T]}]

Backtrack

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 10[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T]}, {5[T], 8[T], 9[T], 10[T]}]

Backtrack

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T], 10[T]}]

Step with 5

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-oldx+2*x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {9[T], 10[T]}, {}]

Backtrack

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {5[-oldx+2*x > 0], 9[T], 10[T]}]

Step with 5

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 5[(-1+x <= 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {5[-oldx+2*x > 0], 9[T], 10[T]}, {}]

Backtrack

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {5[(-oldx+2*x > 0 /\ -1+x <= 0)], 9[T], 10[T]}]

Step with 8

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)], 8[(-oldx+2*x <= 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {5[T], 9[T], 10[T]}, {}]

Covered

	Trace

	0[T], 9[(-oldx+2*x <= 0 /\ 2*nondet1-x <= 0 /\ -1+nondet1 > 0 /\ -1+x > 0)]
	
	Blocked

	[{}, {5[T], 8[T], 10[T]}, {5[T], 8[T], 9[T], 10[T]}]

Backtrack

	Trace

	0[T]
	
	Blocked

	[{}, {5[T], 8[T], 9[T], 10[T]}]

Backtrack

	Trace

	Blocked

	[{0[T]}]

Accept

unknown

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b