From 5a45711f22d92880c771e81e95da0c6525c781a4 Mon Sep 17 00:00:00 2001
From: mattpark <mattpark@microsoft.com>
Date: Mon, 11 Aug 2014 15:44:10 +0100
Subject: [PATCH] Dealt with some concurrency issues due to concurrent GC.

---
 src/api/dotnet/Context.cs  | 2 +-
 src/api/dotnet/Z3Object.cs | 8 ++++----
 2 files changed, 5 insertions(+), 5 deletions(-)

diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index 16073f3b3..5436fe0a0 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -3646,7 +3646,7 @@ namespace Microsoft.Z3
         internal Fixedpoint.DecRefQueue Fixedpoint_DRQ { get { Contract.Ensures(Contract.Result<Fixedpoint.DecRefQueue>() != null); return m_Fixedpoint_DRQ; } }
 
 
-        internal uint refCount = 0;
+        internal int refCount = 0;
 
         /// <summary>
         /// Finalizer.
diff --git a/src/api/dotnet/Z3Object.cs b/src/api/dotnet/Z3Object.cs
index e8654ce21..8e474041a 100644
--- a/src/api/dotnet/Z3Object.cs
+++ b/src/api/dotnet/Z3Object.cs
@@ -19,6 +19,7 @@ Notes:
 
 using System;
 using System.Diagnostics.Contracts;
+using System.Threading;
 
 namespace Microsoft.Z3
 {
@@ -50,8 +51,7 @@ namespace Microsoft.Z3
 
             if (m_ctx != null)
             {
-                m_ctx.refCount--;
-                if (m_ctx.refCount == 0)
+                if (Interlocked.Decrement(ref m_ctx.refCount) == 0)
                     GC.ReRegisterForFinalize(m_ctx);
                 m_ctx = null;
             }
@@ -77,7 +77,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(ctx != null);
 
-            ctx.refCount++;
+            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
         }
 
@@ -85,7 +85,7 @@ namespace Microsoft.Z3
         {
             Contract.Requires(ctx != null);
 
-            ctx.refCount++;
+            Interlocked.Increment(ref ctx.refCount);
             m_ctx = ctx;
             IncRef(obj);
             m_n_obj = obj;