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 FilesMicrosoft Research3-2.19in).

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 FilesMicrosoft Research3-2.19inMicrosoft.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.