search

agra-uni-bremen / metaSMT

MIT License
48 stars 25 forks source link

Can't find Z3++.h #18

Closed anithag closed 9 years ago

anithag commented 9 years ago

From the latest github, on ubuntu (14.10), I get this error while building KLEE. I am using Z3-4.3.1. I modified makefiles in klee and kleaver directories as suggested in build instructions. I could successfully build metaSMT but not Klee from latest github. Can you suggest me a fix?

In file included from Solver.cpp:55:0: /home/anitha/metasmt/build/root/include/metaSMT/backend/Z3_Backend.hpp:8:18: fatal error: z3++.h: No such file or directory

include <z3++.h>

              ^

compilation terminated.

anithag commented 9 years ago

I solved this by including Z3 include directory metasmt/deps/Z3-4.3.1/include in metasmt.Makefile. Seemed like the right thing to do. However now it starts to complain for not finding bootlector.h headers. I did not build bootlector. So is there a way to suppress the building other solvers other than removing/commenting relevant statements from klee/lib/Solver/Solver.cpp?

Note that I have built only Z3-4.3.1.

finnhaedicke commented 9 years ago

Sorry, but klee includes Boolector.hpp. You either have to install all solvers included by Klee or change klee/lib/Solver/Solver.cpp.

anithag commented 9 years ago

Thanks. I just went ahead and removed the presence of boolector & minisat from klee sources. This issue can probably be closed now.