NO

Initial ITS

Start location: __init
Program variables: arg1 arg2
   0: f289_0_createIntList_Return -> f491_0_random_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, (1+arg1 > 0 /\ arg1p1-arg1 <= 0 /\ 1+arg1p1 > 0), cost: 1
   2: f491_0_random_ArrayAccess -> f815_0_main_NULL : arg1'=arg1p3, arg2'=arg2p3, (1+arg1 > 0 /\ 1+arg1p3 > 0 /\ x7 > 0 /\ arg1p3-arg1 <= 0), cost: 1
   1: f1_0_main_Load -> f491_0_random_ArrayAccess : arg1'=arg1p2, arg2'=arg2p2, (1+arg1p2 > 0 /\ arg1 > 0), cost: 1
   6: f1_0_main_Load -> f639_0_createIntList_LE : arg1'=arg1p7, arg2'=arg2p7, (1-arg2p7 == 0 /\ 1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg2 > 0), cost: 1
   3: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p4, arg2'=arg2p4, (1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+x12 < 0 /\ -1+arg1 > 0), cost: 1
   4: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p5, arg2'=arg2p5, (x15 > 0 /\ arg1p5-arg1 <= 0 /\ arg1p5 > 0 /\ arg1 > 0), cost: 1
   5: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p6, arg2'=arg2p6, (-2+arg1 > 0 /\ 2+arg1p6-arg1 <= 0 /\ arg1p6 > 0 /\ -1+x18 < 0), cost: 1
   7: f639_0_createIntList_LE -> f639_0_createIntList_LE : arg1'=arg1p8, arg2'=arg2p8, (-1-arg1p8+arg1 == 0 /\ arg2 > 0 /\ 1-arg2p8+arg2 == 0 /\ arg1 > 0), cost: 1
   8: __init -> f1_0_main_Load : arg1'=arg1p9, arg2'=arg2p9, T, cost: 1

Simplified Transitions

