jeannin / zelus

A synchronous language with ODEs
http://zelus.di.ens.fr
Other
0 stars 4 forks source link

Refinement function check fails for nested functions #12

Open jlvargasme opened 2 years ago

jlvargasme commented 2 years ago

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.