在C＃中运行Z3当出现错误(An error appears when running Z3 in

任何人都可以请帮助！当我试图运行下面的代码，我得到这个错误：

“无法加载文件或程序集‘Microsoft.Z3，版本= 4.0.0.0，文化=中性公钥= 9c8d792caae602a2’或它的一个依赖。试图加载程序格式不正确的”

下面是代码：

class Program
{
    static void Main(string[] args)

    {

        using (Context ctx = new Context())
        {

            RealExpr c = ctx.MkRealConst("c");

            BoolExpr Eqzero = ctx.MkGt(c, ctx.MkReal(0));
            BoolExpr Gezero = ctx.MkGe(c, ctx.MkReal(0));
            BoolExpr Lttwo = ctx.MkLt(c, ctx.MkReal(2));
            BoolExpr Gtthree = ctx.MkGt(c, ctx.MkReal(3));
            BoolExpr b1 = ctx.MkBoolConst("b1");
            BoolExpr b2 = ctx.MkBoolConst("b2");
            BoolExpr b3 = ctx.MkBoolConst("b3");
            BoolExpr b0 = ctx.MkBoolConst("b0");
            RealExpr[] lamb = new RealExpr[1];
            lamb[0] = ctx.MkRealConst("lamb");
            BoolExpr temp = ctx.MkAnd(ctx.MkGt(lamb[0], ctx.MkReal(0)), ctx.MkEq(b0, ctx.MkTrue()), ctx.MkEq(b1, ctx.MkTrue()), ctx.MkGe(ctx.MkAdd(c, lamb[0]), ctx.MkReal(0)), ctx.MkLe(ctx.MkAdd(c, lamb[0]), ctx.MkReal(3)), ctx.MkGe(c, ctx.MkReal(0)), ctx.MkLe(c, ctx.MkReal(3)));
            BoolExpr exist = ctx.MkExists(lamb, temp, 1, null, null, ctx.MkSymbol("Q2"), ctx.MkSymbol("skid2"));
            Console.WriteLine(exist.ToString());
            Solver s1 = ctx.MkSolver();
            s1.Assert(exist);
            if (s1.Check() == Status.SATISFIABLE)
            {
                Console.WriteLine("get pre");
                Console.Write(s1);
            }
            else
            {
                Console.WriteLine("Not reach");
            }
            Console.ReadKey();
        }

    }
}

}

Answer 1:

最简单的方法是使用build.cmd脚本examples/dotnet文件夹，并根据您的需要进行修改。该脚本将Microsoft.Z3.dll和z3.dll到工作目录，编制相应的平台上的代码。

如果您从Visual Studio编译：

确保Microsoft.Z3.dll您引用的版本与你编译到平台（86，64，......）相匹配。有两个Z3版本bin和x64文件夹。
包括含有该文件夹Microsoft.Z3.dll在项目属性 - > 参考路径 。其原因是， Microsoft.Z3.dll使用非托管z3.dll ，你不能在Visual Studio中直接引用。

Answer 2:

在评论到以前的这个问题的答案，参考x86的分布，并在64分布作了，我不知道这个问题解决了。澄清：

当编译一个64位二进制（在Visual Studio中称为64），然后z3.dll和Microsoft.Z3.dll的64位版本是必需的。这些都在Z3分发文件夹名为x64的发现。请注意，这并不取决于是Visual Studio是运行在实际的机器上。

当编译一个32位的二进制，然后从料箱目录中的DLL是必需的。同样，这并不取决于实际的机器上的Visual Studio运行上。

Visual Studio可以交叉编译从32到64位，并且反之亦然，即，有可能编译为32位体系结构（称为86，而不是64位 ）在64位机器的二进制。另外，也可以编译一个32位机器上的64位的二进制文件。根据一种二进制被编译什么文件，DLL权集必须加入。该事项的设定是在您的项目在Visual Studio中创建配置（顶部，通常旁，其中选择调试/发布模式）。在此编译阶段，没关系正在执行什么类型的机器的编制上。当试图运行在32位机器上的64位二进制实际机器唯一重要的（但随后的错误消息将是从一个不同的报道）。运行在64位机器32位二进制文件通常工作正常（但该程序的最大存储器使用将被限制）。

我希望这有助于去除一些混乱！

另外，我们认为，包括这两个版本将合并的分布产生一些不必要的混乱，所以在今后我们将考虑分发用于32位单独的安装程序和64位的二进制文件。

文章来源: An error appears when running Z3 in C#