Displaying 3 results from an estimated 3 matches for "z3_mk_config".
2013 Apr 05
2
[LLVMdev] Z3 and loadable optimization
...o use the Z3 library,
installed in my system, in my optimization. When I include z3++.h (the name
of the library) in the code and use its classes, it compiles well, but when
I try to run it it says:
> opt: symbol lookup error: /home/giacomo/llvm/Debug+Asserts/lib/Acsl.so:
> undefined symbol: Z3_mk_config
>
What's the issue?
Thanks
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.llvm.org/pipermail/llvm-dev/attachments/20130405/bdb9cbee/attachment.html>
2013 Apr 05
0
[LLVMdev] Z3 and loadable optimization
...n my system, in my optimization. When I include
> z3++.h (the name of the library) in the code and use its classes, it
> compiles well, but when I try to run it it says:
>
> opt: symbol lookup error:
> /home/giacomo/llvm/Debug+Asserts/lib/Acsl.so: undefined symbol:
> Z3_mk_config
>
> What's the issue?
If the Z3 library is a dynamically linked library, then it's probably
not being loaded into opt. You might be able to force loading of it
with the -load option or by setting your LD_LIBRARY_PATH environment
variable to include the location of the Z3 library....
2013 Apr 05
1
[LLVMdev] Z3 and loadable optimization
...installed in my system, in my optimization. When I include z3++.h
> (the name of the library) in the code and use its classes, it compiles
> well, but when I try to run it it says:
>
>> opt: symbol lookup error: /home/giacomo/llvm/Debug+Asserts/lib/Acsl.so:
>> undefined symbol: Z3_mk_config
>>
> What's the issue?
>
>
> If the Z3 library is a dynamically linked library, then it's probably not
> being loaded into opt. You might be able to force loading of it with the
> -load option or by setting your LD_LIBRARY_PATH environment variable to
> include t...