From 4549ec73313f69a983339e8aba237f67a8704af8 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 9 May 2022 08:38:35 -0700
Subject: [PATCH] misc

---
 src/api/dotnet/UserPropagator.cs | 8 +++-----
 1 file changed, 3 insertions(+), 5 deletions(-)

diff --git a/src/api/dotnet/UserPropagator.cs b/src/api/dotnet/UserPropagator.cs
index d0f46c189..590b84e9c 100644
--- a/src/api/dotnet/UserPropagator.cs
+++ b/src/api/dotnet/UserPropagator.cs
@@ -153,10 +153,8 @@ namespace Microsoft.Z3
 	   prop.callback = cb;
 	   prop.decide_eh(ref t, ref idx, ref phase);
            prop.callback = IntPtr.Zero;
-	   if (u != t) {
+	   if (u != t) 
 	       a = t.NativeObject;
-	   }
-	   t.Dispose();
 	}
 
         /// <summary>
@@ -203,9 +201,9 @@ namespace Microsoft.Z3
 	public virtual void Pop(uint n) { throw new Z3Exception("Pop method should be overwritten"); } 
 
         /// <summary>
-        /// Virtual method for fresh. It must be overwritten by inherited class.
+        /// Virtual method for fresh. It can be overwritten by inherited class.
 	/// </summary>
-	public virtual UserPropagator Fresh(Context ctx) { throw new Z3Exception("Fresh method should be overwritten"); }
+	public virtual UserPropagator Fresh(Context ctx) { return new UserPropagator(ctx); }
 
         /// <summary>
         /// Declare combination of assigned expressions a conflict