时间戳

首页 > 解决方案 > 编译示例 z3 代码时出现未定义的引用错误

z3 - 编译示例 z3 代码时出现未定义的引用错误

问题描述

我安装了 Z3 并且能够使用 make 示例编译 C/C++ 示例。但是，当我尝试通过包含“z3++.h”和使用 lz3 链接器标志来编译任何示例代码时，我得到未定义的引用错误。

当我之前安装 Z3 并编译相同的代码时，它可以工作。我没有对 Z3 代码进行任何更改，但现在它会引发意外错误。

猫测试.cpp

#include<z3++.h>
using namespace z3;

int main() {
    context c;
    expr x = c.int_const("x");
    std::cout << x + 1 << "\n";
    return 0;
}

g++ -c 测试.cpp

g++ -o 测试 test.o -lz3

错误：test.o：在函数“z3::operator+(z3::expr const&, z3::expr const&)”中：test.cpp:(.text._ZN2z3plERKNS_4exprES2_[_ZN2z3plERKNS_4exprES2_]+0x203)：未定义对“Z3_mk_re_union”的引用test.o：在函数“z3::concat(z3::expr const&, z3::expr const&)”中：test.cpp:(.text._ZN2z36concatERKNS_4exprES2_[_ZN2z36concatERKNS_4exprES2_]+0x76)：未定义对“Z3_is_seq_sort”测试的引用。 cpp:(.text._ZN2z36concatERKNS_4exprES2_[_ZN2z36concatERKNS_4exprES2_]+0xd3): undefined reference to `Z3_mk_seq_concat' test.cpp:(.text._ZN2z36concatERKNS_4exprES2_[_ZN2z36concatERKNS_4exprES2_]+0x11d): undefined reference to `Z3_is_re_sort' test.cpp:(.text. _ZN2z36concatERKNS_4exprES2_[_ZN2z36concatERKNS_4exprES2_]+0x17a)：未定义对“Z3_mk_re_concat”collect2的引用：错误：ld返回1退出状态

标签： z3

解决方案

迟到的答案，但我认为您应该在构建命令中添加“-lz3”标志。

推荐阅读