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 <[email protected]>
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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev [1]
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev [1]
--
Dingbao Xie
Links:
------
[1] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
