Skip to content
New issue

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

sat.euf #5573

Closed
NikolajBjorner opened this issue Sep 28, 2021 · 2 comments
Closed

sat.euf #5573

NikolajBjorner opened this issue Sep 28, 2021 · 2 comments

Comments

@NikolajBjorner
Copy link
Contributor

Known bug: quantifier instantiation is unsound (reports sat when unsat)

z3 C:/UF/grasshopper/instantiated/rec_reverse_acc_check_heap_access_17_4.smt2 sat.euf=true /st
NikolajBjorner added a commit that referenced this issue Sep 29, 2021
@NikolajBjorner
missing continue fixes unsound sat result from #5573
cbe7dd4
@NikolajBjorner
Copy link
Contributor Author

Known bug: E-matching is highly incomplete

z3 C:\uf\grasshopper\uninstantiated\concat_check_heap_access_23_4.smt2 smt.mbqi=false smt.auto_config=false sat.euf=true

NikolajBjorner added a commit that referenced this issue Oct 16, 2021
@NikolajBjorner
fixes to sat.euf ematching #5573
115203e
@NikolajBjorner
Copy link
Contributor Author

Known bug: Skolemization should be eagier, relevancy propagation doesn't work

z3 C:\UF\sledgehammer\Arrow_Order\smtlib.761827.smt2 /st smt.auto_config=false smt.mbqi=false sat.euf=true

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
1 participant
@NikolajBjorner