c++ - Z3，C++ : pointer being freed was not allocated

Question

我决定将 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

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

那位高手，谢谢。

Answer 1

从 C++ 的角度来看，您似乎做的一切都是正确的。此外，您直接从 Z++ example.cpp 复制.

建议:

即使它不应该有所作为......请试试这个:

a) 将 OUT 的 main() 代码复制到一个单独的函数 demorgan()

b) 从 try {} catch() block 将你的调用从“main()”包装到“demorgan()”

或者甚至更好...尝试按原样运行整个 example.cpp，不做任何更改。

所有其他方法都失败了，一个(愚蠢的!)解决方法:context *c = new context();:尝试使用“new”而不是“auto”，看看会发生什么。

问:您使用的是什么编译器？你在什么平台上构建？