==> YES, main.fstb terminates. max_dim = 3

+-----------------------------------------------------------------------------+
|                             Ranking Function                                |
+-----------------------------------------------------------------------------+

state start:
3

state stop:
0

state lbl6:
1

state lbl121:
2
(-1+(2*B))+(-2*G)
A+(-1*E)

state cut:
1

state lbl141:
2
(2*B)+(-2*G)

state start0:
4

state ____start0:
5


+-----------------------------------------------------------------------------+
|                         Worst Case Execution Time                           |
+-----------------------------------------------------------------------------+

/---
/
| 2+(-1*C__o') >= 0
| -2+A__o' >= 0
| 1 >= 0
\

(((1+1)+1)+1)+1

/
| (-1+(-1*A__o'))+C__o' >= 0
| -2+A__o' >= 0
| 1 >= 0
\

(((((1+1)+(C__o'*A__o'))+1)+C__o')+1)+1

/
| -1+A__o' = 0
| -2+C__o' >= 0
| 1 >= 0
\

((((1+1)+(C__o'*A__o'))+((-2+C__o')+A__o'))+1)+1

/
| -2+A__o' = 0
| -3+C__o' >= 0
| 1 >= 0
\

(((((1+1)+(C__o'*A__o'))+1)+((-2+C__o')+A__o'))+1)+1

/
| -3+A__o' >= 0
| A__o'+(-1*C__o') >= 0
| 1 >= 0
\

(((1+1)+1)+1)+1

/
| -1+A__o' >= 0
| 1+(-1*C__o') >= 0
| 1 >= 0
\

(((1+1)+1)+1)+1

/
| -1*A__o' >= 0
| 1 >= 0
\

((1+1)+1)+1

/
| (-1+(-1*A__o'))+C__o' >= 0
| -1*A__o' >= 0
| 1 >= 0
\

((1+1)+1)+1

\---