mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-24 01:25:31 +00:00
Code Activity

Update NativeContext.cs

Browse source 
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.
This commit is contained in:
Nikolaj Bjorner 2022-06-21 09:09:31 -07:00
parent b254f4086b
commit d792d30e88
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

10
src/api/dotnet/NativeContext.cs
View file

@ -1341,13 +1341,13 @@ namespace Microsoft.Z3
#region Tracing
/// <summary>
/// Enable tracint to file
/// Enable trace to file
/// </summary>
/// <param name="file"></param>
public void TraceToFile(string file)
/// <param name="tag">Tag to trace</param>
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