Viper on macOS arm64

[fpoli]

I think that the Viper IDE cannot work on macOS with an arm64 chip (M1) because the Viper releases currently ships the x64 version of Z3. We could consider releasing a ViperToolsMac-arm64.zip that uses e.g. z3-4.11.2-arm64-osx-11.0.zip. However, the arm64 build of Z3 is only available for recent Z3 versions.

[fpoli]

We got reports saying that the x86_64 version of z3 works fine, but it's not clear if it's slower than a z3 compiled for arm64. If someone can evaluate this (comparing the same z3 version compiled for different architectures but all running on M1) it would be great.

[ArquintL]

This is the z3 binary compiled on an ARM MacBook Pro (actually M2 but that shouldn't matter):
z3_4.8.6_macOS_arm.zip

[fpoli]

What allows to run x86 binaries on macOS arm64 is called Rosetta 2, a dynamic binary translator. As expected, some benchmarks show that it's worse than directly running a native arm64 binary.

[ArquintL]

Very interesting, thanks for sharing!

[JonasAlaif]

Fixed by my latest changes, the prebuilt z3-arm64 lives here and that same repo also builds Boogie for arm64. If we ever update to a newer z3 then we can use the prebuilt images for arm64 that they now provide

[fpoli]

Does the Viper IDE detect the architecture in order to download ViperToolsMacARM.zip instead of ViperToolsMac.zip?

[fpoli]

Oh, I just noticed the latest commits. Nice!