使用 iZ3 进行位向量运算答案

【问题标题】：Using iZ3 for bit vector operations使用 iZ3 进行位向量运算
【发布时间】：2013-11-05 11:06:10
【问题描述】：

我试图使用 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

提前致谢

【问题讨论】：

标签： z3

【解决方案1】：

【讨论】：

【解决方案2】：

抱歉，iZ3 仅支持 AUFLIA。

【讨论】：