Z3_test_1。微软.net框架中未处理的exe[2448]异常

Question

我在visual Studio2010(版本:10.0.30319.1RTMREL)中用C#语言编写了以下程序，.net框架的版本是4.0.30319RTMREL。编译时不会出现错误或警告，但运行程序时会抛出异常。例外情况是“微软.net框架中发生Z3_test_1.exe2448未处理异常”，其中Z3_test_1.exe是程序文件名。我使用的Z3验证程序的版本是Z3 4.0，并且在程序中我使用的是Microsoft.Z3.dll而不是Microsoft.Z3V3.dll。

using System;
using System.Collections.Generic;
using System.Linq;
using System.Text;
using Microsoft.Z3;
//using Microsoft.Z3V3;

namespace Z3_test_1
{
    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

我试着重现你的错误。这个测试对我来说很好。我怀疑这是Leo指出的相同的编译问题，因为它对我有效。微妙的问题是，如果您从x64环境或其他环境引用x86程序集，则会开始发生运行时错误。最简单的方法是使用传递给编译器(csc.exe)的参数添加/platform指示。