Open baoluomeng opened 1 month ago
We currently do not have Apple hardware for development and testing. Cross-compilation for Apple might not work. That operating system is special. 💰
If an SMT solver provides native libraries on its own, such as Z3 maybe, we can include it. Otherwise, you can use Java-based SMT solvers like SMTInterpol on any platform.
The latest Z3 has native support for arm64 Mac: https://github.com/Z3Prover/z3/releases/tag/z3-4.13.0. I downloaded the dylib files and plugged them into JavaSMT on my arm64 Mac. It works fine so far. But I would prefer a centralized approach like JavaSMT so that I don't have to tell my teammates how to set it up. Thanks.
See this long-standing discussion. The issue seems to be somewhat orthogonal to MacOS as it applies to all ARM machines.
Curious about the timeline to support Mac with Apple M1,2,3?