[YICES-HELP] troubles compiling first example

Luca Zanetti zanetti.luca at gmail.com
Wed Apr 29 03:59:13 PDT 2009


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?


Il giorno 23/apr/09, alle ore 19:14, Bruno Dutertre ha scritto:

> Luca Zanetti wrote:
>> Hi,
>> I'm a new user of Yices, I've installed it on OSX Leopard on a PPC.
>> this is the example i want to run
>> ----
>> #include"yices_c.h"
>> int main() {
>>    yices_context ctx = yices_mk_context();
>>        yices_del_context(ctx);
>>    return 0;
>> }
>> ----
>> i compile it with the option
>> gcc -o test -I ~/include -L ~lib test.c -lyices -lgmp -lstdc++
>> and this is the output
>> ld: library not found for -lyices
>> collect2: ld returned 1 exit status
>> Can you help me to solve this problem?
>> thanks
>> Luca
>
> Hi Luca,
>
> Make sure you give the right path to the -L command:
>  -L ~/lib
> is more likely to work.
>
> Also check the notes on Mac OS X in the yices wiki
> (http://yices-wiki.csl.sri.com/index.php/FAQ).
> Some of the info is relevant to all Mac OS versions.
>
> Bruno



More information about the YICES-HELP mailing list