From de7fd8ce810d4d27168584e4e7270058cc8f9554 Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Tue, 6 Sep 2011 11:50:31 -0700
Subject: Fix printing of (Array ...) types with /useArrayTheory

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 9 +++------
 1 file changed, 3 insertions(+), 6 deletions(-)

(limited to 'Source/Provers/SMTLib/SMTLibLineariser.cs')

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index e8270787..2cda9d6a 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -102,12 +102,9 @@ namespace Microsoft.Boogie.SMTLib
           MapType m = t.AsMap;
           // Contract.Assert(m.MapArity == 1);
           sb.Append("(Array ");
-          foreach (Type tp in m.Arguments) {
-            TypeToStringHelper(tp, sb);
-            sb.Append(" ");
-          }
-          TypeToStringHelper(m.Result, sb);
-          sb.Append(")");
+          foreach (Type tp in m.Arguments)
+            sb.Append(TypeToString(tp)).Append(" ");
+          sb.Append(TypeToString(m.Result)).Append(")");
         } else if (t.IsMap) {
           MapType m = t.AsMap;
           sb.Append('[');
-- 
cgit v1.2.3