added support for closures in the SMT encoding; sf-poly verifies completely