Abs program loaded in 3 ms.

Rule based representation generated in 1 ms.

Rule based representation stored in /tmp/costabs/rbr.rbr

RBR properties stored in /tmp/costabs/rbr.properties

Class invariants generated and loaded in 0 ms.
Size abstraction not supported for native

Abstract compilation performed in 1 ms.
sabu_memo_table_1(case_0,[A,B,C],[1*C=0,1*B=1],0,0)
sabu_memo_table_1(case_1,[A,B,C,D,E],[1*E=1,1*A+ -1*C=0],0,0)
sabu_memo_table_1(anyEq,[A,B,C],[1*B=1,1*C=0],1,0)
sabu_memo_table_1(case_0,[A,B,C],[-1*C>= -1,1*B+ -1*C>=1,1*C>=0],1,1)
sabu_memo_table_1(anyEq,[A,B,C],[-1*C>= -1,1*B+ -1*C>=1,1*C>=0],2,1)
sabu_memo_table_1(case_1,[A,B,C,D,E],[1*E>=0,1*A+ -1*C+1*E>=1,-1*E>= -1],3,1)
sabu_memo_table_1(case_1,[A,B,C,D,E],[1*E>=0,-1*E>= -1],3,2)
sabu_memo_table_1(case_2,[A,B,C],[1*B+ -1*C>=2,-1*C>= -1,1*C>=0],0,0)
sabu_memo_table_1(lookupBTree,[A,B,C],[1*C>=0,-1*C>= -1,1*B+ -1*C>=2],0,0)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G,H,I],[-1*A+1*E>=0,1*G+ -1*I>=2,-1*I>= -1,1*I>=0],1,0)
sabu_memo_table_1(case_5,[A,B,C,D,E,F,G,H,I],[1*I>=0,-1*I>= -1],1,1)
sabu_memo_table_1(case_4,[A,B,C,D,E,F,G],[1*D>=2,-1*G>= -1,1*G>=0],2,0)
sabu_memo_table_1(case_3,[A,B,C,D,E],[1*D>=2,1*C>=2,-1*E>= -1,1*E>=0],3,0)
sabu_memo_table_1(start,[A,B,C],[1*B+ -1*C>=2,-1*C>= -1,1*C>=0],0,0)
sabu_memo_table_1(start,[A,B],[],0,0)
:- dynamic sabu_memo_table_1/5.

sabu_memo_table_1(case_0, [_, B, A], [-1*A>= -1, 1*B+ -1*A>=1, 1*A>=0], 1, 1).
sabu_memo_table_1(anyEq, [_, B, A], [-1*A>= -1, 1*B+ -1*A>=1, 1*A>=0], 2, 1).
sabu_memo_table_1(case_1, [_, _, _, _, A], [1*A>=0, -1*A>= -1], 3, 2).
sabu_memo_table_1(case_2, [_, A, B], [1*A+ -1*B>=2, -1*B>= -1, 1*B>=0], 0, 0).
sabu_memo_table_1(lookupBTree, [_, B, A], [1*A>=0, -1*A>= -1, 1*B+ -1*A>=2], 0, 0).
sabu_memo_table_1(case_5, [_, _, _, _, _, _, _, _, A], [1*A>=0, -1*A>= -1], 1, 1).
sabu_memo_table_1(case_4, [_, _, _, A, _, _, B], [1*A>=2, -1*B>= -1, 1*B>=0], 2, 0).
sabu_memo_table_1(case_3, [_, _, B, A, C], [1*A>=2, 1*B>=2, -1*C>= -1, 1*C>=0], 3, 0).
sabu_memo_table_1(start, [_, A, B], [1*A+ -1*B>=2, -1*B>= -1, 1*B>=0], 0, 0).
sabu_memo_table_1(start, [_, _], [], 0, 0).


Size analysis performed in 6 ms.

Cost relation system stored in /tmp/costabs/crs.crs

Generated 41 equations 

Cost relation system solved by PUBS in 76 ms.

Method start terminates?: UNKOWN

UB for start(n,node) = c(failed(no_rf,[scc=1,cr=lookupBTree/2]))


Preprocessing Cost Relations
=====================================

#### Computed strongly connected components 
0. non_recursive  : [start/1]
2. recursive  : [anyEq/2,case_0/2,case_1/4]
3. recursive  : [case_2/2,case_3/4,case_4/6,case_5/8,lookupBTree/2]
4. non_recursive  : [start/2]
Warning: the following predicates are never called:[and_op/2,anyEq/2,case_2/2,eq/2,geq/2,gt/2,leq/2,lookupBTree/2,lt/2,maxNorm/2,neg/1,neq/2,or/2]

#### Obtained direct recursion through partial evaluation 
0. SCC is partially evaluated into start/1
2. SCC is partially evaluated into anyEq/2
3. SCC is partially evaluated into lookupBTree/2

Control-Flow Refinement of Cost Relations
=====================================

### Specialization of cost equations start/1 
* CE 1 is refined into CE [2] 


#### Refined cost equations start/1 
* CE 2: start(A) = 1
     [] 

### Cost equations --> "Loop" of start/1 
* CEs [2] --> Loop 2 

#### Loops of start/1 
* Loop 2: start(A) [] 

### Ranking functions of CR start(A) 

#### Partial ranking functions of CR start(A) 


### Resulting Chains:start(A) 
* [2]


Computing Bounds
=====================================

#### Cost of chains of start(A):
* Chain [2]: 1
  with precondition: [] 


Closed-form bounds of start(A): 
-------------------------------------
* Chain [2] with precondition: [] 
    - Lower bound: 1 
    - Complexity: constant
 
### Partitioned lower bound of start(A): 
* 1 
 if []
Possible lower bounds : [1]
Maximum lower bound complexity: constant
* Total analysis performed in 32 ms.