NoClassDefFoundError in all tests

[folone]

Hello,

I'm having a problem with the final step of the installation guide. Packaging seems to work correclty (at least I don't see any errors):

> package
[info] Generating library checksum
[info] Generating library checksum
[info] Wrote checksum 61f7962552d79e96a73fe47615a6b35d as part of /Users/georgii/workspace/scalogno/ScalaZ3/src/main/java/z3/LibraryChecksum.java.
[info] Wrote checksum 61f7962552d79e96a73fe47615a6b35d as part of /Users/georgii/workspace/scalogno/ScalaZ3/src/main/java/z3/LibraryChecksum.java.
[info] Compiling C sources ...
[info] $ install_name_tool -id @loader_path/libz3.dylib /Users/georgii/workspace/scalogno/ScalaZ3/z3/4.3-osx-64b/lib/libz3.dylib
[info] $ gcc -o /Users/georgii/workspace/scalogno/ScalaZ3/lib-bin/libscalaz3.dylib -dynamiclib -install_name /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib -I/Library/Java/JavaVirtualMachines/jdk1.7.0_51.jdk/Contents/Home/jre/../include -I/System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers -I/Users/georgii/workspace/scalogno/ScalaZ3/z3/4.3-osx-64b/include -L/Users/georgii/workspace/scalogno/ScalaZ3/z3/4.3-osx-64b/lib -g -lc -Wl,-rpath,/var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/ -lz3 -fPIC -O2 -fopenmp /Users/georgii/workspace/scalogno/ScalaZ3/src/c/casts.c /Users/georgii/workspace/scalogno/ScalaZ3/src/c/extra.c /Users/georgii/workspace/scalogno/ScalaZ3/src/c/z3_thycallbacks.c /Users/georgii/workspace/scalogno/ScalaZ3/src/c/z3_Z3Wrapper.c
[info] Updating {file:/Users/georgii/workspace/scalogno/ScalaZ3/}ScalaZ3...
[info] Resolving org.fusesource.jansi#jansi;1.4 ...
[info] Done updating.
[info] Compiling 29 Scala sources and 14 Java sources to /Users/georgii/workspace/scalogno/ScalaZ3/target/scala-2.10/classes...
[info] Preparing JNI headers...
[info] $ javah -classpath /Users/georgii/workspace/scalogno/ScalaZ3/target/scala-2.10/classes:/Users/georgii/.sbt/boot/scala-2.10.2/lib/scala-library.jar -d /Users/georgii/workspace/scalogno/ScalaZ3/src/c z3.Z3Wrapper
[info] Bundling files:
[info]  - /Users/georgii/workspace/scalogno/ScalaZ3/lib-bin/libscalaz3.dylib -> lib-bin/libscalaz3.dylib
[info]  - /Users/georgii/workspace/scalogno/ScalaZ3/z3/4.3-osx-64b/lib/libz3.dylib -> lib-bin/libz3.dylib
[info] Packaging /Users/georgii/workspace/scalogno/ScalaZ3/target/scala-2.10/scalaz3_2.10-2.1.jar ...
[info] Done packaging.
[success] Total time: 19 s, completed Jun 13, 2014 12:54:05 PM

But then tests don't work at all:

> test
[info] Compiling 10 Scala sources to /Users/georgii/workspace/scalogno/ScalaZ3/target/scala-2.10/test-classes...
[warn] /Users/georgii/workspace/scalogno/ScalaZ3/src/test/scala/z3/scala/ADTs.scala:111: method delete in class Z3Model is deprecated: Z3Model.delete() not be used, use incref/decref instead
[warn]     model.delete
[warn]           ^
[warn] /Users/georgii/workspace/scalogno/ScalaZ3/src/test/scala/z3/scala/IntArith.scala:43: method delete in class Z3Model is deprecated: Z3Model.delete() not be used, use incref/decref instead
[warn]     model.delete
[warn]           ^
[warn] two warnings found
[info] Sets:
[error] Uncaught exception when running z3.Sets: java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path
[trace] Stack trace suppressed: run last test:test for the full output.
[info] ForComprehension:
[error] Uncaught exception when running z3.ForComprehension: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] Calendar:
[error] Uncaught exception when running z3.Calendar: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] SatSolver:
[error] Uncaught exception when running z3.SatSolver: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] ADTs:
[error] Uncaught exception when running z3.ADTs: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] Core:
[error] Uncaught exception when running z3.Core: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] Quantifiers:
[error] Uncaught exception when running z3.Quantifiers: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] IntArith:
[error] Uncaught exception when running z3.IntArith: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] NQueens:
[error] Uncaught exception when running z3.NQueens: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[info] Arrays:
[error] Uncaught exception when running z3.Arrays: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
[trace] Stack trace suppressed: run last test:test for the full output.
[error] Error: Total 10, Failed 0, Errors 10, Passed 0
[error] Error during tests:
[error]     z3.Core
[error]     z3.NQueens
[error]     z3.Quantifiers
[error]     z3.Arrays
[error]     z3.Sets
[error]     z3.ForComprehension
[error]     z3.ADTs
[error]     z3.Calendar
[error]     z3.SatSolver
[error]     z3.IntArith
[error] (test:test) sbt.TestsFailedException: Tests unsuccessful
[error] Total time: 7 s, completed Jun 13, 2014 12:54:47 PM

Exceptions are all same, here's one of them:

[error] Uncaught exception when running z3.Arrays: java.lang.NoClassDefFoundError: Could not initialize class z3.Z3Wrapper
sbt.ForkMain$ForkError: Could not initialize class z3.Z3Wrapper
    at z3.scala.Z3Config.<init>(Z3Config.scala:6)
    at z3.scala.Z3Context.<init>(Z3Context.scala:31)
    at z3.Arrays$$anonfun$1.apply$mcV$sp(Arrays.scala:10)
    at z3.Arrays$$anonfun$1.apply(Arrays.scala:9)
    at z3.Arrays$$anonfun$1.apply(Arrays.scala:9)
    at org.scalatest.FunSuite$$anon$1.apply(FunSuite.scala:1265)
    at org.scalatest.Suite$class.withFixture(Suite.scala:1974)
    at z3.Arrays.withFixture(Arrays.scala:6)
    at org.scalatest.FunSuite$class.invokeWithFixture$1(FunSuite.scala:1262)
    at org.scalatest.FunSuite$$anonfun$runTest$1.apply(FunSuite.scala:1271)
    at org.scalatest.FunSuite$$anonfun$runTest$1.apply(FunSuite.scala:1271)
    at org.scalatest.SuperEngine.runTestImpl(Engine.scala:198)
    at org.scalatest.FunSuite$class.runTest(FunSuite.scala:1271)
    at z3.Arrays.runTest(Arrays.scala:6)
    at org.scalatest.FunSuite$$anonfun$runTests$1.apply(FunSuite.scala:1304)
    at org.scalatest.FunSuite$$anonfun$runTests$1.apply(FunSuite.scala:1304)
    at org.scalatest.SuperEngine$$anonfun$org$scalatest$SuperEngine$$runTestsInBranch$1.apply(Engine.scala:260)
    at org.scalatest.SuperEngine$$anonfun$org$scalatest$SuperEngine$$runTestsInBranch$1.apply(Engine.scala:249)
    at scala.collection.immutable.List.foreach(List.scala:318)
    at org.scalatest.SuperEngine.org$scalatest$SuperEngine$$runTestsInBranch(Engine.scala:249)
    at org.scalatest.SuperEngine.runTestsImpl(Engine.scala:326)
    at org.scalatest.FunSuite$class.runTests(FunSuite.scala:1304)
    at z3.Arrays.runTests(Arrays.scala:6)
    at org.scalatest.Suite$class.run(Suite.scala:2303)
    at z3.Arrays.org$scalatest$FunSuite$$super$run(Arrays.scala:6)
    at org.scalatest.FunSuite$$anonfun$run$1.apply(FunSuite.scala:1310)
    at org.scalatest.FunSuite$$anonfun$run$1.apply(FunSuite.scala:1310)
    at org.scalatest.SuperEngine.runImpl(Engine.scala:362)
    at org.scalatest.FunSuite$class.run(FunSuite.scala:1310)
    at z3.Arrays.run(Arrays.scala:6)
    at org.scalatest.tools.ScalaTestFramework$ScalaTestRunner.run(ScalaTestFramework.scala:214)
    at sbt.RunnerWrapper$1.runRunner2(FrameworkWrapper.java:220)
    at sbt.RunnerWrapper$1.execute(FrameworkWrapper.java:233)
    at sbt.ForkMain$Run.runTest(ForkMain.java:239)
    at sbt.ForkMain$Run.runTestSafe(ForkMain.java:211)
    at sbt.ForkMain$Run.runTests(ForkMain.java:187)
    at sbt.ForkMain$Run.run(ForkMain.java:251)
    at sbt.ForkMain.main(ForkMain.java:97)

