From fe4a8b44a51e3364f6006b3171973d43a2ba418d Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 16 Oct 2014 22:40:52 -0700
Subject: [PATCH] revert some changes to how 'out' parameters are annotated on
 API calls. Retain the 'out' annotation for so-called managed out parameters.
 The data-type examples in managed API fail with the out parameter annotation
 as no memory is allocated on instances of out parameters, other than the
 interpolation APIs that are new

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/update_api.py         | 8 +++++---
 src/api/dotnet/Constructor.cs | 6 +++---
 src/api/dotnet/Context.cs     | 2 +-
 src/api/dotnet/EnumSort.cs    | 2 +-
 src/api/dotnet/TupleSort.cs   | 4 ++--
 5 files changed, 12 insertions(+), 10 deletions(-)

diff --git a/scripts/update_api.py b/scripts/update_api.py
index 837c2e1f4..e08adf111 100644
--- a/scripts/update_api.py
+++ b/scripts/update_api.py
@@ -263,8 +263,10 @@ def param2dotnet(p):
         return "[In] %s[]" % type2dotnet(param_type(p))
     elif k == INOUT_ARRAY:
         return "[In, Out] %s[]" % type2dotnet(param_type(p))
-    elif k == OUT_ARRAY or k == OUT_MANAGED_ARRAY:
-        return "[Out] out %s[]" % type2dotnet(param_type(p))
+    elif k == OUT_ARRAY:
+        return "[Out] %s[]" % type2dotnet(param_type(p))
+    elif k == OUT_MANAGED_ARRAY:
+	return "[Out] out %s[]" % type2dotnet(param_type(p))
     else:
         return type2dotnet(param_type(p))
 
@@ -476,7 +478,7 @@ def mk_dotnet_wrappers():
                     dotnet.write('out ');
                 else:
                     dotnet.write('ref ')
-            elif param_kind(param) == OUT_ARRAY or param_kind(param) == OUT_MANAGED_ARRAY:
+            elif param_kind(param) == OUT_MANAGED_ARRAY:
                 dotnet.write('out ');
             dotnet.write('a%d' % i)
             i = i + 1
diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs
index 8d478dd85..527b8bc13 100644
--- a/src/api/dotnet/Constructor.cs
+++ b/src/api/dotnet/Constructor.cs
@@ -50,7 +50,7 @@ namespace Microsoft.Z3
                 IntPtr constructor = IntPtr.Zero;
                 IntPtr tester = IntPtr.Zero;
                 IntPtr[] accessors = new IntPtr[n];
-                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
                 return new FuncDecl(Context, constructor);                
             }
         }
@@ -66,7 +66,7 @@ namespace Microsoft.Z3
                 IntPtr constructor = IntPtr.Zero;
                 IntPtr tester = IntPtr.Zero;
                 IntPtr[] accessors = new IntPtr[n];
-                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);
                 return new FuncDecl(Context, tester);                
             }
         }
@@ -82,7 +82,7 @@ namespace Microsoft.Z3
                 IntPtr constructor = IntPtr.Zero;
                 IntPtr tester = IntPtr.Zero;
                 IntPtr[] accessors = new IntPtr[n];
-                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, out accessors);                
+                Native.Z3_query_constructor(Context.nCtx, NativeObject, n, ref constructor, ref tester, accessors);                
                 FuncDecl[] t = new FuncDecl[n];
                 for (uint i = 0; i < n; i++)
                     t[i] = new FuncDecl(Context, accessors[i]); 
diff --git a/src/api/dotnet/Context.cs b/src/api/dotnet/Context.cs
index a9e25de4f..2b88cbab7 100644
--- a/src/api/dotnet/Context.cs
+++ b/src/api/dotnet/Context.cs
@@ -424,7 +424,7 @@ namespace Microsoft.Z3
                 n_constr[i] = cla[i].NativeObject;
             }
             IntPtr[] n_res = new IntPtr[n];
-            Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), out n_res, n_constr);
+            Native.Z3_mk_datatypes(nCtx, n, Symbol.ArrayToNative(names), n_res, n_constr);
             DatatypeSort[] res = new DatatypeSort[n];
             for (uint i = 0; i < n; i++)
                 res[i] = new DatatypeSort(this, n_res[i]);
diff --git a/src/api/dotnet/EnumSort.cs b/src/api/dotnet/EnumSort.cs
index db3d5123f..e62043078 100644
--- a/src/api/dotnet/EnumSort.cs
+++ b/src/api/dotnet/EnumSort.cs
@@ -88,7 +88,7 @@ namespace Microsoft.Z3
             IntPtr[] n_constdecls = new IntPtr[n];
             IntPtr[] n_testers = new IntPtr[n];
             NativeObject = Native.Z3_mk_enumeration_sort(ctx.nCtx, name.NativeObject, (uint)n,
-                                                         Symbol.ArrayToNative(enumNames), out n_constdecls, out n_testers);
+                                                         Symbol.ArrayToNative(enumNames), n_constdecls, n_testers);
         }
         #endregion
     };
diff --git a/src/api/dotnet/TupleSort.cs b/src/api/dotnet/TupleSort.cs
index 7d0b6a853..81a0eaf60 100644
--- a/src/api/dotnet/TupleSort.cs
+++ b/src/api/dotnet/TupleSort.cs
@@ -74,10 +74,10 @@ namespace Microsoft.Z3
             Contract.Requires(name != null);
 
             IntPtr t = IntPtr.Zero;
-            IntPtr[] f;
+            IntPtr[] f = new IntPtr[numFields];
             NativeObject = Native.Z3_mk_tuple_sort(ctx.nCtx, name.NativeObject, numFields,
                                                    Symbol.ArrayToNative(fieldNames), AST.ArrayToNative(fieldSorts),
-                                                   ref t, out f);
+                                                   ref t, f);
         }
         #endregion
     };