Start location: __init
Program variables: arg1 arg2
   0: f289_0_createIntList_Return -> f491_0_random_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, (1+arg1 > 0 /\ arg1p1-arg1 <= 0 /\ 1+arg1p1 > 0), cost: 1
   9: f491_0_random_ArrayAccess -> f815_0_main_NULL : arg1'=arg1p3, arg2'=arg2p3, (1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0), cost: 1
   1: f1_0_main_Load -> f491_0_random_ArrayAccess : arg1'=arg1p2, arg2'=arg2p2, (1+arg1p2 > 0 /\ arg1 > 0), cost: 1
  13: f1_0_main_Load -> f639_0_createIntList_LE : arg1'=arg1p7, arg2'=1, (1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg2 > 0), cost: 1
  10: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p4, arg2'=arg2p4, (1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0), cost: 1
  11: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p5, arg2'=arg2p5, (arg1p5-arg1 <= 0 /\ arg1p5 > 0 /\ arg1 > 0), cost: 1
  12: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p6, arg2'=arg2p6, (-2+arg1 > 0 /\ 2+arg1p6-arg1 <= 0 /\ arg1p6 > 0), cost: 1
  14: f639_0_createIntList_LE -> f639_0_createIntList_LE : arg1'=-1+arg1, arg2'=1+arg2, (arg2 > 0 /\ arg1 > 0), cost: 1
   8: __init -> f1_0_main_Load : arg1'=arg1p9, arg2'=arg2p9, T, cost: 1

	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f491_0_random_ArrayAccess -> f815_0_main_NULL : arg1'=arg1p3, arg2'=arg2p3, (1+arg1 > 0 /\ 1+arg1p3 > 0 /\ x7 > 0 /\ arg1p3-arg1 <= 0), cost: 1
	New rule:
	f491_0_random_ArrayAccess -> f815_0_main_NULL : arg1'=arg1p3, arg2'=arg2p3, (1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p4, arg2'=arg2p4, (1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+x12 < 0 /\ -1+arg1 > 0), cost: 1
	New rule:
	f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p4, arg2'=arg2p4, (1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p5, arg2'=arg2p5, (x15 > 0 /\ arg1p5-arg1 <= 0 /\ arg1p5 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p5, arg2'=arg2p5, (arg1p5-arg1 <= 0 /\ arg1p5 > 0 /\ arg1 > 0), cost: 1
	
	Eliminated Temporary Variables via Transitive Closure

	Original rule:
	f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p6, arg2'=arg2p6, (-2+arg1 > 0 /\ 2+arg1p6-arg1 <= 0 /\ arg1p6 > 0 /\ -1+x18 < 0), cost: 1
	New rule:
	f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p6, arg2'=arg2p6, (-2+arg1 > 0 /\ 2+arg1p6-arg1 <= 0 /\ arg1p6 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f1_0_main_Load -> f639_0_createIntList_LE : arg1'=arg1p7, arg2'=arg2p7, (1-arg2p7 == 0 /\ 1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f639_0_createIntList_LE : arg1'=arg1p7, arg2'=1, (0 == 0 /\ 1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg2 > 0), cost: 1
	
		propagated equality arg2p7 = 1
		
	Simplified Guard

	Original rule:
	f1_0_main_Load -> f639_0_createIntList_LE : arg1'=arg1p7, arg2'=1, (0 == 0 /\ 1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg2 > 0), cost: 1
	New rule:
	f1_0_main_Load -> f639_0_createIntList_LE : arg1'=arg1p7, arg2'=1, (1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg2 > 0), cost: 1
	
	Propagated Equalities

	Original rule:
	f639_0_createIntList_LE -> f639_0_createIntList_LE : arg1'=arg1p8, arg2'=arg2p8, (-1-arg1p8+arg1 == 0 /\ arg2 > 0 /\ 1-arg2p8+arg2 == 0 /\ arg1 > 0), cost: 1
	New rule:
	f639_0_createIntList_LE -> f639_0_createIntList_LE : arg1'=-1+arg1, arg2'=1+arg2, (0 == 0 /\ arg2 > 0 /\ arg1 > 0), cost: 1
	
		propagated equality arg1p8 = -1+arg1
		
		propagated equality arg2p8 = 1+arg2
		
	Simplified Guard

	Original rule:
	f639_0_createIntList_LE -> f639_0_createIntList_LE : arg1'=-1+arg1, arg2'=1+arg2, (0 == 0 /\ arg2 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f639_0_createIntList_LE -> f639_0_createIntList_LE : arg1'=-1+arg1, arg2'=1+arg2, (arg2 > 0 /\ arg1 > 0), cost: 1

Step with 8

	Trace

	8[T]
	
	Blocked

	[{}, {}]

Step with 1

	Trace

	8[T], 1[(1+arg1p2 > 0 /\ arg1 > 0)]
	
	Blocked

	[{}, {}, {}]

Step with 9

	Trace

	8[T], 1[(1+arg1p2 > 0 /\ arg1 > 0)], 9[(1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0)]
	
	Blocked

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

Step with 10

	Trace

	8[T], 1[(1+arg1p2 > 0 /\ arg1 > 0)], 9[(1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0)], 10[(1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0)]
	
	Blocked

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

Acceleration Failed

marked recursive suffix as redundant

Step with 10

	Trace

	8[T], 1[(1+arg1p2 > 0 /\ arg1 > 0)], 9[(1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0)], 10[(1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0)], 10[(1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0)]
	
	Blocked

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

Covered

	Trace

	8[T], 1[(1+arg1p2 > 0 /\ arg1 > 0)], 9[(1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0)], 10[(1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0)]
	
	Blocked

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

Step with 11

	Trace

	8[T], 1[(1+arg1p2 > 0 /\ arg1 > 0)], 9[(1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0)], 10[(1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0)], 11[(arg1p5-arg1 <= 0 /\ arg1p5 > 0 /\ arg1 > 0)]
	
	Blocked

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

Nonterm

Start location: __init
Program variables: arg1 arg2
   0: f289_0_createIntList_Return -> f491_0_random_ArrayAccess : arg1'=arg1p1, arg2'=arg2p1, (1+arg1 > 0 /\ arg1p1-arg1 <= 0 /\ 1+arg1p1 > 0), cost: 1
   9: f491_0_random_ArrayAccess -> f815_0_main_NULL : arg1'=arg1p3, arg2'=arg2p3, (1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0), cost: 1
   1: f1_0_main_Load -> f491_0_random_ArrayAccess : arg1'=arg1p2, arg2'=arg2p2, (1+arg1p2 > 0 /\ arg1 > 0), cost: 1
  13: f1_0_main_Load -> f639_0_createIntList_LE : arg1'=arg1p7, arg2'=1, (1+arg1p7 > 0 /\ arg1 > 0 /\ 1+arg2 > 0), cost: 1
  10: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p4, arg2'=arg2p4, (1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0), cost: 1
  11: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p5, arg2'=arg2p5, (arg1p5-arg1 <= 0 /\ arg1p5 > 0 /\ arg1 > 0), cost: 1
  12: f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p6, arg2'=arg2p6, (-2+arg1 > 0 /\ 2+arg1p6-arg1 <= 0 /\ arg1p6 > 0), cost: 1
  15: f815_0_main_NULL -> LoAT_sink : (-arg1p5+arg1 <= 0 /\ -arg1p5+arg1 >= 0 /\ arg1p5 > 0 /\ arg1 > 0), cost: NONTERM
  14: f639_0_createIntList_LE -> f639_0_createIntList_LE : arg1'=-1+arg1, arg2'=1+arg2, (arg2 > 0 /\ arg1 > 0), cost: 1
   8: __init -> f1_0_main_Load : arg1'=arg1p9, arg2'=arg2p9, T, cost: 1

	Certificate of Non-Termination

	Original rule:
	f815_0_main_NULL -> f815_0_main_NULL : arg1'=arg1p5, arg2'=arg2p5, (arg1p5-arg1 <= 0 /\ arg1p5 > 0 /\ arg1 > 0), cost: 1
	New rule:
	f815_0_main_NULL -> LoAT_sink : (-arg1p5+arg1 <= 0 /\ -arg1p5+arg1 >= 0 /\ arg1p5 > 0 /\ arg1 > 0), cost: NONTERM

		-arg1p5+arg1 >= 0 [0]: monotonic increase yields -arg1p5+arg1 >= 0
		
		arg1p5 > 0 [0]: monotonic increase yields arg1p5 > 0
		
		arg1 > 0 [0]: montonic decrease yields arg1p5 > 0, dependencies: -arg1p5+arg1 >= 0
		
		arg1 > 0 [1]: eventual increase yields (-arg1p5+arg1 <= 0 /\ arg1 > 0)
		
		Replacement map: {-arg1p5+arg1 >= 0 -> -arg1p5+arg1 >= 0, arg1p5 > 0 -> arg1p5 > 0, arg1 > 0 -> (-arg1p5+arg1 <= 0 /\ arg1 > 0)}

Step with 15

	Trace

	8[T], 1[(1+arg1p2 > 0 /\ arg1 > 0)], 9[(1+arg1 > 0 /\ 1+arg1p3 > 0 /\ arg1p3-arg1 <= 0)], 10[(1+arg1p4 > 0 /\ 2+arg1p4-arg1 <= 0 /\ -1+arg1 > 0)], 15[(-arg1p5+arg1 <= 0 /\ -arg1p5+arg1 >= 0 /\ arg1p5 > 0 /\ arg1 > 0)]
	
	Blocked

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

Refute

	Counterexample

	[ arg1=1 arg2=0 ] 8 [ arg1=4 arg2=0 ] 1 [ arg1=4 arg2=0 ] 9 [ arg1=2 arg2=0 ] 10 [ arg1=arg1 arg2=arg2 ] 15
	
NO

Build SHA: a05f16bf13df659c382799650051f91bf6828c7b