IZ3 cpp_example 分段错误答案

【问题标题】：IZ3 cpp_example segmentation faultIZ3 cpp_example 分段错误
【发布时间】：2013-06-27 10:32:36
【问题描述】：

我在使用最新版本的 IZ3 并运行 cpp_example 时遇到段错误。

复制：

克隆z3：git clone https://git01.codeplex.com/z3
切换到分支interp:git checkout interp
按照README 中的构建说明构建
另外，构建cpp_example: cd build ; make cpp_example
运行cpp_example

结果：

unsat core example 3
[1]    30687 segmentation fault  ./cpp_example

如果我以 master 为基础，cpp_example 对我有用。

我在 2012 年 12 月的某个邮件列表上读到一条消息，说 Z3 的插值版本无法针对最新版本的 Z3 构建，但这是一项正在进行的工作。

IZ3 仍然不能与 Z3 版本 4 一起使用吗？

如果是，是否有关于如何针对早期版本的 Z3 构建插值源的说明？（开头：从哪里获取IZ3-3.2的源代码之类的？）

编辑：
操作系统：Linux __ 2.6.37.6-24-desktop #1 SMP PREEMPT __ i686 i686 i386 GNU/Linux

g++:

Using built-in specs.
COLLECT_GCC=g++
COLLECT_LTO_WRAPPER=/usr/lib/gcc/i586-suse-linux/4.5/lto-wrapper
Target: i586-suse-linux
Configured with: ../configure --prefix=/usr --infodir=/usr/share/info --mandir=/usr/share/man --libdir=/usr/lib --libexecdir=/usr/lib --enable-languages=c,c++,objc,fortran,obj-c++,java,ada --enable-checking=release --with-gxx-include-dir=/usr/include/c++/4.5 --enable-ssp --disable-libssp --disable-plugin --with-bugurl=http://bugs.opensuse.org/ --with-pkgversion='SUSE Linux' --disable-libgcj --disable-libmudflap --with-slibdir=/lib --with-system-zlib --enable-__cxa_atexit --enable-libstdcxx-allocator=new --disable-libstdcxx-pch --enable-version-specific-runtime-libs --program-suffix=-4.5 --enable-linux-futex --without-system-libunwind --enable-gold --with-plugin-ld=/usr/bin/gold --with-arch-32=i586 --with-tune=generic --build=i586-suse-linux
Thread model: posix

【问题讨论】：

我无法重现 seg 错误。你可以拉取 interp 分支上的最新更改并再试一次吗？如果它仍然出现段错误，你能告诉我你的平台信息，也许还能得到一个堆栈跟踪吗？插值在 interp 分支上的 Z3v4 中确实有效。它现在集成到 Z3 中，而不是构建在 API 之上。因此，源代码与 Z3v3 不兼容。 --肯

标签： c++ segmentation-fault interpolation z3 smt

【解决方案1】：

崩溃的是 unsat_core_example3()。我将问题追踪到expr_substitution::find() proofs_enabled() == false 那里

但是在rewriter_tpl<Config>::visit(expr * t, unsigned max_depth)， ProofGen == true，但通过调用 'm_cfg.get_subst(t, new_t, new_t_pr)'，new_t_pr 未初始化。

valgrind 不得不说的：

==26885== Conditional jump or move depends on uninitialised value(s)
==26885==    at 0x4C21802: bool rewriter_tpl<th_rewriter_cfg>::visit<true>(expr*, unsigned int) (ast.h:1562)
==26885==    by 0x4C21A77: void rewriter_tpl<th_rewriter_cfg>::process_app<true>(app*, rewriter_core::frame&) (rewriter_def.h:179)
==26885==    by 0x4C23303: void rewriter_tpl<th_rewriter_cfg>::resume_core<true>(obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) (rewriter_def.h:602)
==26885==    by 0x4B1EF9C: propagate_values_tactic::imp::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (propagate_values_tactic.cpp:128)
==26885==    by 0x4B21591: propagate_values_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (propagate_values_tactic.cpp:249)
==26885==    by 0x4B8BA9A: cleanup_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (tactical.cpp:1192)
==26885==    by 0x4B8ED2D: and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (tactical.cpp:157)
==26885==    by 0x4B90914: and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (tactical.cpp:170)
==26885==    by 0x4B8ED2D: and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (tactical.cpp:157)
==26885==    by 0x4B8ED2D: and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (tactical.cpp:157)
==26885==    by 0x4B90914: and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (tactical.cpp:170)
==26885==    by 0x4B94C1A: exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&, ref<model_converter>&, ref<proof_converter>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&) (tactic.cpp:179)

【讨论】：