Issue with lambdas and untyped let bindings from Z3 4.8.5 about inox HOT 2 CLOSED

@samarion any advice on this? What could go wrong with inlining?

from inox.

Inlining the lets should work (probably), but traversing the scala-smtlib trees is a bit painful.

An alternative (but semantically equivalent) implementation approach would be to override the SMTLet case in the Z3Parser and add the unextracted let binding to the context. When the corresponding variable is encountered during extraction, the term can be extracted with its expected type.

Finally, a third approach would be to extract models into @redelmann's intermediate representation and then run elaboration on the extracted expressions. This is probably overkill and the let inlining should work (also if we want model extraction to return values, then it shouldn't return any let bindings).

from inox.