常數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

回答