Ошибка при включая z3 ++ ч

Question

я использую теорему z3 прувер впервые, я установил z3, а затем включен z3 ++ час в моей C++ программу, но когда я компиляции я получаю следующие ошибки:.

/tmp/ccVlHDDf.o: In function `z3::context::check_error() const': 
engine.cpp:(.text._ZNK2z37context11check_errorEv[z3::context::check_error() const]+0x11): undefined reference to `Z3_get_error_code' 
engine.cpp:(.text._ZNK2z37context11check_errorEv[z3::context::check_error() const]+0x3c): undefined reference to `Z3_get_error_msg_ex' 
/tmp/ccVlHDDf.o: In function `z3::ast::ast(z3::context&, _Z3_ast*)': 
engine.cpp:(.text._ZN2z33astC2ERNS_7contextEP7_Z3_ast[_ZN2z33astC5ERNS_7contextEP7_Z3_ast]+0x43): undefined reference to `Z3_inc_ref' 
/tmp/ccVlHDDf.o: In function `z3::cast_ast<z3::expr>::operator()(z3::context&, _Z3_ast*)': 

Я проверил другие файлы, которые были включены, чтобы увидеть, если они были определены и нашел

Z3_error_code Z3_API Z3_get_error_code(__in Z3_context c); 

в z3_api.h. Но я не уверен, объявлен ли его вызов или функция. Может кто-то помочь.

Answer 1

Это ошибка привязки. Какую команду вы используете? Если вы установили в свои системы файлы и библиотеки Z3, то при связывании приложения вы должны включить опцию -lz3. Если библиотека Z3 не находится в стандартном каталоге, вы также должны использовать -L<path-to-Z3-library>.