From 6cd02de973f4160bfb5dc22ad0ddaa7b5600eda9 Mon Sep 17 00:00:00 2001
From: MichalMoskal <unknown>
Date: Fri, 18 Feb 2011 22:05:07 +0000
Subject: Handle /useArrayTheory

---
 Source/Provers/SMTLib/SMTLibLineariser.cs | 19 +++++++++++++++----
 1 file changed, 15 insertions(+), 4 deletions(-)

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

diff --git a/Source/Provers/SMTLib/SMTLibLineariser.cs b/Source/Provers/SMTLib/SMTLibLineariser.cs
index f7a682ad..3c6c611c 100644
--- a/Source/Provers/SMTLib/SMTLibLineariser.cs
+++ b/Source/Provers/SMTLib/SMTLibLineariser.cs
@@ -97,7 +97,15 @@ namespace Microsoft.Boogie.SMTLib
       if (syn != null) {
         TypeToStringHelper(syn.ExpandedType, sb);
       } else {
-        if (t.IsMap) {
+        if (t.IsMap && CommandLineOptions.Clo.UseArrayTheory) {
+          MapType m = t.AsMap;
+          Contract.Assert(m.MapArity == 1);
+          sb.Append("(Array ");
+          TypeToStringHelper(m.Arguments[0], sb);
+          sb.Append(" ");
+          TypeToStringHelper(m.Result, sb);
+          sb.Append(")");
+        } else if (t.IsMap) {
           MapType m = t.AsMap;
           sb.Append('[');
           for (int i = 0; i < m.MapArity; ++i) {
@@ -132,10 +140,13 @@ namespace Microsoft.Boogie.SMTLib
       else if (t.IsBv) {
         return "(_ BitVec " + t.BvBits + ")";
       } else {
-        StringBuilder sb = new StringBuilder();
-        sb.Append("T@");
+        StringBuilder sb = new StringBuilder();        
         TypeToStringHelper(t, sb);
-        return SMTLibNamer.QuoteId(sb.ToString());
+        var s = sb.ToString();
+        if (s[0] == '(')
+          return s;
+        else
+          return SMTLibNamer.QuoteId("T@" + s);
       }
     }
 
-- 
cgit v1.2.3