[YICES-HELP] troubles compiling first example

Bruno Dutertre bruno at csl.sri.com
Wed Apr 29 10:16:51 PDT 2009


Luca Zanetti wrote:
> I moved library in /usr/local/lib/ and I compile correctly
> but when i launch the test i have this error
> 
> Luca at iBook:~/Documents/tesi/yices/code$  gcc -o tst -I 
> /opt/local/include  tst.c -lyices -lgmp -lstdc++
> Luca at iBook:~/Documents/tesi/yices/code$  ./tst dyld: Library not loaded: 
> /usr/local/lib/libgmp.3.dylib
>   Referenced from: /Users/Luca/Documents/tesi/yices/code/./tst
>   Reason: Incompatible library version: tst requires version 9.0.0 or 
> later, but libgmp.3.dylib provides version 8.0.0
> Trace/BPT trap
> 
> any suggest?
>

Luca,

It would help if you could answer the following questions:

What do you get when you type otool -L tst

Why do you need -I/opt/local/include ? Did you install GMP in
there (e.g., using darwin port).

Which version of Yices did you install (what's the tarfile name)?

Thanks,

Bruno



More information about the YICES-HELP mailing list