From 8d1276fa60863c1d4cb726f5c0a6362bac12fdcc Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 3 Mar 2022 11:03:31 -0800
Subject: [PATCH] using directives

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/api/dotnet/NativeContext.cs | 26 ++++++++++++++++++++++++++
 src/api/dotnet/NativeModel.cs   |  7 ++++++-
 src/api/dotnet/NativeSolver.cs  |  5 +++++
 3 files changed, 37 insertions(+), 1 deletion(-)

diff --git a/src/api/dotnet/NativeContext.cs b/src/api/dotnet/NativeContext.cs
index 42a9bab90..a9c4ab775 100644
--- a/src/api/dotnet/NativeContext.cs
+++ b/src/api/dotnet/NativeContext.cs
@@ -1,3 +1,29 @@
+/*++
+Copyright (c) 2012 Microsoft Corporation
+
+Module Name:
+
+    NativeContext.cs
+
+Abstract:
+
+    Z3 Managed API: Native Context
+
+Author:
+
+    Christoph Wintersteiger (cwinter) 2012-03-22
+    Nikolaj Bjorner (nbjorner) 2022-03-01
+
+Notes:
+    
+--*/
+
+using System;
+using System.Collections.Generic;
+using System.Diagnostics;
+using System.Linq;
+using System.Runtime.InteropServices;
+
 namespace Microsoft.Z3
 {
     using Z3_app = System.IntPtr;
diff --git a/src/api/dotnet/NativeModel.cs b/src/api/dotnet/NativeModel.cs
index dc2be0cc8..a4a7f11be 100644
--- a/src/api/dotnet/NativeModel.cs
+++ b/src/api/dotnet/NativeModel.cs
@@ -19,6 +19,11 @@ Notes:
     
 --*/
 
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Diagnostics;
+
 namespace Microsoft.Z3
 {
     using Z3_ast = System.IntPtr;
@@ -36,7 +41,7 @@ namespace Microsoft.Z3
         /// </summary>
         /// <param name="a">A Constant</param>
         /// <returns>An expression if the constant has an interpretation in the model, null otherwise.</returns>
-        public Z3_ast ConstInterp(Z3_ast a) => ConstInterp(Native.Z3_get_app_decl(Context.nCtx, a));
+        public Z3_ast ConstInterp(Z3_ast a) => ConstFuncInterp(Native.Z3_get_app_decl(Context.nCtx, a));
 
         /// <summary>
         /// Retrieves the interpretation (the assignment) of <paramref name="f"/> in the model. 
diff --git a/src/api/dotnet/NativeSolver.cs b/src/api/dotnet/NativeSolver.cs
index 20d6a8e6f..00110d550 100644
--- a/src/api/dotnet/NativeSolver.cs
+++ b/src/api/dotnet/NativeSolver.cs
@@ -18,6 +18,11 @@ Notes:
     
 --*/
 
+using System;
+using System.Collections.Generic;
+using System.Linq;
+using System.Diagnostics;
+
 namespace Microsoft.Z3
 {