Exception: "Expected pattern but found Term" about axiom-profiler HOT 13 CLOSED

Bitbucket user jonhdotnet on 2018-11-20 22:50:

• edited the title

from axiom-profiler.

Bitbucket user jonhdotnet commented on 2018-11-20 22:53

Z3 version that generated the log file is: Z3 [version 4.7.1 - 64 bit].

from axiom-profiler.

@alexanderjsummers commented on 2018-11-20 23:02

Hi Jon, thanks for your detailed report. Right now we have an issue that there are some changes to the log generation that we have not yet made pull requests to Z3 for. I'm not sure if that is the reason for your issue. nilsbecker_ might be able to add more information - Nils?

Would it be possible to attach the .smt2 file (or .bpl file) that corresponds to the log, please? If so, I can test it out locally. If not, you could potentially try regenerating the log with the fork of Z3 here: https://github.com/Nils-Becker/z3 and see whether you get the same problem.

from axiom-profiler.

Bitbucket user jonhdotnet commented on 2018-11-20 23:57

from axiom-profiler.

Bitbucket user jonhdotnet on 2018-11-20 23:57:

• changed attachment from (none) to foo.bpl

from axiom-profiler.

Bitbucket user jonhdotnet commented on 2018-11-20 23:57

A little of column A, a little of column B. I have attached the .bpl file I used to generate the log. I'll also try Nils' z3.

from axiom-profiler.

Bitbucket user jonhdotnet commented on 2018-11-21 00:19

Here's the log output from nils' z3, with PROOF=true.
It causes "An exception occured while parsing the log: The requested operation caused a stack overflow."

Interestingly, collecting the log from Nils' z3 took 17s. Collecting it from the github z3 (https://codeload.github.com/Z3Prover/z3/tar.gz/z3-4.7.1/z3-z3-4.7.1.tar.gz) took more than a half an hour! (I don't know how much more because I went home before it finished. :v)

from axiom-profiler.

Bitbucket user jonhdotnet on 2018-11-21 00:19:

• changed attachment from (none) to nils-z3.log.gz

from axiom-profiler.

Bitbucket user nilsbecker_ on 2018-11-21 10:52:

• changed the assignee from (none) to bitbucket user nilsbecker_

from axiom-profiler.

Bitbucket user nilsbecker_ commented on 2018-11-21 10:53

I'll take a closer look later today.

from axiom-profiler.

@alexanderjsummers commented on 2018-11-21 11:31

Thanks nilsbecker_

jonhdotnet - by the way, the Axiom Profiler should be fine with a prefix of a log file, so in principle if logging with z3 takes too long you can kill it and use what you have. However, I've observed that sometimes killing z3 causes the file to suddenly get truncated to something very small - if you see the same issue, you might want to copy it before killing the process..

Similarly, if loading in the Axiom Profiler takes a long time, you can hit Cancel, and the tool will just use the data that it loaded up until that point.

from axiom-profiler.

Bitbucket user nilsbecker_ commented on 2018-11-21 14:14

jonhdotnet commit 9759936 should solve the issue. I'm now able to load (a prefix of) the log you provided as nils-z3.log. Please let me know if you encounter any other issues.

from axiom-profiler.

Bitbucket user nilsbecker_ on 2018-11-21 14:15:

• changed state from new to resolved

from axiom-profiler.