[klee-dev] metasmt

[felicia]

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

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