epfl-lara / ScalaZ3

DSL in Scala for Constraint Solving with Z3 SMT Solver
Apache License 2.0
122 stars 34 forks source link

`sbt test` fails with NullPointerException when loading jar #76

Open jad-hamza opened 4 years ago

jad-hamza commented 4 years ago

Using Java version openjdk version "1.8.0_242" on Debian, I get this error:

[info] ForComprehension:
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)
        at z3.scala.Z3Context.<init>(Z3Context.scala:23)
        at z3.scala.Z3Context.<init>(Z3Context.scala:45)
        at z3.scala.dsl.package$.findAll(package.scala:245)
        at z3.scala.ForComprehension.$anonfun$new$1(ForComprehension.scala:14)
        at org.scalatest.OutcomeOf.outcomeOf(OutcomeOf.scala:85)
        at org.scalatest.OutcomeOf.outcomeOf$(OutcomeOf.scala:83)
        at org.scalatest.OutcomeOf$.outcomeOf(OutcomeOf.scala:104)
        at org.scalatest.Transformer.apply(Transformer.scala:22)
        at org.scalatest.Transformer.apply(Transformer.scala:20)
        at org.scalatest.FunSuiteLike$$anon$1.apply(FunSuiteLike.scala:186)
        at org.scalatest.TestSuite.withFixture(TestSuite.scala:196)
        at org.scalatest.TestSuite.withFixture$(TestSuite.scala:195)
        at org.scalatest.FunSuite.withFixture(FunSuite.scala:1560)

The tests work fine with openjdk 11.0.6 2020-01-14.

doofin commented 2 years ago

same error,but with jdk 11 (openjdk 11.0.13) under linux.

B10615053 commented 2 years ago

Got NullPointerException and failed all test. :cry:

[info] Run completed in 729 milliseconds.
[info] Total number of tests run: 0
[info] Suites: completed 0, aborted 13
[info] Tests: succeeded 0, failed 0, canceled 0, ignored 0, pending 0
[info] *** 13 SUITES ABORTED ***
[error] Error during tests:
[error]     z3.scala.ForComprehension
[error]     z3.scala.Quantifiers
[error]     z3.scala.Calendar
[error]     z3.scala.Sets
[error]     z3.scala.ADTs
[error]     z3.scala.SatSolver
[error]     z3.scala.Abs
[error]     z3.scala.Core
[error]     z3.scala.Arrays
[error]     z3.scala.NQueens
[error]     z3.scala.Optimizer
[error]     z3.scala.IntArith
[error]     z3.scala.Sequences
[error] (Test / test) sbt.TestsFailedException: Tests unsuccessful

Build with sbt 1.5.8, and openjdk 11.0.16 2022-07-19 under Ubuntu 20.04.5 LTS.