From d792d30e884423d768318cc8d631eca53625f198 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 21 Jun 2022 09:09:31 -0700 Subject: [PATCH] Update NativeContext.cs TraceToFile does not correspond to the functionality of enable_trace. Z3_enable_trace tags a trace tag as input. It can be invoked multiple times with different tags. The debug tracing then shows logs with the corresponding tags. --- src/api/dotnet/NativeContext.cs | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs index 9f285ec84dc..93180e5830b 100644 --- a/src/api/dotnet/NativeContext.cs +++ b/src/api/dotnet/NativeContext.cs @@ -1341,13 +1341,13 @@ internal void InitContext() #region Tracing /// - /// Enable tracint to file + /// Enable trace to file /// - /// - public void TraceToFile(string file) + /// Tag to trace + public static void EnableTrace(string tag) { - Debug.Assert(!string.IsNullOrEmpty(file)); - Native.Z3_enable_trace(file); + Debug.Assert(!string.IsNullOrEmpty(tag)); + Native.Z3_enable_trace(tag); } #endregion