-
Notifications
You must be signed in to change notification settings - Fork 4
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
Out of memory exception on small files #35
Comments
I did some more minimization and came up with the following. First I minimized a silver file that, if any of the contracts are removed, produces a z3.log that loads just fine. If none of the contracts are removed, a z3.log is produced that hangs for me in axiom profiler. Then I started minimizing the .smt2 output from viper, trying to find the line that causes axiom profiler to hang. It is now a file of 264 lines. If the last line is commented, a z3.log is produced that loads just fine. If the last line is not commented, a z3.log is produced that causes axiom profiler to hang. Strangely enough, that last line is a I have diffed the ok and not_ok logs, but I'm not experienced enough to make heads or tails of that diff. The only thing that caught my eye is that that push statement seems to cause a lot of extra proof steps (mk-app/mk-proof/new-match, about 200 lines). We run into quantifier related problems more and more frequently lately with VerCors, so being able to use axiom profiler would be a huge help. If there is anything else I can minimize or debug myself please mention it!
|
I have this z3 log file of 3 gigabytes. When I load it into axiom profiler, axiom profiler gives an out of memory exception. If I cut it down to 800kb, it still gives an OOM. In both these cases, the first 8 quantifiers in the list of axiom profiler have about 20 instances total. Since I started with a 3 gigabyte file, I would expect more instances.
If I cut it down to 500kb, it loads just fine, but contains no quantifier instances.
I can also post a link to the 3 gigabyte version if needed.
If I have a look where visual studio reports the exception, I get the following:
The "explanations" list seems to get filled up up to the memory limit of the system because of some cycle in the input...?
I acquired this file by running viper/silicon with
--numberOfParallelVerifiers 1 --z3Args '"trace=true proof=true"'
. Besides that, I only did truncation on it usingtruncate -s 800K z3.log
.Can axiom profiler be made aware of the cycle in these files? Or is the z3 log output of viper somehow wrong? Since the behavior between the 3gig file and 800k file is identical, I'm assuming truncation does not matter.
The text was updated successfully, but these errors were encountered: