java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path #93

NicolasRouquette · 2015-04-28T17:45:09Z

I built leon on my machine (MacOSX Yosemite, 10.10.3)
I see that the leon script includes in the SCALACLASSPATH.
To make it easier to see what's going on, I edited the leon script like this:

#!/bin/bash --posix

LEON=/Users/rouquett/git.leon/leon
IVY_CACHE=/Users/rouquett/.ivy2/cache

SCALACLASSPATH="$LEON/src/main/resources"
SCALACLASSPATH="$SCALACLASSPATH:$LEON/target/scala-2.11/classes"
SCALACLASSPATH="$SCALACLASSPATH:/Users/rouquett/.sbt/0.13/staging/572f4374f25249fa2000/bonsai/target/scala-2.11/classes"
SCALACLASSPATH="$SCALACLASSPATH:/Users/rouquett/.sbt/0.13/staging/4b46b695466923d859a4/scala-smtlib/target/scala-2.11/classes" 
SCALACLASSPATH="$SCALACLASSPATH:$LEON/unmanaged/64/cafebabe_2.11-1.2.jar" 
SCALACLASSPATH="$SCALACLASSPATH:$LEON/unmanaged/64/scalaz3-unix-64b-2.1.jar"
SCALACLASSPATH="$SCALACLASSPATH:$LEON/unmanaged/64/vanuatoo_2.11-0.1.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang/scala-compiler/jars/scala-compiler-2.11.6.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang/scala-library/jars/scala-library-2.11.6.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang/scala-reflect/jars/scala-reflect-2.11.6.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang.modules/scala-xml_2.11/bundles/scala-xml_2.11-1.0.3.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/org.scala-lang.modules/scala-parser-combinators_2.11/bundles/scala-parser-combinators_2.11-1.0.3.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/com.typesafe.akka/akka-actor_2.11/jars/akka-actor_2.11-2.3.4.jar"
SCALACLASSPATH="$SCALACLASSPATH:$IVY_CACHE/com.typesafe/config/bundles/config-1.2.1.jar"

java -Xmx2G -Xms512M -classpath ${SCALACLASSPATH} -Dscala.usejavacp=false scala.tools.nsc.MainGenericRunner -classpath ${SCALACLASSPATH} leon.Main $@ 2>&1 | tee -i last.log

Then I get this:

[504] $ ./leon.sh  ./testcases/verification/sas2011-testcases/RedBlackTree.scala
java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path
    at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1865)
    at java.lang.Runtime.loadLibrary0(Runtime.java:870)
    at java.lang.System.loadLibrary(System.java:1122)
    at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:97)
    at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:47)
    at z3.scala.Z3Config.<init>(Z3Config.scala:6)
    at leon.solvers.z3.FairZ3Solver.<init>(FairZ3Solver.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1$$anon$1.<init>(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1.apply(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anonfun$leon$solvers$SolverFactory$$getSolver$1$1.apply(SolverFactory.scala:50)
    at leon.solvers.SolverFactory$$anon$12.getNewSolver(SolverFactory.scala:18)
    at leon.verification.AnalysisPhase$.checkVC(AnalysisPhase.scala:129)
    at leon.verification.AnalysisPhase$$anonfun$10.apply(AnalysisPhase.scala:111)
    at leon.verification.AnalysisPhase$$anonfun$10.apply(AnalysisPhase.scala:110)
    at scala.collection.TraversableLike$WithFilter$$anonfun$map$2.apply(TraversableLike.scala:728)
    at scala.collection.immutable.List.foreach(List.scala:381)
    at scala.collection.TraversableLike$WithFilter.map(TraversableLike.scala:727)
    at leon.verification.AnalysisPhase$.checkVCs(AnalysisPhase.scala:110)
    at leon.verification.AnalysisPhase$.run(AnalysisPhase.scala:45)
    at leon.verification.AnalysisPhase$.run(AnalysisPhase.scala:15)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Pipeline$$anon$1.run(Pipeline.scala:12)
    at leon.Main$.execute(Main.scala:236)
    at leon.Main$.main(Main.scala:220)
    at leon.Main.main(Main.scala)
    at sun.reflect.NativeMethodAccessorImpl.invoke0(Native Method)
    at sun.reflect.NativeMethodAccessorImpl.invoke(NativeMethodAccessorImpl.java:62)
    at sun.reflect.DelegatingMethodAccessorImpl.invoke(DelegatingMethodAccessorImpl.java:43)
    at java.lang.reflect.Method.invoke(Method.java:497)
    at scala.reflect.internal.util.ScalaClassLoader$$anonfun$run$1.apply(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$class.asContext(ScalaClassLoader.scala:31)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.asContext(ScalaClassLoader.scala:101)
    at scala.reflect.internal.util.ScalaClassLoader$class.run(ScalaClassLoader.scala:70)
    at scala.reflect.internal.util.ScalaClassLoader$URLClassLoader.run(ScalaClassLoader.scala:101)
    at scala.tools.nsc.CommonRunner$class.run(ObjectRunner.scala:22)
    at scala.tools.nsc.ObjectRunner$.run(ObjectRunner.scala:39)
    at scala.tools.nsc.CommonRunner$class.runAndCatch(ObjectRunner.scala:29)
    at scala.tools.nsc.ObjectRunner$.runAndCatch(ObjectRunner.scala:39)
    at scala.tools.nsc.MainGenericRunner.runTarget$1(MainGenericRunner.scala:65)
    at scala.tools.nsc.MainGenericRunner.run$1(MainGenericRunner.scala:87)
    at scala.tools.nsc.MainGenericRunner.process(MainGenericRunner.scala:98)
    at scala.tools.nsc.MainGenericRunner$.main(MainGenericRunner.scala:103)
    at scala.tools.nsc.MainGenericRunner.main(MainGenericRunner.scala)

Suggestions?

Nicolas.

regb · 2015-04-29T09:33:10Z

This is not a solution to the build problem, but you can run Leon without using the ScalaZ3 library. You need to install Z3 and add the z3 binary to the PATH. Then you can run:

./leon --solvers=smt-z3 INPUT

romac · 2015-04-29T13:29:59Z

I ran into the same error a few times, and haven't found a better workaround than the one given by @colder in epfl-lara/ScalaZ3#40, specifically: epfl-lara/ScalaZ3#40 (comment).

tl;dr:

Make sure you have the ScalaZ3 JAR in unmanaged/64/ and run:

$ rm -rf $TMPDIR/SCALAZ3_*
$ scala -Dscalaz3.debug.load=1 -cp unmanaged/64/scalaz3-osx-64b-2.1.1.jar
scala> new z3.Z3Wrapper
Loading scalaz3
res0: z3.Z3Wrapper = z3.Z3Wrapper@766f9a7e

Note that you don't have to build ScalaZ3 yourself, just grab the appropriate .jar from https://github.com/epfl-lara/ScalaZ3/releases, put it in umanaged/64/, and re-run sbt script.

NicolasRouquette · 2015-04-29T15:43:38Z

Thanks @romac for the suggestion.

I downloaded the latest ScalaZ3 and ran the command you suggested:

$ scala -Dscalaz3.debug.load=1 -cp unmanaged/64/scalaz3-osx-64b-2.1.1.jar
Welcome to Scala version 2.11.6 (Java HotSpot(TM) 64-Bit Server VM, Java 1.8.0_45).
Type in expressions to have them evaluated.
Type :help for more information.

scala> new z3.Z3Wrapper
Extracting lib-bin/libscalaz3.dylib from jar to libscalaz3.dylib...
Extracting lib-bin/libz3.dylib from jar to libz3.dylib...
Loading scalaz3
java.lang.UnsatisfiedLinkError: /private/var/folders/kx/f_xzx22x2hx6vypyfgg8xk4c0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib: dlopen(/private/var/folders/kx/f_xzx22x2hx6vypyfgg8xk4c0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib, 1): Library not loaded: /usr/local/lib/gcc/x86_64-apple-darwin13.2.0/4.8.2/libgomp.1.dylib
  Referenced from: /private/var/folders/kx/f_xzx22x2hx6vypyfgg8xk4c0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib
  Reason: image not found
  at java.lang.ClassLoader$NativeLibrary.load(Native Method)
  at java.lang.ClassLoader.loadLibrary0(ClassLoader.java:1937)
  at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1855)
  at java.lang.Runtime.loadLibrary0(Runtime.java:870)
  at java.lang.System.loadLibrary(System.java:1122)
  at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:97)
  at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:47)
  ... 33 elided

scala>

Indeed, I don't have this gomp library.

This is as far as I got trying to build ScalaZ3 locally as described here:
https://stackoverflow.com/questions/29927823/how-to-build-leon-for-macosx

The workaround @regb described worked for me with smt-z3 (based on the Z3 I built on my machine) and with the most recent development version of CVC4 (per Victor's suggestion)

colder · 2015-05-05T12:35:25Z

Instructions for building the native z3 interface on OS-X should come soon. In the mean time, I implemented a fix in 8674964 that falls back to SMT-based solvers in case the native API is unavailable.

mantognini · 2016-12-05T21:20:30Z

A long time has past and many things changed; it is now possible to use ScalaZ3 with Leon (epfl-lara/ScalaZ3#50). This issue should be re-inspected and probably closed.

NicolasRouquette · 2017-02-26T02:53:59Z

Indeed; they have. I built a fresh clone of leon 3.0 today and followed the instructions.

For MacOSX, assuming that:
./leon points to the clone of Leon itself
./ScalaZ3 points the clone of https://github.com/epfl-lara/ScalaZ3,

then I suggest explaining the following:

build ScalaZ3; which should produce ./ScalaZ3/target/scala-2.11/scalaz3_2.11-3.0.jar
replace ./leon/unmanaged/scalaz3-unix-64.jar (this is for x86-64 linux; not macos):

In ./leon:

cp ../ScalaZ3/target/scala-2.11/scalaz3_2.11-3.0.jar ./leon/unmanaged/scalaz3-unix-64.jar
sbt clean compile script
./leon

Works for me (i.e., it shows that it used the Z3 native library, Z3-f).

colder added the enhancement label May 29, 2015

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path #93

java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path #93

NicolasRouquette commented Apr 28, 2015

regb commented Apr 29, 2015

romac commented Apr 29, 2015

NicolasRouquette commented Apr 29, 2015

colder commented May 5, 2015

mantognini commented Dec 5, 2016

NicolasRouquette commented Feb 26, 2017

java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path #93

java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path #93

Comments

NicolasRouquette commented Apr 28, 2015

regb commented Apr 29, 2015

romac commented Apr 29, 2015

NicolasRouquette commented Apr 29, 2015

colder commented May 5, 2015

mantognini commented Dec 5, 2016

NicolasRouquette commented Feb 26, 2017