Any help really appreciated!

[colder]

Which version of mac osx are you using ?

[folone]

10.9.3, gcc version is:

$ gcc --version
gcc (Homebrew gcc 4.8.3_1) 4.8.3
Copyright (C) 2013 Free Software Foundation, Inc.
This is free software; see the source for copying conditions.  There is NO
warranty; not even for MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.

[colder]

Can you try doing:

$ scala -cp path/to/scalaz3.jar
scala> new z3.scala.Z3Context

You should be getting an error, but I would be interested in what this error will be. Can you also do the same with the released osx jar?

[folone]

The error is:

scala> new z3.scala.Z3Context
java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path
  at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1886)
  at java.lang.Runtime.loadLibrary0(Runtime.java:849)
  at java.lang.System.loadLibrary(System.java:1088)
  at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:97)
  at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:47)
  at z3.scala.Z3Config.<init>(Z3Config.scala:6)
  at z3.scala.Z3Context.<init>(Z3Context.scala:31)
  ... 32 elided

Where can I find the released osx jar?

[colder]

It can be found under "Releases":

https://github.com/epfl-lara/ScalaZ3/releases

[folone]

Oh, thanks. Same error:

$ scala -cp scalaz3-osx-64b-2.1.1.jar
Welcome to Scala version 2.11.1 (Java HotSpot(TM) 64-Bit Server VM, Java 1.7.0_51).
Type in expressions to have them evaluated.
Type :help for more information.

scala> new z3.scala.Z3Context
java.lang.UnsatisfiedLinkError: no scalaz3 in java.library.path
  at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1886)
  at java.lang.Runtime.loadLibrary0(Runtime.java:849)
  at java.lang.System.loadLibrary(System.java:1088)
  at z3.Z3Wrapper.loadFromJar(Z3Wrapper.java:97)
  at z3.Z3Wrapper.<clinit>(Z3Wrapper.java:47)
  at z3.scala.Z3Config.<init>(Z3Config.scala:6)
  at z3.scala.Z3Context.<init>(Z3Context.scala:31)
  ... 32 elided

[koksal]

We actually just noticed that OS X has user-specific temporary folders, which could explain why the jar release doesn't work. However this doesn't tell us why the library cannot be found when you package the tool yourself. From your error messages, I see that both libraries (libscalaz3.dylib and libz3.dylib) should be extracted into /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/ on your computer. Is this indeed the case?

[folone]

@koksal Looks like it is not there. I've tried to re-run sbt package, and look into the directory it mentions in -install_name flag, empty:

$ ls /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/
ls: /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/: No such file or directory

[colder]

