Problem with Z3-Opt and opt.priority box parameter

Jun 14, 2016 at 11:28 AM
Edited Jun 14, 2016 at 11:31 AM

I 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)
The following message i get in my eclipse console:
!MESSAGE [Z3] solving problem with parameters (params priority box timeout 10000)

A fatal error has been detected by the Java Runtime Environment:

SIGSEGV (0xb) at pc=0x0000000135a4b3f4, pid=678, tid=2571

JRE version: Java(TM) SE Runtime Environment (8.0_60-b27) (build 1.8.0_60-b27)
Java VM: Java HotSpot(TM) 64-Bit Server VM (25.60-b23 mixed mode bsd-amd64 compressed oops)
Problematic frame:
C [libz3.dylib+0xc03f4] opt::context::execute_box()+0x34

Failed to write core dump. Core dumps have been disabled. To enable core dumping, try "ulimit -c unlimited" before > starting Java again

An error report file with more information is saved as:
/Users/zverlov/Documents/Development/currentworkspace/plugins/org.fortiss.af3.efficientdeployment.ui >/hs_err_pid678.log

If you would like to submit a bug report, please visit:
The crash happened outside the Java Virtual Machine in native code.
See problematic frame for where to report the bug.
Also a huge log file gets generated, that can be found here:

I am using MacOS, Java 1.8 and the nightly build of Z3.


Jun 14, 2016 at 12:25 PM
This dicussion board is not in use anymore as Z3 has moved to GitHub. Could you please try to reproduce the error using the latest master branch source code from GitHub and, if it still exists, submit a new issue in our new issue tracker? Thanks!