From 24532474a04ef079ab423efb7e2579990985e538 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Wed, 14 Oct 2015 13:58:51 +0100
Subject: [PATCH] Bugfix for concurrent Context creation in Java and .NET.

Relates to #205 #245
---
 src/api/dotnet/Context.cs              | 23 +++++++++++++++--------
 src/api/java/Context.java              | 25 +++++++++++++++----------
 src/api/java/InterpolationContext.java | 22 ++++++++++++++--------
 3 files changed, 44 insertions(+), 26 deletions(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 0aee3f7d8..df502f115 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -37,8 +37,11 @@ namespace Microsoft.Z3
         public Context()
             : base()
         {
-            m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
-            InitContext();
+            lock (creation_lock)
+            {
+                m_ctx = Native.Z3_mk_context_rc(IntPtr.Zero);
+                InitContext();
+            }
         }
 
         /// <summary>
@@ -64,12 +67,15 @@ namespace Microsoft.Z3
         {
             Contract.Requires(settings != null);
 
-            IntPtr cfg = Native.Z3_mk_config();
-            foreach (KeyValuePair<string, string> kv in settings)
-                Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
-            m_ctx = Native.Z3_mk_context_rc(cfg);
-            Native.Z3_del_config(cfg);
-            InitContext();
+            lock (creation_lock)
+            {
+                IntPtr cfg = Native.Z3_mk_config();
+                foreach (KeyValuePair<string, string> kv in settings)
+                    Native.Z3_set_param_value(cfg, kv.Key, kv.Value);
+                m_ctx = Native.Z3_mk_context_rc(cfg);
+                Native.Z3_del_config(cfg);
+                InitContext();
+            }
         }
         #endregion
 
@@ -4381,6 +4387,7 @@ namespace Microsoft.Z3
         #region Internal
         internal IntPtr m_ctx = IntPtr.Zero;
         internal Native.Z3_error_handler m_n_err_handler = null;
+        internal static Object creation_lock = new Object();
         internal IntPtr nCtx { get { return m_ctx; } }
 
         internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
diff --git a/src/api/java/Context.java b/src/api/java/Context.java
index 0955f79ca..9f20f121d 100644
--- a/src/api/java/Context.java
+++ b/src/api/java/Context.java
@@ -30,10 +30,12 @@ public class Context extends IDisposable
      * Constructor.
      **/
     public Context()
-    {
+    {        
         super();
-        m_ctx = Native.mkContextRc(0);
-        initContext();
+        synchronized (creation_lock) {            
+            m_ctx = Native.mkContextRc(0);
+            initContext();
+        }
     }
 
     /**
@@ -56,12 +58,14 @@ public class Context extends IDisposable
     public Context(Map<String, String> settings)
     {
         super();
-        long cfg = Native.mkConfig();
-        for (Map.Entry<String, String> kv : settings.entrySet())
-            Native.setParamValue(cfg, kv.getKey(), kv.getValue());
-        m_ctx = Native.mkContextRc(cfg);
-        Native.delConfig(cfg);
-        initContext();
+        synchronized (creation_lock) {            
+            long cfg = Native.mkConfig();
+            for (Map.Entry<String, String> kv : settings.entrySet())
+                Native.setParamValue(cfg, kv.getKey(), kv.getValue());
+            m_ctx = Native.mkContextRc(cfg);
+            Native.delConfig(cfg);
+            initContext();
+        }
     }
 
     /**
@@ -3638,7 +3642,8 @@ public class Context extends IDisposable
         Native.updateParamValue(nCtx(), id, value);
     }
 
-    long m_ctx = 0;
+    protected long m_ctx = 0;
+    protected static Object creation_lock = new Object();
 
     long nCtx()
     {
diff --git a/src/api/java/InterpolationContext.java b/src/api/java/InterpolationContext.java
index 05746af5d..47a128643 100644
--- a/src/api/java/InterpolationContext.java
+++ b/src/api/java/InterpolationContext.java
@@ -35,8 +35,11 @@ public class InterpolationContext extends Context
      **/
     public InterpolationContext()
     {
-        m_ctx = Native.mkInterpolationContext(0);
-        initContext(); 
+        super();
+        synchronized(creation_lock) {
+            m_ctx = Native.mkInterpolationContext(0);
+            initContext(); 
+        }
     }
 
     /** 
@@ -48,12 +51,15 @@ public class InterpolationContext extends Context
      **/
     public InterpolationContext(Map<String, String> settings)
     { 
-        long cfg = Native.mkConfig();
-        for (Map.Entry<String, String> kv : settings.entrySet())
-            Native.setParamValue(cfg, kv.getKey(), kv.getValue());
-        m_ctx = Native.mkInterpolationContext(cfg);
-        Native.delConfig(cfg);
-        initContext();
+        super();
+        synchronized(creation_lock) {
+            long cfg = Native.mkConfig();
+            for (Map.Entry<String, String> kv : settings.entrySet())
+                Native.setParamValue(cfg, kv.getKey(), kv.getValue());
+            m_ctx = Native.mkInterpolationContext(cfg);
+            Native.delConfig(cfg);
+            initContext();
+        }
     }
 
     /**