Herman Venter

Yes, you need to construct the limits struct in main.rs and pass it to the constructor of MiraiCallbacks, who then needs to pass it to the visitor.

MIRAI runs on Ubuntu (20.04.3 LTS) for every PR (see https://github.com/facebookexperimental/MIRAI/blob/main/.github/workflows/rust.yml). The relevant action installs Z3 via `sudo apt-get install libz3-dev`, which installs 4.8.7-4build1. This seems to be in line...

I can run your test script on my MacBook, see the paste: https://pastebin.com/iJP8D7Jx My guess is that this is a resource limitation error that causes Z3 to to crash.

I did not encounter any failures. If you can investigate some more on your side it may help resolve the issue.

The two tests that time out do quite a lot of work. If you are running then on a smaller, slower machine, it is not surprising that it will time...

I'm seeing tests failing on my mac book, which has 32 GB of RAM, whereas they all pass on the CI machines, which only have 20 GB. Closing apps on...

Thanks for the update. I'll add this solution to the documentation. Since I can no longer merge PRs into this repo, and no-one at Meta seems interested in helping me,...

I believe this problem is already fixed on https://github.com/hermanventer/MIRAI, which should now be regarded as the source of truth for MIRAI since no-one at Meta seems interested in merging pull...

Could you append a full log of a session where you follow the installation instructions and it fails?

From InstallationGuide.md: For macOS the binary will have to be placed somewhere where it can be found and dynamically loaded by the Rust runtime. You'll also need the z3 header...