【发布时间】：2016-02-27 04:58:03
【问题描述】：
假设我想查看“random_split”的跟踪信息。我写了
enable_trace("random_split")
在我使用 z3 python api 的 python 脚本中，但没有显示任何内容。
不知道在使用z3py的时候应该如何查看trace信息？
【问题讨论】：
标签： logic constraints z3 smt z3py
【发布时间】：2016-02-27 04:58:03
【问题描述】：
跟踪仅在调试模式下可用，因此您需要使用python scripts/mk_make.py --debug 自己编译 Z3。如果跟踪没有产生任何输出，则永远不会到达该特定代码段，因此它永远不会打印任何内容。
【讨论】：
-
当我使用“--debug”重新编译 Z3 时，我看到类似“z3-z3-4.4.1/build/../src/util/mpz.h:347: undefined reference to ‘吹捧’”。这张票谈到了同样的错误：github.com/Z3Prover/z3/issues/243 知道我应该如何解决这个问题吗？ （我使用的是 4.4.1 版本）
-
查看 github 上的讨论。在继续之前，请确保您拥有最新版本的源代码。