What happens is that SBT will in advance get the tpmdir so that it can predict where the dylibs will be extracted to when first executing the jar.

Can you make sure the tmpdir obtained within SBT (apparent in the commands it outputs), is the same than the runtime one you obtain using

$ scala -e 'println(System.getProperty("java.io.tmpdir"));'

[folone]

Seems to be the same directory. Here's the gcc command that sbt performs: $ gcc -o /Users/georgii/workspace/ScalaZ3/lib-bin/libscalaz3.dylib -dynamiclib -install_name /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/libscalaz3.dylib -I/Library/Java/JavaVirtualMachines/jdk1.7.0_51.jdk/Contents/Home/jre/../include -I/System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers -I/Users/georgii/workspace/ScalaZ3/z3/4.3-osx-64b/include -L/Users/georgii/workspace/ScalaZ3/z3/4.3-osx-64b/lib -g -lc -Wl,-rpath,/var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_61f7962552d79e96a73fe47615a6b35d/lib-bin/ -lz3 -fPIC -O2 -fopenmp /Users/georgii/workspace/ScalaZ3/src/c/casts.c /Users/georgii/workspace/ScalaZ3/src/c/extra.c /Users/georgii/workspace/ScalaZ3/src/c/z3_thycallbacks.c /Users/georgii/workspace/ScalaZ3/src/c/z3_Z3Wrapper.c Here's result of checking the tmpdir:

$ scala -e 'println(System.getProperty("java.io.tmpdir"));'
/var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/

[colder]

Here is a few steps to try:

1) delete everything scalaz3 might have extracted so far:

rm -rf /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_*

2) run

$ scala -Dscalaz3.debug.load=1 -cp path/to/built/scalaz3.jar
scala> new z3.Z3Wrapper

you should then see something looking like:

Extracting lib-bin/libz3.dylib from jar to libz3.dylib...
Extracting lib-bin/libscalaz3.dylib from jar to libscalaz3.dylib...
Loading scalaz3
<the error>

3) check the content of the extracted dir:

$ ls -alR /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_*

[folone]

I'm really confused right now: somehow it just started working. I don't really know what I did. The only thing I recall was rebooting. I'm getting a persistent segfault in Calendar test (everything passes if I disable it), but tests don't fail with the old linkage error any more.

$ rm -rf /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_*
zsh: no matches found: /var/folders/0b/7l03y9g17rldj97z8_ygqgmc0000gp/T/SCALAZ3_*
$ scala -Dscalaz3.debug.load=1 -cp target/scala-2.10/scalaz3_2.10-2.1.jar
Welcome to Scala version 2.11.1 (Java HotSpot(TM) 64-Bit Server VM, Java 1.7.0_51).
Type in expressions to have them evaluated.
Type :help for more information.

scala> new z3.Z3Wrapper
Extracting lib-bin/libz3.dylib from jar to libz3.dylib...
Extracting lib-bin/libscalaz3.dylib from jar to libscalaz3.dylib...
Loading scalaz3
res0: z3.Z3Wrapper = z3.Z3Wrapper@2c19cee5

