Apple Silicon Issues

[reeselevine]

Getting Dartagnan running on my Apple M3 Air with OSX Sonoma, I ran into a couple issues that I don't see mentioned on the README.

• When trying to run through Docker, I get errors like this one:

[11.09.2024] 17:49:46 [ERROR] Dartagnan.main - The SMT solver Z3 is not available on this machine because of missing libraries (/home/Dat3M/dartagnan/target/libs/libz3.so: /home/Dat3M/dartagnan/target/libs/libz3.so: cannot open shared object file: No such file or directory (Possible cause: can't load AMD 64 .so on a AARCH64 platform)).

It appears that the Docker image is built with binaries that aren't supported on Arm based platforms, or at least Apple Silicon. I didn't investigate to see if there was a workaround to this.

• After building from source and adding Arm Z3 binaries to /Library/Java/Extensions as described here, I get an error when trying to run Dartagnan that Apple can't verify the binaries. The solution seems to be to clear the apple quarantine flag on the binaries, e.g., like this:

sudo xattr -d com.apple.quarantine /Library/Java/Extensions/libz3java.dylib

I'm not sure if there's a better way to do this.

[hernanponcedeleon]

Hi Reese, happy to see my msg last week had the intended behavior and you are giving dartagnan a try 😃.

AFAIK the only developer having an Apple machine is @ThomasHaas (not sure about @xeren). Can you please take a look?

[ThomasHaas]

The issue is exactly what the troubleshooting description tries to solve. I'm pretty sure that I also got the verification error, but I usually resolve it in the security settings. I guess the mentioned command will have the same effect.
I don't think there is a better way to do until the ARM-binaries are available via maven.
Maybe someone has to push the JavaSMT guys again to take a look into this?

[reeselevine]

Thanks for taking a look! The troubleshooting section was definitely useful, I just think it might be useful to add a sentence or two describing the above issues to avoid someone else having to make a couple extra Google searches 😅.

[hernanponcedeleon]

@reeselevine the code in the javasmt branch is working for the M2 series. Would you mind testing this on your M3 before we merge it?

[reeselevine]

Sorry for the slow reply, yes I tested it out and things are working now, including Docker!

[hernanponcedeleon]

Fix by 2d6ef05

Thanks @reeselevine for testing this.