Regression with lambdas: trivial formula now unknown

[nunoplopes]

I'm seeing a regression with lambdas, where a lot of simple formulas that used to be unsat now give unknown.
The commit at fault is: 8f306c6

Error message: smt tactic failed to show goal to be sat/unsat (incomplete quantifiers)

The attached log has 2 calls to Z3_check: they should give sat & unsat, respectively. After the mentioned commit, they give sat & undef.
z3_log.zip

The test case is from Alive2 and is really simple: just transforms a store instruction into a memset (the lambda).

[NikolajBjorner]

It is not true that there is a regression relative to your benchmark on that commit.
I tried d684817 as well, and the result is undef.

You call "reset" methods that obscures logging. If you can create repros in the future without resetting the context it would make life easier.

[nunoplopes]

d684817 gives unsat to me (as well as all the previous commits for the past ~3 years):
(numbers are the output of Z3_solver_check)

master:

Alive2 v0.0-1559-g9025c0b
1
0
max. heap size:     18.548 Mbytes
time:               0.078125

d684817:

Alive2 v0.0-1559-g9025c0b
1
-1
max. heap size:     19.7701 Mbytes
time:               0.359375

This is now breaking Alive2's unit tests on linux & windows at least. Didn't try Mac yet.

[NikolajBjorner]

you disable ematching while having lambdas: the solver relies on ematching instantiation to expand lambdas.
This is not specific to this push.

I added a facility for you to expand select/ite constructs, but with ematching it goes through.

[nunoplopes]

Thank you.
I've tried Z3_global_param_set("rewriter.expand_select_ite", "true"); but doesn't make any material difference. This benchmark still fails and the regression in the benchmarks remain. The number of errors (incomplete quantifiers) tripled.

[NikolajBjorner]

enable ematching?