8000 Regression with lambdas: trivial formula now unknown · Issue #5516 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Regression with lambdas: trivial formula now unknown #5516

New issue

8000 Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
nunoplopes opened this issue Aug 29, 2021 · 5 comments
Closed

Regression with lambdas: trivial formula now unknown #5516

nunoplopes opened this issue Aug 29, 2021 · 5 comments

Comments

@nunoplopes
Copy link
Collaborator

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
Copy link
Contributor

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
Copy link
Collaborator Author

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 added a commit that referenced this issue Sep 2, 2021
@NikolajBjorner
#5516
cf9e55f 
expose ability to expand select/store and select/ite (lambdas are always expanded) during pre-processing for N.P. Lopes.
@NikolajBjorner
Copy link
Contributor

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
Copy link
Collaborator Author

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
Copy link
Contributor

enable ematching?

nunoplopes added a commit to AliveToolkit/alive2 that referenced this issue Sep 11, 2021
@nunoplopes
simplify unit test as z3 cant verify this anymore
cb5aefd 
Z3Prover/z3#5516
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@nunoplopes @NikolajBjorner
0