问构建Z3 for StarExec
EN

Stack Overflow用户

提问于 2015-07-04 16:05:37

回答 1查看 79关注 0票数 1

在即将发布的终止竞争中，它是在StarExec上运行的，我们希望在我们的工具终极Buchi自动机中使用Z3作为SMT的求解器。

首先，我使用了计算机上的Z3可执行文件。在StarExec上，执行失败。这是错误消息：

/usr/lib64/libstdc++.so.6: version `GLIBCXX_3.4.15' not found
/lib64/libc.so.6: version `GLIBC_2.14' not found

接下来，我重新构建了Z3，但是添加了以下一行：

LINK_FLAGS=-static
to build/config.mk.

以获得静态链接的可执行文件。它在我的计算机上运行得很好，但是在StarExec上我得到了以下错误消息：

49541 Illegal instruction     (core dumped)

如何构建Z3以便在StarExec上运行它？

我认为这个问题与CPU的编译器优化有关。当我在旧机器上构建Z3时，它也可以在StarExec上工作。

发布于 2015-07-04 17:47:25

您应该使用mk_make.py脚本命令行参数来指定静态链接

票数 1

页面原文内容由Stack Overflow提供。腾讯云小微IT领域专用引擎提供翻译支持

原文链接：

https://stackoverflow.com/questions/31222630

复制

相似问题

问构建Z3 for StarExecEN