[klee-dev] metasmt

[felicia]

Hi,

Thank you for your suggestion. I tried making symbolic link to 64 bit 
libraries path and it is fine now. Below the command:

ln -s /home/felicia/metasmt/deps/Z3-4.1/lib/libz3.so /usr/lib64/libz3.so

Thank you.

Best Regards,

On 2015-09-21 13:49, Dingbao Xie wrote:
> On Mon, Sep 21, 2015 at 9:17 AM, felicia <felicia at comp.nus.edu.sg>
> wrote:
> 
>> Hi,
>> 
>> Since the last problem was because unable to compile stp-svn. I
>> eventually did not use stp-svn, and just use z3, boolector, and
>> minisat. So, I currently able to compile and install metasmt.
>> 
>> However, when I compile KLEE, it always give error like this:
>> /Release+Asserts/bin/klee: error while loading shared libraries:
>> libz3.so: cannot open shared object file: No such file or directory
> 
> The error information is very clear. Try to search libz3.so in path
> /usr/local/lib and /usr/lib.
> If it exists, try to run command 'sudo ldconfig'.
> 
>> Although, I have run cmake -DCMAKE_INSTALL_PREFIX=/usr/ ../ and
>> cmake -DBUILD_SHARED_LIBS:BOOL=OFF
>> -DENABLE_PYTHON_INTERFACE:BOOL=OFF when installing metasmt, the
>> error still persist.
>> 
>> Please inform me further about this. Thank you very much in
>> advance.
>> 
>> Best Regards,
>> 
>> On 2015-09-20 15:03, felicia wrote:
>> 
>>> Hi,
>>> 
>>> I tried to install metasmt for KLEE because I want to use Z3. I
>>> tried
>>> to compile metasmt and run this command: ./bootstrap.sh --deps
>>> deps/
>>> --non-free -m RELEASE build/
>>> and It seems fine. But, when I run this command: ./bootstrap.sh
>>> --deps
>>> deps/ --free -m RELEASE build/
>>> It always produce error like this:
>>> 
>>> cvc.y: In function ‘int cvcparse()’:
>>> cvc.y:213:13: error: ‘AssertsQuery’ was not declared in this
>>> scope
>>> 
>>> 
>> 
> ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
>>> ^
>>> cvc.y:219:13: error: ‘AssertsQuery’ was not declared in this
>>> scope
>>> 
>>> 
>> 
> ((ASTVec*)AssertsQuery)->push_back(parserInterface->CreateNode(TRUE));
>>> ^
>>> cvc.y:235:13: error: ‘AssertsQuery’ was not declared in this
>>> scope
>>> ((ASTVec*)AssertsQuery)->push_back(asserts);
>>> ^
>>> make[1]: *** [parsecvc.o] Error 1
>>> make[1]: Leaving directory
>>> `/home/felicia/metasmt/deps/build/stp-svn/src/parser'
>>> make: *** [src/parser/libparser.a] Error 2
>>> ERROR: build_install failed for stp-svn
>>> TERMINATING
>>> building dependencies
>>> boost-1_52_0
>>> 
>>> boolector-1.5.118
>>> minisat-git
>>> stp-svn
>>> failed.
>>> 
>>> I probably miss something here. Please inform me further to
>>> handle
>>> this error. Thank you.
>>> 
>>> Other question, is it possible for calling unsat-core method
>>> after
>>> installing metasmt z3?
>>> 
>>> Thank you very much.
>>> 
>>> _______________________________________________
>>> klee-dev mailing list
>>> klee-dev at imperial.ac.uk
>>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev [1]
>> 
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev [1]
> 
> --
> 
> Dingbao Xie
> 
> 
> Links:
> ------
> [1] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev