regression regarding lambdas introduced in 0758c930

[ffrohn]

This example is solved by z3 4.12.1, but not by later versions. The regression was introduced in commit 0758c93, which fixed issue #6591 (I reverted this commit locally, and now it works).

However, this issue was about quantifiers, whereas my example is quantifier free. Can the old behavior be restored for quantifier free instances?

[NikolajBjorner]

Generally, not sound to remove that code, but it can be strengthened to fail sat verdict less often on some cases.
Your formula contains equations between lambdas and variables. Model construction only really understands store for arrays.

[ffrohn]

Great, thanks!