[BUG] How to replace z3-turnkey with z3 installed via a package manager?

[lemmy]

Note that "aarch64" = "arm64".

(Please report an issue at: [https://github.com/informalsystems/apalache/issues],java.lang.UnsatisfiedLinkError: Unsupported CPU architecture: aarch64)
Unhandled exception                                               E@18:44:42.428
java.lang.UnsatisfiedLinkError: Unsupported CPU architecture: aarch64
	at com.microsoft.z3.Z3Loader$CPUArchitecture.identify(Z3Loader.java:183)
	at com.microsoft.z3.Z3Loader.loadZ3(Z3Loader.java:57)
	at com.microsoft.z3.Native.<clinit>(Native.java:36)
	at com.microsoft.z3.Global.setParameter(Global.java:47)
	at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.$anonfun$new$1(Z3SolverContext.scala:41)
	at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.$anonfun$new$1$adapted(Z3SolverContext.scala:40)
	at scala.collection.immutable.List.foreach(List.scala:431)
	at at.forsyte.apalache.tla.bmcmt.smt.Z3SolverContext.<init>(Z3SolverContext.scala:40)
	at at.forsyte.apalache.tla.bmcmt.smt.RecordingSolverContext$.createZ3(RecordingSolverContext.scala:20)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.runIncrementalChecker(BoundedCheckerPassImpl.scala:105)
	at at.forsyte.apalache.tla.bmcmt.passes.BoundedCheckerPassImpl.execute(BoundedCheckerPassImpl.scala:96)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.exec$1(PassChainExecutor.scala:22)
	at at.forsyte.apalache.infra.passes.PassChainExecutor.run(PassChainExecutor.scala:37)
	at at.forsyte.apalache.tla.Tool$.runCheck(Tool.scala:184)
	at at.forsyte.apalache.tla.Tool$.$anonfun$run$3(Tool.scala:95)
	at at.forsyte.apalache.tla.Tool$.handleExceptions(Tool.scala:319)
	at at.forsyte.apalache.tla.Tool$.run(Tool.scala:95)
	at at.forsyte.apalache.tla.Tool$.main(Tool.scala:45)
	at at.forsyte.apalache.tla.Tool.main(Tool.scala)

root@sv-c2-large-arm-01:~/ewd998# dpkg -l|grep z3
ii  libz3-4:arm64                        4.8.7-4build1                     arm64        theorem prover from Microsoft Research - runtime libraries
ii  libz3-dev:arm64                      4.8.7-4build1                     arm64        theorem prover from Microsoft Research - development files
ii  libz3-java                           4.8.7-4build1                     arm64        theorem prover from Microsoft Research - java bindings
ii  libz3-jni:arm64                      4.8.7-4build1                     arm64        theorem prover from Microsoft Research - JNI library
ii  z3                                   4.8.7-4build1                     arm64        theorem prover from Microsoft Research

[shonfeder]

afaik, we've never supported integration with existing z3 installations. Instead, it was previously required to build z3 from source as part of the build for this project.

We might target this, but tbh I don't know off hand what the best strategy is here.

Could you please include your systems specs, @lemmy?

[lemmy]

Fundamentally, I don't care where z3 is coming from.

root@sv-c2-large-arm-01:~/# uname -a
Linux sv-c2-large-arm-01 5.4.0-40-generic #44-Ubuntu SMP Mon Jun 22 23:59:48 UTC 2020 aarch64 aarch64 aarch64 GNU/Linux
root@sv-c2-large-arm-01:~# free -m
              total        used        free      shared  buff/cache   available
Mem:         128290       69394       29313           9       29583       57738
Swap:          4578           0        4578
root@sv-c2-large-arm-01:~/# cat /proc/cpuinfo | tail -20
CPU revision	: 2

processor	: 30
BogoMIPS	: 90.00
Features	: fp asimd evtstrm aes pmull sha1 sha2 crc32 cpuid
CPU implementer	: 0x50
CPU architecture: 8
CPU variant	: 0x3
CPU part	: 0x000
CPU revision	: 2

processor	: 31
BogoMIPS	: 90.00
Features	: fp asimd evtstrm aes pmull sha1 sha2 crc32 cpuid
CPU implementer	: 0x50
CPU architecture: 8
CPU variant	: 0x3
CPU part	: 0x000
CPU revision	: 2

From https://metal.equinix.com/developers/docs/servers/server-specs/#arm-servers

[konnov]

Fundamentally, I don't care where z3 is coming from.

We have to care, as the z3 team is breaking their APIs from time to time.

[konnov]

I am not sure what to do about it. It does not look like a high priority issue. Do you need it for an installation in an AWS instance?

[lemmy]

The z3 loader doesn't know about aarch64 but seems to just copy the libraries to some location from where Java picks it up. For those that run into this problem: I would assume one could load ("linear classpath") a custom implementation of com.microsoft.z3.Z3Loader that does the right thing on aarch64.

[thpani]

I've requested support for aarch64 from upstream in tudo-aqua/z3-turnkey#12. See also #751.

[shonfeder]

We've also just discussed internally about the possibility of adding an option to our build configuration that would allow using the system Z3 instead of z3-turnkey. I'll plan to investigate.

[thpani]

#1718 introduced support for aarch64

Given our heavy reliance on Z3, targeting an arbitrary-version, system-level Z3 is difficult and currently not planned.