【发布时间】：2015-03-16 07:41:17
【问题描述】：
我的问题如下，
环境：64 位 windows 7，vs 2010，z3-4.3.2
首先，从源码编译Z3（从z3主页下载），这一步是可以的，没有任何错误（从命令窗口）；
其次，测试“src/example”下的c++示例，首先，测试函数find_model_example1()，编译，链接，这个没有警告，报错。但是，运行时卡住了。然后，我一步步调试后，卡在第二条语句，“context c”；
1, std::cout << "find_model_example1\n";
2, context c;
3, expr x = c.int_const("x");
在这个语句中继续使用 F11，它卡在函数“reinterpret_cast”，api_context.cpp 中的第 424 行，继续使用 F11，在“context”的构造函数中：“context(config_params *, bool)”，函数“m_replay_stack”会调用函数“copy_core”(vector.h)，触发0xC00000005错误。
【问题讨论】：
-
我无法重现此问题；它还存在吗？如果是这样，您能否尝试从不稳定的分支构建源代码，以便我们查看最新版本是否仍然存在此问题？
-
它仍然存在。最新的测试是使用 vs2012、z3-4.3.2 master(release ,-staticlib) 和不稳定的(release, -staticlib?(不记得))，问题如下： 0x1006CE75(libz3.dll) 处的未处理异常(对于两者xx.exe 中的 master 和不稳定版本）：0XC0000005：访问冲突读取位置 0Xccccccc8。（位置如前）.. Master（发布，而不是 -staticlib）与另一个 xxxxx.dll 而不是 libz3.dll 有同样的问题。此外，z3-4.3.2 在我的 Virtualbox 的 Ubuntu 12.04.64 上运行良好。而且 Z3-4.3.1 与 vs2012/2010/2008 配合得很好。（我更喜欢 z3-4.3.2 而不是 4.3.1）
-
有时用户在构建旧代码时会遇到问题。
-
是的，请确保您像 Nikolaj 所说的那样从头开始构建。我们夜间不稳定的二进制文件也是用 VS2010 编译的，我们之前没有看到任何此类问题。
-
好的！我会再试一次，谢谢 Nikolaj 和 Christoph。