[klee-dev] metasmt

felicia felicia at comp.nus.edu.sg
Sun Sep 20 08:03:58 BST 2015


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.





More information about the klee-dev mailing list