Unable to install jConstraints-z3

[chaofz]

I have followed all the installation descriptions on jConstraints and Z3 but when I type "mvn install" under jconstraints-z3 directory, I get these errors:

[MVNVM] Using maven: 3.3.9
[INFO] Scanning for projects...
[INFO]
[INFO] ------------------------------------------------------------------------
[INFO] Building jConstraints-z3 1.0-SNAPSHOT
[INFO] ------------------------------------------------------------------------
[INFO]
[INFO] --- maven-resources-plugin:2.6:resources (default-resources) @ jConstraints-z3 ---
[INFO] Using 'UTF-8' encoding to copy filtered resources.
[INFO] Copying 1 resource
[INFO]
[INFO] --- maven-compiler-plugin:3.1:compile (default-compile) @ jConstraints-z3 ---
[INFO] Nothing to compile - all classes are up to date
[INFO]
[INFO] --- maven-resources-plugin:2.6:testResources (default-testResources) @ jConstraints-z3 ---
[INFO] Using 'UTF-8' encoding to copy filtered resources.
[INFO] skip non existing resourceDirectory /Users/Chaofeng/jpf/jconstraints-z3/src/test/resources
[INFO]
[INFO] --- maven-compiler-plugin:3.1:testCompile (default-testCompile) @ jConstraints-z3 ---
[INFO] Nothing to compile - all classes are up to date
[INFO]
[INFO] --- maven-surefire-plugin:2.12.4:test (default-test) @ jConstraints-z3 ---
[INFO] Surefire report directory: /Users/Chaofeng/jpf/jconstraints-z3/target/surefire-reports

T E S T S

Running TestSuite
Configuring TestNG with: org.apache.maven.surefire.testng.conf.TestNG652Configurator@c2e1f26
Jun 03, 2016 7:07:44 PM gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory registerProvider
WARNING: Overwriting constraint solver provider with name {0}
Jun 03, 2016 7:07:44 PM gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy createSolver
WARNING: Using deprecated solver name 'NativeZ3' might fail in future releases
((127 & 63) == 'i1')
Jun 03, 2016 7:07:44 PM gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy createSolver
WARNING: Using deprecated solver name 'NativeZ3' might fail in future releases
c1:5.2E-8
c2:1.01E-7
((('i1' + 5.2E-8) * 'i2') > 1.01E-7)
Names: i1 i2
((('int_0' + 5.2E-8) * 'int_1') > 1.01E-7)
(('i1' + 5.2E-8) > 1.01E-7)
Jun 03, 2016 7:07:44 PM gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy createSolver
WARNING: Using deprecated solver name 'NativeZ3' might fail in future releases
Tests run: 8, Failures: 8, Errors: 0, Skipped: 0, Time elapsed: 0.365 sec <<< FAILURE!
testToString(gov.nasa.jpf.constraints.expressions.ContextTest) Time elapsed: 0.041 sec <<< FAILURE!
java.lang.UnsatisfiedLinkError: no libz3java in java.library.path
at java.lang.ClassLoader.loadLibrary(ClassLoader.java:1867)
at java.lang.Runtime.loadLibrary0(Runtime.java:870)
at java.lang.System.loadLibrary(System.java:1122)
at com.microsoft.z3.Native.(Native.java:14)
at com.microsoft.z3.Global.setParameter(Global.java:47)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver.(NativeZ3Solver.java:46)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy.createSolver(NativeZ3SolverProviderLegacy.java:36)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.ContextTest.testToString(ContextTest.java:37)

expressionTest(gov.nasa.jpf.constraints.expressions.ExpressionZ3BVTest) Time elapsed: 0.013 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy.createSolver(NativeZ3SolverProviderLegacy.java:36)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.ExpressionZ3BVTest.expressionTest(ExpressionZ3BVTest.java:69)

expressionTest(gov.nasa.jpf.constraints.expressions.ExpressionZ3Test) Time elapsed: 0.003 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProviderLegacy.createSolver(NativeZ3SolverProviderLegacy.java:36)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.ExpressionZ3Test.expressionTest(ExpressionZ3Test.java:101)

