Command-line crashes when using nativez3

[jad-hamza]

I get this exception when running stainless on any file (e.g. verification/valid/IntSet.scala). There is no crash if I specify smt-z3 or smt-cvc4.

null
java.lang.NullPointerException
        at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1847)
        at java.lang.Runtime.loadLibrary0(Runtime.java:871)
        at java.lang.System.loadLibrary(System.java:1124)
        at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:110)
        at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:49)

Is this a problem on my end?

[samarion]

This looks like the native library in ScalaZ3 can't be loaded for some reason.

Are you running this on linux? Packaging the native library into a jar and then loading it is a pretty big hack and small changes in the OS or JVM implementation can make it fail, unfortunately.

[jad-hamza]

Yes on linux, with openjdk version "1.8.0_242"
I was able to reproduce the error on a fresh installation of stainless on my machine, but not on larabot where it works well (with java version "1.8.0_201")

[samarion]

Can you try running the ScalaZ3 tests on your machine? If they work, then the easiest "fix" is to run package in ScalaZ3 and copy the resulting jars to your unmanaged directory in Stainless (IIRC you'll have to rename them according to the existing jars in the directory).

I remember that when building and packaging the ScalaZ3 jars on my own machine, they wouldn't work on laraquad but the reverse did work. So maybe it's just a question of finding a "most common architecture" that will allow running on arbitrary machines.

[jad-hamza]

I tried the ScalaZ3 tests but they failed with the same kind of errors. On the other hand, the original problem goes away when using Java 11. Should we close this issue?

[samarion]

Rather than just closing it, maybe move it to the ScalaZ3 repo (in case someone else runs into this at some later time).

[jad-hamza]

Yes, good idea: see epfl-lara/ScalaZ3#76