epfl-lara / ScalaZ3

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

Build error on OS X 64 bit #6

Closed msama closed 12 years ago

msama commented 12 years ago

OS X version 10.7.4 - 64 bit Scala 2.9.1 Z3 4.0 - 64 bit sbt 0.7.7

The compiler was first complaining for missing __in and __out. I added them in one of the header files.

Then I receive the following error:

[info] == gcc-osx == [info] Compiling C library [info] gcc -o /Users/rax/git/ScalaZ3/lib-bin/libscalaz3.jnilib -dynamiclib -I/System/Library/Java/JavaVirtualMachines/1.6.0.jdk/Contents/include -I/System/Library/Frameworks/JavaVM.framework/Versions/Current/Headers -I/Users/rax/git/ScalaZ3/z3/x64/4.0/include -L/Users/rax/git/ScalaZ3/z3/x64/4.0/lib -g -lc -lz3 -fPIC -O2 -fopenmp /Users/rax/git/ScalaZ3/src/c/z3_thycallbacks.c /Users/rax/git/ScalaZ3/src/c/extra.c /Users/rax/git/ScalaZ3/src/c/casts.c /Users/rax/git/ScalaZ3/src/c/z3_Z3Wrapper.c [error] Undefined symbols for architecture x86_64: [error] "_Z3_trace_off", referenced from: [error] _Java_z3_Z3Wrapper_traceOff in ccUdOQlM.o [error] "_Z3_trace_to_stdout", referenced from: [error] _Java_z3_Z3Wrapper_traceToStdout in ccUdOQlM.o [error] "_Z3_trace_to_stderr", referenced from: [error] _Java_z3_Z3Wrapper_traceToStderr in ccUdOQlM.o [error] "_Z3_trace_to_file", referenced from: [error] _Java_z3_Z3Wrapper_traceToFile in ccUdOQlM.o [error] ld: symbol(s) not found for architecture x86_64 [error] collect2: ld returned 1 exit status [info] == gcc-osx ==

psuter commented 12 years ago

(Note that I fixed the __in and __out issue in master, I'm really not sure how it got in there in the first place.)

msama commented 12 years ago

True, i pulled your master and now that is disappeared. The other one is still there. It could be a problem with my machine configuration. i know that @matteo-g-rossi is building it without errors, but it fails the tests.

msama commented 12 years ago

Indeed those functions have been removed from Z3 4.0

    public static native boolean traceToFile(long contextPtr, String traceFile);
    public static native void traceToStderr(long contextPtr);
    public static native void traceToStdout(long contextPtr);
    public static native void traceOff(long contextPtr);

This is what is causing the compilation problem. I wonder how my linux build was still working.....

Are those used? can we remove them?

psuter commented 12 years ago

Thanks for taking care of this.