scala> :q
$ sbt
[info] Loading project definition from /Users/georgii/workspace/ScalaZ3/project
[info] Compiling 1 Scala source to /Users/georgii/workspace/ScalaZ3/project/target/scala-2.10/sbt-0.13/classes...
[info] Set current project to ScalaZ3 (in build file:/Users/georgii/workspace/ScalaZ3/)
> test
[info] Compiling 10 Scala sources to /Users/georgii/workspace/ScalaZ3/target/scala-2.10/test-classes...
[warn] /Users/georgii/workspace/ScalaZ3/src/test/scala/z3/scala/ADTs.scala:111: method delete in class Z3Model is deprecated: Z3Model.delete() not be used, use incref/decref instead
[warn]     model.delete
[warn]           ^
[warn] /Users/georgii/workspace/ScalaZ3/src/test/scala/z3/scala/IntArith.scala:43: method delete in class Z3Model is deprecated: Z3Model.delete() not be used, use incref/decref instead
[warn]     model.delete
[warn]           ^
[warn] two warnings found
[info] NQueens:
[info] - NQueens
[info] IntArith:
[info] - Comfusy-like
[info] Core:
[info] - Core
[info] ForComprehension:
[info] - ForComprehension
[info] Quantifiers:
[info] - Quantifiers
[info] SatSolver:
[info] - Sat solver
[info] Arrays:
[info] - Arrays
[info] ADTs:
[info] - ADTs
[info] Sets:
[info] - Sets
[info] Calendar:
#
# A fatal error has been detected by the Java Runtime Environment:
#
#  SIGSEGV (0xb) at pc=0x000000011ddad5d5, pid=11224, tid=6403
#
# JRE version: Java(TM) SE Runtime Environment (7.0_51-b13) (build 1.7.0_51-b13)
# Java VM: Java HotSpot(TM) 64-Bit Server VM (24.51-b03 mixed mode bsd-amd64 compressed oops)
# Problematic frame:
# C  [libz3.dylib+0x9f45d5]  mpz_manager<true>::gcd(mpz const&, mpz const&, mpz&)+0x125
#
# Failed to write core dump. Core dumps have been disabled. To enable core dumping, try "ulimit -c unlimited" before starting Java again
#
# An error report file with more information is saved as:
# /Users/georgii/workspace/ScalaZ3/hs_err_pid11224.log
#
# If you would like to submit a bug report, please visit:
#   http://bugreport.sun.com/bugreport/crash.jsp
# The crash happened outside the Java Virtual Machine in native code.
# See problematic frame for where to report the bug.
#
Exception in thread "Thread-1" java.io.EOFException
    at java.io.ObjectInputStream$BlockDataInputStream.peekByte(ObjectInputStream.java:2598)
    at java.io.ObjectInputStream.readObject0(ObjectInputStream.java:1318)
    at java.io.ObjectInputStream.readObject(ObjectInputStream.java:370)
    at sbt.React.react(ForkTests.scala:110)
    at sbt.ForkTests$$anonfun$mainTestTask$1$Acceptor$2$.run(ForkTests.scala:69)
    at java.lang.Thread.run(Thread.java:744)
[error] Error: Total 0, Failed 0, Errors 0, Passed 0
[error] Error during tests:
[error]     Running java with options -classpath /Users/georgii/workspace/ScalaZ3/target/scala-2.10/test-classes:/Users/georgii/workspace/ScalaZ3/target/scala-2.10/scalaz3_2.10-2.1.jar:/Users/georgii/.sbt/boot/scala-2.10.2/lib/scala-library.jar:/Users/georgii/.ivy2/cache/org.scalatest/scalatest_2.10/jars/scalatest_2.10-1.9.1.jar:/Users/georgii/.ivy2/cache/org.scala-lang/scala-actors/jars/scala-actors-2.10.0.jar:/Users/georgii/.ivy2/cache/org.scala-lang/scala-reflect/jars/scala-reflect-2.10.0.jar:/Users/georgii/.sbt/boot/scala-2.10.2/org.scala-sbt/sbt/0.13.0/test-agent-0.13.0.jar:/Users/georgii/.sbt/boot/scala-2.10.2/org.scala-sbt/sbt/0.13.0/test-interface-1.0.jar sbt.ForkMain 57368 failed with exit code 134
[error] (test:test) sbt.TestsFailedException: Tests unsuccessful
[error] Total time: 10 s, completed Jun 18, 2014 11:43:32 AM

[colder]

If the SCALAZ3_.. directory exists, it won't extract anything. So if for some obscure reason the extraction initially failed, it will never try again as long as it finds this SCALAZ3 directory. As far as the segfault is concerned, which version of z3 did you download/compile? Latest unstable?

[folone]

Probably that. Thanks a lot for your help with this!