CODEWITHSUNDEEP
z3
user1435528
user1435528

Reputation: 11

Z3_test_1.exe[2448] unhandled exception in Microsoft .net framework

I wrote the following program in visual studio 2010(Version: 10.0.30319.1 RTMREL) with C# language and the version of .net framework is 4.0.30319 RTMREL. There is no errors or warnings when compiling, but it throw an exception when running the program. The exception is that "Z3_test_1.exe[2448] unhandled exception happened in Microsoft .net framework", Where Z3_test_1.exe is the program file name. The Z3 prover I used is in version Z3 4.0 and in the program i used Microsoft.Z3.dll rather than 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();
                }   

            }
        }
    }

Upvotes: 0

Views: 190

Answers (1)

Nikolaj Bjorner
Nikolaj Bjorner

Reputation: 111

I tried to reproduce your errors. The test works just fine for me. I suspect it is the same compilation problem that Leo points out because it worked for me. The subtle problem is that if you reference an x86 assembly from a x64 environment, or the other round, then runtime errors start happening. The fool-proof way is to add a /platform indication with the arguments you pass to the compiler (csc.exe).

Upvotes: 1

Related Questions