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/TypeDeclCollector.cs | 17 ++---------------
 1 file changed, 2 insertions(+), 15 deletions(-)

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

diff --git a/Source/Provers/SMTLib/TypeDeclCollector.cs b/Source/Provers/SMTLib/TypeDeclCollector.cs
index 327b2f70..0a03e4ab 100644
--- a/Source/Provers/SMTLib/TypeDeclCollector.cs
+++ b/Source/Provers/SMTLib/TypeDeclCollector.cs
@@ -168,7 +168,6 @@ void ObjectInvariant()
 
       if (type.IsMap && CommandLineOptions.Clo.MonomorphicArrays) {
         KnownTypes.Add(type, true);
-        string declString = "";
         MapType mapType = type.AsMap;
         Contract.Assert(mapType != null);
 
@@ -178,21 +177,9 @@ void ObjectInvariant()
         }
         RegisterType(mapType.Result);
 
-        declString += "(declare-sort " + TypeToString(type) + " 0";
+        if (!CommandLineOptions.Clo.UseArrayTheory)
+          AddDeclaration("(declare-sort " + TypeToString(type) + " 0)");
 
-        /*
-        if (CommandLineOptions.Clo.UseArrayTheory) {
-          declString += " :BUILTIN Array ";
-          foreach (Type t in mapType.Arguments) {
-            declString += TypeToString(t);
-            declString += " ";
-          }
-          declString += TypeToString(mapType.Result);
-        }
-         */
-
-        declString += ")";
-        AddDeclaration(declString);
         return;
       }
 
-- 
cgit v1.2.3