From 0568888a48ab4424d3e5a166b3088db3557b9bd4 Mon Sep 17 00:00:00 2001
From: Michal Moskal <michal@moskal.me>
Date: Tue, 6 Sep 2011 11:45:15 -0700
Subject: Support multi-dimensional arrays in SMTLib2 backend (using Z3
 extension though)

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

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

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index 34a8502a..e8270787 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -100,10 +100,12 @@ namespace Microsoft.Boogie.SMTLib
       } else {
         if (t.IsMap && CommandLineOptions.Clo.UseArrayTheory) {
           MapType m = t.AsMap;
-          Contract.Assert(m.MapArity == 1);
+          // Contract.Assert(m.MapArity == 1);
           sb.Append("(Array ");
-          TypeToStringHelper(m.Arguments[0], sb);
-          sb.Append(" ");
+          foreach (Type tp in m.Arguments) {
+            TypeToStringHelper(tp, sb);
+            sb.Append(" ");
+          }
           TypeToStringHelper(m.Result, sb);
           sb.Append(")");
         } else if (t.IsMap) {
-- 
cgit v1.2.3