錯誤包括Z3 + + H

我使用的是Z3定理證明的第一次，我安裝了Z3，然後包括Z3 ++在我的C++程序小時，但我編譯時收到以下錯誤：錯誤包括Z3 + + H

/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。但我不確定它的調用或函數是否被聲明。有人可以幫忙嗎？

來源

2013-07-08 vigenere

這是一個鏈接錯誤。什麼是你使用的命令行？如果您在系統中安裝了Z3包含文件和庫，那麼在鏈接應用程序時應該包含選項-lz3。如果Z3庫不在標準目錄中，則還應該使用-L<path-to-Z3-library>。

來源

2013-07-08 17:10:20

我按照它在z3網站上提到的方式安裝它，到它的庫安裝在/ usr/lib中，但我不能找到z3在這裏反轉，雖然我有一個可執行文件在/ usr /斌 – vigenere

Z3文件夾將不會被創建。 'sudo make install'命令會將可執行文件複製到'/ usr/bin'，將包含文件複製到'/ usr/include'中，並將該庫複製到'/ usr/lib'中。配置Z3時（即，生成Z3生成文件），可以修改前綴'/ usr'。 –

錯誤包括Z3 + + H

回答

相關問題