[klee-dev] metasmt

[Dingbao Xie]

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
>>
>
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>



-- 
Dingbao Xie
-------------- next part --------------
HTML attachment scrubbed and removed