[SMT-LIB] let vs. assumption construct

[Rémi Delmas]

Hi all and happy new year!

which approach is preferable in SMT-lib between these two to express a 
functional dependency between variables of a model (in the benchmark 
library both approaches are used)?

Using assumptions to encode variable definitions
declare a free symbol and constrain it to be equal to some expression of 
other symbols :
:extrafun (x S)
...
:assumption (= x <some S-sorted expression>)
:formula (<some formula of x>)

Or the use let construct directly in the formula :
:formula (let (x <some S-sorted expression>) <some formula of x>)

Is it possible to run into issues like parser stack overflow when 
nesting lots of let constructs  (hundreds of thousands) ?

Thanks,

/Rémi