testIntegerFunction(gov.nasa.jpf.constraints.expressions.IntegerTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.IntegerTest.testIntegerFunction(IntegerTest.java:47)

testAtan2(gov.nasa.jpf.constraints.expressions.TrigonometricTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.createContext(TrigonometricTest.java:45)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.testAtan2(TrigonometricTest.java:54)

testCoral1(gov.nasa.jpf.constraints.expressions.TrigonometricTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.createContext(TrigonometricTest.java:45)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.testCoral1(TrigonometricTest.java:132)

testCoral2(gov.nasa.jpf.constraints.expressions.TrigonometricTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.createContext(TrigonometricTest.java:45)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.testCoral2(TrigonometricTest.java:174)

testTrigonometrics(gov.nasa.jpf.constraints.expressions.TrigonometricTest) Time elapsed: 0.001 sec <<< FAILURE!
java.lang.NoClassDefFoundError: Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
at gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3SolverProvider.createSolver(NativeZ3SolverProvider.java:59)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:201)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:216)
at gov.nasa.jpf.constraints.solvers.ConstraintSolverFactory.createSolver(ConstraintSolverFactory.java:221)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.createContext(TrigonometricTest.java:45)
at gov.nasa.jpf.constraints.expressions.TrigonometricTest.testTrigonometrics(TrigonometricTest.java:83)

Results :

Failed tests: testToString(gov.nasa.jpf.constraints.expressions.ContextTest): no libz3java in java.library.path
expressionTest(gov.nasa.jpf.constraints.expressions.ExpressionZ3BVTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
expressionTest(gov.nasa.jpf.constraints.expressions.ExpressionZ3Test): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testIntegerFunction(gov.nasa.jpf.constraints.expressions.IntegerTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testAtan2(gov.nasa.jpf.constraints.expressions.TrigonometricTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testCoral1(gov.nasa.jpf.constraints.expressions.TrigonometricTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testCoral2(gov.nasa.jpf.constraints.expressions.TrigonometricTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver
testTrigonometrics(gov.nasa.jpf.constraints.expressions.TrigonometricTest): Could not initialize class gov.nasa.jpf.constraints.solvers.nativez3.NativeZ3Solver

Tests run: 8, Failures: 8, Errors: 0, Skipped: 0

[INFO] ------------------------------------------------------------------------
[INFO] BUILD FAILURE
[INFO] ------------------------------------------------------------------------
[INFO] Total time: 1.860 s
[INFO] Finished at: 2016-06-03T19:07:44-06:00
[INFO] Final Memory: 10M/220M
[INFO] ------------------------------------------------------------------------
[ERROR] Failed to execute goal org.apache.maven.plugins:maven-surefire-plugin:2.12.4:test (default-test) on project jConstraints-z3: There are test failures.
[ERROR]
[ERROR] Please refer to /Users/Chaofeng/jpf/jconstraints-z3/target/surefire-reports for the individual test results.
[ERROR] -> [Help 1]
[ERROR]
[ERROR] To see the full stack trace of the errors, re-run Maven with the -e switch.
[ERROR] Re-run Maven using the -X switch to enable full debug logging.
[ERROR]
[ERROR] For more information about the errors and possible solutions, please read the following articles:
[ERROR] [Help 1] http://cwiki.apache.org/confluence/display/MAVEN/MojoFailureException

I have followed everything on the manual. After I did some research, I have found someone mentioned a ~/.jconstraints folder which the application hasn't created so far. So, is this issue related to that folder?

[ksluckow]

Hi,

Two things:

1. You get an UnsatisfiedLinkError for libz3. Did you update your LD_LIBRARY_PATH (Linux) or DYLD_LIBRARY_PATH (OS X) with the path to that library? Probably this should be /path/to/z3/build. Alternatively you can set java.library.path.
2. To use jconstraints-z3, you should create ~/.jconstraints/extensions and place the resulting Z3 java bindings (com.microsoft.z3.jar) and jConstraints-z3-[version].jar in that folder.

Hope this helps.

[chaofz]

Hi Kasper,

Thanks for the quick reply.

I didn't get how to set DYLD_LIBRARY_PATH (I am using OS X) before so I think that was why I got this error.

I have built Z3 and I did see libz3.dylib and libz3java.dylib under /Users/Chaofeng/jpf/z3/build. So this time, I added export DYLD_LIBRARY_PATH=/Users/Chaofeng/jpf/z3/build to ~/.bashrc file but I still got UnsatisfiedLinkError

[ksluckow]

Okay, if you happen to be on El Capitan, then things inevitably get ugly: if you want to take the route of setting DYLD_LIBRARY_PATH you will have to disable the System Integrity Protection module---I know, it is a pain.
See, e.g., oracle/node-oracledb#231 and Z3Prover/z3#294 for pointers or other posts on DYLD_LIBRARY_PATH issues on El Capitan. Alternatively, you can put z3lib in a folder that is on the path; presumably ~/lib should work.

Let me know if it works.

[ksluckow]

What I did was to temporarily disable SIP and make a symlink of libz3java.dylib to /usr/local/lib/libz3java.dylib. Afterwards, I re-enabled SIP.
However, a better solution might be to simply add (/symlink) it to a location that is on the library path and that you have write permission to. Presumably, ~/lib is on the library path although I haven't tested it myself.

[chaofz]

I am still on Yosemite :) so I guess it doesn't bother SIP?

I tried to put z3lib in /usr/local/lib and ~/lib but things just don't work out. Am I doing right to set DYLD_LIBRARY_PATH by adding export DYLD_LIBRARY_PATH=/urs/local/lib to ~/.bashrc? Is there any other way to set java.library.path?

Thank you!

[ksluckow]

Yes you should put it in your ~/.bashrc. Can you verify that DYLD_LIBRARY_PATH is indeed set in the shell in which you are trying to install jconstraints-z3---i.e. do:

> echo $DYLD_LIBRARY_PATH

Since you are on yosemite, you might want to just set DYLD_LIBRARY_PATH to the build folder of z3.

java.library.path can be set as a jvm option using the -D switch, but using DYLD_LIBRARY_PATH is preferable imo.

[chaofz]

Thank you Kasper!

I have found what went wrong on my side. It didn't work when I added export DYLD_LIBRARY_PATH=/urs/local/lib to ~/.bashrc. However, after I added export DYLD_LIBRARY_PATH=/urs/local/lib to ~/.bashrc_profile, it worked well.

Now, I have successfully built jConstraints-z3, and I am able to use jDart now.

[ksluckow]

Ahh yes, sorry I didn't spot that as a potential source of the issue (Terminal opens a login shell that only sources ~/.bash_profile). Anyway, glad you got it working 👍
Happy hacking!