[SMT-LIB] SMT-LIB semantics

[Viktor Kuncak]

Dear Cesare,

Thanks for all answers, they were helpful.

> > are the function symbols FREE?  Was this supposed to mean
> > UNINTERPRETED?
>
> Yes. "Free symbol" is in fact the common terminoly in logic and
> automated reasoning for what formal methods people traditionally have
> called "unintepreted symbols".

I think my life-long confusion ends here. :)

(Perhaps the reason for some confusion in terminology stems from the
terms "freely generated" and "absolutely free algebra".)

Best regards,

  Viktor