Out of memory exception on small files

[bobismijnnaam]

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.

• 800kb file that causes a crash and has only a handful of quantifier instances: z3_smaller.log
• 500kb file that doesn't crash but has no quantifier instances: z3_smaller_no_quant.log

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 using truncate -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.

[bobismijnnaam]

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.

• minimal_axiom_fail.txt
• z3_ok.log
• z3_not_ok.log

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 (push), which I did not expect to matter. Both the z3 logs with and without that last line are included as well.

• logfile-01-broken.smt2.txt
• z3_ok.log
• z3_not_ok.log

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!

• Viper version: Silicon 1.1-SNAPSHOT (4ca96a49+)
• z3 version: Z3 version 4.8.6 - 64 bit
• Axiom profiler built from master (I can find mono/.net sdk versions if necessary)