时间戳

首页 > 解决方案 > Z3，C++：被释放的指针未被分配

c++ - Z3，C++：被释放的指针未被分配

问题描述

我决定将 Z3 与 C++ 一起使用并从 git 安装最新版本。尝试 git 示例时，（以下代码为简化示例）

#include "z3++.h"
#include <iostream>
using namespace z3;
using namespace std;

int main() {
    context c;
    expr x = c.bool_const("x");
    expr y = c.bool_const("y");
    expr conjunction = (!(x && y)) == (!x|| !y);
    solver s(c);

    s.add(!conjunction);
    cout << s << "\n";
    cout << s.to_smt2() << "\n";
    switch (s.check()) {
        case unsat:   std::cout << "de-Morgan is valid\n"; break;
        case sat:     std::cout << "de-Morgan is not valid\n"; break;
        case unknown: std::cout << "unknown\n"; break;
    }
    return 0;
}

我可以得到这个结果。

(declare-fun y () Bool)
(declare-fun x () Bool)
(assert (not (= (not (and x y)) (or (not x) (not y)))))

;
(set-info :status unknown)
(declare-fun y () Bool)
(declare-fun x () Bool)
(assert
 (not (= (not (and x y)) (or (not x) (not y)))))
(check-sat)

de-Morgan is valid

但我得到了这个错误。

a.out(92870,0x7fff9182c380) malloc: *** error for object 0x7f7fdc6217f8: pointer being freed was not allocated
*** set a breakpoint in malloc_error_break to debug
Abort trap: 6

由此可知，这个错误是在程序终止后发生的。通过引用已经发布的构造函数我们也发现了这个错误，但是在这个示例中我们没有看到这样的点。

哪位高手，谢谢。

标签： c++z3

解决方案

我认为最好的开始方法是检查Z3 的 cpp 示例文件并逐步创建您的“Hello Z3 world”示例。只需进入您的build目录并运行make examples. 一旦 make 成功完成，只需运行./cpp_example. 我看到你的例子取自他们的第一个函数demorgan，所以如果它对你不起作用，也许最好将它发布在他们的问题中。

编辑：

我刚刚测试过它，它工作正常。也许告诉我们你是如何编译你的例子的？

推荐阅读