Mismatched DLL versions?

Question

I am trying to use the Z3 SMT solver for my projects. However it seems there is a mismatch of the Visual Studio versions, which caused my troubles. My Visual Studio 2008 reports that

The referenced component 'Microsoft.Z3' could not be found.

while it is indeed in the installation dir (C:\Program Files\Microsoft Research\Z3-2.19\bin).

When the project is compiled, another warning says

Resolved file has a bad image, no metadata, or is otherwise inaccessible. Could not load file or assembly 'C:\Program Files\Microsoft Research\Z3-2.19\bin\Microsoft.Z3.dll' or one of its dependencies. This assembly is built by a runtime newer than the currently loaded runtime and cannot be loaded.

along with other errors saying the Z3 related types as Context, Term, etc. are not found.

Is this because the new versions of Z3 are compiled using newer versions of the dotNet Framework that I don't have? How can I resolve this issue? Thanks in advance!

PS: the file I used in testing is from the Z3 tutorial (pdf), Chapter 5, pasted below.

using System;
using Microsoft.Z3;

class Program
{
    Context ctx;
    Term mk_int(int a) { return ctx.MkIntNumeral(a); }
    Term mk_var(string name) { return ctx.MkConst(name, ctx.MkIntSort()); }
    Term mk_lo(Term x) { return x >= mk_int(0); }
    Term mk_mid(Term x, Term y, int a) { return y >= (x + mk_int(a)); }
    Term mk_hi(Term y, int b) { return (y + mk_int(b)) <= mk_int(8); }

    Term mk_precedence(Term x, Term y, int a, int b)
    {
        return ctx.MkAnd(new Term[] { mk_lo(x), mk_mid(x, y, a), mk_hi(y, b) });
    }

    Term mk_resource(Term x, Term y, int a, int b)
    {
        return (x >= (y + mk_int(a))) | (y >= (x + mk_int(b)));
    }

    void encode()
    {
        using (Config cfg = new Config())
        {
            cfg.SetParamValue("MODEL", "true");
            using (Context ctx = new Context(cfg))
            {
                this.ctx = ctx;
                Term t11 = mk_var("t11");
                Term t12 = mk_var("t12");
                Term t21 = mk_var("t21");
                Term t22 = mk_var("t22");
                Term t31 = mk_var("t31");
                Term t32 = mk_var("t32");
                ctx.AssertCnstr(mk_precedence(t11, t12, 2, 1));
                ctx.AssertCnstr(mk_precedence(t21, t22, 3, 1));
                ctx.AssertCnstr(mk_precedence(t31, t32, 2, 3));
                ctx.AssertCnstr(mk_resource(t11, t21, 3, 2));
                ctx.AssertCnstr(mk_resource(t11, t31, 2, 2));
                ctx.AssertCnstr(mk_resource(t21, t31, 2, 3));
                ctx.AssertCnstr(mk_resource(t12, t22, 2, 3));
                ctx.AssertCnstr(mk_resource(t12, t32, 3, 1));
                ctx.AssertCnstr(mk_resource(t22, t32, 3, 1));
                Model m = null;
                LBool r = ctx.CheckAndGetModel(out m);
                if (m != null)
                {
                    m.Display(System.Console.Out);
                    m.Dispose();
                }
            }
        }
    }

    static void Main()
    {
        Program p = new Program();
        p.encode();
    }
};

UPDATE: After a few extractions of older .msi installer files, I found the latest version of Z3 which uses dotNet Framework less than v4 is Z3 2.11; in which case I decide to use, instead of updating my VS2008 for the moment.

Didn't you already ask this before? – David Heffernan Jul 20 '11 at 19:21 — David Heffernan, Jul 20 '11 at 19:21

score 1 · Answer 1 · answered Jul 18 '11 at 19:52

1

This is likely caused because you're targetting an older .NET Framework than the Z3 libraries. If you're Z3 version targets .NET 4, for example, make sure you build this in Visual Studio 2010 and target the .NET Framework 4.0.

answered Jul 18 '11 at 19:52

Reed Copsey

554,122
78
1,158
1,373

Thanks for the quick reply. I have two more questions. 1. How can I assure that the Z3 dll I got are indeed from VS2010; now I only suspect this is the reason. 2. If so, no way to do it in VS2008? Thanks! – Xiaopeng You Jul 18 '11 at 19:53
@Xiaopeng: The only "questions" I see all relate to this. You should download VS 2010, and target .NET 4, and it will fix your issues. What are your other questions? – Reed Copsey Jul 18 '11 at 19:55
@Xiaopeng: Run it through Ildasm (http://msdn.microsoft.com/en-us/library/f7dy01k1.aspx) - it will tell you the framework version. If it's targetting .NET 4 (which I suspect is the case), you'll need VS 2010. You can download VS 2010 Express for free at: http://www.microsoft.com/express – Reed Copsey Jul 18 '11 at 19:56
It says `.assembly Microsoft.Z3 { .ver 2:0:4059:30493 } ` Is it framework 2.0? That's odd. – Xiaopeng You Jul 18 '11 at 20:05
@Xiaopeng: Refer to http://stackoverflow.com/questions/325918/how-to-find-out-which-version-of-the-net-framework-an-executable-needs-to-run – Reed Copsey Jul 18 '11 at 21:18
Now everything is clear to me. It is indeed created from .NET 4. Thank you very much! – Xiaopeng You Jul 19 '11 at 02:38

Mismatched DLL versions?

1 Answers1