An error appears when running Z3 in C#

Question

Can anyone please help! When I tried to run the code below, I got this error:

" Could not load file or assembly 'Microsoft.Z3, Version=4.0.0.0, Culture=neutral, PublicKeyToken=9c8d792caae602a2' or one of its dependencies. An attempt was made to load a program with an incorrect format "

Here is the code:

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();
        }

    }
}

}

I think you're referencing 32-bit Microsoft.Z3.dll in a 64-bit machine or vice versa. Make sure you reference the right Z3 version and check the compilation procedure in comments to this thread: stackoverflow.com/questions/10663994/… — pad
thank you but I refereced 64-bit Microsoft.Z3.dll in a 64-bit machine — user1327010

pad pad · Accepted Answer · 2012-06-21T11:45:10

The easiest way is to use build.cmd script in examples/dotnet folder and modify it according to your need. The script copies Microsoft.Z3.dll and z3.dll to the working directory and compiles the code on the corresponding platform.

If you compile from Visual Studio:

Make sure that Microsoft.Z3.dll's version you reference matches with the platform (x86, x64,...) which you're compiling to. There are two Z3 versions in bin and x64 folder.
Include the folder containing the Microsoft.Z3.dll in Project Properties->Reference Paths. The reason is that Microsoft.Z3.dll uses unmanaged z3.dll, which you cannot directly reference in Visual Studio.

An error appears when running Z3 in C#

2 Answers