From a67fe054d54d1fdd4a73dbcee9c56a27db239f92 Mon Sep 17 00:00:00 2001
From: Clemens Eisenhofer <56730610+CEisenhofer@users.noreply.github.com>
Date: Thu, 22 Sep 2022 20:26:08 +0200
Subject: [PATCH] Memory leak in .NET user-propagator (#6360)

The user-propagator object has to be manually disposed (IDisposable), otherwise it stays in memory forever, as it cannot be garbage collected automatically
---
 src/api/dotnet/UserPropagator.cs | 14 ++++++++++++--
 1 file changed, 12 insertions(+), 2 deletions(-)

diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs
index 9b4fbc9b7..b9cd4dc39 100644
--- a/src/api/dotnet/UserPropagator.cs
+++ b/src/api/dotnet/UserPropagator.cs
@@ -37,7 +37,7 @@ namespace Microsoft.Z3
     /// <summary>
     /// Propagator context for .Net
     /// </summary>        
-    public class UserPropagator
+    public class UserPropagator : IDisposable
     {
         /// <summary>
         /// Delegate type for fixed callback
@@ -205,10 +205,20 @@ namespace Microsoft.Z3
         }
 
         /// <summary>
-        /// Release provate memory.
+        /// Release private memory.
         /// </summary>            
         ~UserPropagator()
         {
+            Dispose();
+        }
+        
+        /// <summary>
+        /// Must be called. The object will not be garbage collected automatically even if the context is disposed
+        /// </summary>
+        public virtual void Dispose()
+        {
+            if (!gch.IsAllocated)
+                return;
             gch.Free();
             if (solver == null)
                 ctx.Dispose();