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


i wrote following program in visual studio 2010(version: 10.0.30319.1 rtmrel) c# language , version of .net framework 4.0.30319 rtmrel. there no errors or warnings when compiling, throw exception when running program. exception "z3_test_1.exe[2448] unhandled exception happened in microsoft .net framework", z3_test_1.exe program file name. z3 prover used in version z3 4.0 , in program used microsoft.z3.dll rather 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();                 }                 }         }     }

i tried reproduce errors. test works fine me. suspect same compilation problem leo points out because worked me. subtle problem if reference x86 assembly x64 environment, or other round, runtime errors start happening. fool-proof way add /platform indication arguments pass compiler (csc.exe).


Comments

Post a Comment

Popular posts from this blog

java - Play! framework 2.0: How to display multiple image? -

i need display gallery of photos. here template: @(photos: list[photo]) @title = { <bold>gallery</bold> } @main(title,"photo"){ <ul class="thumbnails"> @for(photo <- photos) { <li class="span3"> <a href="#" class="thumbnail"> <img src="@photo.path" alt=""> </a> </li> } </ul> } and here controller method: public static result getphotos() { return ok(views.html.photo.gallery.render(photo.get())); } and here photo bean : @entity public class photo extends model { @id public long id; @required public string label; public string path; public photo(string path, string label) { this.path = path; this.label = label; } private static finder<long, photo> find = new finder<long, photo>( long.class, photo.class); public static list<phot...
Read more

gmail - Is there any documentation for read-only access to the Google Contacts API? -

i want read-only access user's google contacts. there stackoverflow member wanted this, , received following answer : yes, there is, use https://www.googleapis.com/auth/contacts.readonly scope , "view contacts". this exchange reference read-only access google contacts can find using google. simply using access token obtained attempt read usual google contacts api (i.e. https://www.google.com/m8/feeds ) fails insufficient permissions. similarly, using google contacts api on new target fails 404 errors (for example https://www.googleapis.com/auth/contacts.readonly/default/full ). is there documentation anywhere on how use api, or permissible way access google contacts api full read-write access?
Read more

php - Controller/JToolBar not working in Joomla 2.5 -

relevant code: jtoolbarhelper::custom('savecategories', 'save', '', 'save', false, false); ... <input type="hidden" name="controller" value="easyblogcontroller"> according can dig docs , own previous questions, should call savecategories() function in easyblogcontroller . i've tried setting value easyblog , easyblog.php (file name) current easyblogcontroller (class name). clicking on save button refreshes page. not redirect, echo or var_dump test code put in savecategories() function. var_dump ing jrequest::getvar('controller') , 'task' return correct values. creating controller object , using $controller->execute('task'); works. the values going depend on location of controller trying call, , have couple options here. typically there controller in base folder of component (likely components/com_easyblog) in file called controller.php , class name inside ...
Read more