diff --git a/src/api/java/Context.java b/src/api/java/Context.java index 1e2b5d4fa0c..39d35d9d327 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -30,8 +30,9 @@ public class Context implements AutoCloseable { private final long m_ctx; static final Object creation_lock = new Object(); - public static Context mkContext() { - return new Context(Native.mkContextRc(0)); + public Context () { + m_ctx = Native.mkContextRc(0); + init(); } @@ -52,24 +53,17 @@ public static Context mkContext() { * Note that in previous versions of Z3, this constructor was also used to set global and * module parameters. For this purpose we should now use {@code Global.setParameter} **/ - public static Context mkContext(Map settings) - { + public Context(Map settings) { long cfg = Native.mkConfig(); - for (Map.Entry kv : settings.entrySet()) + for (Map.Entry kv : settings.entrySet()) { Native.setParamValue(cfg, kv.getKey(), kv.getValue()); - long m_ctx = Native.mkContextRc(cfg); + } + m_ctx = Native.mkContextRc(cfg); Native.delConfig(cfg); - return new Context(m_ctx); + init(); } - /** - * Constructor. - **/ - protected Context(long m_ctx) - { - this.m_ctx = m_ctx; - - // Code which used to be in "initContext". + private void init() { setPrintMode(Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT); Native.setInternalErrorHandler(m_ctx); }