diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index cba223f149..715c81626c 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -5256,6 +5256,11 @@ namespace Microsoft.Z3
         internal IntPtr nCtx { get { return m_ctx; } }
         private Z3_ast_print_mode m_print_mode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
 
+        // Estimated native memory used per context, for GC memory pressure hints.
+        // The value is a conservative lower bound; actual usage may exceed this.
+        private const long NativeMemoryPressureEstimate = 8 * 1024 * 1024; // 8 MB
+        private bool m_memPressureAdded = false;
+
         internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
         {
             // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
@@ -5266,6 +5271,11 @@ namespace Microsoft.Z3
             PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
             m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
             Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
+            if (!is_external)
+            {
+                GC.AddMemoryPressure(NativeMemoryPressureEstimate);
+                m_memPressureAdded = true;
+            }
         }
 
         internal void CheckContextMatch(Z3Object other)
@@ -5355,17 +5365,38 @@ namespace Microsoft.Z3
             m_charSort = null;
             if (m_ctx != IntPtr.Zero)
             {
-                IntPtr ctx = m_ctx;
+                // Suppress the finalizer before performing cleanup so that it cannot
+                // run concurrently or redundantly if cleanup raises an exception.
+                GC.SuppressFinalize(this);
+                IntPtr ctx;
+                // Keep a local reference to the error handler delegate to ensure it stays
+                // alive throughout Z3_del_context. Setting m_n_err_handler = null releases
+                // the field reference; without the local variable the GC could collect the
+                // delegate before the native destructor finishes using the handler.
+                Native.Z3_error_handler errHandler;
                 lock (this)
                 {
+                    ctx = m_ctx;
+                    errHandler = m_n_err_handler;
                     m_n_err_handler = null;
                     m_ctx = IntPtr.Zero;
                 }
-                if (!is_external)
-                    Native.Z3_del_context(ctx);
+                // ctx is non-zero only for the thread that wins the lock and zeros m_ctx,
+                // preventing double-free when Dispose() is called concurrently.
+                if (ctx != IntPtr.Zero)
+                {
+                    if (!is_external)
+                    {
+                        Native.Z3_del_context(ctx);
+                        GC.KeepAlive(errHandler);
+                    }
+                    if (m_memPressureAdded)
+                    {
+                        GC.RemoveMemoryPressure(NativeMemoryPressureEstimate);
+                        m_memPressureAdded = false;
+                    }
+                }
             }
-
-            GC.SuppressFinalize(this);
         }
 
 
diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs
index afae66e468..0b0b71f73f 100644
--- a/src/api/dotnet/NativeContext.cs
+++ b/src/api/dotnet/NativeContext.cs
@@ -1334,6 +1334,11 @@ namespace Microsoft.Z3
         internal Native.Z3_error_handler m_n_err_handler = null;
         internal IntPtr nCtx { get { return m_ctx; } }
 
+        // Estimated native memory used per context, for GC memory pressure hints.
+        // The value is a conservative lower bound; actual usage may exceed this.
+        private const long NativeMemoryPressureEstimate = 8 * 1024 * 1024; // 8 MB
+        private bool m_memPressureAdded = false;
+
         internal void NativeErrorHandler(IntPtr ctx, Z3_error_code errorCode)
         {
             // Do-nothing error handler. The wrappers in Z3.Native will throw exceptions upon errors.
@@ -1344,8 +1349,8 @@ namespace Microsoft.Z3
             PrintMode = Z3_ast_print_mode.Z3_PRINT_SMTLIB2_COMPLIANT;
             m_n_err_handler = new Native.Z3_error_handler(NativeErrorHandler); // keep reference so it doesn't get collected.
             Native.Z3_set_error_handler(m_ctx, m_n_err_handler);
-
-            GC.SuppressFinalize(this);
+            GC.AddMemoryPressure(NativeMemoryPressureEstimate);
+            m_memPressureAdded = true;
         }
 
         #endregion
@@ -1365,20 +1370,39 @@ namespace Microsoft.Z3
 
         #region Dispose
 
+        /// <summary>
+        /// Finalizer.
+        /// </summary>
+        ~NativeContext()
+        {
+            Dispose();
+        }
+
         /// <summary>
         /// Disposes of the context.
         /// </summary>
         public void Dispose()
         {
-            if (m_ctx != IntPtr.Zero)
+            IntPtr ctx = System.Threading.Interlocked.Exchange(ref m_ctx, IntPtr.Zero);
+            if (ctx != IntPtr.Zero)
             {
+                // Suppress the finalizer before performing cleanup so that it cannot
+                // run concurrently or redundantly if cleanup raises an exception.
+                GC.SuppressFinalize(this);
+                // Keep a local reference to the error handler delegate to ensure it stays
+                // alive throughout Z3_del_context. Setting m_n_err_handler = null releases
+                // the field reference; without the local variable the GC could collect the
+                // delegate before the native destructor finishes using the handler.
+                var errHandler = m_n_err_handler;
                 m_n_err_handler = null;
-                IntPtr ctx = m_ctx;
-                m_ctx = IntPtr.Zero;
                 Native.Z3_del_context(ctx);
+                GC.KeepAlive(errHandler);
+                if (m_memPressureAdded)
+                {
+                    GC.RemoveMemoryPressure(NativeMemoryPressureEstimate);
+                    m_memPressureAdded = false;
+                }
             }
-            else
-                GC.ReRegisterForFinalize(this);
         }
         #endregion