StackOverflow2013

Note that there are some explanatory texts on larger screens.

plurals

POZ3_test_1.exe[2448] unhandled exception in Microsoft .net framework
text
Body
copied!<p>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.</p> <pre><code>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(); } } } } </code></pre>

Querying!

Guidance

An individual column

Larger individual text columns get their own page to allow for proper reading.

SQuiL has stopped working due to an internal error.

If you are curious you may find further information in the browser console, which is accessible through the devtools (F12).

Reload