Warning (during instrumentation):
  Clight instrumentation is not implemented yet.
Checking execution traces...OK.
ing has cost 0.
Warning: branching to if_jian12 has cost 1; continuing has cost 3.
Warning: branching to if_jian13 has cost 2; continuing has cost 3.
Call(func,stop)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(assign t1,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(assign t2,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(assign t3,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(seq,seq)
Regular(cost,seq)
Regular(assign t4,seq)
Regular(skip,seq)
Regular(seq,seq)
Regular(cost,seq)
Regular(assign t5,seq)
Regular(skip,seq)
Regular(cost,seq)
Regular(assign u,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(22),call)
Regular(skip,seq)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(seq,seq)
Regular(cost,seq)
Regular(assign e,seq)
Regular(skip,seq)
Regular(seq,seq)
Regular(cost,seq)
Regular(assign e,seq)
Regular(skip,seq)
Regular(cost,seq)
Regular(assign g,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(6),call)
Regular(skip,seq)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(assign result,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(2),call)
Regular(skip,seq)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(assign result,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(2),call)
Regular(skip,seq)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(assign min,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(1),call)
Regular(skip,seq)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(assign a,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(assign b,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(3),call)
Regular(skip,seq)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(assign c,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(assign c,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(1),call)
Regular(skip,seq)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(assign c,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(assign d,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(assign v,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(assign w,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(assign z,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(assign c,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(seq,seq)
Regular(cost,seq)
Regular(assign z,seq)
Regular(skip,seq)
Regular(cost,seq)
Regular(assign w,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(assign d,seq)
Regular(skip,seq)
Regular(seq,call)
Regular(cost,seq)
Regular(assign v,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(3),call)
Regular(skip,seq)
Regular(seq,stop)
Regular(cost,seq)
Regular(call,seq)
Call(func,call)
Regular(seq,call)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(ifthenelse,seq)
Regular(cost,seq)
Regular(assign result,seq)
Regular(skip,seq)
Regular(cost,call)
Regular(return,call)
Return(Int(-1),call)
Regular(skip,seq)
Regular(cost,stop)
Regular(return,stop)
Result: Int(-1)
Memory dump: 
n = 54
block 1 : Free.

block 2 : Free.

block 3 : Free.

block 4 : Free.

block 5 : Free.

block 6 : Free.

block 7 : Free.

block 8 : Free.

block 9 : Free.

block 10 : Free.

block 11 : Free.

block 12 : Free.

block 13 : Free.

block 14 : Free.

block 15 : Free.

block 16 : Free.

block 17 : Free.

block 18 : Free.

block 19 : Free.

block 20 : Free.

block 21 : Free.

block 22 : Free.

block 23 : Free.

block 24 : Free.

block 25 : Free.

block 26 : Free.

block 27 : Free.

block 28 : Free.

block 29 : Free.

block 30 : Free.

block 31 : Free.

block 32 : Free.

block 33 : Free.

block 34 : Free.

block 35 : Free.

block 36 : Free.

block 37 : Free.

block 38 : Free.

block 39 : Free.

block 40 : Free.

block 41 : Free.

block 42 : Free.

block 43 : Free.

block 44 : Free.

block 45 : Free.

block 46 : Free.

block 47 : Free.

block 48 : Free.

block 49 : Free.

block 50 : Free.

block 51 : Free.

block 52 : Free.

block 53 : Free.

State_call { function() - stop }
State_regular { seq - stop }
State_regular { cost - seq::cont }
State_regular { call - seq::cont }
State_call { function(Int(1),Int(2),Int(3),Int(4),Int(5),Int(6),Int(7),Int(8),Int(9)) - returnto }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { seq - cost::cont }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(22) - returnto }
State_regular { skip - seq::cont }
State_regular { seq - stop }
State_regular { cost - seq::cont }
State_regular { call - seq::cont }
State_call { function(Int(1),Int(2)) - returnto }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { seq - cost::cont }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(6) - returnto }
State_regular { skip - seq::cont }
State_regular { seq - stop }
State_regular { cost - seq::cont }
State_regular { call - seq::cont }
State_call { function(Int(1),Int(2),Int(3)) - returnto }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(2) - returnto }
State_regular { skip - seq::cont }
State_regular { seq - stop }
State_regular { cost - seq::cont }
State_regular { call - seq::cont }
State_call { function(Int(1),Int(2),Int(3)) - returnto }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(2) - returnto }
State_regular { skip - seq::cont }
State_regular { seq - stop }
State_regular { cost - seq::cont }
State_regular { call - seq::cont }
State_call { function(Int(1),Int(2)) - returnto }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(1) - returnto }
State_regular { skip - seq::cont }
State_regular { seq - stop }
State_regular { cost - seq::cont }
State_regular { call - seq::cont }
State_call { function(Int(1),Int(2)) - returnto }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(3) - returnto }
State_regular { skip - seq::cont }
State_regular { seq - stop }
State_regular { cost - seq::cont }
State_regular { call - seq::cont }
State_call { function(Int(1),Int(2)) - returnto }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(1) - returnto }
State_regular { skip - seq::cont }
State_regular { seq - stop }
State_regular { cost - seq::cont }
State_regular { call - seq::cont }
State_call { function(Int(1),Int(2),Int(3),Int(4)) - returnto }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { ifthenelse - seq::cont }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { ifthenelse - seq::cont }
State_regular { seq - seq::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - seq::cont }
State_regular { assign - seq::cont }
State_regular { skip - seq::cont }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(3) - returnto }
State_regular { skip - seq::cont }
State_regular { seq - stop }
State_regular { cost - cost::cont }
State_regular { call - cost::cont }
State_call { function(Int(1),Int(2),Int(3)) - returnto }
State_regular { seq - returnto }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { ifthenelse - cost::cont }
State_regular { cost - cost::cont }
State_regular { assign - cost::cont }
State_regular { skip - cost::cont }
State_regular { cost - returnto }
State_regular { return - returnto }
State_return { Int(-1) - returnto }
State_regular { skip - cost::cont }
State_regular { cost - stop }
State_regular { return - stop }
Result: Int(-1)
Memory dump: 
n = 11
block 1 : Free.

block 2 : Free.

block 3 : Free.

block 4 : Free.

block 5 : Free.

block 6 : Free.

block 7 : Free.

block 8 : Free.

block 9 : Free.

block 10 : Free.