Fix SyGuS define-fun printing from benchmarks coming from v1 parser (#4256)

Fix SyGuS define-fun printing from benchmarks coming from v1 parser (#4256)

A recent change made it so that defined functions would print as the anonymous lambda corresponding to their definition if the SyGuS v1 parser was used. This was caused by comparison with the wrong kind in the new API.

Notice that the v2 parser does not have this issue.

This also adds a regression to ensure this behavior is maintained by the SyGuS v2 parser.