Refinement function check fails for nested functions

[jlvargasme]

Issue description:

let add ( x : int{x > 0} ) ( y : int{y > 0} ) : int{ add_return >= x && add_return >= y} = x + y
let f2 ( x : int{x < 0} ) : int{ f2_return > 0} = add (x * x) (x * x)

fails with the following message: this is a combinatorial expression and is expected to be static

Action:

Understand why is it failing and fix the issue.