Out of memory exception on small files about axiom-profiler HOT 1 OPEN

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)

from axiom-profiler.