Hi Philipp. Thanks for your answer.
Can we make some assumptions on the variables occurring in let-binders?
For example, given the term (let ((x1 t1)...(xn tn)) t )
the SMT-LIB standard requires that x1...xn are distinct variables but does not say anything about their occurrence in t1...tn.
Thus a term (let ((x y) (y x)) (> x y)) is legal and equivalent to (> y x).
Can we assume that variables x1...xn do not occur in t1...tn?
This would simplify the management of let-binders
and allow us to manage the parallel bindings in a sequential manner.
letas an equality. and (b) write a parser that keeps track of current binding while building the expressions