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.

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

WARNING: unhandled theory N3smt17theory_diff_logicINS_7rdl_extEEE #2410

Closed
prakashmurali opened this issue Jul 18, 2019 · 2 comments
Closed

Comments

@prakashmurali
Copy link

prakashmurali commented Jul 18, 2019

I am running on Z3 on this problem https://github.com/prakashmurali/random/blob/master/z3_warning. I am using the optimization API from Python. While running check(), z3 goes into a loop of printing "WARNING: unhandled theory N3smt17theory_diff_logicINS_7rdl_extEEE".
The solver runs to completion and returns sat. On smaller instances of my problem (which are also sat), this warning doesn't appear. I would like to understand what is triggering this warning. Do you know what I should look at to fix this?

I can supply more instances if that helps. Thanks!

NikolajBjorner added a commit that referenced this issue Jul 18, 2019
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
@NikolajBjorner
Copy link
Contributor

should be fixed now

@prakashmurali
Copy link
Author

Thanks a lot for the quick response!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

2 participants