将有符号位向量表达式转换为整数抛出访问违规异常

Question

我正在使用 Z3 .NET API，并尝试使用以下代码将有符号位向量表达式转换为整数：

using (Context context = new Context())
{
    Expr e = context.MkBV2Int(context.MkBV(-1, 32), true);
}

但是，我得到以下异常：

Unhandled Exception: System.AccessViolationException: Attempted to read or write protected memory. This is often an indication that other memory is corrupt.
   at Microsoft.Z3.Native.LIB.Z3_mk_bv2int(IntPtr a0, IntPtr a1, Int32 a2)
   at Microsoft.Z3.Native.Z3_mk_bv2int(IntPtr a0, IntPtr a1, Int32 a2) in Z3 srcsrcapidotnetNative.cs:line 2386
   at Microsoft.Z3.Context.MkBV2Int(BitVecExpr t, Boolean signed) in Z3 srcsrcapidotnetContext.cs:line 1800

但是，无符号位向量的转换效果很好。

问题出在哪里？我该如何解决它？提前非常感谢你。

Answer 1

感谢您报告此问题！较低级别的 C API 中确实存在一个错误。此问题现已在不稳定的分支中修复（请参阅此处）。