{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/654","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/654/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/654/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/654/events","html_url":"https://github.com/Z3Prover/z3/issues/654","id":160172696,"number":654,"title":"Problem with Z3-Opt and opt.priority box parameter ","user":{"login":"zverlov","id":19929982,"avatar_url":"https://avatars.githubusercontent.com/u/19929982?v=3","gravatar_id":"","url":"https://api.github.com/users/zverlov","html_url":"https://github.com/zverlov","followers_url":"https://api.github.com/users/zverlov/followers","following_url":"https://api.github.com/users/zverlov/following{/other_user}","gists_url":"https://api.github.com/users/zverlov/gists{/gist_id}","starred_url":"https://api.github.com/users/zverlov/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/zverlov/subscriptions","organizations_url":"https://api.github.com/users/zverlov/orgs","repos_url":"https://api.github.com/users/zverlov/repos","events_url":"https://api.github.com/users/zverlov/events{/privacy}","received_events_url":"https://api.github.com/users/zverlov/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":6,"created_at":"2016-06-14T12:47:37Z","updated_at":"2016-06-16T00:00:30Z","closed_at":null,"body":"Hey,\r\n\r\nI get an error in my JRE when i try to optimize a large deployment problem using z3 JAVA-API and opt.priority box parameter. This problem doesnt occur, when I am searching for pareto fronts though. (i my example i use 3 contradicting criteria)\r\nThe following message i get in my eclipse console:\r\n\r\n    \r\n\r\n> !MESSAGE [Z3] solving problem with parameters (params priority box timeout 10000)\r\n> \r\n>     A fatal error has been detected by the Java Runtime Environment:\r\n> \r\n>     SIGSEGV (0xb) at pc=0x0000000135a4b3f4, pid=678, tid=2571\r\n> \r\n>     JRE version: Java(TM) SE Runtime Environment (8.0_60-b27) (build 1.8.0_60-b27)\r\n>     Java VM: Java HotSpot(TM) 64-Bit Server VM (25.60-b23 mixed mode bsd-amd64 compressed oops)\r\n>     Problematic frame:\r\n>     C [libz3.dylib+0xc03f4] opt::context::execute_box()+0x34\r\n> \r\n>     Failed to write core dump. Core dumps have been disabled. To enable core dumping, try \"ulimit -c unlimited\" before > starting Java again\r\n> \r\n>     An error report file with more information is saved as:\r\n>     /Users/zverlov/Documents/Development/currentworkspace/plugins/org.fortiss.af3.efficientdeployment.ui >/hs_err_pid678.log\r\n> \r\n>     If you would like to submit a bug report, please visit:\r\n>     http://bugreport.java.com/bugreport/crash.jsp\r\n>     The crash happened outside the Java Virtual Machine in native code.\r\n>     See problematic frame for where to report the bug.\r\n\r\nAlso a huge log file gets generated, that can be found [here](http://download.fortiss.org/public/zverlov/hs_err_pid674.log):\r\n\r\nI am using MacOS, Java 1.8 and the nightly build of Z3 (https://github.com/Z3Prover/bin/tree/master/nightly).\r\n\r\nbest\r\n\r\nSergey"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/226354282","html_url":"https://github.com/Z3Prover/z3/issues/654#issuecomment-226354282","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/654","id":226354282,"user":{"login":"NikolajBjorner","id":3085284,"avatar_url":"https://avatars.githubusercontent.com/u/3085284?v=3","gravatar_id":"","url":"https://api.github.com/users/NikolajBjorner","html_url":"https://github.com/NikolajBjorner","followers_url":"https://api.github.com/users/NikolajBjorner/followers","following_url":"https://api.github.com/users/NikolajBjorner/following{/other_user}","gists_url":"https://api.github.com/users/NikolajBjorner/gists{/gist_id}","starred_url":"https://api.github.com/users/NikolajBjorner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/NikolajBjorner/subscriptions","organizations_url":"https://api.github.com/users/NikolajBjorner/orgs","repos_url":"https://api.github.com/users/NikolajBjorner/repos","events_url":"https://api.github.com/users/NikolajBjorner/events{/privacy}","received_events_url":"https://api.github.com/users/NikolajBjorner/received_events","type":"User","site_admin":false},"created_at":"2016-06-16T00:00:30Z","updated_at":"2016-06-16T00:00:30Z","body":"Note: The :opt.timeout option should be replaced by :timeout. I will remove this option altogether. There is just the main timeout parameter that will be used by opt."}}
{"actor":{"display_login":"NikolajBjorner"}}