Support chained synthesis

[ilyasergey]

At the moment, synthesis can take "hints" about auxiliary functions, which can be used for synthesing the main one. For instance, this is a specification for tree flattening that takes an auxiliary function:

{ lseg(x1, s1) ** lseg(x2, s2) ** ret :-> x2 }
void lseg_append (loc x1, loc ret)
{ s =i s1 ++ s2 ; lseg(y, s) ** ret :-> y }

{ z :-> x ** tree(x, s) }
void flatten(loc z)
{ z :-> y ** lseg(y, s) }

Even though lseg_append can be synthesized by suslik as a standalone function, it doesn't happen here.

This issue it about extending synthesizer to support "chained" synthesis with auxiliary functions. In this example, it would first synthesize lseg_append and then, using it flatten.