YES(?, 126*a + 24*a^2 + 107)

Initial complexity problem:
1:	T:
		(1, 1)    evalloopsstart(a, b) -> evalloopsentryin(a, b)
		(?, 1)    evalloopsentryin(a, b) -> evalloopsbb6in(a, b) [ a >= 0 ]
		(?, 1)    evalloopsentryin(a, b) -> evalloopsreturnin(a, b) [ 0 >= a + 1 ]
		(?, 1)    evalloopsbb6in(a, b) -> evalloopsbb1in(a, b) [ a >= 0 ]
		(?, 1)    evalloopsbb6in(a, b) -> evalloopsreturnin(a, b) [ 0 >= a + 1 ]
		(?, 1)    evalloopsbb1in(a, b) -> evalloopsbb4in(a, 1) [ a >= 2 ]
		(?, 1)    evalloopsbb1in(a, b) -> evalloopsbb5in(a, c) [ 1 >= a ]
		(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb3in(a, b) [ a >= b + 1 ]
		(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb5in(a, b) [ b >= a ]
		(?, 1)    evalloopsbb3in(a, b) -> evalloopsbb4in(a, 2*b)
		(?, 1)    evalloopsbb5in(a, b) -> evalloopsbb6in(a - 1, b)
		(?, 1)    evalloopsreturnin(a, b) -> evalloopsstop(a, b)
	start location:	evalloopsstart
	leaf cost:	0

Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem:
2:	T:
		(1, 1)    evalloopsstart(a, b) -> evalloopsentryin(a, b)
		(?, 1)    evalloopsentryin(a, b) -> evalloopsbb6in(a, b) [ a >= 0 ]
		(?, 1)    evalloopsbb6in(a, b) -> evalloopsbb1in(a, b) [ a >= 0 ]
		(?, 1)    evalloopsbb1in(a, b) -> evalloopsbb4in(a, 1) [ a >= 2 ]
		(?, 1)    evalloopsbb1in(a, b) -> evalloopsbb5in(a, c) [ 1 >= a ]
		(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb3in(a, b) [ a >= b + 1 ]
		(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb5in(a, b) [ b >= a ]
		(?, 1)    evalloopsbb3in(a, b) -> evalloopsbb4in(a, 2*b)
		(?, 1)    evalloopsbb5in(a, b) -> evalloopsbb6in(a - 1, b)
	start location:	evalloopsstart
	leaf cost:	3

Repeatedly propagating knowledge in problem 2 produces the following problem:
3:	T:
		(1, 1)    evalloopsstart(a, b) -> evalloopsentryin(a, b)
		(1, 1)    evalloopsentryin(a, b) -> evalloopsbb6in(a, b) [ a >= 0 ]
		(?, 1)    evalloopsbb6in(a, b) -> evalloopsbb1in(a, b) [ a >= 0 ]
		(?, 1)    evalloopsbb1in(a, b) -> evalloopsbb4in(a, 1) [ a >= 2 ]
		(?, 1)    evalloopsbb1in(a, b) -> evalloopsbb5in(a, c) [ 1 >= a ]
		(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb3in(a, b) [ a >= b + 1 ]
		(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb5in(a, b) [ b >= a ]
		(?, 1)    evalloopsbb3in(a, b) -> evalloopsbb4in(a, 2*b)
		(?, 1)    evalloopsbb5in(a, b) -> evalloopsbb6in(a - 1, b)
	start location:	evalloopsstart
	leaf cost:	3

Separating problem 3 produces the isolated subproblem
10001:	T:
		(1, 0)    inner_10000_start_sep(a, b) -> evalloopsbb4in(a, 1)
		(?, 1)    evalloopsbb3in(a, b) -> evalloopsbb4in(a, 2*b)
		(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb3in(a, b) [ a >= b + 1 ]
	start location:	inner_10000_start_sep
	leaf cost:	0

=== begin of proof for isolated subproblem 10001 ===
	Initial complexity problem:
	10001:	T:
			(1, 0)    inner_10000_start_sep(a, b) -> evalloopsbb4in(a, 1)
			(?, 1)    evalloopsbb3in(a, b) -> evalloopsbb4in(a, 2*b)
			(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb3in(a, b) [ a >= b + 1 ]
		start location:	inner_10000_start_sep
		leaf cost:	0
	
	Applied AI with 'oct' on problem 20001 to obtain the following invariants:
	  For symbol evalloopsbb3in: X_1 - X_2 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0
	  For symbol evalloopsbb4in: X_2 - 1 >= 0
	
	
	This yielded the following problem:
	10002:	T:
			(?, 1)    evalloopsbb4in(a, b) -> evalloopsbb3in(a, b) [ b - 1 >= 0 /\ a >= b + 1 ]
			(?, 1)    evalloopsbb3in(a, b) -> evalloopsbb4in(a, 2*b) [ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
			(1, 0)    inner_10000_start_sep(a, b) -> evalloopsbb4in(a, 1)
		start location:	inner_10000_start_sep
		leaf cost:	0
	
	A polynomial rank function with
		Pol(evalloopsbb4in) = 2*V_1 - 2*V_2
		Pol(evalloopsbb3in) = 2*V_1 - 2*V_2 - 1
		Pol(inner_10000_start_sep) = 2*V_1 - 2
	orients all transitions weakly and the transitions
		evalloopsbb4in(a, b) -> evalloopsbb3in(a, b) [ b - 1 >= 0 /\ a >= b + 1 ]
		evalloopsbb3in(a, b) -> evalloopsbb4in(a, 2*b) [ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
	strictly and produces the following problem:
	10003:	T:
			(2*a + 2, 1)    evalloopsbb4in(a, b) -> evalloopsbb3in(a, b) [ b - 1 >= 0 /\ a >= b + 1 ]
			(2*a + 2, 1)    evalloopsbb3in(a, b) -> evalloopsbb4in(a, 2*b) [ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
			(1, 0)          inner_10000_start_sep(a, b) -> evalloopsbb4in(a, 1)
		start location:	inner_10000_start_sep
		leaf cost:	0
=== end of proof for isolated subproblem 10001 ===

Applying the information from the isolated subproblem 10001 to problem 3 produces the following problem:
4:	T:
		(?, 0)          inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b)
		(?, 4*a + 4)    inner_10000_in_sep(a, b) -> inner_10000_compl_sep(a, b)
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a >= 0 /\ b_sep >= 0 /\ b_sep <= 3*a + 2*a^2 + 1 ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a >= 0 /\ b_sep < 0 /\ -b_sep <= 3*a + 2*a^2 + 1 ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a < 0 /\ b_sep >= 0 /\ b_sep <= -3*a + 2*a^2 + 1 ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ a < 0 /\ b_sep < 0 /\ -b_sep <= -3*a + 2*a^2 + 1 ]
		(?, 1)          inner_10000_out_sep(a, b) -> evalloopsbb5in(a, b) [ b >= a ]
		(?, 1)          evalloopsbb1in(a, b) -> inner_10000_in_sep(a, 1) [ a >= 2 ]
		(?, 1)          evalloopsbb5in(a, b) -> evalloopsbb6in(a - 1, b)
		(?, 1)          evalloopsbb1in(a, b) -> evalloopsbb5in(a, c) [ 1 >= a ]
		(?, 1)          evalloopsbb6in(a, b) -> evalloopsbb1in(a, b) [ a >= 0 ]
		(1, 1)          evalloopsentryin(a, b) -> evalloopsbb6in(a, b) [ a >= 0 ]
		(1, 1)          evalloopsstart(a, b) -> evalloopsentryin(a, b)
	start location:	evalloopsstart
	leaf cost:	3

Applied AI with 'oct' on problem 4 to obtain the following invariants:
  For symbol evalloopsbb1in: X_1 >= 0
  For symbol evalloopsbb5in: X_1 >= 0
  For symbol inner_10000_compl_sep: -X_2 + 1 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0
  For symbol inner_10000_in_sep: -X_2 + 1 >= 0 /\ X_1 - X_2 - 1 >= 0 /\ X_2 - 1 >= 0 /\ X_1 + X_2 - 3 >= 0 /\ X_1 - 2 >= 0
  For symbol inner_10000_out_sep: X_1 - 2 >= 0


This yielded the following problem:
5:	T:
		(1, 1)          evalloopsstart(a, b) -> evalloopsentryin(a, b)
		(1, 1)          evalloopsentryin(a, b) -> evalloopsbb6in(a, b) [ a >= 0 ]
		(?, 1)          evalloopsbb6in(a, b) -> evalloopsbb1in(a, b) [ a >= 0 ]
		(?, 1)          evalloopsbb1in(a, b) -> evalloopsbb5in(a, c) [ a >= 0 /\ 1 >= a ]
		(?, 1)          evalloopsbb5in(a, b) -> evalloopsbb6in(a - 1, b) [ a >= 0 ]
		(?, 1)          evalloopsbb1in(a, b) -> inner_10000_in_sep(a, 1) [ a >= 0 /\ a >= 2 ]
		(?, 1)          inner_10000_out_sep(a, b) -> evalloopsbb5in(a, b) [ a - 2 >= 0 /\ b >= a ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a < 0 /\ b_sep < 0 /\ -b_sep <= -3*a + 2*a^2 + 1 ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a < 0 /\ b_sep >= 0 /\ b_sep <= -3*a + 2*a^2 + 1 ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= 0 /\ b_sep < 0 /\ -b_sep <= 3*a + 2*a^2 + 1 ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= 0 /\ b_sep >= 0 /\ b_sep <= 3*a + 2*a^2 + 1 ]
		(?, 4*a + 4)    inner_10000_in_sep(a, b) -> inner_10000_compl_sep(a, b) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
		(?, 0)          inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
	start location:	evalloopsstart
	leaf cost:	3

Testing for unsatisfiable constraints removes the following transitions from problem 5:
	inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a < 0 /\ b_sep < 0 /\ -b_sep <= -3*a + 2*a^2 + 1 ]
	inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a < 0 /\ b_sep >= 0 /\ b_sep <= -3*a + 2*a^2 + 1 ]
We thus obtain the following problem:
6:	T:
		(1, 1)          evalloopsstart(a, b) -> evalloopsentryin(a, b)
		(1, 1)          evalloopsentryin(a, b) -> evalloopsbb6in(a, b) [ a >= 0 ]
		(?, 1)          evalloopsbb6in(a, b) -> evalloopsbb1in(a, b) [ a >= 0 ]
		(?, 1)          evalloopsbb1in(a, b) -> evalloopsbb5in(a, c) [ a >= 0 /\ 1 >= a ]
		(?, 1)          evalloopsbb5in(a, b) -> evalloopsbb6in(a - 1, b) [ a >= 0 ]
		(?, 1)          evalloopsbb1in(a, b) -> inner_10000_in_sep(a, 1) [ a >= 0 /\ a >= 2 ]
		(?, 1)          inner_10000_out_sep(a, b) -> evalloopsbb5in(a, b) [ a - 2 >= 0 /\ b >= a ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= 0 /\ b_sep < 0 /\ -b_sep <= 3*a + 2*a^2 + 1 ]
		(?, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= 0 /\ b_sep >= 0 /\ b_sep <= 3*a + 2*a^2 + 1 ]
		(?, 4*a + 4)    inner_10000_in_sep(a, b) -> inner_10000_compl_sep(a, b) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
		(?, 0)          inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
	start location:	evalloopsstart
	leaf cost:	3

A polynomial rank function with
	Pol(evalloopsstart) = 6*V_1 + 6
	Pol(evalloopsentryin) = 6*V_1 + 6
	Pol(evalloopsbb6in) = 6*V_1 + 6
	Pol(evalloopsbb1in) = 6*V_1 + 5
	Pol(evalloopsbb5in) = 6*V_1 + 1
	Pol(inner_10000_in_sep) = 6*V_1 + 4
	Pol(inner_10000_out_sep) = 6*V_1 + 2
	Pol(inner_10000_compl_sep) = 6*V_1 + 3
orients all transitions weakly and the transitions
	inner_10000_out_sep(a, b) -> evalloopsbb5in(a, b) [ a - 2 >= 0 /\ b >= a ]
	inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
	inner_10000_in_sep(a, b) -> inner_10000_compl_sep(a, b) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
	inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= 0 /\ b_sep < 0 /\ -b_sep <= 3*a + 2*a^2 + 1 ]
	inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= 0 /\ b_sep >= 0 /\ b_sep <= 3*a + 2*a^2 + 1 ]
	evalloopsbb6in(a, b) -> evalloopsbb1in(a, b) [ a >= 0 ]
	evalloopsbb5in(a, b) -> evalloopsbb6in(a - 1, b) [ a >= 0 ]
	evalloopsbb1in(a, b) -> inner_10000_in_sep(a, 1) [ a >= 0 /\ a >= 2 ]
	evalloopsbb1in(a, b) -> evalloopsbb5in(a, c) [ a >= 0 /\ 1 >= a ]
strictly and produces the following problem:
7:	T:
		(1, 1)                evalloopsstart(a, b) -> evalloopsentryin(a, b)
		(1, 1)                evalloopsentryin(a, b) -> evalloopsbb6in(a, b) [ a >= 0 ]
		(6*a + 6, 1)          evalloopsbb6in(a, b) -> evalloopsbb1in(a, b) [ a >= 0 ]
		(6*a + 6, 1)          evalloopsbb1in(a, b) -> evalloopsbb5in(a, c) [ a >= 0 /\ 1 >= a ]
		(6*a + 6, 1)          evalloopsbb5in(a, b) -> evalloopsbb6in(a - 1, b) [ a >= 0 ]
		(6*a + 6, 1)          evalloopsbb1in(a, b) -> inner_10000_in_sep(a, 1) [ a >= 0 /\ a >= 2 ]
		(6*a + 6, 1)          inner_10000_out_sep(a, b) -> evalloopsbb5in(a, b) [ a - 2 >= 0 /\ b >= a ]
		(6*a + 6, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= 0 /\ b_sep < 0 /\ -b_sep <= 3*a + 2*a^2 + 1 ]
		(6*a + 6, 0)          inner_10000_compl_sep(a, b) -> inner_10000_out_sep(a, b_sep) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 /\ a >= 0 /\ b_sep >= 0 /\ b_sep <= 3*a + 2*a^2 + 1 ]
		(6*a + 6, 4*a + 4)    inner_10000_in_sep(a, b) -> inner_10000_compl_sep(a, b) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
		(6*a + 6, 0)          inner_10000_in_sep(a, b) -> inner_10000_out_sep(a, b) [ -b + 1 >= 0 /\ a - b - 1 >= 0 /\ b - 1 >= 0 /\ a + b - 3 >= 0 /\ a - 2 >= 0 ]
	start location:	evalloopsstart
	leaf cost:	3

Complexity upper bound 126*a + 24*a^2 + 107

Time: 0.739 sec (SMT: 0.704 sec)