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

Overflow encountered when expanding vector #1251

Closed
delcypher opened this issue Sep 8, 2017 · 4 comments

Comments

@delcypher
Copy link
Contributor

commented Sep 8, 2017

Likely related to #864 #455 and reading those descriptions it sounds like a memory limit issue.

When running the latest Z3 master (1d6f53c) and using Z3's C API in our application we receive an error to our Z3 error handler. The associated error message with the error is Overflow encountered when expanding vector.

This is an error I noticed quite a while ago but hadn't got round to reporting because I hadn't tested on the latest Z3 master.

Attached is a compressed API interaction log. If you need anything else from me to reproduce then let me know.

@NikolajBjorner

This comment has been minimized.

Copy link
Contributor

commented Sep 12, 2017

How long does it take you to produce this overflow based on the log? This seems to run for a long time with modest memory consumption.

@delcypher

This comment has been minimized.

Copy link
Contributor Author

commented Sep 12, 2017

@NikolajBjorner It's approximately 15 minutes. I just tried replaying the log and I don't seem to get same behaviour as we do in our tool. I'm assuming an API error would cause the replay to halt. Does it?.

This is likely going to require more digging on my part.

@NikolajBjorner

This comment has been minimized.

Copy link
Contributor

commented Sep 12, 2017

I added rather many changes since your log was generated and only tried replaying against the newest bits. In the newest bits, the legacy simplifier is gone. If the overflow happened there for whatever reason, then it is not going to come back in that form. We have special vector classes that allow 64 bit indexing, so if your bug identifies a useful place to allow more memory it is one option to address this.

@NikolajBjorner

This comment has been minimized.

Copy link
Contributor

commented Jun 13, 2019

This bug is so old that the relevant code has changed significantly

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
2 participants
You can’t perform that action at this time.