常数Z3 - 在C段故障++ API

在分段故障Z3结果下面的C++ API代码：11 （Z3版本4.4.0在Mac OS 10.10.2运行）常数Z3 - 在C段故障++ API

#include "../z3/include/z3++.h" 

int main() { 
    z3::context c; 

    z3::sort A = z3::sort(c); 
    z3::expr x = c.constant("x", A); 
}

我做有问题？

2015-04-12 szymtor

我不知道z3，但是如果'c'因为没有定义而得到一个随机值，这可能最终会排序谁知道什么。 – deW1

表达式z3::sort(c)将A初始化为与上下文关联但不是实际（较低级别）排序对象的排序对象。（另请参阅C++ example了解如何构建常用的排序。）

我相信目前没有方便的C++风格的构造未解释排序的方法。为此，我们需要去C-API函数Z3_mk_uninterpreted_sort（然后可以使用z3::sort(c, ...)进行打包。）

2015-04-15 15:28:59

回答