z3 - 使用 iZ3 进行位向量运算

Question

我试图使用 iz3 来提取插值。对于文档页面中给出的示例，它似乎工作正常。我尝试运行 iz3 作为 Z3 符合 UNSAT 的示例。但是当我使用 iZ3 时弹出以下错误

iZ3：表达式中不支持 Z3 运算符 (bvule bv100[101] main.a'64'0) iZ3：表达式中不支持 Z3 运算符 (bvadd main.a'64'0 main.b'64'0) 分段错误

iZ3 是否只支持 AUFLIA 理论而不支持 QF_AUFBV ？有没有一种方法可以获得 QF_AUFBV 的插值，它支持上面的 bit_vector 操作？我使用的是 z3 4.1 版本的 iZ3

提前致谢

score 0 · Accepted Answer

0

对不起，iZ3 只支持 AUFLIA。

于 2013-11-05T18:40:08.970 回答

score 0 · Accepted Answer

2 回答 2